Per digitare i connettivi logici:
∧ : \land∨ : \lor¬ : \lnot⇒ : =>, \Rightarrow ⊥ : \bot⊤ : \topPer digitare i quantificatori:
∀ : \forall∃ : \existsPer visualizzare l'albero man mano che viene costruito
dai comandi impartiti al sistema, premere F3 e poi
premere sul bottome home (in genere contraddistinto da
una icona rappresentate una casa).
Si suggerisce di marcare tale finestra come always on top
utilizzando il menu a tendina che nella maggior parte degli
ambienti grafici si apre cliccando nel suo angolo in
alto a sinistra.
Applicazioni di regole errate vengono contrassegnate con il colore rosso.
Una volta dimostrati alcuni utili lemmi come A ∨ ¬A è possibile
riutilizzarli in altre dimostrazioni utilizzando la "regola" lem.
La "regola" lem prende come argomenti:
Il numero delle ipotesi del lemma che si vuole utilizzare, nel
caso del terzo escluso 0, nel caso di ¬¬A⇒A le ipotesi sono 1.
Dopo il numero di ipotesi, è necessario digitare il nome del lemma.
Infine, le formule che devono essere scritte come premesse per la "regola".
Ad esempio, per usare il lemma EM (terzo escluso) basta digitare
lem 0 EM, mentre per usare il lemma NNAA (¬¬A⇒A) bisogna digitare
lem 1 NNAA (¬¬A). Ai lemmi con più di una premessa è necessario
far seguire le parentesi quadre come spiegato in precedenza.
Si noti che "regola" lem non è una vera regola, ma una forma compatta
per rappresentare l'albero di prova del lemma che si sta riutilizzando.
Per motivi che saranno più chiari una volta studiate logiche del
primo ordine o di ordine superiore, i lemmi che si intende
riutilizzare è bene che siano dimostrati astratti sugli atomi.
Ovvero per ogni atomo A...Z che compare nella formula,
è bene aggiungere una quantificazione all'inizio della formula stessa.
Ad esempio scrivendo ∀A:CProp. prima della formula A ∨ ¬A.
La dimostrazione deve poi iniziare con il comando assume.
In tale modo il lemma EM può essere utilizzato sia per dimostrare
A ∨ ¬A, sia B ∨ ¬B, sia (A∨C) ∨ ¬(A∨C), etc ...