Informatik A

Prof. Dr. Norbert Fuhr

fuhr@uni-duisburg.de

auf Basis des Skripts von

Prof. Dr. Wolfram Luther und der Folien von Peter

Fankhauser

1

Teil I

Logik

2

Geschichte

• R. Descartes (17. Jhdt): klassische Euklidische Geometrie mit al-

gebraischen Methoden

• G.W. Leibnitz (17. Jhdt): lingua characteristica, calculus rationa-

tor

• Gottlob Frege (1879): Begriffsschrift Pradikatenlogik erster Stufe

• Skolem (1920): Beweisverfahren

• D. Hilbert, W. Ackermann (1928): Entscheidbarkeitsproblem

• Herbrand (1930): Entscheidbarkeit fur korrekten mathematischen

Satz

• Alan Turing, Alonzo Church (1936): Unentscheidbarkeit PL1

• Robinson (1954): automatisches Beweisverfahren (Resolutions-

prinzip)

• Kowalski, Colmerauer (1972): Prolog

3

Teil I.1

Aussagenlogik

4

Aussagenlogik

Grundlagen

• Aussage (atomare Formel):

Satz der entweder wahr oder falsch ist

abgekurzt mit Großbuchstaben (A, B, ...)

• Beispiel: Heute ist Sonntag

• Interpretation: Zuordnung eines Wahrheitswertes (w oder f)

• Operation: Verknupfung von Aussagen

• Beispiel: Heute ist Sonntag und es ist kalt.

5

Verknupfungen

• Negation: einstellige Operation: ¬A oder A

w f

¬ f w

• Konjunktion: zweistellige Operation: A ∧B

∧ w f

w w ff f f

• Disjunktion: zweistellige Operation: A ∨B

∨ w f

w w wf w f

6

Formeln

Rekursive Konstruktion:

Literal L ::= A Aussage

| ¬A Negierte Aussage

Formel F ::= L Literal

| ¬F Negation

| F ∧ F Konjunktion

| F ∨ F Disjunktion

| (F ) Klammerung

Beispiel

A . . . Heute ist Montag.

B . . . Heute ist Feiertag.

C . . . Heute ist Vorlesung.

¬(A ∧ ¬B) ∨ C

7

Weitere Verkupfungen

• Subjunktion: A→ B ≡ ¬A ∨B

→ w f

w w ff w w

• Bijunktion: A←→ B ≡ (A ∧B) ∨ (¬A ∧ ¬B)

←→ w f

w w ff f w

• Antivalenz (xor): A⊕B ≡ (A ∧ ¬B) ∨ (¬A ∧B)

⊕ w f

w f wf w f

8

Klauseln

Klausel K ::= L Literal| K ∨K Disjunktion

Konjunktive Form KF ::= (K) Klausel| (K) ∧KF Konjunktion von Klauseln

Konjunktion D ::= L Literal| D ∧D Konjunktion

Disjunktive Form DF ::= (D) Konjunktion| (D) ∨DF Disjunktion von

Konjunktionen

Beispiele:

¬A ∨B ∨ C . . . KF und DF

(¬A ∨B ∨ C) ∧ (¬B ∨ ¬C) . . . KF

(¬A ∧ ¬B) ∨ (¬A ∧ ¬C) ∨ (B ∧ ¬C) ∨ (¬B ∧ C) . . . DF

9

Beweisverfahren

Begriffe

• Modell: Interpretation unter der eine Formel F wahr ist.

• Unerfullbare Formel: Formel F , fur die es kein Modell gibt.

• Tautologie: Formel F , fur die jede Interpretationen ein Modell ist.

` F

Beweis uber Wahrheitstafeln

• Durchrechnen fur alle Interpretationen

Axiomatische Verfahren

• Umformen bis zum Wahrheitswert w oder auf konjunktive Form

mit mindestens einer Aussage P ∨ ¬P in jeder Klausel

10

Wahrheitstafel

Zu zeigen: ` ((P → Q) ∧ P )→ Q

P Q P → Q (P → Q) ∧ P ((P → Q) ∧ P )→ Qf f w f wf w w f ww f f f ww w w w w

11

Syntaktische Umformung

Aquivalent sind die folgenden Formeln:

((P → Q) ∧ P )→ Q

¬ ((¬P ∨Q) ∧ P ) ∨Q

((P ∧ ¬Q) ∨ ¬P ) ∨Q

((P ∨ ¬P ) ∧ (¬Q ∨ ¬P )) ∨Q

(w ∧ (¬P ∨ ¬Q)) ∨Q

(¬P ∨ ¬Q) ∨Q

¬P ∨ ww

12

Uberfuhrung in konjunktive Form

((P → Q) ∧ P )→ Q

¬ ((¬P ∨Q) ∧ P ) ∨Q

((P ∧ ¬Q) ∨ ¬P ) ∨Q

((P ∨ ¬P ) ∧ (¬Q ∨ ¬P )) ∨Q

((P ∨ ¬P ∨Q) ∧ (¬Q ∨Q ∨ ¬P ))

13

Aquivalenzregeln

Zwei Formeln F, G sind aquivalent; F ≡ G, wenn gilt: ` F ←→ G

(F ∧ F ) ≡ F, (F ∨ F ) ≡ F Idempotenz

(F ∧G) ≡ (G ∧ F ) ,(F ∨G) ≡ (G ∨ F ) Kommutativitat

((F ∧G) ∧H) ≡ (F ∧ (G ∧H)) ,((F ∨G) ∨H) ≡ (F ∨ (G ∨H)) Assoziativitat

(F ∧ (F ∨G)) ≡ F, (F ∨ (F ∧G)) ≡ F Absorption

(F ∧ (G ∨H)) ≡ ((F ∧G) ∨ (F ∧H)) ,(F ∨ (G ∧H)) ≡ ((F ∨G) ∧ (F ∨H)) Distributivitat

¬¬F ≡ F Doppelnegation¬ (F ∨G) ≡ (¬F ∧ ¬G) ,¬ (F ∧G) ≡ (¬F ∨ ¬G) de Morgansche Regeln

F → G ≡ ¬F ∨G bedingte EliminierungF ∧G ≡ F, F ∨G ≡ G, falls F unerfullbarF ∧G ≡ G, F ∨G ≡ F, falls F Tautologie

14

Logisches Schließen

• Fur S eine Menge von Formeln F1, . . . , Fk und F eine Formel, ist

F eine logische Konsequenz von S, in Zeichen S ` F , wenn jede

Interpretation von S, die ein Modell von S ist, auch ein Modell

von F ist.

• Regeln:

F ` F ∨GF ` G→ F

F ∧G ` FF ∧G ` G↔ F

(F → G) ∧ (G→ H) ` F → H TransitivitatG ∧ (G→ F ) ` F Modus Ponens (Schlussregel)¬F ∧ (G→ F ) ` ¬G Modus Tollens

15

Beispiel: Transitivitat

A: (a ist eine gerade Zahl und b ist eine gerade Zahl)

B: (a+ b ist eine gerade Zahl)

B1: (a = 2n und b = 2m, n, m ganze Zahlen)

B2: (a+ b = 2k, k ganze Zahl)

A a und b sind gerade ZahlenA→ B1 Dann gibt es Zahlen n, m mit a = 2n und b = 2mB1 → B2 Aus a = 2n und b = 2m folgt a+ b = 2(n+m) = 2kB2 → B Aus a+ b = 2k folgt a+ b ist eine gerade ZahlB Mit der Transitivitat gilt B

16

Axiomensysteme

• Theorie: Menge von Axiomen + Menge von Formeln

• Korrektheit: Jede Formel F , die aus einer Theorie T mit Hilfe von

Axiomen AS abgeleitet wird (T `AS) ist eine logische Konsequenz

aus T (T ` F ).

• Vollstandigkeit: Jede Formel F , die eine logische Konsequenz aus

T ist, ist auch tatschlich mit Hilfe von AS ableitbar.

• Konsistenz: Es ist nicht sowohl F als auch ¬F ableitbar.

• Unabhangigkeit: Kein Axiom ist die logische Konsequenz anderer

Axiome.

• Entscheidbarkeit: Fur alle Formeln gilt T `AS F oder T `AS ¬F .

• Aussagenlogik ist entscheidbar und besitzt konsistente, vollstandi-

ge und unabhangige Axiomensysteme.

17

Hilberts Axiomensystem der Aussagenlogik

• AS1: A ∨A→ A

• AS2: A→ (A ∨B)

• AS3: (A ∨B)→ (B ∨A)

• AS4: (A→ B)→ ((C ∨A)→ (C ∨B))

• Definition: A→ B ≡ ¬A ∨B

• Modus Ponens: A ∧ (A→ B) ` B

• Ersetzungsregel: F [A/G] in der Formel F ersetze einige (alle) Vor-

kommen der Aussagenvariablen A durch die Formel G

18

Beispiel

Zeige: ` (F ∨ F )←→ F

Beweis:

(F ∨ F ) → F AS1.

F → (F ∨G) AS2,

F → (F ∨ F ) Ersetzungsregel ((F ∨G)[G/F ]).

19

Automatisches Beweisen

Resolution

• Modus Ponens:

PP → BB

• Verallgemeinerung: P → B ≡ ¬P ∨B

P ∨A1 ∨A2 ∨ . . . ∨An

¬P ∨B1 ∨B2 ∨ . . . ∨Bm

A1 ∨A2 ∨ . . . ∨An ∨B1 ∨B2 ∨ . . . ∨Bm Resolvente

• Um die Aussage A zu beweisen fuge die Negation der Aussage ¬A

zu den Formeln der Theorie und versuche, durch Resolution die

leere Klausel herzuleiten.

20

Beispiel

T = A ∨B, A→ ¬B,¬A

Um B herzuleiten, fugen wir ¬B zur Theorie dazu, und formen A→ ¬B

um.

Das ergibt:

T ′ = A ∨B,¬A ∨ ¬B,¬A,¬B

In Klauselform:

T ′ = (A, B), (¬A,¬B),¬A,¬B

B ist ein Resolvent von (A, B) und ¬A. Der Resolvent von B und ¬B

ist die leere Menge, daher ist T ′ unerfullbar, daher folgt aus T B.

21

Teil I.2

Pradikatenlogik

22

Pradikatenlogik

Erweiterung der Aussagenlogik

• Konstante: a, b, c

• Variablen: x, y, z

• Funktionen: f(a1, . . . , ak)

• Pradikate: P (a1, . . . , ak)

• Quantoren: Allquantor (∀xF ), Existenzquantor (∃xF )

23

Semantik

Interpretation:

Abbildung auf Domane zur Zuordnung eines Wahrheitswertes

Beispiel

F : ∀xP (f(x, a), x).

• Domane: naturliche Zahlen IN := {1,2,3, . . .}

• Konstante a ::= 1

• f(x, a) ::= x ∗ a

• P (x, y) ::= x = y

• Interpretation: Fur alle naturlichen Zahlen x ∈ IN gilt x · 1 = x.

24

Weitere Schlussregeln und Aquivalenzen

∀xF ` ∃xF fur eine nichtleere Domane

∀xF ∨ ∀xG ` ∀x(F ∨G)

∃x(F ∧G) ` ∃xF ∧ ∃xG

¬∀xF ≡ ∃x¬F

¬∃xF ≡ ∀x¬F

∀x∀yF ≡ ∀y∀xF

∃x∃yF ≡ ∃y∃xF

∀x(F ∧G) ≡ ∀xF ∧ ∀xG

∃x(F ∨G) ≡ ∃xF ∨ ∃xG

25

Entscheidbarkeit von PL1

• Die Wahrheitstafelmethode ist nicht ubertragbar

• Erfullbarkeit und Allgemeingultigkeit ist nicht entscheidbar

• PL1 ist halbentscheidbar: Unerfullbare Formeln werden nach end-

licher Zeit erkannt.

26

Beispiel: Peano-Axiome

1. P (1)

2. ∀x (P (x)→ ∃y (P (y) ∧Q(x, y))) .

3. ¬∃x(P (x) ∧Q(x,1)

4.∀x1∀x2∀y1∀y2 (P (x1) ∧ P (x2) ∧Q(x1, y1) ∧Q(x2, y2)∧

¬(x1 = x2)→ ¬(y1 = y2)).

5. ∀M (M(1) ∧ ∀x∀y (P (x) ∧ P (y) ∧M(x) ∧Q(x, y)→M(y))→ (M ≡ P )) .

Interpretation

• P (x) . . . x ist eine naturliche Zahl

• Q(x, y) . . . y = x+1; y ist Nachfolger von x• M . . . Pradikatenvariable (nicht moglich in PL1)

27