☰

编辑

tag-icon • tag-icon tikz-trees forest trees logic proof-package
编辑

我必须在我的文档中排版一些语义表格，看起来类似于下面的示例。

语义表

我的第一个想法就是用tikz这个，所以我创造了下面的怪物：

丑陋的树

\documentclass[convert]{standalone}
\usepackage{tikz,amssymb}
\usetikzlibrary{positioning}
\newcommand{\lnec}{\Box}
\begin{document}
  \begin{tikzpicture}[scale=2]
    \node[label=right:$(\lnec p\to\lnec q)\to\lnec(p\to q)$] (n1) {$\circ_1$};
    \node[label=left:$\lnec p\to\lnec q$, label=right:$\lnec(p\to q)$, below=of n1] (n2) {$\circ_1$};
    \node[label=left:$\lnec q$, label=right:$\lnec(p\to q)$, below left=of n2] (n3) {$\circ_1$};
    \node[label=right:{$\lnec p, \lnec(p\to q)$}, below right=of n2] (n4) {$\circ_1$};
    \node[label=left:$q$, label=right:$\lnec(p\to q)$, below=of n3] (n5) {$\circ_2$};
    \node[label=right:$p$, below left=of n4] (n6) {$\circ_3$};
    \node[label=right:$p\to q$, below right=of n4] (n7) {$\circ_4$};
    \node[label=left:$p$, label=right:$q$, below=of n7] (n8) {$\circ_4$};

    \draw[-] (n1) to (n2);
    \draw[-] (n2) to (n3);
    \draw[-] (n2) to (n4);
    \draw[-, dotted] (n3) to (n5);
    \draw[-, dotted] (n4) to (n6);
    \draw[-, dotted] (n4) to (n7);
    \draw[-] (n7) to (n8); 
  \end{tikzpicture}
\end{document}

显然这不是理想的结果。边缘应该从 s 下方开始，在\circs 上方结束，并且它们应该有直角，这样图表就可以稍微压缩一下。

绘制这类图表对我来说完全是新事物，您能给我一些有用的指导吗？您有什么制作这些语义表的技巧或窍门吗？对于这种树，像forest或produce 这样的软件包是否更容易使用？qtree

编辑：@cfr 的回答很有希望，所以我想研究forest并微调他的风格tableaux。过去两天我试着自己做这件事，但forest对于像我这样的初学者来说，理解文档中的所有高级选项是不可能的。因此，我想给能为我做微调的人悬赏。这意味着

  • \circ应减小wff 和分离器之间的空间，
  • 边缘应与\circ分隔符的中心对齐，忽略可能的下标，
  • \circ当没有给出分隔符的下标时，上述方法也应该有效。

答案1

这个答案使用了完全不同的方法，因为代码不幸从问题的原始版本中丢失了。它可能没有那么有用，因为它不是基于该代码，但我将它留在这里，因为它可能在某个时候对某些人有用。

这是一种基本的森林风格，tableaux可用于这种类型的图表。

使用的问题label在于，在将节点相对于彼此定位时，它不会被考虑在内。tableaux而是为该内容创建与“主”节点一起指定的附加节点。这使得可以将事物与“主”圆正确对齐，同时为 wff 留出足够的空间。

这样做的一个真正缺点是，必须创建一个额外的phantom根节点，否则我们最终会得到 2 或 3 个根（顶层的主节点和两边的 wff）。这是不可能的。因此有了幻影根节点。

如果您要执行很多此类操作，则可以通过创建一个自动执行此操作的新环境来避免亲自添加幻像根。（environ可以使用该包并使用环境主体的自定义名称来实现此目的。）

使用Forest 的edges库来提供forked edges样式。

微调留给读者练习。例如，调整兄弟距离以使 wff 更接近可能会看起来更好。

\documentclass[tikz,multi,border=10pt]{standalone}
\usepackage[edges]{forest}
\usepackage{amssymb}
\begin{document}
\forestset{%
  declare toks={F}{},
  declare toks={T}{},
  tableaux/.style={%
    forked edges,
    for tree={
      math content,
      parent anchor=children,
      child anchor=parent,
    },
    where level=0{%
      for children={no edge},
      phantom,
    }{%
      delay={%
        content/.wrap value={\circ_{##1}},
        insert before/.wrap pgfmath arg={%
          [{##1}, no edge, math content]
        }{T()},
        insert after/.wrap pgfmath arg={%
          [{##1}, no edge, math content]
        }{F()},
      },
      if={n_children("!u")==1}{%
        before packing={calign with current edge},
      }{}
    },
  }
}
\newcommand*{\necc}{\ensuremath{\mathbin{\Box}}}
\newcommand*{\lif}{\ensuremath{\mathbin{\rightarrow}}}
\begin{forest}
  tableaux
  [
    [1, F=(\necc p \lif \necc q) \lif \necc (p \lif q)
      [1, T=\necc p \lif \necc q, F=\necc (p \lif q)
        [1, T=\necc q, F=\necc (p \lif q)
          [2, T=q, F=p \lif q, edge=densely dotted
            [2, T={p, q}, F=q, label=below:$\otimes$]
          ]
        ]
        [1, F={\necc p, \necc(p \lif q)}
          [3, F=p, edge=densely dotted]
          [4, F=p \lif q, edge=densely dotted
            [4, F=q, T=p]
          ]
        ]
      ]
    ]
  ]
\end{forest}
\end{document}

场景

编辑

这解决了问题中增加的 3 个必要条件。我们通过将下标渲染为标签而不是节点的一部分来避免对齐的影响。我们在绘制树之前调整到 wff 的距离，因为我们通常不想减少兄弟距离，而只想减少圆与相关 wff 之间的距离。无论有没有下标，这都可以。

根据您的实际用途、字体系列和大小等，您可能需要调整调整中使用的特定尺寸。这些是-3.5pt和3.5pt用于下标，以及7.5pt和-7.5pt用于下面 MWE 中的 wff。

\documentclass[tikz,multi,border=10pt]{standalone}
\usepackage[edges]{forest}
\usepackage{amssymb}
\begin{document}
\forestset{%
  declare toks={T}{},
  declare toks={F}{},
  tableaux/.style={%
    forked edges,
    for tree={
      math content,
      parent anchor=children,
      child anchor=parent,
    },
    where level=0{%
      for children={no edge},
      phantom,
    }{%
      before typesetting nodes={%
        content/.wrap value={\circ},
      },
      delay={%
        my label/.wrap pgfmath arg={{[inner sep=0pt, xshift=-3.5pt, yshift=3.5pt, anchor=north west, font=\scriptsize]-45:$##1$}}{content()},
        insert before/.wrap pgfmath arg={%
          [{##1}, no edge, math content, before drawing tree={x'+=7.5pt}]
        }{T()},
        insert after/.wrap pgfmath arg={%
          [{##1}, no edge, math content, before drawing tree={x'-=7.5pt}]
        }{F()},
      },
      if={n_children("!u")==1}{%
        before packing={calign with current edge},
      }{}
    },
  }
}
\newcommand*{\necc}{\ensuremath{\mathbin{\Box}}}
\newcommand*{\lif}{\ensuremath{\mathbin{\rightarrow}}}
\begin{forest}
  tableaux
  [
    [1, F=(\necc p \lif \necc q) \lif \necc (p \lif q)
      [1, T=\necc p \lif \necc q, F=\necc (p \lif q)
        [1, T=\necc q, F=\necc (p \lif q)
          [2, T=q, F=p \lif q, edge=densely dotted
            [2, T={p, q}, F=q, label=below:$\otimes$]
          ]
        ]
        [1, F={\necc p, \necc(p \lif q)}
          [3, F=p, edge=densely dotted]
          [4, F=p \lif q, edge=densely dotted
            [4, F=q, T=p
              [99, F=X!, T=XX!!
                [, F=XXX!!!, T=XXXX!!!!]
              ]
            ]
          ]
        ]
      ]
    ]
  ]
\end{forest}
\end{document}

修改版本

编辑 编辑

正如评论中指出的那样，我的编辑导致闭包消失。这是因为它们是使用创建的label，并且节点右上角的数字也是使用添加的label。虽然标签是在不同的地方请求的，并且在通常的 TikZ 代码中是可以的，但 Forest 的定义label方式是每个节点只允许一个。此外，label 还覆盖使用tikz或指定的任何先前注释pin。来自forest.sty：

 label/.style={tikz={\path[late options={%
        name=\forestoption{name},label={#1}}];}},
 pin/.style={tikz={\path[late options={%
        name=\forestoption{name},pin={#1}}];}},

每次调用都会tikz覆盖任何先前的设置。因此，代码不会累积，而是会替换现有代码。

我不确定作者做出此选择的原因是什么，所以我并不完全确定如何最好地解决这个问题。一种选择是使用数字，这应该允许在树本身中afterthought使用。但是，在这种情况下，我们无法将数字指定为TikZ ，而不必首先重现 Forest 使用的代码。由于这样做似乎没有任何好处，因此很容易通过在文档的序言中添加以下代码来重新定义：labellabellabellabel

\forestset{% Sašo Živanović won't like this ...
  label/.style={%
    tikz+={%
      \path[late options={%
        name=\forestoption{name},label={#1}}
      ];
    }
  },
}

这+就是不同之处。现在labels 将会累积，而不是互相覆盖和/或任何先前使用的pin、tikz或tikz+。如上所述，我无法想象这是我应该做的事情，所以我不推荐它，即使它有效：

使用 hack 恢复关闭

一个更复杂的替代方法是使用这个：

\forestset{%
  my label/.style={%
    tikz+={%
      \path[late options={%
        name=\forestoption{name},label={#1}}
      ];
    }
  }
}

然后数字的放置只需使用my label代替label。完整配置：

\forestset{%
  declare toks={T}{},
  declare toks={F}{},
  my label/.style={%
    tikz+={%
      \path[late options={%
        name=\forestoption{name},label={#1}}
      ];
    }
  },
  tableaux/.style={%
    forked edges,
    for tree={
      math content,
      parent anchor=children,
      child anchor=parent,
    },
    where level=0{%
      for children={no edge},
      phantom,
    }{%
      before typesetting nodes={%
        content/.wrap value={\circ},
      },
      delay={%
        my label/.wrap pgfmath arg={{[inner sep=0pt, xshift=-3.5pt, yshift=3.5pt, anchor=north west, font=\scriptsize]-45:$##1$}}{content()},
        insert before/.wrap pgfmath arg={%
          [{##1}, no edge, math content, before drawing tree={x'+=7.5pt}]
        }{T()},
        insert after/.wrap pgfmath arg={%
          [{##1}, no edge, math content, before drawing tree={x'-=7.5pt}]
        }{F()},
      },
      if={n_children("!u")==1}{%
        before packing={calign with current edge},
      }{}
    },
  }
}

它产生与上述相同的结果，但无需重新定义 Forest 的label风格。

相关内容