Úvod
Pozorovánípozorováním lze získat omezené znalosti týkající se objektů v našem dosahu.
UvažováníKonstruování (neintuitivních) závěrů z daných předpokladů. Cílem uvažování je odvodit znalost, kterou nemůžeme (nebo nechceme) získat pozorováním. Uvažování je smysluplné (korektní), pokud jím získané závěry jsou pravdivé.
LogikaMatematický obor zkoumající exaktní postupy uvažování.
SyntaxeSyntaxe logiky je ta část logiky, která se zabývá formální popisem logického jazyka, aniž by mu přiřazovala význam či zkoumala pravdivost.
Sémantikaje ta část logiky, která se zabývá přiřazováním významu symbolům a dalším konstrukcím jazyka logiky.
KorektnostUvažování (v logice i jinde) přináší prospěch jen pokud jeho výsledky jsou pravdivá tvrzení. Takovému uvažování (takovým deduktivním pravidlům) říkáme korektní.
nekonzistentní systémysystémy, v nichž lze dokázat nepravdivá tvrzení.
neúplné systémysystémy ve kterých nelze dokázat to, co potřebujeme.
Russelův paradoxPokud použijeme neformální definici množiny: Všechny objekty s danou vlastnosti tvoří množinu.
Gödelova větane všechna pravdivá tvrzení lze formálně dokázat.
Algoritmus Britského muzeakaždé dokazatelné tvrzení lze dokázat strojově. Pomocí odvozovacích pravidel postupně generujeme důkazy všech pravdivých tvrzení. Jistě takto jednou najdeme i důkaz tvrzení, které chceme dokázat. Obecně ale nelze každé dokazatelné tvrzení dokázat efektivně.
Automatické uvažovánízkratka ATP (automated theorem proving). Rozdělení: Hledání modelů (model finding), Kontrola modelů.
Automatické dokazováníCílem je počítačem z dané množiny předpokladů logicky odvodit platnost daného závěru. Výsledkem je: důkaz závěru z předpokladů (nebo jen konstatování, že je tvrzení dokazatelné). Nebo konstatování, že tvrzení je nedokazatelné (pouze někdy!). Nebo není schopen systém rozhodnout v rámci daných omezení (čas, paměť, ...).
Kontrola modelůFormálně: zkoumáme, zda platí tvrzení v dané interpretaci – v rámci daného přiřazení významu logického jazyka.
Hledání modelůFormálně: hledáme model množiny formulí.
Interaktivní systémypracují v menších krocích. Operátor systému „napovídá“, jaké taktiky má zkoušet a směruje ho tak k cíli.
Automatické systémyse snaží zcela samostatně vyřešit úlohu.
Dostupné nástroje automatického uvažování
- Pro predikátovou logiku prvního řádu: E, Otter, Prover9, SPASS, Vampire,
Waldmeister (rovnicový), aj.
- Pro logiky vyšších řádů: ACL2, Coq, HOL, Isabelle, Nqthm, Agda, aj.
- Knihovna TPTP (www.tptp.org) s problémy zapsanými v predikátové logice prvního řádu. Má interface na webu.
Rezoluční kalkulus pro výrokovou logiku
InterpretaceInterpretace M je zobrazení, které přiřazuje každé výrokové proměnné význam – nepravda nebo pravda, nebo jako hodnoty 0 nebo 1.
ModelJestliže je formule φ pravdivá v dané interpretaci M, říkáme, že M je model φ, značíme: M |= φ. Říkáme též, že M splňuje φ.
Sémantický důsledekJestliže ψ platí ve všech interpretacích, ve kterých platí φ, říkáme, že ψ je sémantický důsledek φ. Značení: φ ⊨ ψ
Poznámky
- Pozorování: Relace "⊨" na formulích je reflexivní a tranzitivní.
- Je-li současně φ ⊨ ψ a ψ ⊨ φ, říkáme, že tyto formule jsou sémanticky ekvivalentní nebo také ekvi-splnitelné, někdy značeno φ ⧦ φ.
- Někdy se rozlišuje značením, že M je model formule ψ a že ψ je sémantickým důsledkem φ: M⊧ψ, φ⊨ψ.
TautologieJestliže formule φ platí ve všech interpretacích, nazýváme jí tautologie. Značení: ⊨ φ
Tautologie - vlastnosti
- Každá interpretace je modelem (libovolné) tautologie.
- Každá tautologie je sémantickým důsledkem libovolné formule, například b ⊨ (a | ¬a)
- Důsledek: všechny tautologie jsou sématicky ekvivalentní.
Kontradikce (Spor)Jestliže formule ψ není splněná v žádné interpretaci, nazveme jí kontradikce, nebo sporná formule.
Sporná množinaMnožinu formulí, která není splněná v žádné interpretaci, nazveme spornou množinou.
Kontradikce (spor) – vlastnosti
- Sporná formule (množina) nemá žádný model.
- Libovolná formule je sémantickým důsledkem sporné formule (množiny), například: (a & ¬a) ⊨ b
- Důsledek: Všechny kontradikce jsou sémanticky ekvivalentní.
- Formule je sporná právě když její negace je tautologie a naopak.
Logický kalkulus (Logický deduktivní kalkulus)Mechanismus, které umožňují zjistit (odvodit) pravdivost formule syntaktickými prostředky, tedy pouze prací se symboly, kterými jsou formule zapsány. Každý logický kalkulus se skládá z:
jazyka, ve kterém se zapisují jeho formule;
axiomů, což jsou formule, jejichž platnost v daném kalulu implicitně předpokládáme;
odvozovacích pravidel, která říkají, jaké formule můžeme odvodit z axiomů, nebo z jiných již odvozených formulí.
DůkazDůkaz v daném logickém kalkulu je taková konečná posloupnost formulí, kde každá formule je buďto:
jeden z axiomů, nebo
odvozená pomocí některého logického pravidla kalkulu z předcházejících formulí v posloupnosti.
DokazatelnostŘekneme, že formule ψ je dokazatelná z množiny formulí A, pokud existuje důkaz ψ z A. Značení: A ⊦ ψ.
Hilbertův implikativní kalkulus pro výrokovou logikumá odvozovací pravidlo modus ponens.
Korektnost logického kalkuluLogický kalkulus je korektní, jestliže platí: všechny axiomy jsou tautologie, a pokud z formulí φ1,...,φn odvodíme ψ, musí platit φ,...,φ⊨ ψ. Čili, vše, co je dokazatelné, je pravda.
Úplnost logického kalkuluVše, co je pravda, je dokazatelné.
Rezoluční kalkulusRezoluční kalkulus umožňuje dokázat, že je daná množina tzv. klauzulí sporná, tedy zda v žádné interpretaci nelze splnit všechny dané formule. Úlohu je tedy nejprve nutné převést na hledání důkazu sporu z nějaké množiny klauzulí.
Jazyk rezolučního kalkulu pro výrokovou logiku
Literálje výroková proměnná nebo její negace.
Klauzuleje disjunkce libovolného počtu literálů.
Prázdná klauzuleje klauzule, která neobsahuje žádný literál. Tato je ekvivalentní (každé) kontradikci. Značení , někdy též ⊥ nebo {}.
Axiomy, odvozovací pravidlo výrokové rezoluce
- Výroková rezoluce nemá žádné axiomy (stejně tak predikátová).
- Výroková rezoluce má pouze jedno odvozovací pravidlo:
D|a ¬a | G
----------------------
D|G
- kde D a G jsou disjunkce libovolného počtu literálů (klauzule).
- Výsledná klauzule „D | G“ se nazývá rezolventa.
Věta (o úplnosti rezolučního kalkulu) (refutationally complete)Buď A sporná množina klauzulí. Pak lze rezolučním kalkulem odvodit prázdnou klauzuli (spor).
Použití rezolučního kalkulu
- Převedeme úlohu na hledání důkazu
spornosti množiny formulí.
- Formule převedeme do CNF (na klauzule).
- Aplikujeme rezoluční kalkulus.
Metoda důkazu sporemVěta: A ⊨ φ právě když A∪{¬φ} ⊨ (jinak řečeno, A∪{¬φ} je sporná množina formulí).
Převedení formulí na CNF
- Všechny logické spojky přepíšeme pomocí konjunkce, disjunkce a negace.
- Pomocí DeMorganových pravidel přesuneme všechny negace co nejhlouběji, až k výrokovým proměnným.
- Průběžně eliminujeme dvojité negace.
- Distributivním pravidlem roznásobíme konjunkce a disjunkce tak, aby všechny disjunkce byly uvnitř konjunkcí.
Strategie aplikace rezolučního pravidla
- Při použití rezoluce (i jiných důkazových
mechanismů) musíme (my, nebo automatický dokazovač) volit, na které dvě klauzule použít rezoluční pravidlo.
- Snahou je vybírat takové klauzule, které nejspíš povedou ke krátkému důkazu.
Strategie aplikace rezolučního pravidla
Optimalizace konverze na CNF
SubsumpceJestliže φ⊆ψ ve smyslu množin literálů, říkáme, že formule φ subsumuje formuli ψ. Značme φ ⊑ ψ.
Subsumpce v rezoluciPokud existuje rezoluční důkaz sporu z B a platí-li A ⊑ B, pak:
- existuje rezoluční důkaz sporu z A;
- ten lze mechanicky sestrojit, a
- není delší než důkaz z B.
Dopředná subsumpce (forward)Vždy ponecháváme subsumující klauzuli (tu s méně literály, vlevo od ⊑ )
Zpětná subsumpce (backward)zahazujeme subsumovanou klauzuli (tu s více literály, vpravo od ⊑ ).
Uspořádaná rezoluceMyšlenka: Abychom dospěli k prázdné klauzuli, musíme z nějaké klauzule odstranit postupně všechny literály.
Nezávisí na pořadí, v jakém literály odstraňujeme.
Tím, že nějaké pořadí zvolíme, omezíme množství odvozených klauzulí.
Kvaziuspořádání≼ je reflexivní tranzitivní relace.
Lineární uspořádání≼ je totální kvaziuspořádání, tedy takové, kde platí, že pro libovolné A a B platí A ≼ B nebo B ≼ A (obecně může platit i obojí najednou).
Úplnost uspořádané rezoluceVěta: Z každé sporné množiny klauzulí S lze uspořádanou rezolucí odvodit spor.
Tableau pravidla pro predikátovou logiku
- Na začátku přepokládejme tableau tvořené jen jedním
uzlem - kořenem obsahujícím konjunkci všech formulí ze
vstupní množiny.
- Někdy se také tento kořen označuje symbolem Т (top).
Tento uzel se obvykle v grafické podobě tabla nezobrazuje.
- Nyní se začnou na tableau aplikovat postupně jednotlivá
pravidla.
konjuknceA & B -> připojíme větev s A a B
disjunkceA | B -> vytvoříme jednu větev s A a druhou s B
negacepřevedení negace blíže k literálům. Pokud budeme zpracovávat pomocí tableau metody pouze formule v tzv. negativní normální formě (NNF), není třeba žádné pravidlo pro zpracování negace zavádět.
univerzální kvantifikacenahrazením všech volných výskytů proměnné x za novou proměnnou x’, která se ještě nikde v tableau nevyskytuje.
existenční kvantifikacenahrazením všech volných výskytů x termem f(x1 ,…,xn). Zde f je nový funkční symbol, který se ještě nikde v tableau nevyskytuje.
uzavření větvepokud se na některé větvi v tableau vyskytují dva komplementární literály co dávají po unifikační substituci spor, potom aplikujeme substituci θ na všechny uzly tableau a takovou větev označíme za uzavřenou.
uzavřené tableauTableau je uzavřené, pokud jsou všechny jeho větve uzavřené.
LeanTAPLeanTAP je jeden z nejkratších úplných dokazovačů pro predikátovou logiku. LeanTAP používá tableau metodu a skládá se z pěti klauzulí v programovacím jazyku Prolog. Jako vstup přepokládá dokazovač konjunkci skolemizovaných uzavřených formulí v NNF.
DPLL a metody pro SAT
SATBoolean SATisfiability problem. Řeší problém nalezení ohodnocení proměnných v booleovské formuli bez kvantifikátorů tak, že je formule splněna.
DPLLDavis-Putnam-Logemann-Loveland algoritmus pro řešení SAT. The basic backtracking algorithm runs by choosing a literal, assigning a truth value to it, simplifying the formula and then recursively checking if the simplified formula is satisfiable. The DPLL algorithm enhances over the backtracking algorithm by the eager use of the following rules at each step: unit propagation and pure literal elimination.
unit clause (jednotková klauzule)je klausule která obsahuje právě jeden literál. Tento literál obsahuje nenastavenou proměnnou.
unit propagation (unit propagation)If a clause is a unit clause, i.e. it contains only a single unassigned literal, this clause can only be satisfied by assigning the necessary value to make this literal true. Thus, no choice is necessary. In practice, this often leads to deterministic cascades of units, thus avoiding a large part of the naive search space.
pure výskytznamená, že se literál všude ve Φ vyskytuje buď ve tvaru x anebo se všude ve Φ vyskytuje ve tvaru ¬x.
pure literal eliminationIf a propositional variable occurs with only one polarity in the formula, it is called pure. Pure literals can always be assigned in a way that makes all clauses containing them true. Thus, these clauses do not constrain the search anymore and can be deleted.
MiniSatvelmi výkonný SAT solver
MiniSat – analýza konfliktuKonflikt nastane pokud se nějaká klauzule stane nesplnitelnou během propagace unit klauzule (boolean_constraint_propagation()).