Aussagenlogik

1. Satz, der wahr oder falsch sein kann

2. logische Operatoren, die Aussagen zu Formeln verknüpfen

3. atomare Formeln = Aussagen,

   zusammengesetzte Formeln = mit Junktoren

   
   

Syntax legt äußere Form der logischen Formeln fest

alle weiteren Junktoren sind auf Konjunktion, Disjunktion und Negation zurückzuführen

Bedeutung einer Formel ist im wesentlich ihr Wahrheitswert

Interpretation (Bewertung) ist eine Abbildung der atomaren Aussage auf die Wahrheitswerte 1 (wahr) und 0 (falsch)

• im Kontext der Wissensverarbeitung ist die logische Implikation insbesondere von Bedeutung

• ex falso quodlibet

• Äquivalenz

• XOR

• NAND

• NOR

• Negation vor Konjunktion

• Konjunktion vor Disjunktion

• Disjunktion vor Implikation

• lässt sich durch sukzessives Auswerten der Teilformeln unter Berücksichtigung der Vorrangregeln bestimmen

Übergang von F zu nicht F kann durch Spiegelungsprinzip veranschaulicht werden

• eine allgemeingültige Formel wird zu unerfüllbaren Formel und umgekehrt

• erfüllbare aber nicht allgemeingültige Formel wird wieder zu erfüllbarer aber nicht allgemeingültiger Formel

• endlich viele Belegungen, die auf den in der Formel F vorkommenden atomaren Formeln definiert sind, zu testen

• F hat n verschiedene Atome, dann 2^n zu testende Belegungen

• -> Wahrheitstafelmethode: algorithmusches Verfahren, um Erfüllbarkeit einer Formel zu bestimmmen

• Exponentialverhalten der Rechenzeit ist Thema der Komplexitätstheorie

• syntaktisch unterschiedliche Formeln, die identische Wahrheitswerte haben

• bei jeder Bewertung/Interpretation der Formeln ergibt sich derselbe Wahrweitswert

Bedeutung

• standartisierte, möglichst einfache Darstellung von Formeln wichtig

  • Wissensverarbeitung, Schaltkreisminimierung

• In diese Form muss jede Formel überführbar sein

• z.B. DNF, KNF

• Ablesen aus Wahrheitstabelle

• durch äquivalentes Umformen

• Zu jeder aussagenlogische Formel F gibt es eine aquivalente Formel sowohl in KNF als aich in DNF

• Darstellung nicht eindeutig

• Erstellung Wahrheitstabelle aufwendig, bei n Atomen, 2^n Zeilen

• unnötig große Normalformen

Anwendung semantischer Äquivalenzen, ersetzen Teilformeln durch äquivalente Teilformeln

• NAND, NOR besonders wichtig für Schaltungsentwurf

  • reicht NOR-Operation elektronisch zu realisieren, alle anderen logischen Operationen auf NOR zurückführbar

• minimal vollständig:

  • {NICHT, UND}, {NICHT, ODER}, {nand}, {nor}

• vollständig, aber nicht minimal:

  • {NICHT, UND, ODER}

• Aus A und A -> B folgt B

• 
  

• für diese Formeln existiert schnelles Verfahren zur Überprüfung der Folgerbarkeit

• Formel F ist Hornformel, falls F in KNF ist und jedes Disjunktionsglied höchstens ein positives Literal enthält

In der Praxis: können darstellen

• Fakten: A, A und B

• Regeln aus X und Y folgt Z

• (negierte Fragen): Gilt H1 und H2?

• efizienter Unerfüllbarkeitstest für Hornformeln

Der Markierungsalgorithmus ist (für Hornformeln als Eingabe) korrekt und stoppt spätestens nach n Markierungsschritten, wobei n Anzahl der atomaren Formeln in F

Folgerungen

1. Ist meine Datenmenge M überhaupt konsistent?

2. Kann ich aus M eine neue Aussage G ableiten?

3. Ist F eine Tautologie?

Unerfüllbarkeitstests, die als maschinelle Beweiser (Kalküle) auf Computer durchgeführt werden können

• Wahrheitstafelverfahren: für jede AL-Formel, Komlexität 2^n

• Markierungsalgorithmus: Hornformeln, Komlexität n

• Resolution