Student World

Automatické dokazování vět (Automated Theorem Proving, ATP) je obor na pomezí umělé inteligence a formální matematiky zabývající se vývojem a implementací algoritmů ukazujících, že zadané matematické tvrzení (domněnka, conjecture) je logickým důsledkem zadané množiny axiomů. Automatické dokazovače se dnes používají v řadě oborů. Matematici mohou dokazovače používat jak k rychlému formálnímu ověřování jednoduchých domněnek (například že operace inverze v grupě je involucí), tak k těžkým novým důkazům, jako je uvedená Robbinsova domněnka. Vývojáři hardwaru a softwaru mohou automatické dokazování použít pro částečnou nebo úplnou formální kontrolu správnosti kritických částí svých návrhů, pokud tyto návrhy formálně popíší matematickými axiomy a požadovanou funkčnost vyjádří jako matematickou domněnku.

Automatické dokazování lze použít k řešení logických problémů a hlavolamů, od sudoku přes rozestavování dam na šachovnici tak, aby se neohrožovaly, až po problém složení Rubikovy kostky. Tyto a podobné úlohy se dají řešit automatickým dokazovačem, pokud se problémy správně popíší pomocí axiomů a domněnek. Jazykem (a formalismem) používaným pro formulaci problémů ATP je nejčastěji klasická predikátová logika (logika prvního řádu). Vyvíjejí se však také dokazovače jak pro výrazově silnější logiky (logiky vyšších řádů, neklasické logiky, modální logiky), tak pro výrazově slabší formalismy, jako je rovnostní logika, nebo dokonce čistá výroková logika a její různá zesílení. Použití přesného matematického formalismu v zápisu problémů je nutné pro práci dnešních dokazovačů. Na rozdíl od přirozeného jazyka (jako je čeština nebo angličtina) je matematická formulace jednoznačná a má přesně definovaný význam. Matematický formalismus také přesně definuje, jaká pravidla je možné použít pro odvozování nových tvrzení z axiomů, a tím i vymezuje pojem korektního důkazu. Převod problému z přirozeného jazyka do formálního matematického jazyka (formalizace nebo matematizace problému) je často netriviálním procesem, který ale na druhou stranu také často přispívá k lepšímu porozumění problému.

Výsledkem práce automatických dokazovačů je obvykle detailní formální důkaz domněnky z axiomů, tedy posloupnost odvozovacích kroků povolených daným matematickým formalismem. Správnost takového formálního důkazu lze tedy obvykle snadno nezávisle ověřit, ať už lidmi, nebo dalšími počítačovými programy (tzv. ověřovači formálních důkazů, formal proof checkers). To je také obecně jedna z velkých výhod formálních a počítači srozumitelných důkazů oproti důkazům nebo vysvětlením zapsaným v přirozeném jazyce. Není totiž neobvyklé, že lidé navrhnou a „pochopí“ i důkazy, které jsou nesprávné nebo nedovysvětlené. Detailnost formálních důkazů ale může být i jejich nevýhodou, někdy je totiž těžké z dlouhé posloupnosti formálně korektních kroků vyextrahovat to, co lidé nazývají „podstatnými myšlenkami“ daného důkazu, tedy důkaz lidsky pochopit. V některých případech lze z formálních důkazů také získat proceduru vedoucí k řešení nějakého problému. Například důkaz řešitelnosti uvedeného hlavolamu rozestavení dam na šachovnici by obvykle v sobě obsahoval popis takového rozestavení, kde se dámy neohrožují, a důkaz řešitelnosti problému složení Rubikovy kostky by v sobě obsahoval posloupnost kroků vedoucí z výchozí konfigurace do cílové.
Automatické dokazovače vět jsou tedy počítačové programy snažící se o řešení libovolného problému zapsaného v daném matematickém formalismu, obvykle logice prvního řádu. Logika prvního řádu je ale velmi silný výrazový prostředek, který umožňuje popsat v podstatě veškerou matematiku. Od Gödelových, Churcheových a Turingových dob (30. léta 20. století) je známo, že tato výrazová síla není zadarmo.

Zjednodušeně řečeno, cenou za velkou výrazovou sílu je neexistence obecné efektivní procedury pro řešení problémů zapsaných v logice prvního řádu. Řečeno přesněji, logika prvního řádu není rozhodnutelná (decidable), je pouze semirozhodnutelná (semidecidable). Tyto pojmy znamenají, že neexistuje algoritmus, který pro každý problém logiky prvního řádu zaručeně někdy skončí a oznámí výsledek, tedy zda příslušná domněnka je nebo není logickým důsledkem příslušných axiomů. Lze pouze najít algoritmus (a takové algoritmy často používají systémy ATP), který vždy skončí úspěchem, pokud je domněnka skutečně důsledkem axiomů, ale který nemusí nikdy skončit, pokud tomu tak není. V praxi to znamená, že pokud automatické dokazování trvá dlouho, je to buď proto, že důkaz existuje, ale je těžký, nebo proto, že důkaz vůbec neexistuje (i v tom případě může dokazovač často po nějaké době skončit neúspěchem, místo aby neskončil vůbec). Dokazovač můžeme nechat pracovat hodinu, den nebo rok, ale dokud neskončí, tak nevíme, o který z těchto případů jde.
Tyto vlastnosti automatického dokazování vedou k tomu, že systémy ATP k řešení netriviálních problémů v rozumném čase často vyžadují ovládání specialistou, který do nějaké míry rozumí jak řešené matematické problematice, tak způsobu práce daného dokazovače. Slovo automatické v názvu systémů ATP je tedy třeba brát s rezervou, protože tito specialisté obvykle používají systémy ATP do jisté míry interaktivně. Tato interakce může být na různých úrovních. Uživatel může dokazovači například detailně říkat, která odvozovací pravidla se mají použít. Nebo se naopak uživatel vůbec nemusí o způsob práce dokazovače zajímat, pouze může daný problém rozdělit na menší podproblémy (lemmata), o kterých ví, že budou pro celkový důkaz potřebné. Systémy ATP a jejich uživatelé se tedy během procesu dokazování často navzájem ovlivňují a doplňují:

…

Automatické dokazování je dnes používané v řadě oborů, jmenujme alespoň matematiku (logiku, algebru a řadu dalších matematických teorií) a informatiku (verifikaci hardwaru a softwaru, zpracování přirozeného jazyka a další). Nejvýznamnější aplikace jsou popsány v následujícím výkladu. Potenciální použití ATP je však mnohem širší, téměř pro jakýkoliv obor, který dosáhl alespoň částečné logické (sémantické) formulace svých znalostí. Díky rychle postupujícímu pronikání počítačové techniky do celé vědy a rozvoji velkých znalostních bází veřejně přístupných na internetu tak ATP začíná pronikat i do oborů, jako je biologie, chemie, medicína, obchod atd. Dá se říci, že technologie ATP v dnešní době čeká na své nové uživatele z těchto oborů.

(pokračování článku)

Tento text je úryvkem z knihy:
Vladimír Mařík a kolektiv: Umělá inteligence 6, Academia 2013
O knize na stránkách vydavatele

autor