☰

論理証明ツリーのノード間の整列がフォレストでタイプセットされている

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 つの方法は、各ブランチに沿って最も幅の広い行番号、数式、および位置揃えの幅を保存し、ブランチ上の各ノードの内容を、列幅がこれらの最大幅に固定された 3 列の表にラップすることです。次に、ノードのアンカーの位置を数式列の北に設定して、ブランチ間の線が数式の中心に描画されるようにします。

かなりエレガントさには欠けますが、はるかに簡単なアプローチは、ブランチ上のすべての数式を含む複数行の表を作成することです (つまり、1、2、3 の数式用に 1 つ、4 用に 1 つ、5、8、11 用に 1 つ、など)。ただし、スタイルではなくツリー自体に大幅な変更が必要になるこのようなアプローチは避けたいと思います。

残念ながら、私は現時点では、より洗練されたソリューションを実際に実装するにはどこから始めればよいのかさえわからないほどの技術的な専門知識を持っていないので、提供されたあらゆる支援をいただければ幸いです。

アップデート

以下は、コンテンツを 3 つの列 (行番号用、wff 用、正当化用) を持つ 1 行の表に処理する部分的な回答です。

\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によるものです各数式の幅を計算する方法についてのヒント。しかし、幅を保存して、数式の各セットに最も適切な幅を選択する方法がわかりません。

もう一つのアップデート

数式列の幅に渡される tokを作成しましたfwidth。これですべてがうまく整列しましたが、トレードオフとして、ユーザーはツリー上のすべてのノードにこのキーを設定する必要があります。設定すべき値を見つける最良の方法は、ブランチの最も広い数式をコードに挿入することです。

\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

これは、中央の列の幅を自動的に決定する (wff の場合) tabular/のアイデアのバリエーションです。align

% 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}

テーブル分割ライン番号と位置合わせ

Sašo ならいずれにせよこれをより速くできるでしょうが、私は練習不足なので、他の誰かがもっとうまくできるかもしれません。複雑な列指定子はforestのパーサーと絡み合っているようです。そのため、やや扱いにくいアプローチになっています。私が言うように、他の誰かが間違いなくこれをより丁寧に動作させるでしょう。

関連情報