Hlavní navigace

Rezoluce aneb předstupeň logického programování

6. 8. 2013 18:57 (aktualizováno) zboj

Logické programování (Prolog a spol.) je v mnohém revoluční a přinejmenším poskytuje jiný úhel problému na řešený problém. Málokdo ví, jak se tzv. logické programování vlastně vyvinulo.

Prvopočátkem bylo tzv. automatické dokazování tvrzení (anglicky Automated Theorem Proving – ATM, někdy také Mechanical Theorem Proving). Bývá často považováno za součást umělé inteligence, nicméně spadá pod formální logiku. Vše začalo v roce 1965, kdy John Alan Robinson objevil rezoluci. Její jednoduché verzi ve výrokové logice ((p⋁Q)⋀(¬p⋁R)→(Q⋁R)) v predikátové logice odpovídá (p⋁Q)⋀(¬q⋁R)→(Q⋁R)σ, přičemž σ je nejobecnější unifikátor p a q. Protože z množiny formulí Φ plyne φ (Φ ⊢ φ), právě když {Φ,¬φ} je nesplnitelná, dostaneme z {Φ,¬φ} (vzhledem k tomu, že rezoluce je refutačně úplná) prázdnou klauzuli, tedy spor, a tvrzení φ je tím dokázáno (je zřejmé, že předpoklady dokazované věty musíme převést do konjunktivní normální formy). Není složité pomocí výše popsaného jednoduchého principu automaticky dokázat například tvrzení, že odmocnina z každého prvočísla většího něž 1 je iracionální.

Později bylo zjištěno, že i lineární rezoluce (taková, jež resovuje vůči množině formulí pouze naposledy přidanou klauzuli) je úplná, a nakonec Brit Robert Kowalski dokázal, že selektivní lineární definitní (SLD) rezoluce je úplná pro Hornovy klauzule (tj. takové, jež mají nejvýše jeden pozitivní literál). Právě na SLD rezoluci je založen Prolog a podobné jazyky logického programování.

Jako zajímavost uveďme, že rezoluci lze použít rovněž v predikátové logice s rovností (a některá rozšíření Prologu toho využívají). Rovnost lze sice zahrnout přímo do předpokladů (přidáním axiomů o reflexivitě, symetrii a tranzitivitě), ovšem takové řešení je velmi neefektivní. Mnohem výhodnější je zavést zvláštní derivační pravidlo, tzv. paramodulaci, jež vypadá následovně: Pokud A=B a C=D a C se unifikuje s podtermem A na pozici (A|p), pak A[D]pσ=Bσ, kde σ je unifikátorem A|p a C. S použitím paramodulace se podařilo dokázat například tzv. Robbinsovu domněnku o Booleových algebrách, na níž si vylámal zuby i takový génius jako Alfred Tarski.

Pokud vás problematika zajímá (nebo zaujala), můžete si zkusit promyslet, jak byste rezoluci (nebo alespoň SLD rezoluci) implementovali v běžných procedurálních jazycích (C++, C#, Java). Nápovědou budiž yield a lambda výrazy.

Doplnění: Rezoluce pracuje s formulemi bez kvantifikátorů. Zatímco univerzálních kvantifikátorů se můžeme bez problémů zbavit, odstranění existenčních kvantifikátorů by mohlo změnit (ne)splnitelnost formule. Špatná zpráva je, že některé formule vhodně přetvořit při zachování logické ekvivalence nelze. Dobrou zprávou je, že vždy můžeme existenční kvantifikátory eliminovat a zachovat přitom splnitelnost formule (i když její sémantický obsah se může změnit). Řešením je tzv. skolemizace, při níž se existenčně kvantifikované proměnné nahradí funkčními symboly. Při absenci univerzálních kvantifikátorů si vystačíme s konstantami, jinak musíme použít funkce závisející na univerzálně kvantifikovaných proměnných. Máme-li například φ=∃x∀y∃z P(x,y,z), vytvoříme formuli ψ=P(a,y,f(y)), kde a je skolemizační konstanta a f skolemizační funkce s univerzálně kvantifikovanými proměnnými. Je snadné nahlédnout, že φ je splnitelná, právě když je splnitelná ψ.

Sdílet