FrontPage > TuWienMitschriften > WissensbasierteSysteme > AussagenLogik

AussagenLogik

Signatur

SIGMA = { A1, ..., An }

• Aussagenvariable Ai
• Repräsentiert ein Faktum:

"Nero ist ein Hund"
"Informatik macht Spaß"

Formeln:

• Atomare Formeln A
• Komplexere Formeln mit Junktoren

!P nicht P (Negation)
P AND Q P und Q (Konjunktion)
P OR Q P oder Q (Disjunktion)
P => Q P impliziert Q (Implikation)
P <=> Q P äquivalent zu Q (Äquivalenz)

"Induktiv" definiert

kommt immer wieder vor

Man gebe mir einen String. Programm rekursiv. Ist String Multiform einer Formel?

Rekursion terminiert!

Übersichtlich und einfach Implementiertbar

Für Informatiker übersichtlich und einfach umsetzbar, Stichwort Parsing

Auswertung von Wahrheitstabellen

Interpretationen: |: SIGMA -> { true, false }

• I(A)=true: Das Faktum A gilt in der betrachteten Welt
• I(A)=false: Das Faktum A gilt _nicht_ in der betrachteten Welt

Erfüllungsrelation:

I |= F gdw |[F]|_I = true

F wird ausgerechnet, das geht aber nur mit einer Wahrheitstabelle.

wobei

|[A]|_I=I(A), falls A eine atomare Formel ist.

klassisch-logische Interpretation der Junktioen !, AND, OR, =>, <=>:

Wahrheitstabellen.

Semantische Äquivalenzen

Idempotenz

F AND F &equiv; F
F OR F &equiv; F

Kommunitativität

F AND G &equiv; G AND F
F OR G &equiv; G OR F

Assoziativität

(F AND G) AND H usw.

Absorption

Distributivgesetz

Doppelnegation

!!F &equiv; F

deMorgan

!(F AND G) &equiv; !F OR !G
!(F OR G) &equiv; !F AND !G

Kontraposition

F => G &equiv; !G => !F

Implikation

F => G &equiv; !F OR G

Koimplikation

F <=> G &equiv; (F => G) AND (G => F)

Anwendung bei Regelbasierten Systemen.

Ziel: Syntaktisch einfache Regeln - keine Disjunktion im Regelrumpf.

A1 OR A2 => B &equiv; (A_1 => B) AND (A_2 => B)

(Implikation, deMorgan, Distributivität)

Hornklausl / SLD

Wurde in logikorientierte Programmiersprachen unterrichtet, allerdings scheinbar nicht bei Prof. Neumerkel (wo ich Prolog ca. 1998 gemacht habe).

NP-Vollständig, nicht deterministisch polynomiell

Konzept: Guess and Check (Einfach mal raten und nachher prüfen, ob's stimmt)

Die Lösungsverifikation (Check) ist zwar polynomiell, jedoch gibt es exponentiell viele Lösungskandidaten. Im worst-case: Nicht erfüllbar.

Hornformeln hingegen sind polynomienell entscheidbar!

Hornklauselmengen

{ H1, ..., H5 } = Konjunktion

&equiv; FORALL(i=1, 5) H_i

Ziel

syntaktisch einfache Regeln -- ein einziges Literal im Folgerungsteil

A => B1 OR B2 &equiv; (A AND !B1 => B2) AND .....

Inferenzregeln

Notation:

F1, ..., Fn
________
F

Modus ponens (MP):

F, F => G
________
G

Modus tolens (MT):

F => G, !G
_________
!F

Grenzen

Max hat lange Ohren. Dafür brauchen wir die Prädikatenlogik!

FORALL(x) hase(x) -> langohr(x)
hase(m)
_______
langohr(m)

PrädikatenLogik

Last modified 2005-03-07 19:38 by rck