Inżynieria ontologiczna

W domenach „zabawkowych” wybór reprezentacji nie jest tak ważny; wiele opcji będzie działać. Złożone domeny, takie jak zakupy w Internecie czy jazda samochodem w ruchu, wymagają bardziej ogólnych i elastycznych reprezentacji. Ten rozdział pokazuje, jak tworzyć te reprezentacje, koncentrując się na ogólnych pojęciach — takich jak zdarzenia, czas, obiekty fizyczne i przekonania — które występują w wielu różnych dziedzinach. Reprezentowanie tych abstrakcyjnych pojęć jest czasami nazywane inżynierią ontologiczną. Nie możemy mieć nadziei, że przedstawimy wszystko na świecie, nawet 1000-stronicowy podręcznik, ale zostawimy miejsca, w których zmieści się nowa wiedza dla dowolnej domeny. Na przykład określimy, co to znaczy być fizycznym obiektem, a szczegóły różnych typów obiektów — robotów, telewizorów, książek lub czegokolwiek — można później wypełnić. Jest to analogiczne do sposobu, w jaki projektanci struktur programistycznych zorientowanych obiektowo (takich jak środowisko graficzne Java Swing) definiują ogólne koncepcje, takie jak Window, oczekując, że użytkownicy będą używać ich do definiowania bardziej szczegółowych pojęć, takich jak SpreadsheetWindow. Ogólna struktura pojęć nazywana jest wyższą ontologią ze względu na konwencję rysowania grafów z pojęciami ogólnymi na górze i pojęciami bardziej szczegółowymi pod nimi, jak na rysunku

Zanim dalej zajmiemy się ontologią, powinniśmy podać jedno ważne zastrzeżenie. Zdecydowaliśmy się użyć logiki pierwszego rzędu do omawiania zawartości i organizacji wiedzy, chociaż niektóre aspekty realnego świata są trudne do uchwycenia w FOL. Główna trudność polega na tym, że większość uogólnień ma wyjątki lub obowiązuje tylko do pewnego stopnia. Na przykład, chociaż „pomidory są czerwone” jest użyteczną zasadą, niektóre pomidory są zielone, żółte lub pomarańczowe. Podobne wyjątki można znaleźć w prawie wszystkich regułach w tym rozdziale. Umiejętność radzenia sobie z wyjątkami i niepewnością jest niezwykle ważna, ale jest ortogonalna do zadania polegającego na zrozumieniu ogólnej ontologii. Jaki jest pożytek z wyższej ontologii? Rozważ ontologię obwodów. Zawiera wiele upraszczających założeń: całkowicie pomija się czas; sygnały są stałe i nie rozchodzą się; struktura obwodu pozostaje stała. Bardziej ogólna ontologia uwzględniałaby sygnały w określonych momentach i obejmowałaby długości przewodów i opóźnienia propagacji. To pozwoliłoby nam symulować właściwości czasowe obwodu i rzeczywiście takie symulacje są często przeprowadzane przez projektantów obwodów. Moglibyśmy również wprowadzić ciekawsze klasy bramek, na przykład opisując technologię (TTL, CMOS itd.) oraz specyfikację wejścia-wyjścia. Gdybyśmy chcieli omówić niezawodność lub diagnozę, uwzględnilibyśmy możliwość spontanicznej zmiany struktury obwodu lub właściwości bramek. Aby uwzględnić rozproszenie pojemności, musielibyśmy przedstawić, gdzie znajdują się przewody na płytce. Jeśli spojrzymy na świat wumpusów, mamy do czynienia z podobnymi rozważaniami. Chociaż reprezentujemy czas, ma on prostą strukturę: nic się nie dzieje poza momentami działania agenta, a wszystkie zmiany są natychmiastowe. Bardziej ogólna ontologia, lepiej dopasowana do świata rzeczywistego, pozwoliłaby na jednoczesne zmiany rozciągnięte w czasie. Użyliśmy również predykatu zagłębienia, aby powiedzieć, które kwadraty mają zagłębienia. Mogliśmy pozwolić na różne rodzaje dołów, mając kilka osobników należących do klasy dołów, z których każdy ma inne właściwości. Podobnie możemy chcieć pozwolić na inne zwierzęta oprócz wumpusów. Być może nie da się określić dokładnego gatunku na podstawie dostępnych spostrzeżeń, więc musielibyśmy stworzyć biologiczną taksonomię, aby pomóc agentowi przewidzieć zachowanie mieszkańców jaskini na podstawie skąpych wskazówek. W przypadku każdej ontologii specjalnego przeznaczenia możliwe jest dokonanie takich zmian, aby przejść w kierunku większej ogólności. Powstaje wtedy oczywiste pytanie: czy wszystkie te ontologie zbiegają się w ontologii ogólnego przeznaczenia? Po wiekach filozoficznych i obliczeniowych dociekań odpowiedź brzmi „może”. W tej części przedstawiamy jedną ontologię ogólnego przeznaczenia, która łączy idee z tamtych wieków. Dwie główne cechy ontologii ogólnego przeznaczenia odróżniają je od zbiorów ontologii specjalnego przeznaczenia:

* Ontologia ogólnego przeznaczenia powinna mieć zastosowanie w mniej więcej dowolnej domenie specjalnego przeznaczenia (z dodatkiem aksjomatów dziedzinowych). Oznacza to, że żaden problem reprezentacyjny nie może być finezyjny ani zamiatany pod dywan.

* W każdej wystarczająco wymagającej dziedzinie różne obszary wiedzy muszą być ujednolicone, ponieważ rozumowanie i rozwiązywanie problemów może obejmować kilka obszarów jednocześnie. Na przykład system naprawy obwodów robota musi analizować obwody pod kątem połączeń elektrycznych i układu fizycznego oraz czasu, zarówno w celu analizy synchronizacji obwodów, jak i szacowania pracy, którą można połączyć z tymi, które opisują układ przestrzenny i muszą działać równie dobrze dla nanosekund i minut oraz dla angstremów i metrów.

Powinniśmy z góry powiedzieć, że przedsięwzięcie ogólnej inżynierii ontologicznej odniosło jak dotąd jedynie ograniczony sukces. Żadna z najlepszych aplikacji AI  nie korzysta z ogólnej ontologii – wszystkie wykorzystują inżynierię wiedzy specjalnego przeznaczenia i maszynę uczenia się. Względy społeczne/polityczne mogą utrudnić konkurującym stronom uzgodnienie ontologii. Jak mówi Tom Gruber : „Każda ontologia jest traktatem – umową społeczną – pomiędzy ludźmi, dla których istnieje jakiś wspólny motyw dzielenia się”. Kiedy rywalizujące obawy przeważają nad motywacją do dzielenia się, nie może być wspólnej ontologii. Im mniejsza liczba interesariuszy, tym łatwiej jest stworzyć ontologię, a co za tym idzie trudniej stworzyć ontologię ogólnego przeznaczenia niż taką o ograniczonym przeznaczeniu, taką jak Open Biomedical Ontology (Smith i in., 2007). Te ontologie, które istnieją, zostały stworzone czterema ścieżkami:

  1. Przez zespół przeszkolonych ontologów lub logików, którzy projektują ontologię i piszą aksjomaty. System CYC był w większości zbudowany w ten sposób.
  2. Importując kategorie, atrybuty i wartości z istniejącej bazy danych lub baz danych. DBPEDIA została zbudowana poprzez import ustrukturyzowanych faktów z Wikipedii.
  3. Analizując dokumenty tekstowe i wydobywając z nich informacje. TEXTRUNNER został zbudowany poprzez czytanie dużego zbioru stron internetowych.
  4. Zachęcając niewykwalifikowanych amatorów do wchodzenia w wiedzę zdroworozsądkową. System OPENMIND został zbudowany przez wolontariuszy, którzy przedstawiali fakty w języku angielskim.

Na przykład w Grafie wiedzy Google wykorzystano częściowo ustrukturyzowaną treść z Wikipedii, łącząc ją z innymi treściami zebranymi z całej sieci pod nadzorem człowieka. Zawiera ponad 70 miliardów faktów i dostarcza odpowiedzi na około jedną trzecią wyszukiwań w Google

Reprezentacja wiedzy

Wcześniej pokazano, w jaki sposób agent z bazą wiedzy może wyciągać wnioski, które umożliwiają mu właściwe działanie. Tu odpowiadamy na pytanie, jakie treści umieścić w bazie wiedzy takiego agenta – jak reprezentować fakty dotyczące świata. Będziemy używać logiki pierwszego rzędu jako języka reprezentacji, ale w kolejnych częściach wprowadzimy różne formalizmy reprezentacji, takie jak hierarchiczne sieci zadań do wnioskowania o planach, sieci bayesowskie do wnioskowania z niepewnością , modele Markowa do wnioskowania o czas oraz głębokie sieci neuronowe do wnioskowania o obrazach, dźwiękach i innych danych. Ale bez względu na to, jakiego przedstawienia użyjesz, fakty dotyczące świata nadal wymagają rozwiązania, a ten rozdział daje ci wyczucie problemów

Praktyczne zastosowania rozwiązań dowodzących twierdzeń o rozdzielczości

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.

Strategie rozwiązywania

Wiemy, że wielokrotne stosowanie reguły wnioskowania rozdzielczości ostatecznie znajdzie dowód, jeśli taki istnieje. W tym podrozdziale przyjrzymy się strategiom, które pomagają skutecznie znajdować dowody.

PREFERENCJA JEDNOSTEK: Ta strategia preferuje rozwiązania, w których jedno ze zdań jest pojedynczym literałem (znanym również jako klauzula jednostkowa). Ideą strategii jest to, że próbujemy stworzyć pustą klauzulę, więc dobrym pomysłem może być preferowanie wnioskowania, które tworzą krótsze zdania. Rozwiązanie zdania jednostkowego (takiego jak P ) z dowolnym innym zdaniem (takim jak ¬P V ¬Q V R ) zawsze daje klauzulę (w tym przypadku ¬Q V R ), która jest krótsza niż druga klauzula. Kiedy strategia preferencji jednostkowych została po raz pierwszy wypróbowana dla wnioskowania zdaniowego w 1964 r., doprowadziła ona do dramatycznego przyspieszenia, umożliwiając udowodnienie twierdzeń, z którymi nie można sobie poradzić bez preferencji. Rozdzielczość jednostkowa to ograniczona forma rozwiązywania, w której każdy krok rozstrzygania musi zawierać klauzulę jednostkową. Rozstrzyganie jednostek jest ogólnie niekompletne, ale kompletne w przypadku klauzul Horn. Dowody rozdzielczości jednostek w klauzulach Horn przypominają łańcuchowanie w przód.

Dowód twierdzenia OTTER , wykorzystuje formę przeszukiwania najlepszy-pierwszy. Jego funkcja heurystyczna mierzy „wagę” każdej klauzuli, przy czym preferowane są klauzule lżejsze. Dokładny wybór heurystyki zależy od użytkownika, ale generalnie waga klauzuli powinna być skorelowana z jej rozmiarem lub trudnością. Klauzule jednostkowe są traktowane jako lekkie; poszukiwania można zatem postrzegać jako uogólnienie strategii preferencji jednostkowych.

ZESTAW WSPARCIA: Preferencje, które najpierw wypróbowują określone rozdzielczości, są pomocne, ale ogólnie lepiej jest spróbować całkowicie wyeliminować niektóre potencjalne rozwiązania. Na przykład możemy nalegać, aby każdy krok rozwiązywania zawierał co najmniej jeden element specjalnego zestawu klauzul – zestawu wsparcia. Rezolwenta jest następnie dodawana do zestawu podpór. Jeśli zestaw wsparcia jest mały w stosunku do całej bazy wiedzy, przestrzeń poszukiwań zostanie drastycznie zmniejszona.

Aby zapewnić kompletność tej strategii, możemy dobrać zbiór podpór S tak, aby pozostałe zdania były łącznie spełnialne. Na przykład, można użyć zanegowanej kwerendy jako zestawu wsparcia, zakładając, że pierwotna baza wiedzy jest spójna. (W końcu, jeśli nie jest spójny, to fakt, że zapytanie wynika z niego, jest bezsensowny.) Strategia zestawu wsparcia ma dodatkową zaletę, że generuje ukierunkowane na cel drzewa dowodów, które często są łatwe do zrozumienia dla ludzi.

ROZDZIELCZOŚĆ WEJŚCIOWA: W tej strategii każda rozdzielczość łączy jedno ze zdań wejściowych (z KB lub zapytania) z innym zdaniem. Dowód wykorzystuje tylko rozdzielczości wejściowe i ma charakterystyczny kształt pojedynczego „grzbietu” z pojedynczymi zdaniami łączącymi się na grzbiecie. Wyraźnie widać, że przestrzeń drzewek dowodowych o takim kształcie jest mniejsza niż przestrzeń wszystkich grafów dowodowych. W bazach wiedzy Horn, Modus Ponens jest rodzajem strategii rozwiązywania danych wejściowych, ponieważ łączy implikacje z oryginalnego KB z kilkoma innymi zdaniami. Nie jest więc niespodzianką, że rozdzielczość danych wejściowych jest kompletna dla baz wiedzy w formie Horn, ale niekompletna w ogólnym przypadku. Strategia rozdzielczości liniowej jest niewielkim uogólnieniem, które pozwala na rozwiązanie P i Q razem, jeśli P znajduje się w oryginalnym KB lub jeśli P jest przodkiem Q w drzewie dowodowym. Rozdzielczość liniowa jest zakończona.

SUBSUMPCJA: Metoda subsumcji eliminuje wszystkie zdania, które są podciągane przez (czyli bardziej szczegółowe niż) zdanie istniejące w KB. Na przykład, jeśli P(x) jest w KB, to nie ma sensu dodawanie P(A) i jeszcze mniej sensu dodawanie P(A) V Q(B) . Subsumowanie pomaga utrzymać małą KB, a tym samym pomaga utrzymać małą przestrzeń wyszukiwania.

Nauka: możemy ulepszyć dowodzenie twierdzenia, ucząc się na podstawie doświadczenia. Mając zbiór wcześniej udowodnionych twierdzeń, wytrenuj system uczenia maszynowego, aby odpowiedzieć na pytanie: mając zestaw przesłanek i cel do udowodnienia, jakie kroki dowodowe są podobne do kroków, które były skuteczne w przeszłości? System DEEPHOL  robi dokładnie to, wykorzystując głębokie sieci neuronowe do budowania modeli (zwanych osadzaniami) celów i przesłanek oraz wykorzystując je do dokonywania wyborów. Szkolenie może wykorzystywać jako przykłady zarówno dowody generowane przez ludzi, jak i komputery, zaczynając od zbioru 10 000 dowodów.

Równość

Żadna z metod wnioskowania opisanych do tej pory w tym rozdziale nie poradzi sobie z twierdzeniem postaci x = y bez dodatkowej pracy. Można zastosować trzy różne podejścia. Pierwszym z nich jest aksjomatyzacja równości – zapisanie zdań o relacji równości w bazy wiedzy. Musimy powiedzieć, że równość jest zwrotna, symetryczna i przechodnia, a także musimy powiedzieć, że możemy zastąpić równaniami równymi w dowolnym predykacie lub funkcji. Potrzebujemy więc trzech podstawowych aksjomatów, a następnie po jednym dla każdego predykatu i funkcji:

Biorąc pod uwagę te zdania, standardowa procedura wnioskowania, taka jak rozdzielczość, może wykonywać zadania wymagające wnioskowania o równości, takie jak rozwiązywanie równań matematycznych. Jednak te aksjomaty wygenerują wiele wniosków, z których większość nie będzie pomocna w dowodzie. Tak więc drugie podejście polega na dodawaniu reguł wnioskowania, a nie aksjomatów. Najprostsza zasada, demodulacja, przyjmuje klauzulę jednostkową x = y i pewną klauzulę α który zawiera termin x i daje nową klauzulę utworzoną przez podstawienie y za x w obrębie α. Działa, jeśli termin w α łączy się z ; nie musi być dokładnie równe x. Zauważ, że demodulacja jest kierunkowa; biorąc pod uwagę x = y , x zawsze jest zastępowany przez y, nigdy odwrotnie. Oznacza to, że demodulację można wykorzystać do uproszczenia wyrażeń za pomocą demodulatorów, takich jak z+0 = z lub z1 = z . Jako inny przykład podano

możemy zakończyć demodulacją

Bardziej formalnie mamy

* DEMODULACJA: Dla dowolnych terminów x, y  i z, gdzie z pojawia się gdzieś w dosłownym m i gdzie  UNIFY(x,z) = θ

gdzie SUBST jest zwykłym podstawieniem listy wiążącej, a SUB(x,y,m) oznacza zastąpienie x przez y gdzieś w obrębie m . Reguła może być również rozszerzona o obsługę klauzul niejednostkowych, w których pojawia się znak równości:

* PARAMODULACJA: dla dowolnych wyrażeń x, y i z , gdzie występuje gdzieś w literze m , a gdzie , UNIFY(x,z) = θ

Na przykład z

mamy θ = UNIFY(F(A,y),F(x,B)) = {x/A , y/B} , i możemy zakończyć przez paramodulację zdania

Paramodulacja daje pełną procedurę wnioskowania dla logiki pierwszego rzędu z równością. Trzecie podejście obsługuje wnioskowanie o równości w całości w ramach rozszerzonego algorytmu unifikacji. Oznacza to, że terminy są unifikowalne, jeśli są równorzędne do udowodnienia przy pewnym podstawieniu, gdzie „dowieść” pozwala na wnioskowanie o równości. Na przykład terminy 1 + 2 i 2 + 1 zwykle nie są unifikowalne, ale algorytm unifikacji, który wie, że x + y = y + x może je ujednolicić za pomocą pustego podstawienia. Tego rodzaju unifikację równań można przeprowadzić za pomocą wydajnych algorytmów zaprojektowanych dla poszczególnych używanych aksjomatów (przemienność, asocjatywność itd.), a nie poprzez jawne wnioskowanie z tymi aksjomatami. Dowodzące twierdzeń przy użyciu tej techniki są ściśle związane z systemami CLP.

Twierdzenie Gödla o niezupełności

Rozszerzając nieco język logiki pierwszego rzędu, aby uwzględnić matematyczny schemat indukcji w arytmetyce, Kurt Gödel był w stanie wykazać w swoim twierdzeniu o niezupełności, że istnieją prawdziwe zdania arytmetyczne, których nie można udowodnić. Dowód twierdzenia o niezupełności wykracza nieco poza zakres tej książki, zajmując co najmniej 30 stron, ale tutaj możemy dać wskazówkę. Zaczynamy od logicznej teorii liczb. W tej teorii istnieje pojedyncza stała 0 i pojedyncza funkcja S (funkcja następnika). W zamierzonym modelu S(0) oznacza 1, S(S(0)) oznacza 2 i tak dalej; język ma zatem nazwy dla wszystkich liczb naturalnych. Słownik zawiera również symbole funkcji + , x i Expt(potęgowanie) oraz zwykły zestaw spójników logicznych i kwantyfikatorów. Pierwszym krokiem jest zauważenie, że zbiór zdań, które możemy napisać w tym języku, można wyliczyć. (Wyobraźmy sobie zdefiniowanie porządku alfabetycznego na symbolach, a następnie ułożenie w porządku alfabetycznym każdego ze zbiorów zdań o długości 1, 2 itd.) Następnie możemy ponumerować każde zdanie α z unikalną liczbą naturalną #α (liczba Gödla). Ma to kluczowe znaczenie: teoria liczb zawiera nazwę dla każdego ze swoich własnych zdań. Podobnie możemy ponumerować każdy możliwy dowód P liczbą Gödla G(P) , ponieważ dowód jest po prostu skończonym ciągiem zdań. Załóżmy teraz, że mamy rekurencyjnie przeliczalny zbiór zdań A, które są prawdziwymi stwierdzeniami dotyczącymi liczb naturalnych. Przypominając, że A można nazwać za pomocą danego zbioru liczb całkowitych, możemy sobie wyobrazić napisanie w naszym języku zdania α(j,A) następującego rodzaju:

∀i   i nie jest liczbą Gödla dowodu zdania, którego liczbą Gödla jest j , gdzie dowód wykorzystuje tylko przesłanki w A

Następnie niech sigma; niech będzie zdanie alfa;(σA) , czyli zdanie, które stwierdza własną niedowodliwość na podstawie A . (To, że to zdanie zawsze istnieje, jest prawdziwe, ale nie do końca oczywiste).

Teraz przedstawiamy następujący pomysłowy argument: Załóżmy, że sigma; można udowodnić z A; następnie sigma; jest fałszywe (ponieważ sigma; mówi, że nie można tego udowodnić). Ale wtedy mamy fałszywe zdanie, które można udowodnić z A , więc A nie może składać się tylko ze zdań prawdziwych – a naruszenie naszego założenia. Dlatego sigma; nie da się udowodnić z A . Ale to jest właśnie sigma; sama twierdzi; stąd sigma; to prawdziwe zdanie.

Wykazaliśmy więc (z wyjątkiem 29 1/2 strony), że dla każdego zestawu zdań prawdziwych teorii liczb, a w szczególności zestawu podstawowych aksjomatów, istnieją inne zdania prawdziwe, których nie można udowodnić na podstawie tych aksjomatów. Ustala to między innymi, że nigdy nie możemy udowodnić wszystkich twierdzeń matematyki w ramach danego systemu aksjomatów. Oczywiście było to ważne odkrycie dla matematyki. Jego znaczenie dla sztucznej inteligencji było szeroko dyskutowane, poczynając od spekulacji samego Gödla

Kompletność rozstrzygnięcia

Ta sekcja zawiera dowód kompletności rozwiązania. Może być bezpiecznie pominięty przez tych, którzy są gotowi przyjąć ją na wiarę. Pokazujemy, że rozwiązanie jest obalające zupełne, co oznacza, że jeśli zbiór zdań jest niezadowalający, to rozwiązanie zawsze będzie w stanie wyprowadzić sprzeczność. Rozdzielczość nie może być użyta do wygenerowania wszystkich logicznych konsekwencji zbioru zdań, ale może być użyta do ustalenia, że dane zdanie jest zawarte w zbiorze zdań. Można go zatem wykorzystać do znalezienia wszystkich odpowiedzi na zadane pytanie Q(x) , udowadniając, że KB Λ ¬Q(x) jest ono niezadowalające.

Przyjmujemy, że każde zdanie w logice pierwszego rzędu (bez równości) może zostać przepisane jako zbiór klauzul w CNF. Można to udowodnić przez indukcję na formie zdania, używając zdań atomowych jako przypadku bazowego. Naszym celem jest zatem udowodnienie, co następuje: jeśli S jest to niespełniony zbiór klauzul, to zastosowanie skończonej liczby kroków rozstrzygnięcia do S przyniesie sprzeczność.

Nasz szkic dowodowy podąża za oryginalnym dowodem Robinsona z pewnymi uproszczeniami zaczerpniętymi z Genesereth i Nilsson. Podstawowa struktura dowodu jest następująca:

  1. Po pierwsze, zauważamy, że jeśli S jest niespełniony, to istnieje określony zbiór podstawowych wystąpień zdań S o takim charakterze, że ten zbiór również jest niespełniony (twierdzenie Herbranda).
  2. Następnie odwołujemy się do twierdzenia o rozstrzygnięciu w podstawie podanego w rozdziale 7, które stwierdza, że ​​rozstrzyganie zdaniowe jest kompletne dla zdań gruntowych.
  3. Następnie używamy lematu unoszącego, aby pokazać, że dla każdego dowodu rozstrzygnięcia zdań przy użyciu zbioru zdań podstawowych istnieje odpowiedni dowód rozstrzygnięcia pierwszego rzędu wykorzystujący zdania pierwszego rzędu, z których otrzymano zdania podstawowe.

Aby wykonać pierwszy krok, potrzebujemy trzech nowych koncepcji:

* HERBRAND UNIVERSE: Jeśli S jest zbiorem klauzul, to HS , uniwersum Herbranda  S , jest zbiorem wszystkich podstawowych terminów, które można skonstruować z następującego:

  1. Symbole funkcji w S , jeśli istnieją.
  2. Symbole stałe w S , jeśli istnieją; jeśli brak, to domyślny symbol stałej, S.

Na przykład, jeśli S zawiera tylko zdanie  to HS jest następującym nieskończonym zbiorem terminów podstawowych:

{A,B,F(A,A),F(A,B),F(B,A),F(B,B),F(A,F(A,A)),…}.

* NASYCENIE: Jeśli S jest zbiorem klauzul i P jest zbiorem warunków podstawowych, to  P(S) , nasycenie  S względem P , jest zbiorem wszystkich klauzul podstawowych uzyskanych przez zastosowanie wszystkich możliwych zgodnych podstawień warunków podstawowych w P dla zmiennych w S .

* BAZA HERBRAND: Nasycenie zbioru klauzul S w odniesieniu do jego uniwersum Herbranda nosi nazwę bazy Herbrand , pisanej jako HS(S) . Na przykład, jeśli S zawiera wyłącznie klauzulę podaną powyżej, to HS(S) jest nieskończonym zbiorem klauzul

Definicje te pozwalają na sformułowanie formy twierdzenia Herbranda (Herbrand, 1930):

Jeśli zbiór klauzul jest niespełniony, to istnieje skończony podzbiór HS(S), który również jest niespełniony.

Niech S’ będzie tym skończonym podzbiorem zdań podstawowych. Teraz możemy odwołać się do twierdzenia o rozdzielczości podstawowej (strona 228), aby pokazać, że zamknięcie rozdzielczości RC(S’) zawiera pustą klauzulę. Oznacza to, że uruchomienie rozwiązania zdań do zakończenia na S” wyprowadzi sprzeczność.

Teraz, gdy ustaliliśmy, że zawsze istnieje dowód rozdzielczości obejmujący jakiś skończony podzbiór bazy Herbranda z , następnym krokiem jest wykazanie, że istnieje dowód rozdzielczości wykorzystujący klauzule samego S, które niekoniecznie są klauzulami podstawowymi. Zaczynamy od rozważenia pojedynczego zastosowania zasady resolution. Robinson stwierdził ten lemat:

Niech C1 i C2 będą dwoma klauzulami bez wspólnych zmiennych, a C1′ i C2′ będą podstawowymi instancjami C1 i C2 . Jeśli C’ jest rezolwentą C1′ i C2′ , to istnieje klauzula C taka, że (1) C jest rezolwentą C1 i C2 oraz (2) C’ jest podstawową instancją C.

Nazywa się to lematem znoszącym, ponieważ przenosi krok dowodowy z klauzul podstawowych do ogólnych klauzul pierwszego rzędu. Aby udowodnić swój podstawowy lemat podnoszenia, Robinson musiał wymyślić unifikację i wyprowadzić wszystkie właściwości większości ogólnych unifikatorów. Zamiast powtarzać tutaj dowód, po prostu zilustrujemy lemat:

Widzimy, że rzeczywiście C’ jest podstawową instancją C . Ogólnie, aby C1’i C2′ miały jakiekolwiek rezolwenty, muszą być skonstruowane przez zastosowanie najpierw do C1 i C2 najbardziej ogólnego unifikatora pary komplementarnych literałów w C1 i C2 . Z lematu o podnoszeniu łatwo wyprowadzić podobne stwierdzenie o dowolnej kolejności zastosowań reguły rozstrzygania:

Dla każdej klauzuli C’ w zamknięciu rezolucji S’ istnieje klauzula C w zamknięciu rezolucji S taka, że ​​C’ jest podstawową instancją C, a wyprowadzenie C ma taką samą długość jak wyprowadzenie C’.

Z tego faktu wynika, że ​​jeżeli klauzula pusta pojawia się w zamknięciu rezolucji S’ , to musi ona również pojawić się w zamknięciu rezolucji S . Dzieje się tak, ponieważ pusta klauzula nie może być podstawową instancją żadnej innej klauzuli. Reasumując: pokazaliśmy, że jeśli S jest niespełnialne, to istnieje skończone wyprowadzenie pustej klauzuli za pomocą reguły rozwiązywania. Zniesienie dowodzenia twierdzeń z klauzul podstawowych do klauzul pierwszego rzędu zapewnia ogromny wzrost mocy. Ten wzrost wynika z faktu, że dowód pierwszego rzędu wymaga zmiennych instancji tylko w takim stopniu, w jakim jest to konieczne dla dowodu, podczas gdy metody klauzul podstawowych były wymagane do zbadania ogromnej liczby arbitralnych instancji.

Przykładowe dowody

Rozdzielczość dowodzi, że KB |= α, udowadniając, że KB Λ ¬α jest niezadowalająca — to znaczy wyprowadzając pustą klauzulę. Podejście algorytmiczne jest identyczne z przypadkiem zdaniowym opisanym na rysunku 7.13, więc nie musimy go tutaj powtarzać. Zamiast tego podajemy dwa przykładowe dowody. Pierwszy to przykład przestępstwa. Zdania w CNF są

Uwzględniamy również zanegowany cel ¬Criminal(West). Dowód rozdzielczości pokazano na rysunku

Zwróć uwagę na strukturę: pojedynczy „kręgosłup” rozpoczynający się od klauzuli celu, rozstrzygany na podstawie klauzul z bazy wiedzy, aż do wygenerowania pustej klauzuli. Jest to charakterystyczne dla rozwiązania opartego na bazach wiedzy o klauzulach Horn. W rzeczywistości zdania wzdłuż głównego kręgosłupa odpowiadają dokładnie kolejnym wartościom zmiennej goli w algorytmie tworzenia łańcucha wstecznego . Dzieje się tak dlatego, że zawsze wybieramy rozwiązanie za pomocą zdania, którego pozytywny dosłowny łączy się z najbardziej wysuniętym na lewo dosłownym zdaniem „bieżącego” na grzbiecie; to jest dokładnie to, co dzieje się w łańcuchu wstecznym. Tak więc łańcuch wsteczny jest tylko szczególnym przypadkiem rozwiązania z określoną strategią sterowania, aby zdecydować, które rozwiązanie wykonać w następnej kolejności.

Nasz drugi przykład wykorzystuje Skolemization i obejmuje klauzule, które nie są klauzulami określonymi. Powoduje to nieco bardziej złożoną strukturę dowodu. 

Każdy, kto kocha wszystkie zwierzęta, jest przez kogoś kochany.

Każdy, kto zabija zwierzę, nie jest przez nikogo kochany.

Jack kocha wszystkie zwierzęta.

Albo Jack, albo Curiosity zabili kota o imieniu Tuna.

Czy ciekawość zabiła kota?

Najpierw wyrażamy oryginalne zdania, pewną podstawową wiedzę i zanegowany cel G w logice pierwszego rzędu:

Teraz stosujemy procedurę konwersji, aby przekonwertować każde zdanie na CNF:

Dowód rozdzielczości, że Curiosity zabił kota, jest pokazany na rysunku

Dowód można sparafrazować w następujący sposób:

Załóżmy, że Curiosity nie zabił tuńczyka. Wiemy, że zrobili to Jack lub Curiosity; tak Jack musi mieć. Tuńczyk to kot, a koty to zwierzęta, więc tuńczyk jest zwierzęciem. Ponieważ nikt, kto zabija zwierzę, nie jest przez nikogo kochany, wiemy, że nikt nie kocha Jacka. Z drugiej strony Jack kocha wszystkie zwierzęta, więc ktoś go kocha; więc mamy sprzeczność. Dlatego Curiosity zabił kota.

Dowód odpowiada na pytanie „Czy ciekawość zabiła kota?” ale często chcemy zadawać bardziej ogólne pytania, takie jak „Kto zabił kota?” Rozwiązanie może to zrobić, ale uzyskanie odpowiedzi wymaga trochę więcej pracy. Celem jest który po zanegowaniu staje się w CNF. Powtarzając dowód z rysunku z nowym zanegowanym celem, otrzymujemy podobne drzewo dowodowe, ale z podstawieniem  {w/Curiosity} w jednym z kroków. Tak więc w tym przypadku ustalenie, kto zabił kota, jest tylko kwestią śledzenia powiązań dla zmiennych zapytania w dowodzie. Niestety, rozdzielczość może czasami dawać niekonstruktywne dowody na cele egzystencjalne, gdy wiemy, że zapytanie jest prawdziwe, ale nie ma unikalnego powiązania dla zmiennej.

Zasada wnioskowania o rozdzielczości

Reguła rozstrzygania dla klauzul pierwszego rzędu jest po prostu zniesioną wersją reguły rozwiązywania zdań podanej na stronie 226. Dwie klauzule, które z założenia są znormalizowane oddzielnie, tak że nie mają wspólnych zmiennych, mogą zostać rozwiązane, jeśli zawierają komplementarne literały. Literały zdaniowe są komplementarne, jeśli jeden jest negacją drugiego; Literały pierwszego rzędu są komplementarne, jeśli jeden łączy się z negacją drugiego. Tak więc mamy

gdzie . Na przykład możemy rozwiązać dwie klauzule

eliminując dopełniające się literały  Loves (G(x),x) i ¬Loves(u,v) z unifikatorem

, wytworzyć klauzulę rezolucyjną

Ta reguła jest nazywana regułą rozwiązywania binarnego, ponieważ rozwiązuje dokładnie dwa literały. Sama reguła rozwiązywania binarnego nie daje pełnej procedury wnioskowania. Reguła pełnej rozdzielczości rozwiązuje podzbiory literałów w każdej klauzuli, które są unifikowalne. Alternatywnym podejściem jest rozszerzenie faktoringu – usunięcie zbędnych literałów – do przypadku pierwszego rzędu. Faktoring zdaniowy redukuje dwa literały do jednego, jeśli są identyczne; faktoring pierwszego rzędu redukuje dwa literały do jednego, jeśli są one unifikowalne. Unifikator musi być zastosowany do całej klauzuli. Połączenie rozdzielczości binarnej i faktoringu jest kompletne.

Spójna postać normalna dla logiki pierwszego rzędu

Pierwszym krokiem jest przekształcenie zdań w spójną formę normalną (CNF) — czyli koniunkcję klauzul, gdzie każda klauzula jest alternatywą literałów. W CNF literały mogą zawierać zmienne, co do których zakłada się, że są uniwersalnie kwantyfikowalne. Na przykład zdanie

staje się

Kluczem jest to, że każde zdanie logiki pierwszego rzędu może zostać przekształcone w inferencyjnie równoważne zdanie CNF. Zasadnicza różnica wynika z potrzeby wyeliminowania kwantyfikatorów egzystencjalnych. Zilustrujemy tę procedurę, tłumacząc zdanie „Każdy, kto kocha wszystkie zwierzęta, jest przez kogoś kochany” lub

Kroki są następujące:

* WYELIMINUJ IMPLIKACJE: Zamień P => Q na ¬P  Q . W przypadku naszego przykładowego zdania należy to zrobić dwukrotnie:

* MOVE ¬ INWARDS: Oprócz zwykłych reguł dla zanegowanych spójników, potrzebujemy reguł dla zanegowanych kwantyfikatorów. Tak więc mamy

Nasze zdanie przechodzi następujące przekształcenia:

Zwróć uwagę, jak uniwersalny kwantyfikator (  ) w założeniu implikacji stał się kwantyfikatorem egzystencjalnym. Teraz zdanie brzmi: „Albo jest jakieś zwierzę, które nie kocha xc, albo (jeśli tak nie jest) ktoś kocha x”. Oczywiście znaczenie pierwotnego zdania zostało zachowane.

* STANDARYZUJ ZMIENNE: Dla zdań takich jak które używają tej samej nazwy zmiennej dwukrotnie, zmień nazwę jednej ze zmiennych. Pozwala to uniknąć późniejszych nieporozumień, gdy odrzucimy kwantyfikatory. Tak więc mamy

* SKOLEMIZUJ: Skolemizacja to proces usuwania kwantyfikatorów egzystencjalnych przez eliminację. W prostym przypadku jest to tak, jak reguła egzystencjalnej instancji: przetłumacz  P(x)  na P(A), gdzie A jest nową stałą. Nie możemy jednak zastosować egzystencjalnego wystąpienia do naszego zdania powyżej, ponieważ nie pasuje ono do wzorca α; tylko części zdania pasują do wzorca. Jeśli ślepo zastosujemy regułę do dwóch pasujących części, które otrzymamy

co ma całkowicie błędne znaczenie: mówi, że każdy albo nie kocha konkretnego zwierzęcia A, albo jest kochany przez jakąś konkretną istotę. W rzeczywistości nasze pierwotne zdanie pozwala każdemu nie kochać innego zwierzęcia lub być kochanym przez inną osobę. Zatem chcemy, aby encje Skolema zależały od x:

Tutaj F i G są funkcjami Skolema. Ogólna zasada jest taka, że argumentami funkcji Skolema są wszystkie uniwersalnie kwantyfikowalne zmienne, w których zakresie występuje kwantyfikator egzystencjalny. Podobnie jak w przypadku egzystencjalnego wystąpienia, zdanie skolemizowane jest spełnialne dokładnie wtedy, gdy zdanie oryginalne jest spełnialne.

* DROP UNIVERSAL QUANTIFIERS: W tym momencie wszystkie pozostałe zmienne muszą być uniwersalnie kwantyfikowane. Dlatego nie tracimy żadnych informacji, jeśli opuścimy kwantyfikator:

* ROZPOCZĘCIE V NA  Λ:

Ten krok może również wymagać spłaszczenia zagnieżdżonych spójników i rozłączeń. Zdanie jest teraz w CNF i składa się z dwóch klauzul. Jest znacznie trudniejszy do odczytania niż oryginalne zdanie z implikacjami. (Może pomóc wyjaśnienie, że funkcja Skolema F(x) odnosi się do zwierzęcia potencjalnie niekochanego przez x , podczas gdy G(x) odnosi się do kogoś, kto może kochać x.) Na szczęście ludzie rzadko muszą patrzeć na zdania CNF – tłumaczenie proces jest łatwo zautomatyzowany