Musterlösung 1. Aufgabenblatt.

Aufgabe 1

Zu zeigen: alle Zahlen teilen 0.
use_thy "gcd";

goalw thy [divides_def] "x divides 0";

br exI 1; 
br (mult_0 RS sym) 1;
result();
Wichtig: einen Beweis immer mit result() oder qed() abschliessen. No subgoals heisst nicht notwendigerweise, das der Beweis erfolgreich war. Hier ist ein Gegenbeispiel:
use_thy "gcd";
goal thy "x divides 0";
by (rewrite_tac [divides_def]);
br exI 1;
br (mult_0 RS sym) 1;
result(); 

Aufgabe 2:

  1. Symmetrie der Gleichheit.

    Der Schlüssel ist hier, die richtige Unfikation für die Substitutionsregel zu finden:

    val [p]= goal thy "r=s ==> s=r";
    br subst 1;
    back();
    back();
    br p 1;
    br refl 1;
    result();
    
  2. Transitivität der Gleichheit.

    Eine andere Möglichkeit ist Verwendung von res_inst_tac. Bei dieser Taktik kann man der Unifikation eine Substitution, geschrieben als eine Liste von Paaren bestehend aus dem Variablennamen (ohne das Fragezeichen) und einem Wert, vorgeben.

    val [p1,p2]= goal thy "[| r= s;  s= t |] ==> r= t";
    by (res_inst_tac [("P", "%x. r= x")] subst 1);
    br p2 1;
    br p1 1;
    result();
    
  3. Wir beweisen die Einführungsregel für den Existenzquantor, und die Eliminationsregel für den Allquantor.

    Hier vergessen wir die Prämissen und verwenden wir mal premises().

    goalw thy [Ex_def] "P x==> ? x. P x";
    br selectI 1;
    br (hd(premises())) 1;
    result();
    
    Die Eliminationsregel (genauer gesagt, die Destruktionsregel) des Allquantors erfordert die Kongruenz der Funktionsapplikation, und wieder eine Suche nach der richtigen Unifikation:
    val [p]= goalw thy [All_def] "! x. P(x)==> P(y)";
    br eqTrueE 1;
    br fun_cong 1;
    back();  
    back();
    br p 1;
    result();
    
  4. Für die Kongruenzregeln benötigt man auch wieder die Substitutivität. Hier kürzen wird die Suche nach der richtigen Unifikation ab, indem wir mit der Prämisse vorwärtsresolvieren (anstelle von Rückwärtsresolution mit subst, gefolgt von der mehreren back()'s):
    val [p]= goal thy "x=y ==> f(x)= f(y)";
    br (p RS subst) 1;
    br refl 1;
    result();
    
    Dieses Verfahren läßt sich auch einfach auf den zweiten Beweis verallgemeinern:
    val [p1,p2]= goal thy "[| x= y; f= g |] ==> f x= g y";
    br (p1 RS subst) 1;
    br (p2 RS subst) 1;
    br refl 1;
    result();
    

Aufgabe 3

Zu erst einmal wird an drei Stellen Rückwärtsresolution, gefolgt von Beweis durch Annahme durchgeführt, was durch eine Eliminationsresolution ersetzt werden kann. Damit ergibt sich nach den ersten für die ersten Schritte:
goal thy "(A|B)&~A-->B";
br impI 1;
be conjE 1;

Level 2
(A | B) & ~ A --> B
 1. [| A | B; ~ A |] ==> B
val it = () : unit
Eine Rückwärtsresolution mit conjE erzeugt jetzt nur eine Konjunktion mit einer Meta-Variablen, die später wieder durch Rückwärtsresolution mit conjI bewiesen werden muß. Das ist überflüssig, wir können vielmehr direkt mit der Elimination der Disjunktion, gefolgt von der Elimination der Negation, forfahren. Der Rest folgt dann durch Annahme:
be disjE 1;
be notE 1;
ba 1;
ba 1;
result();

Christoph Lueth
Last modified: Fri Apr 5 18:16:49 CEST 2002