Prädikatenlogische Inferenz
| Dieser Artikel bedarf einer Überarbeitung. Eine Begründung befindet sich in der Regel auf der Diskussionsseite. Wenn du Lust hast, verbessere den Artikel und entferne anschließend diesen Baustein. |
Die prädikatenlogische Inferenz ist ein mehrstufiges Verfahren, um prädikatenlogische Aussagen zu widerlegen. Es ist geeignet, um prädikatenlogische Aussagen zu beweisen, indem man von der zu beweisenden Behauptung das Gegenteil annimmt, und diese Annahme dann zum Widerspruch führt.
Die prädikatenlogische Inferenz ist semi-entscheidbar, das heißt:
- Lässt sich tatsächlich ein Widerspruch finden, so geschieht dies in endlicher Zeit.
- Lässt sich aber kein Widerspruch finden, so terminiert das Verfahren normalerweise nicht, man rechnet also unendlich lange weiter.
Indem zwei prädikatenlogische Inferenzen parallel betrieben werden, wo bei der einen die Behauptung, bei der anderen das Gegenteil der Behauptung angenommen wird, lässt sich ein Beweis in endlicher Zeit führen, denn eines der beiden Verfahren terminiert immer in endlicher Zeit.
Verfahren
(TODO: das alles an einem mittleren Beispiel: Eingabe des Algorithmus (Menge von PL-Aussagen, die semantisch UND-Verknüpft sind, da sie alle gelten sollen); Quantoren nach außen, Pränex-Normalform; konjunktive Normalform der Matrix; Skolemform; Klauselform; Resolution, eventuell Widerspruch)