TU Wien:Theoretische Informatik und Logik VU (Fermüller)/Zusammenfassung Logik

Für die Zusammenfassung vom vorigen Teil, siehe hier.

---

Wir beschäftigen uns mit klassischer Prädikatenlogik erster Stufe.

• Stufe 0: Aussagenlogik (AL), keine Quantifikation
• Stufe 1: Quantifikation über Elemente des Gegenstandbereichs (Domäne)
• Stufe 2: Quantifikation auch über Prädikate (Relation) und Funktionen

Im Folgenden sprechen wir einfach von Prädikatenlogik (PL).

Zwei wichtige syntaktische Konzepte sind:

Kalkül

Ein Regelsystem mit dem sich Formeln aus anderen Formeln durch systematische Regelanwendungen herleiten lassen.

Theorie

Eine Menge von Formeln. Theorien sind oft durch eine Menge von Formeln (Axiome) definiert.

Syntax der Prädikatenlogik

• Logische Symbole
  • (aussagenlogische) Konnektive (Junktoren, Operatoren)

  1-stellig: $\neg$, 2-stellig: $\land ,\lor ,\subset$

  • aussagenlogische Konstanten (Wahrheitskonstanten)

  $\bot$ (falsum), $\top$ (verum)

  • Quantoren (All-Quantor $\forall$, Existenz-Quantor $\exists$)
  • Gleicheit (Identität): $=$
• Außerlogisches Alphabet (Signatur) $\langle PS,KS,FS\rangle$
  • Prädikatensymbole (PS), P, Q, R
  • Konstantensymbole (KS), a, b, c, d, e
  • Funktionssymbole (FS), f, g, h
• Hilfssymbole: Klammern '(' und ')'
• Individuenvariablensymbole (IVS, kurz Variable) x, y, z, u, v, w

Von Syntax zu Semantik

• Grammatik vs. induktive Definition
• Modellstrukturen $\langle D,P,K,F\rangle$
  • D ... Domäne (nicht-leere Menge)
  • P ... Prädikate über D
  • K ... Konstanten in D
  • F ... totale Funktionen über D
• Terme über Modellstrukturen
• Boolesche Ausdrücke über Modellstrukturen

Semantik, Formalisieren

Semantik der Prädikatenlogik

Eine prädikatenlogische Interpretation ${\mathcal {I}}$ über der Signatur $\Sigma =\langle PS_{\Sigma },KS_{\Sigma },FS_{\Sigma }\rangle$ ist ein Tupel $\langle D,\Phi ,\varepsilon \rangle$, wobei:

• D: Domäne: eine beliebige nicht-leere Menge
• $\Phi$ eine Signaturinterpretation
• $\varepsilon :IVS\to D$ eine Variablenbelegung

${\mathit {PINT}}_{\Sigma }$ .... Menge aller PL-Interpretationen über der Signatur $\Sigma$

Eine Formel $F\in {\mathcal {PF}}_{\Sigma }$ heißt:

• erfüllbar, wenn $val_{\mathcal {I}}(F)=t$ für ein ${\mathcal {I}}\in {\mathit {PINT}}_{\Sigma }$
• wiederlegbar in ${\mathcal {D}}$, wenn $val_{\mathcal {I}}(F)=f$ für ein ${\mathcal {I}}\in {\mathit {PINT}}_{\Sigma }$
• unerfüllbar in ${\mathcal {D}}$, wenn $val_{\mathcal {I}}(F)=t$ für alle ${\mathcal {I}}\in {\mathit {PINT}}_{\Sigma }$
• (logisch bzw. allgemein) gültig in ${\mathcal {D}}$, wenn $val_{\mathcal {I}}(F)=t$ für alle ${\mathcal {I}}\in {\mathit {PINT}}_{\Sigma }$

Tableau-Kalkül

• $\models$ sem. Folgerung
• $\vdash$ syn. Ableitung

• Ein Tableau heißt geschlossen, wenn alle Äste geschlossen sind (also zu einem Widerspruch führen).

• $\mathbf {t} :\forall xF$ und $\mathbf {f} :\exists xF$ heißen $\gamma$-Formeln
• $\mathbf {f} :\forall xF$ und $\mathbf {t} :\exists xF$ heißen $\delta$-Formeln

Hoare-Kalkül

Sammlung von Regeln, die Korrektheitsaussagen in einfachere zerlegen bis nur noch prädikatenlogische Formeln bleiben, deren Gültigkeit zu zeigen ist.

Korrektheitsaussage

{Vorbedingung} Programm {Nachbedingung}

{F} α {G}

partielle Korrektheit

Falls die Eingabe zulässig ist und falls das Programm terminiert, dann ist das Ergebnis richtig.

totale Korrektheit

Falls die Eingabe zulässig ist, dann terminiert das Programm und das Ergebnis ist richtig.

$F\left[{A \atop B}\right]$ oder $F[A/B]$ ... Formel F, in der jedes freie B durch A ersetzt wurde

Zuweisung (zw ↑)

         v <- e {F}
{F[e/v]} v <- e {F}

Konditionale (if ↓)

{F} if e then         ... else
{F} if e then {F ∧ e} ... else {F ∧ ¬e}

Konditionale (fi ↑)

if e then ...     else ...     fi {G}
if e then ... {G} else ... {G} fi {G}

partielle Korrektheit von Schleifen (wh)

Inv: Schleifeninvariante: gilt vor, während und nach der Schleife

      while e do           ...       done
{Inv} while e do {Inv ∧ e} ... {Inv} done {Inv ∧ ¬e}

totale Korrektheit von Schleifen (wht'')

t: Terminationsfunktion oder Variante

      while e do                    ...                     done
{Inv} while e do {Inv ∧ e ∧ t = t0} ... {Inv ∧ 0 <= t < t0} done {Inv ∧ ¬e}