Czy istnieje oprogramowanie do automatycznego weryfikowania argumentów?

Question

Chciałbym

1. Wyprowadź logiczne argumenty z języka angielskiego i
2. sprawdzić ich ważność za pomocą programu.

Czy istnieje oprogramowanie dla kroku 2? Byłoby dobrze, gdyby się poddał, ponieważ

1. Ważność nie jest obliczalna lub
2. zgłoszenie wyniku zajęłoby zbyt dużo czasu.

Zdaję sobie sprawę, że zadanie tego pytania może ujawnić moją nieznajomość logiki, więc jeśli jest to głupie pytanie, byłbym wdzięczny za pewne odniesienia, które wyjaśniają, dlaczego tak jest. Zacznę od Metalogic: An Introduction to the Metatheory of Standard First Order .

Answer 1

Szukasz tak zwanego automatycznego dowodu twierdzenia .

Zobacz np. PyPL lub Tree Proof Generator dla dwóch implementacji rachunku analitycznego tablic dla klasycznej logiki zdaniowej i pierwszego rzędu.

Rachunek tablicowy jest kompletny dla ważności pierwszego rzędu, co oznacza, że ​​każde prawidłowe wnioskowanie zostanie wykryte jako takie.
Ale logika pierwszego rzędu nie jest współrozstrzygalna, co oznacza, że ​​niemożliwe jest znalezienie algorytmu, który wykryje wszystkie nie-wnioskowania jako takie; na niektórych błędnych wnioskach algorytm tableau dojdzie do nieskończoności.
Z drugiej strony, logika zdań jest w pełni rozstrzygalna; algorytm tableau ostatecznie wykryje wszystkie prawidłowe i wszystkie niepoprawne argumenty propozycji jako takie.

Istnieją również ograniczenia dotyczące złożoności; Drzewa tabeli są szczególnie podatne na eksplozję kombinatoryczną, chyba że zaimplementowano wyrafinowaną heurystykę, więc powyższe dwa programy będą działać realistycznie tylko dla stosunkowo prostych argumentów.

Wdrożono również wiele innych systemów dowodowych. Wikipedia podaje kilka przykładów, ale sam z żadnym z nich nie pracowałem, więc musisz sprawdzić, które z nich nadają się do zastosowań pozaakademickich i nieprzemysłowych.