David Stanovský    //   

AUTOMATICKÉ DOKAZOVÁNÍ VĚT 2010/11

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. Cílem kurzu je

  1. naučit se automatické dokazovače používat
  2. pochopit základní principy, na kterých dokazovače fungují
  3. zjistit k čemu je automatické dokazování dobré
Kurz je vhodný pro studenty informatiky (zejména teoretické) i matematiky (zejména matematických struktur a informační bezpečnosti). Předpokládá se základní znalost matematické logiky v rozsahu kteréhokoliv úvodního kurzu.

Kurz budou letos přednášet David Stanovský (KA), Ondřej Kunčar a Martin Suda (KTIML). Koná se v pondělky 12:20 v S11.

Obsah + předběžný plán:

  1. (D+O) aplikace automatického dokazování
  2. (D) princip rezolučních dokazovačů a dokazovač Prover9
  3. (D) infrastruktura (knihovna TPTP, soutěž CASC, ...)
    (D) výroková logika, rezoluční kalkulus a jeho úplnost
  4. (D) automatické dokazování ve výrokové logice: klauzifikace a DPLL
  5. (D) predikátová logika, skolemizace a klauzifikace, unifikace
  6. (O) automatické dokazování v predikátové logice (1. řádu): inferenční pravidla, inferenční proces, redundance, saturační algoritmus
  7. (M 3x) důkaz že to celé funguje, na konci stručně k superpozici
  8. (D 2.5x) rovnost: přepisující systémy, Knuth-Bendixův algoritmus a automatické dokazování v rovnicové logice (Waldmeister), simplifikační uspořádání
  9. (M 1.5x nebo 2.5x) implementace dokazovačů - datové struktury, indexování termů, ...
  10. (D?) konstrukce konečných modelů

Materiály ke kurzu: (budou doplňovány průběžně)

  1. Voronkovův úvod (viz sekce Introduction), slajdy ATP v algebře, slajdy formalizace matematiky
    (doplňující materiály: přehled ATP od Geoffa Sutcliffa, článek Toma Halese Formal proof, článek o ATP v neasociativní algebře)
  2. slajdy Michaela Kinyona
    (doplňující materiály: pokračování slajdů Michaela Kinyona (skoro na konci stránky), dokumentace k Prover9)
  3. TPTP (problémy, SystemOnTPTP, soutěž CASC, ...), text Jana Krajíčka o rezolučním kalkulu (str. 11-13)
    (doplňující materiály: více o Geoffově podpůrném software)
  4. Ganzingerovy slajdy 27.+29.4.
  5. predikátová logika: Ganzingerovy slajdy 4.+6.5., unifikace: základní info Ganzinger 18.5. str. 9-17
    (doplňující materiály: mnohem více o unifikaci v kurzu Temura Kutsii)
  6. Ganzingerovy slajdy: 18.5. str. 7 (inf. pravidla), 11.5. celé (uspořádání a multimnožiny), 25.5. skoro celé (algoritmus)
  7. Weidenbachovy slajdy strany 51-80, 106-111
  8. Weidenbachovy slajdy strany 81-105
    (doplňující čtení o superpozici: 112-121) přepisující systémy - moje poznámky část 1, část 2, případně též skripta J. Ježka, kapitola 13]
    vnitřnosti Waldmeistera (viz článek Citius, Altius, Fortius... v záhlaví, sekce 3.1)
  9. přednáška Stephana Schulze

Užitečné odkazy:

Podobné kurzy:

Zde jsou informace k loňskému kurzu (obsah, materiály, úlohy). Kurz letos projde větší revizí, po stránce obsahové, materiálů i příkladů ke zkoušce.

Zkouška: bude formou domácích prací, úlohy budou zadávány během semestru. Minimální počty bodů: 1 - 30 bodů, 2 - 27.5 bodů, 3 - 25 bodů. Úlohy lze opravovat, ale za opravenou část lze získat nejvýše polovinu bodů. To vše jen do časového limitu.

Stav bodů: AC 21, RM 32, PJ 27, DH 19, JB 10, RB 7.5, MF 1

Předběžný seznam úloh viz níže. Přibydou ještě nějaké úlohy na teorii.

Použití dokazovačů - stačí znalost druhé a třetí přednášky, termín odevzdání 7.11.
Odpovědí jsou vždy vstupní a výstupní soubory z nějakého automatického dokazovače.

  1. (2 body) Formalizujte a dokažte následující úlohu:
    a) Mějme grupu (G,*,',e) a zobrazení f:G->G. Pokud f(x*y)=f(x)*f(y) pro všechna x,y z G, pak také f(x')=f(x)' a f(e)=e.
    b) Mějme grupy (G,*,',e), (H,+,-,o) a zobrazení f:G->H. Pokud f(x*y)=f(x)+f(y) pro všechna x,y z G, pak f(x')=-f(x) a f(e)=o.
  2. (2 body) Formalizujte a vyřešte následující hádanku:
    Marťané a Venušanky vždy mluví pravdu, Marťanky a Venušané vždy lžou. Pozemšťan nedokáže rozeznat ani Marťana od Venušana, ani kdo je muž a kdo žena. Pozemšťanovi byl představen manželský pár. Jedna postava říká: "Jsem z Marsu.". Druhá říká: "To není pravda!". Jde o rasově smíšené manželství?
  3. (2 body) Uvažujme standardní Hilbertův kalkulus pro výrokovou logiku s axiomy
    p -> (q -> p), (p -> (q -> r)) -> ((p -> q) -> (p -> r))), (~p -> ~q) -> (q -> p)
    a odvozovacím pravidlem modus ponens, tj. A, A->B |- B. Zformalizujte tento systém v logice prvního řádu (návod: formule jsou termy, jeden unární predikátový symbol kóduje dokazatelnost) a dokažte, že
    a) následující formule jsou v dokazatelné: A -> A, ~A -> (A -> B), (~~A) <-> A.
    b) uvedené axiomy jsou navzájem nezávislé (návod: použijte hledač modelů).
  4. (3 body) Vyřešte úlohy SWV037+1, GRP164-1 a BOO060-1 z databáze TPTP pomocí nějakého dokazovače.
  5. (2 body) Nastavte Prover9 tak, aby v časovém limitu jedné minuty dokázal následující úlohu:
    assumption: f(f(f(f(y,x),f(x,z)),u),f(x,f(f(x,f(f(y,y),y)),z))) = x.
    goal: f(x,f(f(y,z),f(y,z))) = f(y,f(f(x,z),f(x,z))).
    Návod: využijte následujících definic:
    x v y = f(f(x,x),f(y,y)).
    x ^ y = f(f(x,y),f(x,y)).
    x' = f(x,x).

Teorie - termín odevzdání úloh 1.-6. 31.12., zbytek 31.1., doporučuji řešit průběžně. Formule jsou zapisovány ve formátu Prover9.

  1. (1 bod) 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?
    x*z!=y*z | x=y | z=0 | -P(x,y).
    A*0!=B | -P(A,x) | A=B.
    [odpověď: klauzule + příslušná substituce]
  4. (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.)
    47 (x * (x * y)) * x = x * (x * (y * x)).
    660 x * (i(x) * d(x,y)) = i(x) * y.
    671 x * (x * ((i(x) * y) * x)) = x * (y * x).
    720 x * (d(x,y) * x) = (x * (i(x) * y)) * x. [para(660(a,1),47(a,1,1,2)),rewrite([671(10)]),flip(a)].
  5. (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)])
  6. (1 bod) Spočtěte mgu(E), kde E = { (f(x,g(x)), y), (h(y), h(v)), (v, f(g(z),w)) }.

  7. (1 bod) Najděte uspořádání > na atomech A,B,C,D,E takové, že odpovídající uspořádání na klauzulích (viz Weidenbach str. 16 a 57) dá
    B | C > A | A | -C > C | E > C | D > -A | D > -E
  8. (2 body) Buď > lineární (totální) uspořádání na ground atomech takové, že pokud atom A obsahuje více symbolů než atom B, pak A>B. Uvažujme množinu klauzulí N sestávající z
    -q(z,z).
    -q(f(x),y) | q(f(f(x)),y) | p(x).
    -p(a) | -p(f(a)) | q(f(a),f(f(a))).
    p(f(x)) | p(g(y)).
    -p(g(a)) | p(f(f(a))).
    Které literály jsou v jednotlivých klauzulích maximální? Definujte selekční funkci S takovou, že N je saturovaná vzhledem k rezoluci omezené uspořádáním > a selekční funkcí S.
  9. (3 body) Buď > uspořádání na ground atomech takové, že p(f^n(a)) > p(f^m(a)) právě tehdy, když n>m. Uvažujme množinu klauzulí N sestávající z
    p(f(f(a))).
    -p(x) | p(f(x)).
    Ukažte, jak vypadá množina G_Sigma(N) všech ground instancí a jak je uspořádaná. Spočtěte Herbrandův model I_(G_Sigma(N)) vzhledem k tomuto uspořádání.
  10. (1 bod) Rozhodněte následující tvrzení: "pro každé termy t,u,v a různé proměnné x,y platí (t[x->u])[y->v] = t[x->u,y->v]". (Tímto zápisem se rozumí příslušná substituce aplikovaná na daný term.)
  11. (1 bod) Buď E množina rovnic, t,s termy a sigma substituce. Dokažte formálně, že pokud E |- t=s, pak E |- sigma(t)=sigma(s).
  12. (2 body) Dokažte, že následující přepisující systém je konvergentní, a určete, jak vypadají normální formy termů:
    f(f(x)) -> f(x), g(g(x)) -> f(x), g(f(x)) -> g(x), f(g(x)) -> g(x)
  13. (2 body) Spočtěte všechny kritické páry a rozhodněte, které z následujících přepisujících systémů jsou lokálně konfluentní:
    a) f(g(f(x))) -> x, f(g(x)) -> g(f(x)),
    b) x*x -> a, x*f(x) -> b
    c) (x*y)*z -> x*(y*z), x*1 -> x
    d) (x*y)*z -> x*(y*z), 1*x -> x
  14. (3 body) Vyberte si buď LPO nebo KBO a dokažte, že jde o simplifikační uspořádání, které je lineární (totální) na ground termech.
  15. (1 bod) Dokažte pomocí LPO, že následující přepisující systém terminuje:
    0*y -> f(y).
    f(x)*0 -> x*f(0).
    f(x)*f(y) -> x*(f(x)*y).
  16. (1 bod) Dokažte pomocí KBO, že následující přepisující systém terminuje:
    f(x)*(y*z) -> x*(f(f(y))*z).
    f(x)*(y*(z*w)) -> x*(z*(y*w)).

Implementace - žádný časový limit, programovací jazyk libovolný

  1. (6+1 bodů) Naprogramujte SAT-solver, tj. dokazovač pro výrokovou logiku (vstup stačí pro klauzule), který je úplný a pro splnitelné formule vypisuje ohodnocení. 1 bod navíc pro toho, kdo dokáže v limitu 1 minuty vyřešit PHP(n) pro největší n.
  2. (až 24 bodů) Naprogramujte dokazovač pro predikátovou logiku (vstup stačí pro klauzule), který
    • (6 bodů) umí dokázat cokoliv netriviálního
    • (2 body) je úplný,
    • (2 body) vypisuje důkazy,
    • (3 body) provádí subsumpci,
    • (3 body) provádí nějaká simplifikační pravidla,
    • (2 body) umí dokázat, že grupy exponentu 2 jsou abelovské (jednoduchá úloha s rovností),
    • (2 body) umí vyřešit úlohu PUZ001-1 nebo MGT003-1 (jednoduché úlohy bez rovnosti)
    • (2 body) umí vyřešit alespoň dvě z následujících úloh: PUZ031-1, HWC001-1, GRP602-1, výše uvedená úloha o homomorfismech grup (o něco těžší úlohy, různého typu)
    • (2 body) umí vyřešit úlohu KRS005-1 nebo SYN059-1 (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é).
  3. (10 bodů) Naprogramujte Knuth-Bendixův algoritmus a na něm založený rovnicový dokazovač.
    • 5 bodů 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 nebo kvazigrup.
    • 5 bodů za funkční dokazovač. Implementace by měla umět dokázat, že grupy exponentu 2 jsou abelovské.