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