☰

與森林排版的邏輯證明樹中的節點之間的良好對齊

tag-icon • tag-icon forest trees logic proof-package
與森林排版的邏輯證明樹中的節點之間的良好對齊

在這個答案，使用者 cfr 提供了以下程式碼，其輸出如下圖所示：

\documentclass[border=11pt]{standalone}
\usepackage[linguistics]{forest}
\usepackage{amsmath,amssymb}
\forestset{
  declare toks={from}{},
  declare toks register={claim},
  claim=,
  ll proof/.style={
    for tree={math content},
    before typesetting nodes={
      if claim={}{}{
        replace by/.process={Rw{claim}{[##1, math content, append]}},
        no edge,
        before computing xy={l'=2\baselineskip},
      },
      tempcounta'=0,
      for tree breadth-first={
        tempcounta'+=1,
        content/.process={ OR OSl+tt= ? w  w3 {content}{tempcounta}{from}{}{}{(##1)}{##2.\quad ##1\quad ##3} }
      }
    },
    where n children=1{!1.no edge, before computing xy={!1.l'=\baselineskip}}{},
    close/.style={label=below:\textsf{x}},
  },
}
\begin{document}
\begin{forest}
  ll proof,
  claim=\vdash ((p\lor (q\land r))\to((p\lor q)\land (p\lor r)))
  [ \lnot ((p\lor (q\land r))\to((p\lor q)\land (p\lor r)))    
    [ (p\lor (q\land r)) , from=1
      [ \lnot ((p\lor q)\land (p\lor r)) , from=1
        [ p , from=2
          [ \lnot (p\lor q) , from=3
            [ \lnot p , from=6
              [ \lnot q , from=6, close
          ]]]
          [ \lnot (p\lor r) , from=3
            [1 \lnot p , from=7
            [1 \lnot r , from=7, close
        ]]]]
        [ (q\land r) , from=2
          [1 q , from=5
            [1 r , from=5
              [1 \lnot (p\lor q) , from=3
                [1 \lnot p , from=14
                  [1 \lnot q , from=14, close
              ]]]
              [1 \lnot (p\lor r) , from=3
                [1 \lnot p , from=15
                  [1 \lnot r , from=15, close
  ]]]]]]]]]
\end{forest}
\end{document}

證明樹，其中每個節點都有行號、四元空間、公式、四元空間和理由

我想知道是否有人知道如何修改程式碼以產生如下圖所示的輸出：

證明樹，其中分支上的行號、公式和理由水平對齊 我能想到的一種方法是儲存每個分支上每個最寬行號、公式和對齊方式的寬度，然後將分支上每個節點的內容包裝在三個列表格中，其中列寬固定為這些最大寬度。然後，節點錨點的位置將設置在公式列的北部，以便將分支之間的線繪製到公式的中心。

一種明顯不太優雅但更簡單的方法是使用包含分支上所有公式的多行表格（即一個用於編號為1、2、3 的公式；另一個用於4；另一個用於5、8 、11；依此類推） ）。但我想避免這樣的方法，它需要對樹本身而不是其風格進行重大改變。

不幸的是，我目前確實不具備技術專業知識，甚至不知道從哪裡開始實際實施更優雅的解決方案，所以我很感激所提供的任何幫助。

更新

這是部分答案，其中涉及將內容處理為包含三列的單行表格，一列用於行號，一列用於 wff，另一列用於說明理由：

\documentclass[border=11pt]{standalone}
\usepackage[linguistics]{forest}
\usepackage{amsmath,amssymb}
\usepackage{array}
\forestset{
  declare toks={from}{},
  declare toks register={claim},
  claim=,
  ll proof/.style={
    before typesetting nodes={
      if claim={}{}{
        replace by/.process={Rw{claim}{[##1, math content, append]}},
        no edge,
        before computing xy={l'=2\baselineskip},
      },
      tempcounta'=0,
      for tree breadth-first={
        tempcounta'+=1,
        content/.process={ OR OSl+tt= ? w  w3 {content}{tempcounta}{from}{}{}{(##1)}{\begin{tabular}{>{\raggedleft}p{1em}cp{1em}}##2. & \ensuremath{##1} & \ensuremath{##3}\\\end{tabular}} }
      }
    },
    where n children=1{!1.no edge, before computing xy={!1.l'=\baselineskip}}{},
    close/.style={label=below:\textsf{x}},
  },
}
\begin{document}
\begin{forest}
  ll proof,
  claim=\vdash ((p\lor (q\land r))\to((p\lor q)\land (p\lor r)))
  [ \lnot ((p\lor (q\land r))\to((p\lor q)\land (p\lor r)))    
    [ (p\lor (q\land r)) , from=1
      [ \lnot ((p\lor q)\land (p\lor r)) , from=1
        [ p , from=2
          [ \lnot (p\lor q) , from=3
            [ \lnot p , from=6
              [ \lnot q , from=6, close
          ]]]
          [ \lnot (p\lor r) , from=3
            [1 \lnot p , from=7
            [1 \lnot r , from=7, close
        ]]]]
        [ (q\land r) , from=2
          [1 q , from=5
            [1 r , from=5
              [1 \lnot (p\lor q) , from=3
                [1 \lnot p , from=14
                  [1 \lnot q , from=14, close
              ]]]
              [1 \lnot (p\lor r) , from=3
                [1 \lnot p , from=15
                  [1 \lnot r , from=1500, close
  ]]]]]]]]]
\end{forest}
\end{document}

上述使得公式的中心水平對齊。這樣我們就得到

對齊的配方中心

代替

配方中心錯位

如原始程式碼所示。這已經提高了易讀性和美觀性。

拼圖中缺少的部分是組織一些內容，以便將 17. 和 19. 處的公式列的寬度設定為 15. 處的公式列的寬度，以便行號和對齊方式也水平對齊。 （整個樹也是如此。）

我覺得CFR 的這個回答提示計算每個公式寬度的方法。但我不知道如何儲存寬度，然後為每組公式選擇最寬的合適寬度。

另一個更新

我建立了一個fwidth傳遞給公式列寬度的 tok。現在一切都很好地對齊了，但需要權衡的是用戶需要為樹上的每個節點設定此鍵。找出應設定的內容的最佳方法是將分支的最寬公式插入程式碼中

\newlength{\myl}
\settowidth{\myl}{formula goes here}
\the\myl

然後fwidth為分支中的每個公式設定該長度。請參閱下面的範例程式碼：

\documentclass[border=11pt]{standalone}
\usepackage[linguistics]{forest}
\usepackage{amsmath,amssymb}
\usepackage{array}
\forestset{
  declare toks={from}{},
  declare toks={fwidth}{},
  declare toks register={claim},
  claim=,
  ll proof/.style={
    before typesetting nodes={
      if claim={}{}{
        replace by/.process={Rw{claim}{[##1, math content, append]}},
        no edge,
        before computing xy={l'=2\baselineskip},
      },
      tempcounta'=0,
      for tree breadth-first={
        tempcounta'+=1,
        content/.process={ OR OSl+tt= ? w  Ow4 {content}{tempcounta}{from}{}{}{(##1)}{fwidth}{\begin{tabular}{p{1em}>{\centering\arraybackslash}p{##4}p{1em}}##2. & \ensuremath{##1} & \ensuremath{##3}\\\end{tabular}} }
      }
    },
    where n children=1{!1.no edge, before computing xy={!1.l'=\baselineskip}}{},
    close/.style={label=below:\textsf{x}},
  },
}
\begin{document}
\begin{forest}
  ll proof,
  claim=\vdash ((p\lor (q\land r))\to((p\lor q)\land (p\lor r)))
  [ \lnot ((p\lor (q\land r))\to((p\lor q)\land (p\lor r))), fwidth=158.8pt    
    [ (p\lor (q\land r)) , from=1, fwidth=158.8pt
      [ \lnot ((p\lor q)\land (p\lor r)) , from=1, fwidth=158.8pt
        [ p , from=2, fwidth=5.1pt
          [ \lnot (p\lor q) , from=3, fwidth=35.5pt
            [ \lnot p , from=6, fwidth=35.5pt
              [ \lnot q , from=6, close, fwidth=35.5pt
          ]]]
          [ \lnot (p\lor r) , from=3, fwidth=35.5pt
            [1 \lnot p , from=7, fwidth=35.5pt
            [1 \lnot r , from=7, close, fwidth=35.5pt
        ]]]]
        [ (q\land r) , from=2, fwidth=28.6pt
          [1 q , from=5, fwidth=28.6pt
            [1 r , from=5, fwidth=28.6pt
              [1 \lnot (p\lor q) , from=3, fwidth=40.5pt
                [1 \lnot p , from=14, fwidth=40.5pt
                  [1 \lnot q , from=14, close, fwidth=40.5pt
              ]]]
              [1 \lnot (p\lor r) , from=3, fwidth=40.5pt
                [1 \lnot p , from=15, fwidth=40.5pt
                  [1 \lnot r , from=1500, close, fwidth=40.5pt
  ]]]]]]]]]
\end{forest}
\end{document}

fwidth現在看起來確實不錯，但如果能自動計算和設定那就方便多了。 （隱藏因將行號和對齊列設置為較小的固定寬度而產生的過滿警告也很好。）我等待對 TikZ 有更深入了解的人來forest指路。

答案1

這是tabular/align想法的變體，它會自動確定中心列的寬度（對於 wff）。

% ref.: https://tex.stackexchange.com/q/570449/

\documentclass[border=11pt]{standalone}
\usepackage[linguistics]{forest}
\usepackage{amsmath,amssymb,array}
\newcolumntype{C}[1]{>{\centering $}p{#1}<{$}}
\forestset{
  declare toks={from}{},
  declare toks register={claim},
  declare boolean={align me}{0},
  declare dimen={my width}{0pt},
  declare dimen register={lmeas},
  lmeas/.pgfmath=width("99."),
  declare dimen register={rmeas},
  rmeas/.pgfmath=width("(99)"),
  claim=,
  ll proof/.style={
    for tree={
      math content,
    },
    for root=align me,
    before typesetting nodes={
      if claim={}{}{
        replace by/.process={Rw{claim}{[##1, math content, append]}},
        no edge,
        before computing xy={l'=2\baselineskip},
      },
    },
    where n children=1{!1.no edge, before computing xy={!1.l'=\baselineskip},}{},
    for root={align me},
    where n children>=2{
      for children={align me}}{},
    before packing={
      tempcountb'=0,
      where align me={%
        tempcountb'+=1,
        tempdima/.max={>{OOw2+d}{max x}{min x}{##1-##2}}{%
          walk and save={temptoksa}{current,
             until={> O_=!{n children}{1}}{first,typeset node}}%
        },
        for nodewalk={load=temptoksa}{my width/.register=tempdima, typeset node}, 
      }{},
      tempcounta'=0,
      for tree breadth-first={
        tempcounta'+=1,
        align=p{\foresteregister{lmeas}}C{\foresteoption{my width}}p{\foresteregister{rmeas}},
        content/.process={ OR OSl+tt= ? w  w3 {content}{tempcounta}{from}{}{}{(##1)}{##2.\quad & ##1\quad & ##3} },
        typeset node,
      }
    },
    close/.style={label=below:\textsf{x}},
  },
}
\begin{document}
\begin{forest}
  ll proof,
  claim=\vdash ((p\lor (q\land r))\to((p\lor q)\land (p\lor r)))
  [ \lnot ((p\lor (q\land r))\to((p\lor q)\land (p\lor r)))    
    [ (p\lor (q\land r)) , from=1
      [ \lnot ((p\lor q)\land (p\lor r)) , from=1
        [ p , from=2
          [ \lnot (p\lor q) , from=3
            [ \lnot p , from=6
              [ \lnot q , from=6, close
          ]]]
          [ \lnot (p\lor r) , from=3
            [1 \lnot p , from=7
            [1 \lnot r , from=7, close
        ]]]]
        [ (q\land r) , from=2
          [1 q , from=5
            [1 r , from=5
              [1 \lnot (p\lor q) , from=3
                [1 \lnot p , from=14
                  [1 \lnot q , from=14, close
              ]]]
              [1 \lnot (p\lor r) , from=3
                [1 \lnot p , from=15
                  [1 \lnot r , from=15, close
  ]]]]]]]]]
\end{forest}
\end{document}

表格分割線編號與對齊方式

無論如何，薩索可以做得更快，但我缺乏練習，所以其他人可能也能做得更好。花哨的列說明符似乎與forest的解析器糾纏在一起。因此，這種方法有點笨拙。就像我說的，其他人無疑會讓它表現得更有禮貌。

相關內容