David Stanovský    //   

AUTOMATICKÉ DOKAZOVÁNÍ VĚT 2009/10

Přednáška podává přehled o základních technikách automatického dokazování matematických vět a jeho využití v matematice i informatice.
Obsah je podřízen následujícím cílům: 1) naučit se používat dokazovače, 2) naučit se jak dokazovače fungují, 3) zjistit k čemu je automatické dokazování dobré.

Obsah přednášky:

  1. Co je ATP - Overview Geoffa Sutcliffa (doma si přečtěte), grafické prostředí Prover9 (doma si nainstalujte), TPTP.org - knihovna problémů, soutěž CASC, SystemOnTPTP (doma si pohrajte)
  2. ATP v matematice - přehled úspěchů, začátek 1. přednášky Michaela Kinyona, [doplňující čtení: ATP v teorii kvazigrup]
  3. Princip dokazovače Prover9 - 1. přednáška M.K.
  4. Nastavení parametrů v Prover9 - 2. přednáška M.K., Robbins pomocí definic, [doplňující čtení: manuál k Prover9]
  5. Pokročilé techniky v Prover9 - 2. přednáška M.K. (hints), 3. přednáška M.K. (semantic guidance, zjednodušování důkazů), [doplňující čtení: použití probraných technik na konkrétním příkladě]
  6. Unifikace - slajdy Temura Kutsii, [doplňující čtení: zbytek kurzu Temura Kutsii, event. přednáška prof. Štěpánka]
  7. Dokazování ve výrokové logice - teorie, DPLL, [doplňující čtení: sekce Propositional logic/resolution v kurzech Geoffa Sutcliffa, a Andreje Voronkova; pro zajímavost, na téma délka důkazu PHP v rezolučním kalkulu]
  8. úplnost rezoluce (str.12)
    Dokazování v predikátové logice (ground level) - Voronkovovy slajdy část II
  9. Dokazování v predikátové logice (lifting) - Voronkovovy slajdy část III
  10. Dokazování v predikátové logice (implementace) - Voronkovovy slajdy část IV [alternativní značně zjednodušený výklad: 1. část této prezentace]
  11. Přepisující systémy a Waldmeister - zápisky část 1, část 2, [více: skripta J. Ježka, kapitola 13], vnitřnosti Waldmeistera (hlavně teda ten článek Citius, Altius, Fortius... v záhlaví, sekce 3.1)
  12. Tableaux
    Konstrukce modelů - článek o Paradoxu (úplně vpravo dole)
  13. Formální matematika - článek Toma Halese, prezentace Freeka Wiedijka, srovnání interaktivních dokazovačů, formalizace top 100 matematických vět, knihovna Mizar

Literatura:
materiály budou průběžně dávány k dispozici
TPTP.org - základní zdroj
Prover9 - dokazovač ke stažení (ne nejlepší, ale určitě nejvíc user friendly) [L:\Matematika\Prover9]
všechny dokazovače (Systems on TPTP)
přednáška Geoffa Sutcliffa
přednáška Andreje Voronkova
přednáška Michaela Kinyona (úplně dole)
přednáška v Saarbrückenu

Zkouška: bude formou domácích prací.
Minimální počty bodů: 1 - 29 bodů, 2 - 26 bodů, 3 - 23 bodů.
Po nápovědách jsou bodová ohodnocení snížena na polovinu.

Úlohy ke zkoušce (definitivní stav!):

Použití dokazovačů:
Úlohy 1-4 mají nápovědu 16.11. 15:30, poslední možnost odevzdání 30.11. 15:30.

  1. (1 bod) Rozhodněte, zda platí následující tvrzení (uvedené pojmy viz Sekce 2 zde).
    a) V Bruckově lupě pro každé dva prvky a,b platí: jestliže a^4=1 a b^5=1, pak ab=ba.
    b) V Bruckově lupě pro každé dva prvky a,b platí: jestliže a^3=1 a b^6=1, pak ab=ba.
    [odpověď: vstupní a výstupní soubory z nějakého dokazovače]
  2. (2 body) Formalizujte a dokažte následující úlohu.
    a) Mějme grupu G(*) a zobrazení f:G->G. Pokud f(x*y)=f(x)*f(y) pro všechna x,y z G, pak je f homomorfismus.
    b) Mějme grupy G(*),H(+) a zobrazení f:G->H. Pokud f(x*y)=f(x)+f(y) pro všechna x,y z G, pak je f homomorfismus.
    [odpověď: vstupní a výstupní soubory z nějakého dokazovače]
  3. (1 bod) Vyřešte úlohy SWV294-1.p a BOO060-1.p z databáze TPTP pomocí nějakého dokazovače.
    [odpověď: výstupní soubory z nějakého dokazovače]
  4. (1 bod) Dokažte pomocí jiného dokazovače než z dílny Billa McCuna, že z Robbinsových axiomů plyne Winkerova podmínka (tj. ten slavný problém, který vyřešil McCune pomocí EQP, viz slajd 13 zde)
    [odpověď: vstupní a výstupní soubor z nějakého dokazovače]
Teorie:
Úlohy 1-6 mají nápovědu 16.11. 15:30, poslední možnost odevzdání 30.11. 15:30. Ostatní úlohy mají termín odevzdání 11.1. 15:30.
  1. (2 body) Najděte ekvivalentní množinu klauzulí k následujícím formulím.
    a) -( P(x,a) & ( y=f(y) | -P(a,a) ) )
    b) exists u ( ( all x (f(x,a)=y) ) -> ( (all v exists z P(v,z)) | f(y,g(u))!=a) )
    [stačí uvést výsledek, nikoliv postup]
  2. (1 bod) Aplikujte alespoň dvěma způsoby paramodulaci na následující dvě klauzule.
    (x * y) * (x * z) = x * (y * z).
    (x * y) * (z * y) = (x * z) * y.
    [odpověď: klauzule + příslušná substituce (2ks)]
  3. (1 bod) Aplikujte rezoluci na následující klauzule. Kolika způsoby to lze provést? (Uvědomte si, co říká v lidské řeči první klauzule.)
    x*z!=y*z | x=y | z=0 | -P(x,y).
    A*0!=B | -P(A,A) | A=B.
    [odpověď: klauzule + příslušná substituce]
  5. (2 body) Vysvětlete na následujícím příkladě použití paramodulace (jaká substituce byla provedena?) a přepište uvedenou dedukci do "lidské formy". Zde "para" znamená paramodulaci, do které vstupují příslušné dvě klauzule, "rewrite" znamená postupnou demodulaci pomocí příslušných rovnic (ty jsou již orientované, zleva doprava). (Část výstupu z dokazovače Prover9.)
    118 (x * y) * (y * (x * z)) = y * (x * z).
    440 x * ((y + x) * z) = x * z.
    616 (x * y) * (y * z) = (x * y) * z.
    617 (x * y) * (x * z) = (x * y) * z.
    664 (x * y) * z = y * (x * z). [para(440(a,1),118(a,1,2,2)),rewrite([616(4),617(3),440(5)])].
  6. (2 body) Vysvětlete na následujícím příkladě použití rezoluce (jaká substituce byla provedena?) a přepište uvedenou dedukci do "lidské formy". Zde "hyper" znamená (hyper)rezoluci, "rewrite" znamená demodulaci. Jeden z axiomů úlohy byl, že * je asociativní, proto jsou vynechávány závorky. (Část výstupu z dokazovače Prover9.)
    57 x * y * z != u * w * z | x * y = u * w.
    443 (x + y) * y * x = x * y.
    719 (x + (y * x)) * y * x = y * x * (x + (y * x)).
    933 x * y * (y + (x * y)) = y * x. [hyper(57,a,443,a),rewrite([719(4)])].
  7. (1 bod) Simulujte běh unifikačního algoritmu na termech f(x,y,z) a f(g(y),g(z),g(x)).
    [odpověď: výpis kroků tohoto algoritmu]
  8. (2 body) a) Formalizujte ve výrokové logice PHPn (Pigeon Hole Principle), tj. vymyslete instanci SAT, která prokazuje, že pokud se snažím nacpat n+1 holubů do n holubníků, tak musím mít v nějakém holubníku aspoň 2 holuby. b) Simulujte běh DPLL pro PHP2.
  9. (3 body) Dokažte, že binární rezoluce se selekcí nemusí být úplná, i když vezmeme neomezenou selekci na faktorizaci.
    [odpověď: selekční funkce + nesplnitelná množina klauzulí + důkaz, že z ní nelze odvodit prázdná klauzule]
  10. (2 body) Najděte konvergentní přepisující systém pro teorii lup.
    [odpověď: přepisující systém s náznakem důkazu, že to funguje (nemusíte jej sespisovat celý)]
  11. (2 body) Dokažte, že Knuth-Bendixův algoritmus pro rovnicovou teorii danou jednou rovnicí x*(y*y)=x*y neskončí.
  12. (2 body) Simulujte běh Otter loop na níže uvedeném zadání. Použijte superpoziční kalkulus se subsumpcí, selekční funkci "lightest first". S jakým uspořádáním algoritmus odvodí prázdnou klauzuli nejrychleji?
    -r(x) | -p(x). p(x) | -p(B) | -r(x). r(A). p(B). r(C).
    [odpověď: výpis pasivního a aktivního seznamu v čase + která klauzule byla vybraná]
Implementace: (žádný časový limit)
Použít můžete libovolný programovací jazyk, ve kterém není příslušná úloha triviální (jako například unifikace v Prologu).
  1. (2 body) Naprogramujte unifikaci.
  2. (5+1 bodů) Naprogramujte nějaký úplný dokazovač pro výrokovou logiku (vstup stačí pro klauzule). 3 body za dokazovač, další 2 body pokud bude vracet také ohodnocení, resp. důkaz sporu. Jeden bod navíc pro toho, kdo dokáže v limitu 1 minuty dokázat PHPn pro největší n.
    [odpověď: funkční implementace, důkaz PHPn pro nějaké n v limitu 1 minuty]
  3. (13 bodů) Naprogramujte dokazovač pro predikátovou logiku (vstup stačí pro klauzule), který
    • (2 body) je úplný,
    • (2 body) vypíše důkaz,
    • (2 body) provádí subsumpci,
    • (2 body) umí dokázat, že grupy exponentu 2 jsou abelovské (jednoduchá úloha s rovností),
    • (2 body) umí vyřešit úlohu PUZ001-1.p nebo MGT003-1.p (jednoduché bez rovnosti)
    • (2 body) umí vyřešit alespoň dvě z následujících úloh: PUZ031-1.p, HWC001-1.p, GRP602-1.p, výše uvedená úloha 2a o homomorfismech grup (o něco těžší úlohy, různého typu)
    • (1 bod) umí vyřešit úlohu KRS005-1.p nebo SYN059-1.p (splnitelné(!) úlohy)
    Jednotlivé podúlohy mohou řešit různé varianty vašeho programu (tj. např. varianty, které řeší uvedené úlohy, nemusí být úplné).
  4. (6 bodů) Naprogramujte Knuth-Bendixův algoritmus a na něm založený rovnicový dokazovač.
    • 3 body za funkční konstrukci konvergentního přepisujícího systému. Implementace by měla umět najít konvergentní přepisující systém pro teorii grup či kvazigrup.
    • 3 body za funkční dokazovač. Implementace by měla umět dokázat, že grupy exponentu 2 jsou abelovské.