Lauseloogika

Aatom:

\begin{equation*} P \end{equation*}

Literaal (?) võib olla aatom või tema eitus:

\begin{equation*} P, \neg P \end{equation*}

Lausevorm (clausal form) koosneb literaalide disjunktsioonist, tegu on ka DNF-iga (disjunctive normal form):

\begin{equation*} P \lor Q \lor \neg R \end{equation*}

Lauseloogikat võib mõneti nimetada ka kui nullindat järku loogika (zeroth-order logic). Kuna lauseloogikas pole kvantifikaatoreid siis ei saa formaalselt kirja panna "Kõik mehed on surelikud. Socrates on mees. Järelikult Socrates on surelik." väidet, sest "on mees" puhul on juba tegu universaalse kvantifikaatoriga ∀ (universal quantification).

Lauseloogika operaatorid

Loogika sümboleid on läbi aja üles märgitud erineval moel:

Eitus (negation), loetakse kui "mitte" (not): ¬, ~, !, not
Konjunktsioon (conjunction), loetakse kui "ja" (and): ∧, •, &, &&, and
Disjunktsioon (disjunction), loetakse kui "või" (or): ∨, +, |, ||, or
Välistav disjunktsioon (exclusive disjunction), "xor": ⊕, ⊻, ^, xor
Eitav konjunktsioon (negated and), loetakse kui "nand": ⊼, nand
Eitav disjunktsioon (negated or), loetakse kui "ega" (nor): ⊽, nor
Tautology, loetakse kui "tõene" (top, verum): ⊤, T, 1, true, False
Vastuolu (contradiction), loetakse kui "väär" (bottom, falsum), ⊥, F, 0, false, False
Ekvivalents (equivalence), loetakse kui "... kui ja ainult kui ..." (... if and only if ...): ⇔, ↔, ≡, iff, ==
Implikatsioon (implication), loetakse kui "kui ... siis ..." (if ... then ...): ⇒, →, ⊃

Iga rea viimane on ka Pythonis kasutatav operaator või konstant.

Tuletamisreeglid

Modus poens, ehk implikatsiooni kõrvaldamine (implication elimination):

\begin{equation*} \frac {P \implies Q, P}{\therefore Q} \end{equation*}

Järjestikuses vormingus näeks modus poens välja järgnev:

\begin{equation*} P \implies Q, P \models Q \end{equation*}

MP (modus ponens)
kui P ja Q siis P
kui P siis P või Q
kui !!P siis P
if P then Q if Q then R leads to if P then R

Rahuldatavus

interpretation is a mapping to a world sentence is satifsiable by an interpretation if under that interpretation the sentence evaluates to true

if no interpreatation makes all the sentences in the set to be tru, then set of sentences is unsatisfiable or incorrect (?)

If set of sentences make another set of sentences true under certain interpretation it is said that one sentence

S logically entails S_1 entailment

Näide kolmnurkadega

resolution = a sound inrefence mechanism, convert all sentences to clausal form

Eesmärk (goal) on tõestada, et võrdkülgse kolmnurga nurgad B ja C on võrdsed:

\begin{equation*} Võrdkülgne(ABC) \implies Võrdsed(B, C) \end{equation*}

Esiteks paneme kirja aksioomid. Võrdkülgne kolmnurk on alati võrdhaarne:

\begin{equation*} Võrdkülgne(ABC) \implies Võrdhaarne(ABC) \end{equation*}

Teine aksioom: Võrdhaarne tähendab et kaks külge on võrdse pikkusega:

\begin{equation*} Võrdhaarne(ABC) \implies Võrdsed(AB, AC) \end{equation*}

Kolmas aksioom: Kaks võrdset külge tähendab et nendele vastavad nurgad on võrdsed:

\begin{equation*} Võrdne(AB, AC) \implies Võrdsed(B, C) \end{equation*}

Kirjutades aksioomid ümber lausekujule saame:

\begin{equation*} \neg Võrdkülgne(ABC) \lor Võrdhaarne (ABC) \end{equation*}

\begin{equation*} \neg Võrdhaarne(ABC) \lor Võrdsed(AB, AC) \end{equation*}

\begin{equation*} \neg Võrdsed(AB, AC) \lor Võrdsed(B, C) \end{equation*}

Lahendamine(?) (resolution) tähendab vastupidise lahenduse puudumise tõestamist (prove by refutal, disprove):

\begin{equation*} \neg Võrdsed(B, C) \end{equation*}

QAoES TU Berlin