:: LyX ::
Scrivere dimostrazioni con LyX
LyX offre in automatico la possibilità di inserire formule matematiche, ma queste sono insufficienti per scrivere sequenti. Occorre lo stile bussproofs.sty, che dovrebbe essere incluso nel MikTeX che LyX installa di suo, nel caso di Windows, e da qualche parte nei pacchetti di texlive per Linux.
Occorre mettere, nelle impostazioni del documento, alla voce preambolo la seguente roba:
\usepackage{bussproofs}
Qui il path di bussproofs non è installato, in quanto dovrebbe essere rintracciabile nel path di default. Questa inclusione permette a LaTex di interpretare il codice qui sotto.
Per inserire un frammento di codice Tex direttamente si preme CTRL-L e compare un quadrato apposito.
Per mettere un albero di prova (cioè i bei sequenti uno sopra l'altro etc.) si deve inserire la formula tra queste robe:
\begin{prooftree}
\end{prooftree}
I sequenti lavorano così: i vari sequenti si introducono con la scrittura \AxiomC{} mentre i segni di "frazione" li genera automaticamente, basta che gli dici di inferirne uno, due o tre. Per intenderci:
\begin{prooftree}
\AxiomC{A}
\UnaryInfC{B}
\end{prooftree}
ti crea una "frazione" con sopra la A e sotto il B.
Invece:
\begin{prooftree}
\AxiomC{A}
\AxiomC{B}
\UnaryInfC{C}
\end{prooftree}
crea una frazione con sopra A e B, e sotto C.
I comandi delle frazioni sono:
\UnaryInfC{}
\BinaryInfC{}
\TrinaryInfC{}
Una cosa da ricordare è che questi tre comandi prendono gli Assiomi o il risultato dei comandi che stanno prima di loro. UnaryInfC ha bisogno di un solo Assioma prima, BinaryInfC di due e TrinaryInfC di tre. Se mancano, salterà fuori un errore. Inoltre, per annidare le cose, occorre tenere a mente questa regola. Infatti, in:
\begin{prooftree}
\AxiomC{A}
\AxiomC{B}
\UnaryInfC{C}
\BinaryInfC{D}
\end{prooftree}
l'UnaryInfC{C} prenderà B e C e creerà una frazione con sopra B e sotto C. BinaryInfC{D} prenderà la A e il RISULTATO di UnaryInfC{D}, e sotto tutti e due mette la D.
LogicaMatematica
