Emesta resposta, o usuário cfr oferece o seguinte código que fornece saída como na imagem a seguir:
\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}
Gostaria de saber se alguém sabe como modificar o código para produzir uma saída como na imagem a seguir:
Uma abordagem que posso imaginar é armazenar as larguras de cada número de linha mais largo, fórmula e justificação ao longo de cada ramificação e, em seguida, agrupar o conteúdo de cada nó na ramificação em uma tabela de três colunas onde as larguras das colunas são fixadas para essas larguras máximas. Em seguida, a posição das âncoras dos nós seria definida ao norte da coluna de fórmula, de modo que as linhas entre os ramos fossem desenhadas para os centros das fórmulas.
Uma abordagem significativamente menos elegante, mas muito mais fácil, seria ter tabulares de múltiplas linhas contendo todas as fórmulas em uma ramificação (ou seja, uma para as fórmulas numeradas 1, 2, 3; outra para 4; outra para 5, 8, 11; e assim por diante ). Mas eu gostaria de evitar uma abordagem como essa, que exigiria mudanças significativas na própria árvore, e não no seu estilo.
Infelizmente, no momento não tenho o conhecimento técnico para saber por onde começar a implementar uma solução mais elegante, por isso agradeceria qualquer ajuda oferecida.
ATUALIZAR
Aqui está uma resposta parcial que envolve o processamento do conteúdo em uma tabela de uma linha com três colunas, uma para o número da linha, uma para a wff e outra para a justificativa:
\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}
O acima faz com que os centros das fórmulas fiquem alinhados horizontalmente. Assim obtemos
em vez de
como no código original. Isso já melhora a legibilidade e a estética.
A peça que falta no quebra-cabeça é organizar as coisas de forma que as larguras das colunas da fórmula em 17. e 19. sejam definidas para a largura da coluna de fórmula em 15. para que os números das linhas e as justificações também sejam alinhados horizontalmente. (E da mesma forma em toda a árvore.)
eu penso issoesta resposta por cfrsugere uma maneira de calcular a largura de cada fórmula. Mas não sei como armazenar as larguras e depois selecionar a mais larga e apropriada para cada conjunto de fórmulas.
Outra atualização
Criei um fwidthtok que é passado para a largura da coluna da fórmula. Agora tudo está bem alinhado, mas a desvantagem é que o usuário precisa definir essa chave para cada nó da árvore. A melhor maneira de descobrir como deve ser definido é inserir a fórmula mais ampla de uma ramificação no código
\newlength{\myl}
\settowidth{\myl}{formula goes here}
\the\myl
e, em seguida, defina fwidthesse comprimento para cada fórmula na ramificação. Veja o código de exemplo abaixo:
\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}
As coisas parecem muito boas agora, mas seria consideravelmente mais conveniente se fwidthpudesse ser calculado e definido automaticamente. (Também seria bom ocultar os avisos excessivos que surgem ao definir o número da linha e as colunas de justificação para uma pequena largura fixa.) Aguardo alguém com um conhecimento mais profundo do TikZ e forestque mostre o caminho.
Responder1
Aqui está uma variação da ideia tabular/ alignque determina automaticamente a largura da coluna central (para a 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}
Sašo poderia tornar isso mais rápido de qualquer maneira, mas estou sem prática, então outra pessoa também poderá fazer melhor. O especificador de coluna sofisticado parecia estar emaranhado com foresto analisador. Daí a abordagem um tanto desajeitada. Como eu disse, outra pessoa sem dúvida fará com que ele se comporte de maneira mais educada.