☰

Хорошее выравнивание по узлам в деревьях логического доказательства, набранных с помощью леса

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намекает на способ вычисления ширины каждой формулы. Но я не знаю, как хранить ширины, а затем выбирать наиболее широкую подходящую для каждого набора формул.

Еще одно обновление

Я создал fwidthtok, который передается ширине столбца формулы. Теперь все хорошо выровнено, но компромисс заключается в том, что пользователю нужно задать этот ключ для каждого узла в дереве. Лучший способ узнать, что ему следует задать, — это вставить самую широкую формулу ветви в код

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

таблица-разделить-строку-nos-с-выравниванием

Sašo мог бы сделать это быстрее в любом случае, но я не практиковался, так что кто-то другой тоже может сделать лучше. Причудливый спецификатор столбцов, похоже, запутался в forestпарсере '. Отсюда и несколько неуклюжий подход. Как я уже сказал, кто-то другой, несомненно, заставит его вести себя более вежливо.

Связанный контент