Gibt es Software zur automatischen Validierung eines Arguments?
ich möchte gerne
- Leiten Sie logische Argumente aus dem Englischen ab und
- Testen Sie ihre Gültigkeit mit einem Programm.
Gibt es Software für Schritt 2? Es wäre in Ordnung, wenn es aufgeben würde, weil
- Die Gültigkeit ist nicht berechenbar, oder
- Es würde zu lange dauern, ein Ergebnis zu melden.
Mir ist klar, dass das Stellen dieser Frage meine Unkenntnis über Logik offenbaren kann. Wenn es also eine dumme Frage ist, wäre ich dankbar für einige Referenzen, die erklären, warum das so ist. Ich werde mit Metalogic beginnen: Eine Einführung in die Metatheorie der Standard First Order .
Antworten
Sie suchen einen sogenannten automatisierten Theorembeweiser .
Siehe z. B. pyPL oder Tree Proof Generator für zwei Implementierungen des Kalküls der analytischen Tableaus für die klassische Aussagenlogik und Logik erster Ordnung.
Der Tableau-Kalkül ist für die Gültigkeit erster Ordnung vollständig, was bedeutet, dass jede gültige Folgerung als solche erkannt wird.
Die Logik erster Ordnung ist jedoch nicht halbentscheidbar, was bedeutet, dass es unmöglich ist, einen Algorithmus zu finden, der alle Nicht-Schlussfolgerungen als solche erkennt. Bei einigen ungültigen Schlussfolgerungen wird der Tableau-Algorithmus ins Unendliche laufen.
Die Aussagenlogik ist dagegen völlig entscheidbar; Der Tableau-Algorithmus erkennt schließlich alle gültigen und alle ungültigen Aussagenargumente als solche.
Es bestehen auch Komplexitätsbeschränkungen; Tableau-Bäume sind besonders anfällig für kombinatorische Explosionen, wenn keine ausgeklügelten Heuristiken implementiert werden. Daher funktionieren die beiden oben genannten Programme nur für vergleichsweise einfache Argumente realistisch.
Es wurden auch viele andere Beweissysteme implementiert. Wikipedia listet eine Reihe auf, aber ich habe selbst mit keinem von ihnen gearbeitet, daher müssen Sie prüfen, welche für nicht akademische und nicht industrielle Anwendungsfälle geeignet sind.