有没有简单的方法可以在 LaTex 中绘制逻辑树？

Question

我选修了入门逻辑，我们需要绘制逻辑树。我们的老师不接受除他之外的任何类型的编号位置。所以我搜索了操作指南，但我没有看到它的确切版本，而且由于我编码很差，所以我认为最好问一下。我如何在 LaTex 中绘制这个？

Answer 1

这将帮助您开始使用。您可以对每个节点forest使用。array

\documentclass{article}

\usepackage{forest}

\renewcommand{\iff}{\leftrightarrow}
\newcommand{\T}{\mathrm{T\,}}
\newcommand{\F}{\mathrm{F\,}}

\begin{document}

\begin{forest}
[$\begin{array}{r@{\,}l} & \lnot(p\iff q)\iff(\lnot p\iff q)\\ 1. & \F\lnot(p\iff q)\iff(\lnot p\iff q)\end{array}$
  [$\begin{array}{r@{\,}l}2. & \T\lnot(p\iff q)\,(1)\\ 3. & \F\lnot p\iff q\,(1)\\ 6. & \F p\iff q\,(2)\end{array}$
    [4
      [8][9]
    ]
    [5
      [10][11]
    ]
  ]
  [$\begin{array}{r@{\,}l}4. & \F\lnot(p\iff q)\,(1)\\ 5. & \T\lnot p\iff q\,(1)\\ 20. & \T p\iff q\,(4)\end{array}$
    [6
      [12][13]
    ]
    [7
      [14][15]
    ]
  ]
]
\end{forest}

\end{document}

Answer 2

由于forest内置了对tabular节点的支持，我修改了Sandy G 的回答来利用这一点。我还演示了一种使用 圈出矛盾的简单方法tikzmark。请注意，原始图像中的编号不正确：不应该有重复的行号。因此，下面的解决方案具有相同的行数，但似乎有一个额外的行号（如果你不仔细看的话）。

我的列定义区分了证明的每一行的各个部分。默认情况下，tab infer除第一个节点外，所有节点均为 类型，第一个节点为 类型tab theorem。可以通过附加 来创建假设tab ass，如下所示。

• tab theorem只是将其内容放入数学模式并期望<wff>作为内容。
• tab ass使用三部分定义并期望形式的内容<line number> & <semantic value> & <wff>。
• tab infer使用四部分定义并期望<line number> & <semantic value> & <wff> & <reference(s)>。

默认情况下，所有列都设置为文本模式，但用于 wffs 的列除外，它们使用数学模式。T并且F不是语言语法的一部分，而是语义值。虽然这里有使用数学模式的论据，但至少应该在标记中单独处理它们。行号是简单的引用，因此文本模式在这里似乎也最合适，尽管如果包含规则，更复杂的理由可能需要使用数学模式。

\documentclass{standalone}
\usepackage{forest}
\usepackage{array}
\usetikzlibrary{tikzmark}
\newcolumntype{C}{>{$}c<{$}}
\forestset{%
  declare boolean={only child}{0},
  for tableau/.style={%
    /utils/exec={\setlength{\tabcolsep}{1pt}},
    tab theorem,
    for descendants={tab infer},
    where n children=1{!1.no edge,!1.only child}{},
    before computing xy={%
      where only child={l'=\baselineskip}{}
    }
  },
  tab theorem/.style={math content},
  tab ass/.style={align=rlC},
  tab infer/.style={align=rlCl},
}
\newcommand*{\liff}{\ensuremath{\mathbin{\leftrightarrow}}}
% ateb: https://tex.stackexchange.com/a/700793/
% addaswyd o ateb Sandy G.: https://tex.stackexchange.com/a/668471/
\begin{document}
\begin{forest}
  for tableau,
  [
    \lnot(p\liff q)\liff(\lnot p\liff q)
    [
      1. & F & \lnot(p\liff q)\liff(\lnot p\liff q), tab ass
      [ 2. & T & \lnot(p\liff q) & (1)
        [3. & F & \lnot p\liff q & (1)
          [6. & F & p\liff q & (2)
            [7. & T & \lnot p & (3)
              [8. & F & q & (3)
              [11. & \subnode{fp1}{F} & \subnode{fp2}{p} & (7)
                [13. & \subnode{tp1}{T} & \subnode{tp2}{p} & (6)
                    [14. & F & q & (6)]
                  ]
                  [15. & F & p & (6)
                    [16. & T & q & (6)]
                  ]
                ]
              ]
            ]
            [9. & F & \lnot p & (3)
              [10. & T & q & (3)
                [12. & T & p & (9)
                  [17. & T & p & (6)
                    [18. & F & q & (6)]
                  ]
                  [19. & F & p & (6)
                    [20. & T & q & (6)]
                  ]
                ]
              ]
            ]
          ]
        ]
      ]
      [4. & F & \lnot(p\liff q) & (1)
        [5. & T & \lnot p\liff q & (1)
          [21. & T & p\liff q & (4)
            [22. & T & \lnot p & (3)
              [23. & T & q & (3)
                [26. & F & p & (7)
                  [27. & T & p & (6)
                    [28. & T & q & (6)]
                  ]
                  [29. & F & p & (6)
                    [30. & F & q & (6)]
                  ]
                ]
              ]
            ]
            [24. & F & \lnot p & (3)
              [25. & F & q & (3)
                [31. & T & p & (9)
                  [32. & T & p & (6)
                    [33. & T & q & (6)]
                  ]
                  [34. & F & p & (6)
                    [35. & F & q & (6)]
                  ]
                ]
              ]
            ]
          ]
        ]
      ]
    ]
  ]
\end{forest}
\begin{tikzpicture}[remember picture,overlay]
    \node [draw=red,circle,inner sep=0pt,fit=(fp1) (fp2)] {};
    \node [draw=red,circle,inner sep=0pt,fit=(tp1) (tp2)] {};
\end{tikzpicture}
\end{document}

请注意，这是一个相当广泛的证明。虽然你可以减少s sep，但我认为sidewaysfigure可能需要类似的东西。