...

diff --git a/helm/software/matita/library/didactic/exercises/natural_deduction.ma b/helm/software/matita/library/didactic/exercises/natural_deduction.ma
index 5e71888149f9047fcab44fe45da3a8a8798e9c56..7f941c1189ed34d408ace19df731848b1007f895 100644 (file)
--- a/helm/software/matita/library/didactic/exercises/natural_deduction.ma
+++ b/helm/software/matita/library/didactic/exercises/natural_deduction.ma
@@ -1,3 +1,9 @@
+(* Istruzioni: 
+
+     http://mowgli.cs.unibo.it/~tassi/exercise-natural_deduction.html 
+
+*)
+
 (* Esercizio 0
    ===========
 
@@ -17,6 +23,16 @@
 
 (*DOCBEGIN
 
+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
 ===================
 
@@ -32,11 +48,8 @@ Per digitare i connettivi logici:
 I termini, le formule e i nomi delle ipotesi
 ============================================
 
-* I termini quantificati da `∀` e `∃`, quando argomenti di
-  una regola, vengono scritti tra `{` e `}`.
-
 * Le formule, quando argomenti di
-  una regola, vengono scritti tra `(` e `)`.
+  una regola, vengono scritte tra `(` e `)`.
 
 * I nomi delle ipotesi, quando argomenti di
   una regola, vengono scritti tra `[` e `]`.
@@ -50,7 +63,7 @@ sulla sinistra dopo aver premuto `F2`.
 
 L'albero si descrive partendo dalla radice. Le regole
 con premesse multiple sono seguite da `[`, `|` e `]`.
-Ad esempio 
+Ad esempio: 
 
         apply rule (∧_i (A∨B) ⊥);
           [ …continua qui il sottoalbero per (A∨B)
@@ -60,12 +73,16 @@ Ad esempio
 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.
+regola stessa. Ad esempio:
 
-Le formule sono racchiuse tra `(` e `)`, mentre i nomi
-che date ad ipotesi aggiuntive (nella regola di eliminazione
-dell' OR, in RAA, e nella regola di introduzione 
-dell'implicazione) sono ragghiusi tra `[` e `]`.  
+        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
 =====================
@@ -91,8 +108,10 @@ theorem EM: ∀A:CProp. A ∨ ¬ A.
 (* Il comando assume è necessario perchè dimostriamo A∨¬A
    per una A generica. *)
 assume A: CProp.
+(* Questo comando inizia a disegnare l'albero *)
 apply rule (prove (A ∨ ¬A));
-
+(* qui inizia l'albero, eseguite passo passo osservando come
+   si modifica l'albero. *)
 apply rule (RAA [H] (⊥)).
 apply rule (¬_e (¬(A ∨ ¬A)) (A ∨ ¬A));
        [ apply rule (discharge [H]).
@@ -176,6 +195,8 @@ apply rule (∨_e (B∨¬B) [h5] (C) [h6] (C));
 (*END*)
 qed.
 
+(* Per dimostrare questo teorema torna comodo il lemma EM
+   dimostrato in precedenza. *)
 theorem ex3: (F ⇒ G∨E) ⇒ (G ⇒ ¬L∨E) ⇒ (L⇒F) ⇒ L ⇒ E.
 apply rule (prove ((F ⇒ G∨E) ⇒ (G ⇒ ¬L∨E) ⇒ (L⇒F) ⇒ L ⇒ E));
 (*BEGIN*)