He estado usando elA prueba de lógicapaquete para escribir pruebas en estilo Fitch. Crea entornos utilizando tabulares para que la redacción de pruebas sea menos molesta.
Parece que no puedo entender cómo crear un cuadro discontinuo en una subprueba como en este ejemplo:
Esto es lo que tengo hasta ahora. Sin embargo, la segunda subprueba debería utilizar un cuadro discontinuo.
\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}
¿Alguien sabe si es posible crear una subprueba discontinua usando prueba lógica?
Si eso no es posible, ¿cómo se podría crear un entorno similar al entorno subprueba?
Respuesta1
Como nadie ha respondido a esto en casi un mes, publicaré mi solución parcial con la esperanza de que alguien más acepte el desafío.
El paquete utiliza un tabularentorno, básicamente, para construir la prueba. Se utiliza \clinepara dibujar las líneas horizontales. Entonces, si podemos sustituir las líneas discontinuas, podríamos resolver la mitad del problema.
arydshlnadmite reglas horizontales y verticales discontinuas en tabularentornos array. Entonces podemos sustituirlo \cdashline{}por el estándar \cline{}.
Hacemos esto haciendo una copia modificada del logicproofcomando de ' \lp@cr@clines, al que llamamos \lp@cr@cdashlines, y una copia modificada del logicproofentorno de ' subproof, al que llamamos subproofd. subproofdusos \lp@cr@cdashlinesdonde subproofse usa \lp@cr@clinesy \lp@cr@cdashlinesusos \cdashline{}donde \lp@cr@clinesse usa cline{}.
El resultado de esto es que podemos usar subproofden lugar de subproofpara componer una subprueba cuyas líneas horizontales del cuadro sean discontinuas en lugar de continuas.
Obviamente, el problema restante es hacer que las líneas verticales del cuadro sean discontinuas. El problema es que arydshlnadmite reglas de guiones verticales al proporcionar una alternativa a |/ tabularespecificaciones array.
Pero logicproofno utiliza este mecanismo para dibujar las líneas verticales de sus cuadros como muestra su especificación de columna estándar:
{{r@{~~~}*{#1}{l}@{~}>{$}l<{$}@{~~~~}l@{~}*{#1}{r}}}
En cambio, usa \vliney no estoy seguro de cómo hacerestosesparcido en el 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}