Eu tenho usado oÀ prova de lógicapacote para escrever provas no estilo Fitch. Ele cria ambientes usando tabelas para tornar as provas escritas menos incômodas.
Não consigo descobrir como criar uma caixa tracejada em uma subprova como neste exemplo:
Isso é o que tenho até agora. A segunda subprova deve, entretanto, usar uma caixa tracejada.
\documentclass{article}
\usepackage{logicproof}
\usepackage{amssymb}
\begin{document}
\begin{logicproof}{2}
\begin{subproof}
\square p \land \square q & assumption\\
\square p & $\land \mathrm{e}_1$ 1\\
\square q & $\land \mathrm{e}_2$ 1\\
\begin{subproof} %This should have a dashed box
p & $\square \mathrm{e}$ 2\\
q & $\square \mathrm{e}$ 3\\
p \land q & $\land \mathrm{i}$ 4, 5
\end{subproof}
\square (p \land q) & $\square \mathrm{i}$ 4--6
\end{subproof}
\square p \land \square q \to \square (p \land q) & $\to \mathrm{i}$ 1--7
\end{logicproof}
\end{document}
Alguém sabe se é possível criar uma subprova tracejada usando prova lógica?
Se isso não for possível, como criar um ambiente semelhante ao ambiente subproof?
Responder1
Como ninguém respondeu a isso há quase um mês, vou postar minha solução parcial na esperança de que alguém aceite o desafio.
O pacote utiliza um tabularambiente, basicamente, para construir a prova. Ele usa \clinepara desenhar as linhas horizontais. Portanto, se pudermos substituir as linhas tracejadas, poderemos resolver metade do problema.
arydshlnsuporta regras horizontais e verticais tracejadas em tabularambientes array. Portanto, podemos substituí-lo \cdashline{}pelo padrão \cline{}.
Fazemos isso fazendo uma cópia modificada do logicproofcomando ' \lp@cr@clines, que chamamos \lp@cr@cdashlines, e uma cópia modificada do logicproofambiente ' subproof, que chamamos subproofd. subproofdusa \lp@cr@cdashlinesonde subproofusa \lp@cr@clinese \lp@cr@cdashlinesusa \cdashline{}onde \lp@cr@clinesusa cline{}.
O resultado disso é que podemos usar subproofdno lugar de subproofpara compor uma subprova cujas linhas horizontais da caixa são tracejadas em vez de contínuas.
Obviamente, o problema restante é fazer com que as linhas verticais da caixa sejam tracejadas. O problema é que ele arydshlnsuporta regras tracejadas verticais, fornecendo uma alternativa para |especificações / tabular.array
Mas logicproofnão utiliza esse mecanismo para desenhar as linhas verticais de suas caixas, como mostra sua especificação de coluna padrão:
{{r@{~~~}*{#1}{l}@{~}>{$}l<{$}@{~~~~}l@{~}*{#1}{r}}}
Em vez disso, ele usa \vlinee não sei como fazeressesespalhado no subproofdambiente.
\documentclass{article}
\usepackage{logicproof}
\usepackage{arydshln}
\usepackage{amssymb}
\newcommand*{\nec}{\ensuremath{\mathord{\square}}}
\makeatletter
\newcommand{\lp@cr@cdashlines}{% modified copy of lp@cr@clines
\lp@set@clines%
\lp@orig@arraycr%
\cdashline{\value{lp@cline@1}-\value{lp@cline@2}}%
}
\newenvironment{subproofd}{% modified copy of subproof
\ifthenelse{%
\value{lp@total@nests}>\value{lp@nested}%
}{% All is well; don't do anything.
}{%
\PackageError{logicproof}{Too many nested subproofs!}{%
Increase the maximum number of nested subproofs allowed
in the current logicproof environment.%
}%
}%
\endgroup%
\lp@stop@proof@line%
\lp@orig@arraycr%
\lp@add@space%
\lp@go@up@a@line%
\stepcounter{lp@nested}%
\lp@cr@cdashlines%
&%
\lp@continue@proof@line%
}{%
\ifthenelse{%
0<\value{lp@nested}%
}{% All is well; don't do anything.
}{%
\PackageError{logicproof}{Cannot end a subproof before it begins}{%
You must have a \protect\begin{subproof} before you can use %
\protect\end{subproof}.%
}%
}%
\lp@stop@proof@line%
\lp@cr@cdashlines%
\addtocounter{lp@nested}{-1}%
\lp@extend@space%
\lp@start@proof@line%
\begingroup%
\def\@currenvir{subproofd}%
}
\makeatother
\begin{document}
\begin{logicproof}{2}
\begin{subproof}
\nec p \land \nec q & assumption\\
\nec p & $\land \mathrm{e}_1$ 1\\
\nec q & $\land \mathrm{e}_2$ 1\\
\begin{subproofd} %This should have a dashed box
p & $\nec \mathrm{e}$ 2\\
q & $\nec \mathrm{e}$ 3\\
p \land q & $\land \mathrm{i}$ 4, 5
\end{subproofd}
\nec (p \land q) & $\nec \mathrm{i}$ 4--6
\end{subproof}
\nec p \land \nec q \to \nec (p \land q) & $\to \mathrm{i}$ 1--7
\end{logicproof}
\end{document}