Dlaczego niektóre silniki wnioskowania potrzebują ludzkiej pomocy, a inne nie?

^{Uczę się samodzielnie Automated Theorem Proving / Solver SMT / Proof Assistants i zamieszczam serię pytań na temat tego procesu, zaczynając tutaj .}

Dlaczego automatyczne dowodzenia twierdzeń, tj. ACL2 i solwery SMT, nie potrzebują ludzkiej pomocy, podczas gdy asystenci dowodzenia, tj. Isabelle i Coq , tak?

^{Znajdź następne pytanie z serii tutaj .}

Ważność formuł wyższego rzędu zasadniczo nie jest rozstrzygalna, a przestrzenie wyszukiwania są ogromne , więc wszystko, co możesz zrobić, to spróbować znaleźć dowód - zakładając, że istnieje - poprzez sprytne wyliczenie przestrzeni dowodu (pomyśl młot , trafnie nazwany) ale to jest szorstkie. Ludzie mogą grać w wyrocznię, dostarczając kluczowych lematów do poprowadzenia dowodu.

Z drugiej strony, zautomatyzowane dowody zwykle zajmują się tylko rozstrzygającymi (podzbiorami) logikami, na przykład logiką zdań lub podklasami logiki pierwszego rzędu, więc mogą działać długo, ale wiesz, że ostatecznie się uda.

Zauważ, że istnieją podejścia umożliwiające asystentom dowodu znalezienie tych ważnych lematów, np . IsaPlanner . Narzędzie zgaduje (indukcyjne) lematy poprzez wyliczenie i losowe testy, a następnie próbuje je udowodnić. Poprzez iterację procesu wiele lematów np. Typowych definicji typów danych można znaleźć automatycznie.

Małe ABC

• validity - formuła jest poprawna i zawiera wszystko, co przypisujesz wolnym zmiennym.
• zmienne swobodne - te zmienne, które nie są powiązane kwantyfikatorami, takimi jak i$\forall$$\exists$
• decidability - właściwość (boolowska) jest (Turinga) rozstrzygalna, jeśli istnieje algorytm, który odpowiada „tak” lub „nie” (poprawnie) po skończonym czasie.
• logika zdań - także logika zerowego rzędu ; niedozwolone jest określenie ilościowe.
• $\forall x. P(x)$$\forall f. f(4) > 0$
• logika wyższego rzędu - można kwantyfikować (i „budować”) dowolnie złożone obiekty, np. funkcje wyższego rzędu (funkcje przyjmujące funkcje).

Powiedziałbym, że klasyczne rozróżnienie między „automatycznym dowodzeniem twierdzeń” (ATP) a „interaktywnym dowodzeniem twierdzeń” (ITP) wymaga ponownego rozważenia. Jeśli weźmiesz dziś dobrze znany system ITP, taki jak Isabelle / HOL (Isabelle2013 od lutego 2013 r.), Integruje on całkiem sporo narzędzi dodatkowych z portfolio ATP:

• Ogólne, zautomatyzowane narzędzia sprawdzające na pokładzie: oldschoolowe narzędzia Isabelle, takie jak fasti blast(autor: L. Paulson) i nowsze automatyczne automaty, takie jak metis(autor: J. Hurd).

• Zewnętrzne ATP dla logiki pierwszego rzędu, które są wywoływane przez Sledgehammer: E prover, SPASS, Vampire. Znaleziony dowód jest analizowany, aby dowiedzieć się, które lematy przyczyniły się do tego, zmniejszając 10000 do 10 sekund i karmiąc wynik metis.

• Zewnętrzne SMT z częściową rekonstrukcją dowodu, szczególnie dla Z3 (autor: S. Boehme).

• Narzędzia do znajdowania przeciwnych przykładów niepotwierdzonych stwierdzeń: Nitpick / Kodkodi (J. Blanchette) i Quickcheck (L. Bulwahn).

Czy wszystkie te zautomatyzowane rzeczy sprawiają, że Isabelle jest automatyczną powieścią do twierdzeń?

Ostatecznie myślę, że rozróżnienie „ATP” vs. „ITP” to po prostu pewnego rodzaju „etykieta”, która mówi, jak chcesz pozycjonować lub „sprzedawać” swój system: ATP twierdzą, że są „narzędziami naciskanymi”, ale w ćwiczyć będziesz musiał wchodzić w interakcje (pośrednio), podając parametry lub wskazówki lub przeformułowując swój problem. To może być naprawdę trudne, ze względu na długie środowiska uruchomieniowe, które są powszechne w społeczności ATP.

Natomiast system ITP jest stworzony dla osób czekających na miejscu, z pół przyzwoitym dostępem do wewnętrznych stanów dowodu, aby zobaczyć, czego brakuje, aby ukończyć dowód. System ITP, który zamyka narzędzia ATP w sposób podobny do Isabelle, może okazać się bardziej atrakcyjny dla większej liczby użytkowników i większej liczby aplikacji niż sam ITP lub ATP.