Zautomatyzowane dowodzenie twierdzeń

Zautomatyzowane dowodzenie twierdzeń (znane również jako ATP lub zautomatyzowane odliczenie ) jest poddziedziną zautomatyzowanego wnioskowania i logiki matematycznej zajmującej się dowodzeniem twierdzeń matematycznych za pomocą programów komputerowych . Zautomatyzowane wnioskowanie na podstawie dowodu matematycznego było głównym bodźcem do rozwoju informatyki .

Podstawy logiczne

Podczas gdy korzenie logiki sformalizowanej sięgają Arystotelesa , koniec XIX i początek XX wieku przyniósł rozwój nowoczesnej logiki i sformalizowanej matematyki. Frege 's Begriffsschrift (1879) wprowadził zarówno kompletny rachunek zdań , jak i to, co jest zasadniczo nowoczesną logiką predykatów . Jego Podstawy arytmetyki , opublikowane w 1884 r., wyrażały (części) matematyki w logice formalnej. Podejście to było kontynuowane przez Russella i Whiteheada w ich wpływowych Principia Mathematica , opublikowanych po raz pierwszy w latach 1910–1913, oraz w poprawionym drugim wydaniu w 1927 r. Russell i Whitehead myśleli, że mogą wyprowadzić całą matematyczną prawdę za pomocą aksjomatów i reguł wnioskowania logiki formalnej, w zasadzie otwarcie procesu na automatyzację. W 1920 roku Thoralf Skolem uprościł poprzedni wynik Leopolda Löwenheima , prowadząc do twierdzenia Löwenheima-Skolema , aw 1930 roku do pojęcia wszechświata Herbranda i interpretacji Herbranda , która dopuszczała (nie) spełnialność formuł pierwszego rzędu (a zatem ważność twierdzenia) do (potencjalnie nieskończenie wielu) propozycjonalnych problemów spełnialności .

W 1929 roku Mojżesz Presburger wykazał, że teoria liczb naturalnych z dodawaniem i równością (nazywana obecnie na jego cześć arytmetyką Presburgera ) jest rozstrzygalna i podał algorytm, który mógł rozstrzygnąć, czy dane zdanie w języku jest prawdziwe, czy fałszywe. Jednak wkrótce po tym pozytywnym wyniku Kurt Gödel opublikował O formalnie nierozstrzygalnych twierdzeniach Principia Mathematica i systemów pokrewnych (1931), pokazując, że w każdym wystarczająco silnym systemie aksjomatycznym istnieją zdania prawdziwe, których nie można udowodnić w systemie. Temat ten został rozwinięty w latach trzydziestych XX wieku przez Alonzo Churcha i Alana Turinga , którzy z jednej strony podali dwie niezależne, ale równoważne definicje obliczalności , az drugiej strony podali konkretne przykłady pytań nierozstrzygalnych.

Pierwsze wdrożenia

Wkrótce po drugiej wojnie światowej pojawiły się pierwsze komputery ogólnego przeznaczenia. W 1954 roku Martin Davis zaprogramował algorytm Presburgera dla komputera lampowego JOHNNIAC w Institute for Advanced Study w Princeton, New Jersey. Według Davisa „jego wielkim triumfem było udowodnienie, że suma dwóch liczb parzystych jest parzysta”. Bardziej ambitna była maszyna teorii logiki z 1956 r., system dedukcji dla logiki zdań Principia Mathematica , opracowany przez Allena Newella , Herberta A. Simona i JC Shawa . Działająca również na JOHNNIAC, Maszyna Teorii Logiki skonstruowała dowody na podstawie małego zestawu aksjomatów zdań i trzech reguł dedukcji: modus ponens , (zdaniowe) podstawienie zmiennej i zastąpienie formuł przez ich definicję. System wykorzystywał wskazówki heurystyczne i zdołał udowodnić 38 z pierwszych 52 twierdzeń Principia .

Podejście „heurystyczne” Maszyny Teorii Logiki próbowało naśladować ludzkich matematyków i nie mogło zagwarantować, że można znaleźć dowód dla każdego ważnego twierdzenia, nawet w zasadzie. W przeciwieństwie do tego inne, bardziej systematyczne algorytmy osiągnęły, przynajmniej teoretycznie, kompletność logiki pierwszego rzędu. Początkowe podejścia opierały się na wynikach Herbranda i Skolema w celu przekształcenia formuły pierwszego rzędu w kolejno większe zestawy formuł zdań poprzez tworzenie instancji zmiennych z terminami ze wszechświata Herbranda . Formuły zdaniowe można następnie sprawdzić pod kątem niespełnialności za pomocą szeregu metod. Program Gilmore'a wykorzystywał konwersję do dysjunktywnej postaci normalnej , postaci, w której spełnialność formuły jest oczywista.

Rozstrzygalność problemu

W zależności od leżącej u podstaw logiki problem decydowania o ważności formuły waha się od trywialnego do niemożliwego. W częstym przypadku logiki zdań problem jest rozstrzygalny, ale współ-NP-zupełny , a zatem uważa się, że istnieją tylko algorytmy czasu wykładniczego dla ogólnych zadań dowodowych. W przypadku rachunku predykatów pierwszego rzędu twierdzenie Gödla o kompletności stwierdza , że ​​twierdzenia (twierdzenia możliwe do udowodnienia) są dokładnie poprawnymi logicznie, dobrze sformułowanymi formułami , więc identyfikacja prawidłowych formuł jest rekurencyjnie wyliczalna : przy nieograniczonych zasobach można ostatecznie udowodnić każdą prawidłową formułę. Jednak nieważne formuły (te, które nie wynikają z danej teorii) nie zawsze mogą zostać rozpoznane.

Powyższe odnosi się do teorii pierwszego rzędu, takich jak arytmetyka Peano . Jednak w przypadku konkretnego modelu, który można opisać teorią pierwszego rzędu, niektóre stwierdzenia mogą być prawdziwe, ale nierozstrzygalne w teorii użytej do opisu modelu. Na przykład z twierdzenia Gödla o niezupełności wiemy, że żadna teoria, której aksjomaty właściwe są prawdziwe dla liczb naturalnych, nie może udowodnić, że wszystkie zdania pierwszego rzędu są prawdziwe dla liczb naturalnych, nawet jeśli lista aksjomatów właściwych może być nieskończenie przeliczalna. Wynika z tego, że automatyczny dowódca twierdzeń nie zakończy poszukiwania dowodu dokładnie wtedy, gdy badane stwierdzenie jest nierozstrzygalne w stosowanej teorii, nawet jeśli jest prawdziwe w interesującym nas modelu. Pomimo tego teoretycznego ograniczenia, w praktyce dowodzący twierdzeniami mogą rozwiązać wiele trudnych problemów, nawet w modelach, które nie są w pełni opisane przez żadną teorię pierwszego rzędu (takich jak liczby całkowite).

Powiązane problemy

Prostszym, ale powiązanym problemem jest weryfikacja dowodu , w przypadku której istniejący dowód twierdzenia jest poświadczony jako ważny. W tym celu ogólnie wymaga się, aby każdy indywidualny krok dowodu mógł zostać zweryfikowany przez prymitywną funkcję lub program rekurencyjny, a zatem problem jest zawsze rozstrzygalny.

Ponieważ dowody generowane przez zautomatyzowane programy dowodzenia twierdzeń są zazwyczaj bardzo duże, problem kompresji dowodu jest kluczowy i opracowano różne techniki mające na celu zmniejszenie wyniku dowodzenia, a co za tym idzie, łatwiejszego zrozumienia i sprawdzenia.

Asystenci sprawdzający wymagają, aby użytkownik dawał wskazówki systemowi. W zależności od stopnia automatyzacji, program dowodowy można zasadniczo zredukować do kontrolera dowodu, w którym użytkownik dostarcza dowód w sposób formalny lub istotne zadania dowodowe mogą być wykonywane automatycznie. Interaktywne dowody są wykorzystywane do różnych zadań, ale nawet w pełni automatyczne systemy udowodniły wiele interesujących i trudnych twierdzeń, w tym przynajmniej jedno, które przez długi czas wymykało się ludzkim matematykom, a mianowicie hipotezę Robbinsa . Sukcesy te są jednak sporadyczne, a praca nad trudnymi problemami zwykle wymaga biegłego użytkownika.

Czasami dokonuje się innego rozróżnienia między dowodzeniem twierdzeń a innymi technikami, w których proces jest uważany za dowodzenie twierdzeń, jeśli składa się z tradycyjnego dowodu, zaczynając od aksjomatów i tworząc nowe kroki wnioskowania przy użyciu reguł wnioskowania. Inne techniki obejmowałyby sprawdzanie modelu , które w najprostszym przypadku polega na brutalnym wyliczeniu wielu możliwych stanów (chociaż faktyczna implementacja kontrolerów modeli wymaga dużo sprytu i nie sprowadza się po prostu do brutalnej siły).

Istnieją hybrydowe systemy dowodzenia twierdzeń, które wykorzystują sprawdzanie modelu jako regułę wnioskowania. Istnieją również programy, które zostały napisane w celu udowodnienia określonego twierdzenia, z (zwykle nieformalnym) dowodem, że jeśli program zakończy się pewnym wynikiem, to twierdzenie jest prawdziwe. Dobrym tego przykładem był wspomagany maszynowo dowód twierdzenia o czterech kolorach , który był bardzo kontrowersyjny, ponieważ pierwszy twierdził, że dowód matematyczny był zasadniczo niemożliwy do zweryfikowania przez ludzi ze względu na ogromny rozmiar obliczeń programu (takie dowody nazywane są nie -sprawdzalne dowody ). Innym przykładem dowodu wspomaganego przez program jest ten, który pokazuje, że grę w Connect Four zawsze może wygrać pierwszy gracz.

Zastosowania przemysłowe

Komercyjne wykorzystanie zautomatyzowanego dowodzenia twierdzeń koncentruje się głównie na projektowaniu i weryfikacji układów scalonych . Od czasu błędu Pentium FDIV skomplikowane jednostki zmiennoprzecinkowe nowoczesnych mikroprocesorów zostały zaprojektowane z dodatkową uwagą. AMD , Intel i inne firmy używają zautomatyzowanego dowodzenia twierdzeń, aby sprawdzić, czy dzielenie i inne operacje są poprawnie realizowane w ich procesorach.

Dowód twierdzenia pierwszego rzędu

Pod koniec lat 60. agencje finansujące badania nad zautomatyzowaną dedukcją zaczęły podkreślać potrzebę praktycznych zastosowań. Jednym z pierwszych owocnych obszarów była weryfikacja programów , w ramach której do sprawdzania poprawności programów komputerowych w językach takich jak Pascal, Ada itp. stosowano dowodzenie twierdzeń pierwszego rzędu. Wśród wczesnych systemów weryfikacji programów wyróżniał się Stanford Pascal Verifier opracowany przez Davida Luckhama z Uniwersytetu Stanforda . Zostało to oparte na Stanford Resolution Prover, również opracowanym w Stanford przy użyciu rozdzielczości Johna Alana Robinsona . Był to pierwszy zautomatyzowany system dedukcji, który wykazał zdolność rozwiązywania problemów matematycznych, które zostały ogłoszone w Zawiadomieniach Amerykańskiego Towarzystwa Matematycznego przed formalną publikacją rozwiązań. [ potrzebne źródło ]

pierwszego rzędu jest jedną z najbardziej dojrzałych dziedzin zautomatyzowanego dowodzenia twierdzeń. Logika jest wystarczająco wyrazista, aby umożliwić specyfikację dowolnych problemów, często w dość naturalny i intuicyjny sposób. Z drugiej strony, nadal jest częściowo rozstrzygalny i opracowano szereg solidnych i kompletnych rachunków, umożliwiających w pełni zautomatyzowane systemy. Logiki bardziej ekspresyjne, takie jak logiki wyższego rzędu , umożliwiają wygodne wyrażanie szerszego zakresu problemów niż logika pierwszego rzędu, ale dowodzenie twierdzeń dla tych logik jest mniej rozwinięte.

Benchmarki, konkursy i źródła

Na jakość wdrożonych systemów wpłynęła duża biblioteka standardowych przykładów wzorcowych — Biblioteka Problemów Tysiąca Problemów dla Dowódców Twierdzeń (TPTP) — jak również CADE ATP System Competition (CASC), doroczny konkurs pierwszych -systemy rzędu dla wielu ważnych klas problemów pierwszego rzędu.

Niektóre ważne systemy (wszystkie wygrały co najmniej jedną dywizję konkursową CASC) są wymienione poniżej.

Theorem Prover Museum to inicjatywa mająca na celu zachowanie źródeł systemów dowodzenia twierdzeń do przyszłych analiz, ponieważ są one ważnymi artefaktami kulturowymi / naukowymi. Ma źródła wielu z wyżej wymienionych systemów.

Popularne techniki

Systemy oprogramowania

Zobacz także: Asystent dowodu § Porównanie i Kategoria: Systemy oprogramowania do sprawdzania twierdzeń
Porównanie
Nazwa Rodzaj licencji Serwis internetowy Biblioteka Samodzielny Ostatnia aktualizacja ( format RRRR-mm-dd )
ACL2 3-klauzulowe BSD NIE NIE Tak maj 2019 r
Prover9/Wydra Domena publiczna Przez system na TPTP Tak NIE 2009
Żart GPLv2 Tak Tak NIE 15 maja 2015 r
PVS GPLv2 NIE Tak NIE 14 stycznia 2013 r
Leon II Licencja BSD Przez system na TPTP Tak Tak 2013
EQP ? NIE Tak NIE maj 2009
SMUTNY GPLv3 Tak Tak NIE 27 sierpnia 2008
PhoX ? NIE Tak NIE 28 września 2017 r
KeYmaera GPL Przez Java Webstart Tak Tak 11 marca 2015 r
Gandalfa ? NIE Tak NIE 2009
mi GPL Przez system na TPTP NIE Tak 4 lipca 2017 r
SNARK Licencja publiczna Mozilli 1.1 NIE Tak NIE 2012
Wampir Licencja wampira Przez system na TPTP Tak Tak 14 grudnia 2017 r
System dowodzenia twierdzeń (TPS) Umowa dystrybucyjna TPS NIE Tak NIE 4 lutego 2012 r
SPAS Licencja FreeBSD Tak Tak Tak listopad 2005
IsaPlanner GPL NIE Tak Tak 2007
Klucz GPL Tak Tak Tak 11 października 2017 r
Księżniczka lgpl v2.1 Poprzez Java Webstart i System na TPTP Tak Tak 27 stycznia 2018 r
iProver GPL Przez system na TPTP NIE Tak 2018
Twierdzenie meta Darmowe NIE NIE Tak lipiec 2022 r
Dowód twierdzenia Z3 Licencja MIT Tak Tak Tak 19 listopada 2019 r

Darmowe oprogramowanie

Własne oprogramowanie

  • Acumen RuleManager (produkt komercyjny)
  • ALIGATOR (CC BY-NC-SA 2.0 UK)
  • KARINA
  • KIV (dostępny bezpłatnie jako wtyczka do Eclipse )
  • Prover Plug-In (komercyjny produkt silnikowy)
  • ProverBox
  • Wolfram Mathematica
  • BadaniaCyc
  • Spear modularny dowód twierdzeń arytmetycznych

Zobacz też

Notatki

Linki zewnętrzne

Pobrano z „ https://en.wikipedia.org/w/index.php?title=Automated_theorem_proving&oldid=1136357083 ”