Istnieje wiele innych metod, które mają większą wydajność i generują bardziej czytelne dowody. Do najprostszych z nich należą sekwenty Gentzena, systemy Hilberta oraz dedukcja naturalna. W praktyce używa się zwykle metod bazowanych na procedurze Davisa-Putnama. Można też używać uproszczonych wersji metod dla rachunku predykatów pierwszego rzędu.
Problem spełnialności jest jednak w każdym systemie NP zupełny, zaś problem tautologii – CoNP zupełny.
Automatyczne dowodzenie twierdzeń rachunku predykatów Dominujące metody to tableau, a przede wszystkim różne wersje rezolucji. W systemach z równością używa się też paramodulacji. Warto zaznaczyć, że "ogólny" język I rzędu jest nierozstrzygalny. W szczególności nie istnieje algorytm, który dla ogólnego języka I rzędu może określić, czy dane zdanie jest w nim prawdziwe, czy nie. Istnieją jednak "szczególne" języki I rzędu, które są rozstrzygalne. Przykładem rozstrzygalnego języka I rzędu może być arytmetyka liczb rzeczywistych, co udowodnił Alfred Tarski. Do weryfikacji zdań o liczbach rzeczywistych służy metoda eliminacji kwantyfikatorów.
Zobacz też rachunek lambda CADE CASC subsumpcja unifikacja term indeksowanie termów system wspomagający dowodzenie twierdzeń system Mizar
Przypisy
Linki zewnętrzne