Scopo della lezione

Lo scopo della lezione è di farvi imparare ad usare Matita per auto-correggervi gli esercizi di deduzione naturale, che saranno parte dell'esame scritto. Il consiglio è di fare prima gli esercizi su carta e poi digitarli in Matita per verificarne la correttezza. Fare direttamente gli esercizi con Matita è difficile e richiede molto più tempo.

I connettivi logici

Per digitare i connettivi logici:

I termini, le formule e i nomi delle ipotesi

Le regole di deduzione naturale

Per digitare le regole di deduzione naturale è possibile utilizzare la palette che compare sulla sinistra dopo aver premuto F2.

L'albero si descrive partendo dalla radice. Le regole con premesse multiple sono seguite da [, | e ]. Ad esempio:

    apply rule (∧#i (A∨B) ⊥);
      [ …continua qui il sottoalbero per (A∨B)
      | …continua qui il sottoalbero per ⊥
      ]

Le regole vengono applicate alle loro premesse, ovvero gli argomenti delle regole sono le formule che normalmente scrivete sopra la linea che rappresenta l'applicazione della regola stessa. Ad esempio:

    aply rule (∨#e (A∨B) [h1] C [h2] C);
      [ …prova di (A∨B)
      | …prova di C sotto l'ipotesi A (di nome h1)  
      | …prova di C sotto l'ipotesi B (di nome h2)
      ]

Le regole che hanno una sola premessa non vengono seguite da parentesi quadre.

L'albero di deduzione

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