...

[helm.git] / helm / software / matita / library / didactic / exercises / natural_deduction.ma

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
    ===========
 
 (* Esercizio 0
    ===========
 


@@ -17,6 +23,16 @@
 
 (*DOCBEGIN
 
 
 (*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
 ===================
 
 I connettivi logici
 ===================
 


@@ -32,11 +48,8 @@ Per digitare i connettivi logici:
 I termini, le formule e i nomi delle ipotesi
 ============================================
 
 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
 * 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 `]`.
 
 * 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 `]`.
 
 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)
 
         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
 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
 =====================
 
 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.
 (* 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));
 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]).
 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.
 
 (*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*)
 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*)