Indiese Antwortbietet der Benutzer cfr den folgenden Code an, der die Ausgabe wie im folgenden Bild liefert:
\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}
Ich frage mich, ob jemand weiß, wie man den Code ändert, um eine Ausgabe wie im folgenden Bild zu erzeugen:
Ein Ansatz, der mir einfällt, besteht darin, die Breiten der breitesten Zeilennummer, Formel und Ausrichtung entlang jedes Zweigs zu speichern und dann den Inhalt jedes Knotens auf dem Zweig in eine dreispaltige Tabelle einzuschließen, in der die Spaltenbreiten auf diese maximalen Breiten festgelegt sind. Dann würde die Position der Anker der Knoten nördlich der Formelspalte festgelegt, sodass die Linien zwischen den Zweigen in die Mitte der Formeln gezeichnet werden.
Ein deutlich weniger eleganter, aber viel einfacherer Ansatz wäre, mehrzeilige Tabellen zu haben, die alle Formeln eines Zweigs enthalten (also eine für die Formeln mit den Nummern 1, 2, 3, eine andere für 4, eine andere für 5, 8, 11 usw.). Aber ich möchte einen solchen Ansatz vermeiden, der erhebliche Änderungen am Baum selbst und nicht an seinem Stil erfordern würde.
Leider verfüge ich derzeit nicht über das erforderliche technische Fachwissen, um zu wissen, wo ich mit der Implementierung einer eleganteren Lösung beginnen soll. Daher wäre ich für jede angebotene Hilfe dankbar.
AKTUALISIEREN
Hier ist eine Teilantwort, bei der der Inhalt in eine einzeilige Tabelle mit drei Spalten verarbeitet wird, eine für die Zeilennummer, eine für das WFF und eine weitere für die Begründung:
\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}
Das Obige sorgt dafür, dass die Mittelpunkte der Formeln horizontal ausgerichtet sind. Somit erhalten wir
anstatt
wie im Originalcode. Dies verbessert bereits die Lesbarkeit und Ästhetik.
Das fehlende Puzzleteil besteht darin, die Dinge so zu organisieren, dass die Breiten der Formelspalten bei 17. und 19. auf die Breite der Formelspalte bei 15. eingestellt sind, sodass die Zeilennummern und Ausrichtungen ebenfalls horizontal ausgerichtet sind. (Und ähnlich im gesamten Baum.)
ich denke, dassdiese Antwort von cfrHinweise zu einer Methode zum Berechnen der Breite jeder Formel. Aber ich weiß nicht, wie ich die Breiten speichern und dann für jeden Formelsatz die breiteste geeignete auswählen kann.
Ein weiteres Update
Ich habe einen fwidthToken erstellt, der an die Breite der Formelspalte übergeben wird. Jetzt ist alles schön ausgerichtet, aber der Nachteil ist, dass der Benutzer diesen Schlüssel für jeden Knoten im Baum festlegen muss. Der beste Weg, um herauszufinden, auf welchen Wert er eingestellt werden sollte, besteht darin, die breiteste Formel eines Zweigs in den Code einzufügen.
\newlength{\myl}
\settowidth{\myl}{formula goes here}
\the\myl
und dann fwidthfür jede Formel im Zweig auf diese Länge setzen. Siehe den Beispielcode unten:
\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}
Jetzt sieht alles wirklich gut aus, aber es wäre wesentlich praktischer, wenn fwidthes automatisch berechnet und eingestellt werden könnte. (Es wäre auch schön, die Überfüllwarnungen auszublenden, die auftreten, wenn die Zeilennummern- und Rechtfertigungsspalten auf eine kleine feste Breite eingestellt werden.) Ich warte auf jemanden mit tieferen Kenntnissen von TikZ, der mir forestden Weg zeigt.
Antwort1
Hier ist eine Variation der tabular/ align-Idee, die die Breite der mittleren Spalte (für das wff) automatisch bestimmt.
% 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 könnte das auf jeden Fall schneller machen, aber ich bin aus der Übung, also kann es vielleicht auch jemand anderes besser machen. Der ausgefallene Spaltenspezifizierer schien sich mit forestdem Parser von zu verheddern. Daher der etwas schwerfällige Ansatz. Wie ich schon sagte, wird es zweifellos jemand anderes höflicher machen.