 Ernest 2004
3. Rezolu ní metoda
3.1 Úvod
V této ásti budeme dokazovat výroky v mluveném jazyce pomocí
rezolu ní metody. Odvozování posloupností formulí užitím axiom a
odvozovacích pravidel p edstavovalo formu p ímého d kazu. Pro
dokázání n jaké formule resp. skupiny formulí lze použít i nep ímého
d kazu - rezolu ní metody. Postupuje se tak, že se snažíme dokázat,
že výchozí axiomy nebo formule jsou ve sporu s negací dokazované
formule.
3.2 Rezolu ní metoda
Jak již bylo e eno, rezolu ní metoda je metodou pro hledání sporu v
kone né množin klauzulí. Rezolu ní metoda je úplná dokazovací
metoda (nalezne spor v libovolné sporné množin klauzulí) a je
univerzální dokazovací metodou, kterou lze využít pro strojové
dokazování (pomocí po íta e). Rezolu ní metoda vyžaduje formule v
konjunktivn -disjunktním tvaru (klauzule - disjunkce literál ).
• Pravidlo základní rezoluce
Pravidlo základní rezoluce umož uje odvodit ze dvou základních
klauzulí klauzuli další takto:
Jsou-li ϕ a Ψ dv klauzule a je-li α atomická formule, pak z dvojice
klauzulí α ∨ ϕ a ¬α ∨Ψ lze odvodit formuli Ψ ∨ϕ, které se íká
rezolventa formulí α ∨ ϕ a ¬α ∨Ψ. Literály α a ¬α, které
umožnily rezolvovat ob formule, se nazývají dopl kovými
literály.
Pokud se nám tímto zp sobem povede odvodit v množin klauzulí
M prázdnou klauzuli, pak teorie M nem že mít žádný model, a je
sporná. Platí i opa né tvrzení, je-li teorie M sporná, pak v ní lze
pomocí základní rezoluce odvodit prázdnou klauzuli (kontradikce).
 Ernest 2004
• Metoda unifikace
Úkolem metody unifikace je hledat takovou substituci, která by
dovolovala ztotožnit literály, které se liší pouze výskytem n jaké
prom nné. Vzhledem k použití strojového dokazování má zásadní
význam obecná unifikace pro zvolenou kone nou množinu výraz
{Ei}i∈I tzn. substituce s za volné prom nné výraz taková, že
pro všechny výrazy Ei , Ej platí, že Ei(s) = Ej(s).
• Rezolu ní zamítnutí
Rezolu ní metoda hledá spor vyplývající z dané množiny klauzulí.
každá rezolventa je logickým d sledkem rodi ovských klauzulí,
tedy i celé množiny klauzulí. D kaz sporu je dokon en, poda í-li se
nám odvodit prázdnou klauzuli. V tomto p ípad mluvíme o
zamítnutí výchozí množiny klauzulí. Strategií pro vytvo ení
zamítnutí je celá ada. Zvlášt vhodné pro postupné vytvá ení
jednotlivých rezolvent jsou grafické prost edky. Mezi n pat í nap .
deriva ní graf, jehož listy jsou ohodnoceny výchozími klauzulemi
a nov vzniklá rezolventa je spojena hranami s ob ma svými
rodi ovskými klauzulemi. Rezolu ní zamítnutí je potom každý
podgraf deriva ního grafu, který je stromem, jehož listy pat í do
výchozí množiny klauzulí a ko en je ohodnocen prázdnou klauzulí.
¬
V e lk y ( Z )
∨
K u la ty ( Z )
V e lk y ( A )
¬
K u la ty ( A )
¬
¬
H ra n a ty (A )
¬
K u la ty ( Y )
R u z o v y (A )
∨ ¬
R u z o v y (X )
∨
H ra n a ty (Y )
H ra n a ty (X )
R u z o v y (A )
 Ernest 2004
3.3 Úlohy
1. Máme n kolik údaj v databázi:
a) Každá ryba má žábry.
b) Savci nemají žábry.
c) N kte í savci dovedou plavat.
d) N kte í živo ichové dokážou plavat a nejsou ryby.
Prove te následující úkoly:
- p eve te tvrzení a) - d) do jazyka logiky 1. ádu
- na základ tvrzení a) - c) dokažte tvrzení d)
2. Chlapci Standa a Tomáš jsou synové paní a pana Novákových.
Víme o nich, že chodí na základní školu a že:
a) Všichni žáci z Tomášovy t ídy jsou v tší, než žáci ze t ídy
kterou navšt vuje Standa.
b) Jeden ze Standových spolužák je v tší, než Standova
maminka.
c) Ten kdo je u Novák nejstarší, je v tší než oba synové
Standa a Tomáš.
Prove te následující úkoly:
- Formalizujte výše uvedenou úlohu a dopl te
implicitní (nevy ené avšak z ejmé) informace
týkající
se
predikátu
v tší_než
a
nejstarší_v_rodin _Novák .
- Zjist te pomocí rezoluce že paní Nováková není
nejstarší.
 Ernest 2004
3. Máme n kolik údaj v databázi:
a) Pro každý p edm t existuje aspo jeden student, který si
vybere z tohoto p edm tu diplomku.
b) Jestliže student d lá diplomku z n jakého p edm tu, pak
mu rozumí nebo se jedná o lehký p edm t.
c) Jestliže existuje n jaký p edm t, kterému student rozumí a
není lehký, pak onen student musí být chytrý.
d) Vím alespo o jednom p edm tu, který není lehký.
Prove te následující úkoly:
- p eve te tvrzení a) - d) do jazyka logiky 1. ádu
- Dokažte, že existuje chytrý student.
Použitá literatura
[1]
[2]
[3]
[4]
Ma ík, Št pánková, Lažanský a kol., Um lá inteligence 1,
Academia, 1993.
Kotek, Vysoký, Zdráhal, Kybernetika, SNTL, 1990.
Demlová, Pond lí ek, Matematická logika, skriptum VUT,
1997.
Stránky p edm tu – p ednášky http://gerstner.felk.cvut.cz.
Download

3. Rezoluční metoda