Seite parallel anzeigen
Aussagenlogische Beweisverfahren
(Aussagenlogik Kapitel 7.2)Weitere Themen dieses Kapitels
Erinnern wir uns:
Der logische Beweis ist das rein formale, syntaktische Pendant der Schlussfolgerung.
Der logische Beweis bezeichnet den Vorgang, bei dem eine Menge von Prämissen unter eventueller Hinzunahmen von Axiomen (als gültig vorausgesetzte Aussagen) durch Anwendung von Schlussregeln so lange umgeformt werden, bis die Konklusion entsteht. Gibt es so eine Abfolge von Regeln, so ist die Konklusion "ableitbar".
Für die Aussagenlogik wurden viele unterschiedliche Kalküle eingeführt, welche direkte, aber auch indirekte Beweise konstruieren. Bevor wir den Tableau-Kalkül näher betrachten, soll in den nächsten drei Kapiteln 3 weitere, bedeutende Kalküle kurz vorgestellt werden, um einen Eindruck unterschiedlicher Ableitungsmethoden zu geben:
Der logische Beweis ist das rein formale, syntaktische Pendant der Schlussfolgerung.
Der logische Beweis bezeichnet den Vorgang, bei dem eine Menge von Prämissen unter eventueller Hinzunahmen von Axiomen (als gültig vorausgesetzte Aussagen) durch Anwendung von Schlussregeln so lange umgeformt werden, bis die Konklusion entsteht. Gibt es so eine Abfolge von Regeln, so ist die Konklusion "ableitbar".
Ist γ aus Γ ableitbar, schreiben wir Γ|--γ um den logischen Beweis auszudrücken.
Für die Aussagenlogik wurden viele unterschiedliche Kalküle eingeführt, welche direkte, aber auch indirekte Beweise konstruieren. Bevor wir den Tableau-Kalkül näher betrachten, soll in den nächsten drei Kapiteln 3 weitere, bedeutende Kalküle kurz vorgestellt werden, um einen Eindruck unterschiedlicher Ableitungsmethoden zu geben:
- der Sequentialkalkül,
- der Hilbert-Typ-Kalkül und
- die Resolution
- zurück zu Semantisches Prüfverfahren für die Gültigkeit eines Schlusses
- zum Seitenanfang
- weiter zu
