K čemu je teorie (důkazů)

Teorie důkazů, součást formální logiky, se může jevit jako něco abstraktního (a určitě vyžaduje jistou dávku matematického myšlení, spousta studentů na ní u zkoušky pohoří). Proto je vždy přínosné vidět aplikaci něčeho takového v praxi (a hlavně pochopit, jak a proč to funguje). Jistě se shodneme, že umělá inteligence je obor praktický, a i její podobor – automatické plánování – je na hony vzdálen šedivé teorii.

Teorie důkazů se ve velmi elementární formě (základy deduktivního dokazování) probírá v rámci studia IT. Ještě teoretičtější jsou abduktivní důkazy, o jejichž použití v praxi bude řeč níže. Máme-li teorii T a “hypotézu” (množinu literálů) H, abduktivním důkazem se rozumí množina literálů E taková, že platí

T ∪ E ⊨ H a T ∪ E ⊭ ⊥

tj. z T a E plyne H a T a E je bezesporná. Názornější bude příklad. Pokud T je

mosquito(x) & bite(x,y) & infected(x) → infected(y)

tj. kousnutí komárem přenáší malárii, a H = { infected(John) }, bude (abduktivním) důkazem E

mosquito(m) & bite(m,John) & infected(m)

pro nějaké (do univerza nově zavedené) m. Obecně existuje pro nějakou hypotézu takových důkazů větší množství a většinou se zavádí nějaké jejich hodnocení, přičemž hledáme “nejlepší” důkaz (kde “nejlepší” závisí na konkrétní úloze, může jít o nejkratší důkaz, nejredundantnější apod.).

Automatické plánování je nalezení plánu (sekvence akcí) k dosažení cíle z nějakého počátečního stavu. Často se jako příklad uvádí problém “opice a banánů”. V místnosti je opice a židle a ze stropu visí banány. Úkolem je najít sekvenci akcí pro opici, aby se dostala k banánům. Typicky to bude něco jako “1. jdi z A na B, 2. přesuň židli z B na C, 3. vylez na židli, 4. sněz banány”, pokud počáteční stav byl “opice na A, židle na B, banány na C”. Možné akce jsou přechod opice z X na Y, posunutí židle z X na Y (tím změní pozici opice i židle), vylezení na židli a konzumace banánů. Nalezení optimálního plánu je NP-těžká úloha a tedy obtížně řešitelná i pro malé instance problémů. Navíc není na první pohled zřejmé, jak takový plán nalézt.

Naštěstí se dá celý problém převést na hledání abduktivního důkazu. Plány jsou ve své podstatě lineární vzhledem k času. Každá možná akce se zakóduje jako přechod z jednoho okamžiku do následujícího, například

agentAt(x,t) & action(move,x,y,t) → agentAt(y,t+1)

tedy je-li agent v čase t na pozici x, akce action(move,x,y,t) jej dostane na pozici y v čase t+1. Dále bude teorie obsahovat integritní omezení, například že nelze být na dvou místech zároveň apod. (podle charakteru řešeného problému). Hypotézou bude cílový stav a počáteční stav bude součástí teorie (tím si vynutíme, že budou nalezeny pouze důkazy zahrnující počáteční stav). Nyní zbývá najít všechny abduktivní důkazy s co nejnižším koncovým t (chceme nejkratší možný plán). Z důkazu vybereme pozitivní literály action a máme výsledek.

Převedli jsme do logiky NP-těžkou úlohu, takže i hledání abduktivních důkazů bude NP-těžké. Naštěstí pro to existují superrychlé algoritmy. V případě automatického plánování není uvedená metoda rychlejší než SATPLAN nebo GRAPHPLAN (ale ani pomalejší), je ovšem o dost jednodušší na pochopení. Pro některé jiné úlohy (např. parsing podle unifikačních gramatik, jenž je také NP-těžký) je ovšem převedení na abdukci nejrychlejším známým algoritmem.