Drugie główne podejście do ILP polega na odwróceniu normalnego procesu dedukcyjnego dowodu. Rozwiązanie odwrotne opiera się na spostrzeżeniu, że jeśli przykładowe Klasyfikacje wynikają z Tło Ʌ Hipoteza Ʌ Opisy, to trzeba być w stanie udowodnić ten fakt za pomocą rozwiązania (ponieważ rozwiązanie jest kompletne). Jeśli możemy „przeprowadzić dowód wstecz”, to możemy znaleźć Hipotezę taką, że dowód przejdzie. Kluczem jest zatem znalezienie sposobu na odwrócenie procesu restrukturyzacji i uporządkowanej likwidacji. Pokażemy proces weryfikacji wstecznej dla rozwiązania odwrotnego, który składa się z pojedynczych kroków wstecznych. Przypomnijmy, że zwykły krok rozwiązania obejmuje dwie klauzule C1 i C2 oraz rozwiązuje je, aby wytworzyć rezolucję C. Krok odwrotnej rezolucji bierze rezolucję C i tworzy dwie klauzule C1 i C2, takie, że C jest wynikiem rozwiązania C1 i C2. Alternatywnie, może wziąć rezolwentę C i klauzulę C1 i stworzyć klauzulę C2 taką, że C jest wynikiem rozwiązania C1 i C2.
Wczesne etapy procesu rozwiązywania odwrotnego są pokazane na rysunku 20.13, gdzie skupiamy się na pozytywnym przykładzie Dziadka(George;Anne). Proces rozpoczyna się na końcu dowodu (pokazanego na dole rysunku). Przyjmujemy rezolwentę C jako pustą klauzulę (tj. sprzeczność), a C2 jako ¬Grandparent(George;Anne), co jest negacją przykładu celu. Pierwszy odwrotny krok bierze C i C2 i generuje klauzulę Grandparent(George;Anne) dla C1. Następny krok przyjmuje tę klauzulę jako C, a klauzulę Parent(Elizabeth;Anne) jako C2 i generuje klauzulę ¬Parent(Elizabeth;y) V _Grandparent(George;y) jako C1. Ostatni krok traktuje tę klauzulę jako rezolucję. Z Parent(George; Elizabeth) jako C2, jedną z możliwych klauzul C1 jest hipoteza Parent(x,z)ɅParent(z;y) => Grandparent(x;y) . Teraz mamy dowód rozwiązania, że hipoteza, opisy, i podstawowa wiedza pociąga za sobą klasyfikację Dziadkowie (George; Anne). Oczywiście odwrotna rozdzielczość obejmuje wyszukiwanie. Każdy krok rozwiązywania odwrotnego jest niedeterministyczny, ponieważ dla dowolnego C może istnieć wiele lub nawet nieskończona liczba klauzul C1 i C2, które rozstrzygają na C. Na przykład zamiast wybierać ¬Parent(Elizabeth;y) V Grandparent(George;y) dla C1 w ostatnim kroku na rysunku krok odwrotnego rozwiązywania mógł wybrać dowolne z następujących zdań
Ponadto, klauzule uczestniczące w każdym kroku mogą być wybrane z Wiedzy Podstawowej, z przykładowych Opisów, z zanegowanych Klasyfikacji lub z hipotetycznych klauzul, które zostały już wygenerowane w drzewie odwrotnej rozdzielczości. Duża liczba możliwości oznacza duży współczynnik rozgałęzienia (a tym samym nieefektywne wyszukiwanie) bez dodatkowych kontroli. We wdrożonych systemach ILP wypróbowano kilka podejść do oswajania poszukiwań:
- Zbędne wybory można wyeliminować – na przykład, generując tylko najbardziej szczegółowe hipotezy i wymagając, aby wszystkie hipotezy były spójne ze sobą i z obserwacjami. To ostatnie kryterium wykluczyłoby klauzulę ¬Parent(z;y) V Grandparent(George;y), wymienioną wcześniej.
- Strategia dowodowa może być ograniczona. Na przykład w rozdziale 9 widzieliśmy, że rozdzielczość liniowa jest kompletną, ograniczoną strategią. Rozdzielczość liniowa tworzy drzewa dowodów, które mają liniową strukturę rozgałęzień – całe drzewo podąża za jedną linią, z tylko pojedynczymi klauzulami odchodzącymi od tej linii.
- Język reprezentacji można ograniczyć, na przykład eliminując symbole funkcji lub dopuszczając tylko klauzule Horn. Na przykład PROGOL działa z klauzulami Horna, wykorzystując odwrotne wywoływanie. Chodzi o to, aby zmienić ograniczenie wynikania.
do formy równoważnej logicznie
Na tej podstawie można użyć procesu podobnego do normalnej dedukcji klauzuli Prologa Horna, z negacją jako niepowodzeniem w celu wyprowadzenia Hipotezy. Ponieważ jest ograniczona do klauzul Horn, jest to niekompletna metoda, ale może być bardziej wydajna niż pełna rozdzielczość. To jest również możliwe zastosowanie pełnego wnioskowania z odwrotnym wnioskowaniem.
- Wnioskowanie można przeprowadzić za pomocą sprawdzania modelu, a nie dowodzenia twierdzeń. System PROGOL wykorzystuje formę sprawdzania modelu w celu ograniczenia wyszukiwania. Oznacza to, że podobnie jak programowanie zestawu odpowiedzi, generuje możliwe wartości dla zmiennych logicznych i sprawdza spójność.
- Wnioskowanie można przeprowadzić za pomocą podstawowych zdań zdaniowych, a nie w logice pierwszego rzędu. System LINUS działa poprzez tłumaczenie teorii pierwszego rzędu na logikę zdań, rozwiązywanie ich za pomocą systemu uczenia się zdań, a następnie tłumaczenie z powrotem. Praca z formułami zdaniowymi może być bardziej wydajna w przypadku niektórych problemów, jak widzieliśmy w przypadku SATPLAN .