Pravdivost, dokazatelnost. Důkazové metody a
systémy.
Luboš Popelínský
E-mail: popel@fi.muni.cz http://nlp.fi.muni.cz/uui/
Obsah:
• Pravdivost v interpretaci a logická pravdivost
• Axiomatické systémy pro výrokovou logiku
• Formální systémy
• Normální formy
• DPLL
Úvod do umělé inteligence 6/12 1/28
Logický agent
function KB-AGENT(percept) # vrací akci
# globální: KB - báze znalostí; t - číslo, na začátku 0
tell {KB, make_percept_sentence(percepř, ť)) action ^— ask(/C8, make_action_query(ř)) tell {KB, make_action_sentence(acř/OA7, ť)) t <- í+1 return action
Úvod do umělé inteligence 6/12 2/28
Pravdivost v interpretaci a logická pravdivost
Pravdivost v interpretaci
Formule A je pravdivá v interpretaci / (Interpretace / splňuje formuli A), jestliže po substituci za výrokové symboly vrací hodnotu TRUE
Dokážeme dosazením z / do A a vyhodnocením (valuací) logických spojek, viz Animace
Silnější vlastnost: pravdivost ve všech interpretacích
Úvod do umělé inteligence 6/12
3/28
Pravdivost v interpretaci a logická pravdivost
Logická pravdivost I
Formule je pravdivá (logicky pravdivá), jestliže je pravdivá ve všech interpretacích.
pravdivá formule == tautologie, anglicky též a valid formula
Důkaz (logické) pravdivosti formule: model checking; ukážeme, že formule je pravdivá ve všech interpretacích.
Vytvoříme pravdivostní tabulku a pro každou interpretaci ověříme, že formule je v této interpretaci pravdivá.
Složitost n výrokových symbolů, tj. 2n intrepretací Existuje efektivnější způsob?
Úvod do umělé inteligence 6/12 4/28
Pravdivost v interpretaci a logická pravdivost
Logická pravdivost II
Příklad: p     (q p) Příklad: p V (->p A r) Příklad: p V (->p A r) V ^p Příklad: (p V q) A (^p V -./■)
např. znegování formule a důkaz nesplnitelnosti? == důkaz sporem
Úvod do umělé inteligence 6/12 5/28
Pravdivost v interpretaci a logická pravdivost
Formule s implikací a důkaz sporem
Q
ověření tautologií tvaru implikace metodou protipříkladu: =4> je nepravdivá pouze pro pravdivý předpoklad a nepravdivý důsledek. Pro tuto variantu - za předpokladu nepravdivosti důsledku - pro příslušné interpretace ověříme (ne)pravdivost předpokladu.
• příklad: p =4> (q =4> p)
■ předpoklad: p pravdivá, q     p nepravdivá
■ jediná možnost nepravdivosti q p: q pravdivá, p nepravdivé
■ spor s předpokladem pravdivosti p
== důkaz sporem, proof by refutation or proof by contradiction
a
= f3 právě když je formule a A nesplnitelná
Úvod do umělé inteligence 6/12
6/28
Axiomatické systémy pro výrokovou logiku	
Axiomatický systém	
• jazyk: stejný jako jazyk výrokové logiky; primárně používáme systém spojek {=^, -i}, ostatní spojky jsou chápány jako zkrácené zápisy:
A A B =<jf ^{A    -.6), AV B =df ^A B, A & B =df (A => B) A (B => A)
• axiomy (resp. schémata axiomů; A, 6, C jsou formule): Ai A=>(B=>A)
A2 (A=>(B=> C))     ((A    B)^(A^ C)) A3 (-.6 => ^A) ^(A^ B)
9 odvozovací (inferenční) pravidlo modus ponens (MP) (pravidlo odloučení): jsou-li z axiomů dokazatelné (odvoditelné) formule A a A =>■ B, pak je dokazatelná i B. Zapisujeme též
A      A^ B B
Úvod do umělé inteligence 6/12 7/28
Príklad
Axiomatické systémy pro výrokovou logiku
• důkaz A: konečná posloupnost formulí, jejíž každý člen je axiom nebo důsledek MP, jehož předpoklady jsou mezi předchozími členy, a poslední člen je formule A. Je-li A dokazatelná, píšeme h A.
• příklad: dokažte h A    A (vpravo jsou komentáře k jednotlivým krokům)
A=>{(A=> A)=> A) Ai
2. \-(A=> {(A ^A)^ A)) ((A ^(A^ A))     (A => A)) A2
3. h (A => {A    A)) => {A A) MP(1,2)
4. h A => (A    A) Ai
5. \-A=>A MP(3,4)
Úvod do umělé inteligence 6/12
Axiomatické systémy pro výrokovou logiku
Vlastnosti uvedného axiomatického systému
• Věta (korektnost a úplnost): A je dokazatelná právě tehdy, když je pravdivá, tj. h A ^ |= A
Důkaz: =4> (korektnost): ověříme, že axiomy jsou tautologie a jsou-li předp. MP tautologie, pak i důsledek je tautologie (tabulky, věta o implikaci)
(úplnost): složitější, na základě pomocných tvrzení (lemma o neutrální formuli a lemma o odvození z atomických komponent) Pozn.: věta vystihuje vztah mezi syntaxí a sémantikou výr. logiky
• rozhodnutelnost: neexistuje systematická procedura (jde spíše o "hádánfjednotlivých kroků důkazu), nevhodné pro strojové zpracování. Dokazování lze zjednodušit pomocí dokazatelnosti
z předpokladů a syntaktické věty o dedukci (7,/l h 8     T \- A ^ B).
• axiomy jsou nezávislé (žádný nelze odvodit ze zbývajících dvou)
Úvod do umělé inteligence 6/12
9/28
Formální systémy
Formální systémy
Axiomatický systém je příkladem deduktivního systému (nebo též formálního systému).
Formální systém
o postavený výhradně na syntaktické bázi: jazyk logiky neinterpretujeme, provádíme s ním pouze syntaktické manipulace - důkazy
• cíl: získat formální teorii jako souhrn dokazatelných formulí - teorémů
• formální systém tvoří
■ jazyk + formule (symbolický jazyk výrokové logiky) - bez interpretací
■ odvozovací pravidla - operace na formulích umožňující konstrukce důkazů
■ případně axiomy - výchozí tvrzení přijímaná bez důkazu; (axiomy spolu s odvozovacími pravidly tvoří dedukční systém)
• formální systémy lze rozdělit na
■ axiomatické (méně pravidel)
■ předpokladové (méně axiomů)
Úvod do umělé inteligence 6/12
10 / 28
Formální systémy
Požadované vlastnosti formálních systémů
• korektnost (bezespornost): je dána výběrem axiomů a odvozovacích pravidel; systém je korektní, nelze-li v něm zároveň odvodit tvrzení i jeho negaci. Ve sporném systému lze odvodit cokoliv. Vyžadována vždy. (Sémantická korektnost: existuje alespoň jeden model.)
• úplnost: připojením neodvoditelné věty k úplnému systému se tento stane sporným. Nevyžadována vždy - úplné jsou pouze velmi jednoduché teorie. (Sémantická úplnost: každé tvrzení pravdivé ve std. interpretaci lze odvodit.)
• rozhodnutelnost: existence algoritmu pro ověření dokazatelnosti libovolné formule. V axiom, systémech podmíněna úplností; zpravidla splněna pouze pro určité třídy formulí.
• nezávislost axiomů: nezávislý axiom nelze odvodit z ostatních axiomů; závislý axiom může být vypuštěn z dané soustavy axiomů
Úvod do umělé inteligence 6/12        11 / 28
Formální systémy
Další axiomatické systémy
JXnn HCHHCTOHHH BbICKa3I>IBaHHfí MOryT 6bITb nOCTpOeHM aKCHOMaTH3aiXHH
n c omoŘ eaHHCTBeHHOfl cxeMofl aKCHOM. TaK, HanpHMep, ecJiH 3a np™n-
THBHHe CBH3KH íipHHHTb "1 H ZD, TO npH Gj3,HHCTB6HHOM npaBH/ie BblBOJia —
modus ponens — AOCTaTOMHOfl OKapusaetca cxeiwa aKCHOM:
(Mepe/iHT [1953]).
JIpyrHM npHMepoM TaKoro po^a mo)K6t c/iy>KHTb CHcreMa H h k o ä a [1917], b KOTOpoft ynoTpeÔ^HeTCH e/iHHCTBeHHaa CBH3Ka | (ak3t>k)hkuhh
OTpHUaHHfl), HM66TCH e/lHHCTBeHHOe npaBHJIO BblBO^a, nO KOTOpOMy % CJie-
ÄyeT H3 &é h q/č \{3š\íě\ h eÄHHCTBeHHan cxeivia aKCHOM
(«* i (a i so) i {[B i [sr 19)\ i [(í i S) \ «^ *))]}.
Jla^bHefluiHe CBeaeHHH m sicfl oó^acTH, b tom ™c/ie n HCTOpnqecKHíl oôsop, mohcho mňm b KHHre H e p h a [1956].
Introduction to Mathematical Logic by Elliott Mendelson, 1964
Úvod do umělé inteligence 6/12 12 / 28
Formální systémy
Gentzenovský systém (kalkul sekventů)
• příklad pravidlového systému formální logiky: pouze nástin, nikoliv úplná definice
9 další typ výrazů formálního jazyka: sekventy (sekvence) Al, ^2? • • • 5 An h B,
kde Aj, B jsou formule, h je symbol odvoditelnosti (dokazatelnosti). Posloupnost na levé straně chápeme jako konečnou množinu formulí (budeme ozn. I~) - nezáleží na pořadí, lze vynechat duplicity, může být prázdná.
9 jediný axiom: V, A h A
Úvod do umělé inteligence 6/12
13 / 28
Formální systémy
Gentzenovský systém: pravidla
i        x     i x .i,   předpoklad-) ... předpoklade
• obecné schéma pravidel: -—--1-—--—---
r zaver
• pravidla zavedení a eliminace předpokladu:
9 řada pravidel pro spojky (uvedeme pouze některá na ukázku) zavedení a eliminace V:
r^A        r,/ihc    r,ehc rh/ive
rh/ive rhc
zavedení a eliminace A:
A      ThS rh/lABTh/lAB
rh/iAB r h ^ rhB
Úvod do umělé inteligence 6/12        14 / 28
Formální systémy
Gentzenovský systém: důkazy
9 důkaz sekventu: strom, v jehož kořeni je dokazovaný sekvent, v listech axiomy a každý uzel (závěr) se svými přímými následníky (předpoklady) představuje instanci některého z pravidel systému
• je-li dokázaný sekvent tvaru h A, pak formuli A nazýváme teorém (odvoditelná resp. dokazatelná formule)
o systém je korektní a úplný (platí h A ^ |= A)
• příklad: důkazu sekventu h pV^p:
^P^P P^P
-iphpV-ip phpV-ip hpV^p
(použito pravidlo eliminace předpokladu a dvakrát pravidlo zavedení V)
Úvod do umělé inteligence 6/12        15 / 28
function KB-AGENT(percept) # vrací akci
# globální: KB - báze znalostí; t - číslo, na začátku 0
tell (KB, make_percept_sentence(percept, t)) action ^— ask(KB, make_action_query(ř)) tell (KB, make_action_sentence(acř/OA7, t)) t <- í+1 return action
Jak se liší uvedené důkazové metody od znalostního agenta a v čem se podobají ?
Úvod do umělé inteligence 6/12
16 / 28
Formální systémy
Logická pravdivost III
Příklad 1: p^(pVr)
Příklad 2: p V (-.p A r)
Příklad 3: p V (->p A r) V ->p
Příklad 4: (p V q) A (-.p V ->r)
všechny formule 2. - 4. jsou v normální formě.
Úvod do umělé inteligence 6/12
17 / 28
Normální formy
Normální formy
• Věta o reprezentaci: každou /7-ární pravdivostní funkci lze reprezentovat formulí výrokové logiky /4(pi, P2,..., pm) obsahující pouze spojky -i, A a V, kde m < n.
• Jak zkonstruovat k funkci tuto formuli (základ důkazu věty): nechť je funkce reprezentována standardní tabulkou. Jsou-li všechny funkční hodnoty rovny 0, je reprezentující formulí libovolná kontradikce, například pi A —ipi. Jinak pro každý řádek, v němž je funkční hodnota rovna 1, vytvoříme konjunkci K\ — 1 pi A 1P2 A • • • A 1 pn, kde pro
j = 1, 2,..., A7
Pj je-li v /-tém řádku hodnota j-tého argumentu 1 ^Pj  je-li v /-tém řádku hodnota j-tého argumentu 0
Disjunkce D všech konjunkcí K\ reprezentuje danou pravdivostní funkci.
Úvod do umělé inteligence 6/12
18 / 28
Príklad
Normální formy
Příklad: určete formuli reprezentující následující pravdivostní funkci:
X	y	f (x, v)	K,	D;
1	i	i	Ki = p A q	
1	0	0		D2 = ->p V q
0	i	i	K3 = -.p A q	
0	0	i	K4 = -73 A ->q	
• atomické formule a jejich negace == literály. Elementární konjunkcí nad pi, P2,..., pn nazveme každou konjunkci, v níž se každý z těchto symbolů vyskytuje jako literál právě jednou. Úplnou normálni disjunktivní formou (úndf) nad týmiž symboly nazveme každou disjunkci vesměs různých elementárních konjunkcí.
9 podobně úplná normální konjunktivní forma (únkf) bude konjunkcí všech disjunkcí v sloupci D;
• (p A q) V (-ip A q) V (-ip A -iq) je v úplné normální disjunktivní formě
• (-ip V q) je v úplné normální konjunktivní formě
Úvod do umělé inteligence 6/12        19 / 28
DPLL
DPLL (Davis-Putnam-Logemann-Loveland Procedure)
základ většiny prakticky používaných důkazových nástrojů pracuje s formulí v konjunktivní normální formě Pravidla
UNSAT If F contains □, then F is unsatisfiable. SAT     If F is empty set {}, then F is satisfiable. MULT  If a literal occurs more than once in a clause,
then all but one can be deleted. SUBS   A clause in F can be deleted, if it is a superset of another
clause in F.
UNIT   An element -i L of a clause in F can be deleted, if F contains {!_}.
Úvod do umělé inteligence 6/12
20 / 28
Pravidla
DPLL
TAUT    A clause can be deleted, if it contains a literal
and its complement. PURE    A clause can be deleted, if it contains L and
-i L does not occur in F.
SPLIT
If F is semantically equivalent to a formula of the form
{ {Ci V L}, ...,{Ck V L},{Ck+1 V -.L},{Cm V -.L},
where neither Z. nor -1/. occur in C/, 1 < i < n, then replace F by the CNF of
Úvod do umělé inteligence 6/12        21 / 28
UNSAT { □, Ci.....C„ } = {□}
MULT  {L, L, LI, . . . , Lm} = {L, LI.....Lm}.
SUBS   { {LI, . . . , Lm}, {LI.....Lm, . . . Lk},Cl, . . . ,Cn }
= { {LI, . . . , Lm},Cl.....Cn}.
UNIT   {{LI.....Lm, L}, {-> L }} = {LI_____Lm}, {-. L } }
TAUT   { { LI.....Lm, L, n L},C1.....Cm } = {CI.....Cm }.
Uvod do umele inteligence 6/12        22 / 28
PURE   { {p, - q}, { - r}} ^ { {p, - q}},
but {CI, . . . ,Cm, {L, LI, ... , Ln}} is unsatisfiable
iff {CI, . . . ,Cm} is unsatisfiable, where -i L
does neither occur in Ci, 1 < i < nor in Lj, 1 < j < n
SPLIT   {{p, r}, { -n r }, {q}} ± {{p}, {q}} V {□, {q}}, but the rule preserves unsatisfiability.
Úvod do umělé inteligence 6/12
23 / 28
Vlastnosti pravide
DPLL
• Let F be a formula in CNF and F' be obtained from F by applying a rule.
• MULT, SUBS, UNIT and TAUT are equivalence preserving, i.e., F' = F.
• They are polynomial simplification rules.
o PURE and SPLIT are unsatisfiability preserving,i.e., F is unsatisfiable iff F is unsatisfiable.
Úvod do umělé inteligence 6/12        24 / 28
DPLL algoritmus
DPLL
1. Input F. Transform F into CNF.
2. Apply the rules MULT, SUBS, UNIT, TAUT, PURE and SPLIT until SAT or UNSAT become applicable.
3. If SAT is applicable then terminate with F is satisfiable.
4. If UNSAT is applicable then terminate with F is unsatisfiable.
Remarks
• The algorithm always terminates.
• Whenever the application of a rule in step 3 yields a formula H, then H is unsatisfiable iff F is unsatisfiable.
• The algorithm is sound and complete.
Úvod do umělé inteligence 6/12        25 / 28
DPLL
DPLL: An Example
{ {pl, P2}, {p4, -p2, -p3}, { - pl, p3}, {-p4} }
Initialization
{ {pl, P2}, {-p2, -p3}, { - pl, p3}, {-p4 }}
UNIT wrt {^p4}
{ {pl, p2}, {-p2, -np3}, { -n pl, p3} }
PURE wrt -np4
{ {p2}, {-P2, -P3}} V {{p3}, {-P2, -P3 } }
SPLIT wrt pl
Úvod do umělé inteligence 6/12
26 / 28
{ {p2}, { -p3}} V {{p3}, {-p2 } }
UNIT wrt -np2 in 1st disjunct and UNIT wrt -np3 in 2nd one
{ { -P3}} V { {^p2 } }
PURE wrt p2 in 1st disjunct and PURE wrt p3 in 2nd one
{} v{}
PURE wrt { -. p3} in 1st dis. and PURE wrt {-.p2 } in 2nd
SAT (satisfiable for both branches)
Úvod do umělé inteligence 6/12
27 / 28
Shrnutí
DPLL
Víme,
• co je logická pravdivost
o co jsou axiomatické systémy
• co jsou formální důkazové systémy
• jak se liší od logického agenta
• co jsou normální formy o DPLL
Úvod do umělé inteligence 6/12
28 / 28