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.