cerca
LyX
modifica cronologia stampa login logout

Wiki

UniCrema


Materie per semestre

Materie per anno

Materie per laurea


Help

Return to LyX  (Edit)

Uni.Lyx History

Hide minor edits - Show changes to output

Added lines 68-70:

----
[[LogicaMatematica]]
Added lines 1-67:
(:title LyX:)
%titolo%''':: LyX ::'''

%rframe%Attach:lyx.jpg

!!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.