Scopo della lezione

Lo scopo della lezione è di usare Matita come strumento per la correzione automatica degli esercizi di deduzione naturale, che saranno parte dell'esame scritto.

Per risolvere gli esericizi dovrete

  1. Risolvere su carta gli esercizi qui proposti.

  2. Ricopiare gli esercizi su Matita secondo le istruzioni che seguono.

Gli esercizi

  1. (A ⇒ (B ⇒ C)) ⇒ (A ∧ B) ⇒ C
  2. ¬(A∨B) ⇒ (¬A ∧ ¬B)
  3. ¬A ∧ ¬B ⇒ ¬(A∨B)
  4. ¬((A ∧ B) ⇒ C) ⇒ ¬(A ⇒ (B ⇒ C))
  5. (F ⇒ G∨E) ⇒ (G ⇒ ¬L∨E) ⇒ (L⇒F) ⇒ L ⇒ E
  6. (C∧G ⇒ E) ⇒ (¬L ⇒ E∨C) ⇒ G ∨ L ⇒ ¬L ⇒ E
  7. ¬(A ∧ (¬A ∨ B ∨ C) ∧ (¬B ∨ D) ∧ ¬C ∧ ¬D)

La tabella vista a lezione

Le istruzioni per Matita

  1. Con il comando F2 aprire la palette con le shortcut per le regole di deduzione naturale

  2. Con il comando F3 aprire un nuovo CIC browser e cliccare sul simbolo Home (una casa). In questa finestra verrà disegnato l'albero man mano che lo costruite.

  3. Cominciate a ricopiare l'albero di deduzione naturale che avete scritto su carta. La copiatura procede dal basso verso l'alto.

I connettivi logici

Per digitare i connettivi logici:

Le regole di deduzione naturale

Per digitare le regole di deduzione naturale utilizzate la palette che è comparsa sulla sinistra.

In questa palette troverete i template per tutte le regole di introduzione ed eliminazione dei connettivi viste a lezione TRANNE il template della regola di eliminazione dell'AND.

Ogni regola si occupa di riscrivere una riga/sottoalbero della vostra dimostrazione: immaginate che ogni comando apply_rule si occupi di riscrivere la premessa e la regola sotto utilizzata in questo modo

premessa

---------------- regola

Regola generica con una sola premessa

apply rule (nome_regola [eventuali ipotesi] (premessa) )

Esempio: se nell'ultimo passo di una deduzione naturale avessi utilizzato la regola di eliminazione dell'implica per concludere A → B scriverei:

apply rule (⇒_i [h1] (B));

dove ho chiamato h1 l'ipotesi A.

Regola generica con diverse premesse: queste regole sono seguite da
[, | e ] in questo modo

apply rule (nome_regola (premessa_1) ...  (premessa_n));
[ dimostrazione per premessa 1
| dimostrazione per premessa 2
...
| dimostrazione per premessa n
]

Ad esempio:

apply rule (∧_i (F) (G));
[ …continua qui il sottoalbero per (F)
| …continua qui il sottoalbero per (G)
]

Se nelle varie premesse vengono introdotte delle ipotesi queste vanno aggiunte tra parentesi quadre. Ad esempio nella regola di eliminazione dell'∨

apply rule (∨_e (A∨B) [h1] C [h2] C);
[ dimostrazione di (A∨B)
| dimostrazione di C sotto l'ipotesi A (di nome h1)  
| dimostrazione di C sotto l'ipotesi B (di nome h2)
]

In sintesi 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.

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

Quando arrivate ad una foglia del vostro albero utilizzerete la regola Discharge (Si trova tra Misc Rules)

apply rule (discharge [nome ipotesi]);

Template per la regola di eliminazione dell'

apply rule (∧_e (A ∧ B) [h1] [h2] (C));
  [ dimostrazione di (A ∧ B)
  | dimostrazione di (C) utilizzando le ipotesi A (chiamata h1) e B (chiamata h2)
  ]

Notazione: I termini, le formule e i nomi delle ipotesi

L'albero di deduzione

Nella finestra che avete aperto con il comando F3 man mano che lo costruite comparirà l'albero di deduzione.

Applicazioni di regole errate vengono contrassegnate con il colore rosso.

Suggerimenti