6) Automatsko zaključivanje Flashcards
Razlikovati izmedu dokazivanja logičkih i deduktivnih posljedica
Formula G je dedukcija (engl. deduction) ili deduktivna posljedica (engl. deductive consequence) formula F1, F2, . . . , Fn akko je G moguće izvesti (engl. derive) iz premisa F1, F2, . . . , Fn pravilima zaključivanja.
Pišemo F1, F2, . . . , Fn ` G i čitamo “F1, . . . , Fn izvodi (engl. derives) ili deduktivno povlači (engl. deductively entails) G ”.
Zaključak (novoizvedeno znanje) zapravo nije ništa drugo nego logička posljedica premisa (postojećeg znanja). Dakle, izvođenje novog znanja svodi se na dokazivanje logičkih posljedica postojećeg znanja
staro znanje |= novo znanje
Ljudi ne zaključuju tako da pokuašavju dokazati semantičku/logičku posljedicu tj. pronaći interpretaciju koja je istinita za F i nije istita za G nego izvode G iz premisa pomoći pravila zaključivanja. Dokazivanje logičke posljedice je netraktabilno zbog velikog broja slučajeva koje treba pokriti i neodlučivo. Deduktivne posljedice tj. teorija dokaza je učinkovitija i interpretabilna za razliku od logičke posljedice.
Definirati deduktivnu posljedicu i dati primjere
Formula G je dedukcija (engl. deduction) ili deduktivna posljedica (engl. deductive consequence) formula F1, F2, . . . , Fn akko je G moguće izvesti (engl. derive) iz premisa F1, F2, . . . , Fn pravilima zaključivanja.
Pišemo F1, F2, . . . , Fn ` G i čitamo “F1, . . . , Fn izvodi (engl. derives) ili deduktivno povlači (engl. deductively entails) G ”.
Dokaz F|- G je isto kao dokazati |- F->G
Definirati svojstva ispravnosti i potpunosti te dati primjere za oba svojstva
Pravilo zaključivanja je ispravno (engl. sound) ako, primijenjeno na skup premisa, izvodi formulu koja je logička posljedica tih premisa.
Formalno, pravilo zaključivanja r je ispravno ako i samo ako:
ako F1, . . . , Fn |-r G onda F1, . . . , Fn |- G
Npr. Modus ponens je ispravan (F->G, F|- G)
Skup pravila R je potpun (engl. complete) ako i samo ako je njime moguće izvesti sve logičke posljedice:
ako F1, . . . , Fn |-G onda F1, . . . , Fn |-R G
Dokazati ispravnost danog pravila zaključivanja
U tablici zaključivanja sve treba biti T
Definirati rezolucijsko pravilo za PL i FOL te njegova svojstva
Metoda rezolucije (metoda razrješavanja) je jedno pravilo zaključivanja i koristi se u propozicijskoj logici i logici prvoga reda. Rezolucijsko pravilo kaže: A ∨ F, ¬A ∨ G |- F ∨ G tj.
¬F → A, A → G |- ¬F → G
Ono je ispravno (dokaže se tablicom istinitosti za sve dijelove pravila) i nije potpuno (F|= F V G , ali ne možemo izvesti F |- F V G (samo iz F se nemože izvedi
FvG))
Rezolucijsko pravilo može se primijeniti samo na disjunkcije (klauzule).
Skup premisa je konjunkcija klauzula (CNF).
Premise nazivamo roditeljske klauzule, a dedukciju nazivamo rezolventa.
U FOL je potrebno/moguće komplementarno unificirati najopćenitijim unifikatorom
Definirati i objasniti faktorizaciju i standardizaciju te dati primjere
Faktorizacija: G v G možemo smanjiti na G (osigurava potpunost)
Standardizacija: u FOL, ne smiju postojati 2 klauzule koje sadrže iste varijable pa ako
se to desi moramo raditi preimenovanje (F(x) i F(x, y) moramo pretvoriti npr. u
F(x’), F(x’, y))
Objasniti i ilustrirati nepotpunost izravne rezolucije
Jer rezolucijom ne možemo izvesi sve logičke posljedice, npr. ne može se izvesti FvG samo pomoću F
Definirati rezoluciju opovrgavanjem za PL
pokušava dokazati da je F1 ∧ · · · ∧ Fn ∧ ¬G nekonzistentno tj. proturječna formula.
Dokazano je (ground resolution theorem) da, uvijek kada je skup klauzula proturječan, rezolucijom možemo izvesti klauzulu NIL, što znači da uvijek možemo dokazati nekonzistentnost skupa klauzula.
možemo dokazati svaku logičku posljedicu -> rezolucija opovrgavanjem je ispravna i potpuna
Navesti i objasniti dvije osnovne rezolucijske strategije
Strategije pojednostavljivanja uklanjaju redundantne i nevažne klauzule generirane tijekom postupka dokazivanja čime se sprječava njihovo daljnje nepotrebno razrješavanje.
Upravljačke strategije odreduju način odabira roditeljskih klauzula.
Rezolucijska strategija treba biti potpuna: mora izvesti NIL, ako je skup klauzula nekonzistentan
Definirati najopćenitji zajednički unifikator i dati primjere
Supstitucija δ je najop´cenitiji unifikator (MGU) akko za svaki unifikator γ od K1 i K2 postoji supstitucija θ za koju vrijedi γ = δ ◦ θ. Primjenjuje se u unifikaciji prilikom
pretvaranja u klauzalni oblik.
Unifikatori za P(x) i P(y):
δ = {y/x} (MGU)
γ = {b/x, b/y} = δ ◦ θ, gdje θ = {b/y}
Odrediti najopćenitiju zajedničku instancu dvaju izraza
šrimijeniti MGU algoritam:
Prvi element liste je glava liste, a ostatak je rep liste
Nadi MGU izraza K1 = P(g(u), z, f(z)) K2 = P(x, y, f(b))
Korak 1:
I {g(u)/x} unificira prve podizraze od K1 i K2 koji se ne slažu
I K1{g(u)/x} = P(g(u), z, f(z))
I K2{g(u)/x} = P(g(u), y, f(b))
Korak 2:
I {y/z} unificira sljedeće podizraze koji se ne slažu
I kompozicija {g(u)/x} ◦ {y/z} = {g(u)/x, y/z}
I K1{g(u)/x, y/z} = P(g(u), y, f(y))
I K2{g(u)/x, y/z} = P(g(u), y, f(b))
Korak 3:
I {b/y} unificira posljednje podizraze koji se ne slažu
I kompozicija {g(u)/x, y/z} ◦ {b/y} = {g(u)/x, b/z, b/y} = δ
I K1δ = P(g(u), b, f(b))
I K2δ = P(g(u), b, f(b))
Primijeniti pretvorbu u klauzalni oblik zadane PL ili FOL formule
onih 10 koraka za FOL i prva 4 i zadnji za PL
Primijeniti rezoluciju opovrgavanjem na zadani skup PL ili FOL formula
PL:
dovedi u CNF i klauzalni oblik, opovrgavanje
FOL:
dovedi u CNF i klauzalni oblik
unifikacija i faktorizacija
opovrgavanje
Objasniti koje su posljedice neodlučivosti FOL na rezoluciju opovrgavanjem
Zbog poluodlučivosti moć rezolucije u FOL je ograničena. Ne postoji algoritam koji za svaku formulu F daje “da” ako je F valjana ili “ne” ako F nije valjana - postoje algoritmi koji daju “da” ako je F valjana, ali ako F nije valjana, algoritam može nikada ne završiti, npr.
Ako G jest logička posljedica od F, postupak će uvijek izvesti NIL
I Ako G nije logička posljedica F, postupak može nikada ne zavrˇsiti
