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é.
Logika
Matematický obor zkoumající exaktní postupy uvažování.
Syntaxe
Syntaxelogiky 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émantika
je ta část logiky, která se zabývá přiřazováním významu symbolům a dalším konstrukcím jazyka logiky.
Korektnost
Uvaž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émy
systémy, v nichž lze dokázat nepravdivá tvrzení.
neúplné systémy
systémy ve kterých nelze dokázat to, co potřebujeme.
Russelův paradox
Pokud použijeme neformální definici množiny: Všechny objekty s danou vlastnosti tvoří množinu.
Gödelova věta
ne všechna pravdivá tvrzení lze formálně dokázat.
Algoritmus Britského muzea
kaž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ě.
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.
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ůkaz
Dů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 logiku
má odvozovací pravidlo modus ponens.
Korektnost logického kalkulu
Logický 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.
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
Subsumpce
Jestliže φ⊆ψ ve smyslu množin literálů, říkáme, že formule φ subsumuje formuli ψ. Značme φ ⊑ ψ.
Subsumpce v rezoluci
Pokud existuje rezoluční důkazsporu z B a platí-li A ⊑ B, pak: - existuje rezoluční důkazsporu 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á rezoluce
Myš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í.
se užívaná pro automatické dokazování vět v predikátové logice, ale i
v dalších (modálních, temporálních, aj.) logikách.
Sémantické tableau je strom, kde každý uzel je logická
formule.
Sémantické tableau vzniká iterativně z předchozích
tableaux postupnou aplikací určitých pravidel.
Dokazování pomocí tableau metody postupně rozděluje
vstupní formuli na menší formule, dokud na všech větvích
stromu nenajde komplementární páry formulí nebo pokud
už nemůže aplikovat žádné z pravidel.
Vstupem pro tableau metodu bude množina formulí
predikátové logiky.
Cílem metody bude, tak jako v případě rezoluční metody,
najít spor v této množině.
Negation normal form
Formule v negativní normální formě (NNF) je taková logická formule, která obsahuje negaci pouze v literálech.
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.
konjuknce
A & B -> připojíme větev s A a B
disjunkce
A | B -> vytvoříme jednu větev s A a druhou s B
negace
př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í kvantifikace
nahrazení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í kvantifikace
nahrazení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ětve
pokud 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é tableau
Tableau je uzavřené, pokud jsou všechny jeho větve uzavřené.
LeanTAP
LeanTAP 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
SAT
Boolean SATisfiability problem. Řeší problém nalezení ohodnocení proměnných v booleovské formuli bez kvantifikátorů tak, že je formule splněna.
DPLL
Davis-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ýskyt
znamená, že se literál všude ve Φ vyskytuje buď ve tvaru x anebo se všude ve Φ vyskytuje ve tvaru ¬x.
pure literal elimination
If 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.