我如何使用森林或其他东西来排版命题逻辑公式的解析树？

Question

以下解析树来自Mathematical Logic2007 年由 Ian Chiswell 和 Wilfrid Hodges 编写的。它看起来像一棵森林树，但我猜其他包可以更好地排版它。我该如何排版它？

Answer 1

或多或少地使用公式摘自 egreg 的 do-it-for-me 图片当原贴作者没有提供任何帮助时，tableaux我为其开发了一个修改后的版本这个答案，我使用 Forest 绘制了树的一个版本，如下所示。顺便说一句，我想我不应该回答这个问题，但我屈服于我对树的迷恋。

\documentclass[border=5pt,tikz,multi]{standalone}
\usepackage{forest}
\newcommand*{\lif}{\ensuremath{\mathbin{\rightarrow}}}
\forestset{%
  declare toks={wff}{},
  declare toks={cyswllt}{},
  declare toks register={nod safonol},
  nod safonol=\circ,
  dosbarthu/.style={%
    for tree={
      math content,
      parent anchor=children,
      child anchor=parent,
      inner sep=0pt,
    },
    where level=0{%
      for children={no edge},
      phantom,
    }{%
      delay={%
        content'/.register=nod safonol,
        insert before/.wrap pgfmath arg={%
          [{##1}, no edge, math content, before drawing tree={x'+=7.5pt}]
        }{wff()},
        if={strequal(cyswllt(),"")}{cyswllt/.option=wff}{},
        insert after/.wrap pgfmath arg={%
          [{##1}, no edge, math content, before drawing tree={x'-=7.5pt}]
        }{cyswllt()},
      },
      if={n_children("!parent")==1}{%
        before packing={calign with current edge},
      }{%
        if n=1{%
          before packing={%
            !parent.calign primary child/.process args={O}{n},
          },
        }{%
          before packing={%
            !parent.calign secondary child/.process args={O}{n},
          },
       }
      }
    },
  }
}
\begin{document}
\begin{forest}
  dosbarthu
  [
    [, wff=((\lnot(p_1\lif(\lnot p_0)))\lif p_0), cyswllt=\lif
      [, wff=(\lnot(p_1\lif(\lnot p_0))), cyswllt=\lnot
        [, wff=(p_1\lif(\lnot p_0)), cyswllt=\lif
          [, wff=p_1]
          [, wff=(\lnot p_0), cyswllt=\lnot
            [, wff=p_0]
          ]
        ]
      ]
      [, wff=p_0]
    ]
  ]
\end{forest}
\end{document}

Answer 2

图片模式已足够；pict2e加载以便与较新的引擎更好地兼容。

\documentclass{article}
\usepackage{amsmath}
\usepackage{pict2e,color}

\begin{document}

\begin{equation}
\begin{gathered}
\setlength{\unitlength}{0.5in}
\begin{picture}(5,4)
\put(5,3){\line(-3,2){1.5}}
\put(3.5,4){\line(-3,-2){1.5}}
\put(2,3){\line(0,-1){1}}
\put(2,2){\line(-1,-1){1}}
\put(2,2){\line(1,-1){1}}
\put(3,1){\line(0,-1){1}}
\begingroup\color{white}
\put(5,3){\circle*{0.1}}
\put(3.5,4){\circle*{0.1}}
\put(2,3){\circle*{0.1}}
\put(2,2){\circle*{0.1}}
\put(1,1){\circle*{0.1}}
\put(3,1){\circle*{0.1}}
\put(3,0){\circle*{0.1}}
\endgroup
\put(5,3){\circle{0.1}}
\put(3.5,4){\circle{0.1}}
\put(2,3){\circle{0.1}}
\put(2,2){\circle{0.1}}
\put(1,1){\circle{0.1}}
\put(3,1){\circle{0.1}}
\put(3,0){\circle{0.1}}
\put(5,3){\makebox(0,0){$p_0$\qquad$p_0$}}
\put(3.15,4){\makebox(0,0){\makebox[0pt][r]{%
  $((\lnot(p_1\mathbin{\to}(\lnot p_0)))\mathbin{\to}p_0)$}}%
}
\put(3.7,4){\makebox(0,0){\makebox[0pt][l]{$\to$}}}
\put(1.65,3){\makebox(0,0){\makebox[0pt][r]{%
  $(\lnot(p_1\mathbin{\to}(\lnot p_0)))$}}%
}
\put(2.2,3){\makebox(0,0){\makebox[0pt][l]{$\lnot$}}}
\put(1.65,2){\makebox(0,0){\makebox[0pt][r]{%
  $(p_1\mathbin{\to}(\lnot p_0))$}}%
}
\put(2.2,2){\makebox(0,0){\makebox[0pt][l]{$\to$}}}
\put(1,1){\makebox(0,0){$p_1$\qquad$p_1$}}
\put(2.65,1){\makebox(0,0){\makebox[0pt][r]{$(\lnot p_0)$}}}
\put(3.2,1){\makebox(0,0){\makebox[0pt][l]{$\lnot$}}}
\put(3,0){\makebox(0,0){$p_0$\qquad$p_0$}}
\end{picture}
\end{gathered}
\end{equation}

\end{document}