Pokazaliśmy, w jaki sposób logika pierwszego rzędu może reprezentować prosty scenariusz ze świata rzeczywistego, obejmujący takie pojęcia, jak sprzedaż, broń i obywatelstwo. Ale złożone scenariusze rzeczywistego świata mają zbyt wiele niepewności i zbyt wiele niewiadomych. Logika okazała się bardziej skuteczna w scenariuszach obejmujących formalne, ściśle określone koncepcje, takie jak synteza i weryfikacja zarówno sprzętu, jak i oprogramowania. Badania dowodzące twierdzeń są prowadzone w dziedzinie projektowania sprzętu, języków programowania i inżynierii oprogramowania – nie tylko w sztucznej inteligencji. W przypadku sprzętu aksjomaty opisują interakcje między sygnałami a elementami obwodu. Logiczne wnioskowania zaprojektowane specjalnie do weryfikacji były w stanie zweryfikować całe procesory, w tym ich właściwości czasowe. Dowód twierdzenia AURA został zastosowany do projektowania obwodów, które są bardziej zwarte niż jakikolwiek inny projekt . W przypadku oprogramowania wnioskowanie o programach jest dość podobne do wnioskowania o akcjach: aksjomaty opisują warunki wstępne i skutki każdej instrukcji. Formalna synteza algorytmów była jednym z pierwszych zastosowań dowodzenia twierdzeń, jak nakreślił to Cordell Green , który oparł się na wcześniejszych pomysłach Herberta Simona . Chodzi o to, aby konstruktywnie udowodnić twierdzenie, że „istnieje program spełniający określoną specyfikację”. Chociaż w pełni zautomatyzowana synteza dedukcyjna, jak się ją nazywa, nie stała się jeszcze możliwa do zastosowania w programowaniu ogólnego przeznaczenia, ręcznie sterowana synteza dedukcyjna odniosła sukces w projektowaniu kilku nowatorskich i zaawansowanych algorytmów. Aktywnym obszarem badań jest również synteza programów celowych, takich jak naukowy kod obliczeniowy. Podobne techniki są obecnie stosowane do weryfikacji oprogramowania przez systemy takie jak kontroler modeli SPIN . Na przykład program kontroli statku kosmicznego Remote Agent został zweryfikowany przed lotem i po nim .Klucz publiczny RSA, algorytm szyfrowania i algorytm dopasowywania ciągów Boyer-Moore zostały zweryfikowane w ten sposób .
Streszczenie
Przedstawiliśmy analizę wnioskowania logicznego w logice pierwszego rzędu oraz szereg algorytmów do tego.
* Pierwsze podejście wykorzystuje reguły wnioskowania (instancja uniwersalna i egzystencjalna) w celu przedstawienia problemu wnioskowania. Zazwyczaj to podejście jest powolne, chyba że domena jest mała.
* Użycie unifikacji do identyfikacji odpowiednich podstawień dla zmiennych eliminuje etap tworzenia instancji w dowodach pierwszego rzędu, czyniąc proces bardziej wydajnym w wielu przypadkach.
* Podniesiona wersja Modus Ponens wykorzystuje unifikację, aby zapewnić naturalną i potężną regułę wnioskowania, uogólnioną Modus Ponens. Algorytmy tworzenia łańcuchów w przód i w tył stosują tę zasadę do zestawów klauzul określonych.
* Uogólniony Modus Ponens jest kompletny dla zdań określonych, chociaż problem implikacji jest częściowo rozstrzygalny. W przypadku baz wiedzy Datalog składających się z niefunkcjonalnych klauzul określonych, rozstrzygnięcie jest możliwe.
* Łańcuchy do przodu są używane w dedukcyjnych bazach danych, gdzie można je łączyć z operacjami na relacyjnych bazach danych. Jest również używany w systemach produkcyjnych, które wykonują wydajne aktualizacje z bardzo dużymi zestawami reguł. Tworzenie łańcucha w przód jest zakończone dla Datalog i działa w czasie wielomianowym.
* Łańcuchy wsteczne są używane w systemach programowania logicznego, które wykorzystują zaawansowaną technologię kompilatora, aby zapewnić bardzo szybkie wnioskowanie. Łańcuchy wsteczne cierpią z powodu nadmiarowych wnioskowań i nieskończonych pętli; można je złagodzić poprzez zapamiętywanie.
* Prolog, w przeciwieństwie do logiki pierwszego rzędu, używa zamkniętego świata z założeniem unikalnych nazw i negacją jako porażką. Dzięki temu Prolog jest bardziej praktycznym językiem programowania, ale oddala go od czystej logiki.
* Uogólniona reguła wnioskowania o rozdzielczości zapewnia kompletny system dowodowy dla logiki pierwszego rzędu, wykorzystujący bazy wiedzy w spójnej postaci normalnej.
* Istnieje kilka strategii zmniejszania przestrzeni wyszukiwania w systemie rozdzielczości bez narażania kompletności. Jedną z najważniejszych kwestii jest zajmowanie się równością; pokazaliśmy, jak można zastosować demodulację i paramodulację.
* Wydajne dowodzenie twierdzeń oparte na rozdzielczości zostało użyte do udowodnienia interesujących twierdzeń matematycznych oraz do weryfikacji i syntezy oprogramowania i sprzętu.