Zdania rogowe i zdania określone

Kompletność rozwiązania sprawia, że ​​jest to bardzo ważna metoda wnioskowania. Jednak w wielu praktycznych sytuacjach nie jest potrzebna pełna moc rozdzielczości. Niektóre bazy wiedzy ze świata rzeczywistego spełniają pewne ograniczenia dotyczące formy zawartych w nich zdań, co umożliwia im stosowanie bardziej ograniczonego i wydajnego algorytmu wnioskowania. Jedną z takich ograniczonych form jest zdanie określone, które jest alternatywą literałów, z których dokładnie jeden jest pozytywny. Na przykład zdanie (¬L_1,1 V ¬Breeze V B_1,1)jest zdaniem określonym, podczas gdy (¬B_1,1 V P_1,2 V P_2,1 )nie jest, ponieważ zawiera dwie zdania pozytywne. Nieco ogólniejsza jest klauzula Horn, będąca alternatywą dosłownych, z których co najwyżej jeden jest pozytywny. Zatem wszystkie zdania określone są zdaniami Horna, podobnie jak zdania bez literałów dodatnich; są to tak zwane klauzule bramkowe. Klauzule rogów są zamykane po rozwiązaniu: jeśli rozpatrzysz dwie klauzule rogów, otrzymasz z powrotem klauzulę rogów. Jeszcze jedna klasa to zdanie k-CNF, które jest zdaniem CNF, w którym każda klauzula ma co najwyżej k literałów.

Bazy wiedzy zawierające tylko zdania określone są interesujące z trzech powodów:

1. Każde zdanie określone można zapisać jako implikację, której przesłanką jest koniunkcja literałów pozytywnych, a zakończeniem jest pojedynczy literał pozytywny. Na przykład zdanie (¬L_1,1 ∨ ¬Breeze ∨ B_1,1) określone może być zapisane jako implikacja (L_1,1 ∧ Breeze) ⇒ B_1,1 . W formie implikacyjnej zdanie jest łatwiejsze do zrozumienia: mówi, że jeśli agent jest w [1,1] i istnieje przewiewny percept, to [1,1] jest przewiewny. W formie Horn założenie nazywa się ciałem, a zakończenie nazywa się głową. Zdanie składające się z jednego pozytywnego literału, takiego jak L1,1, nazywa się faktem. Można go również napisać w formie implikacji jako True ⇒ L_1,1 ale prościej jest napisać po prostu L_1,1 .
2. Wnioskowanie z klauzulami Horna można wykonać za pomocą algorytmów łączenia w przód i wstecz, które wyjaśnimy dalej. Oba te algorytmy są naturalne, ponieważ kroki wnioskowania są oczywiste i łatwe do naśladowania dla ludzi. Ten rodzaj wnioskowania jest podstawą programowania logicznego
3. Decydowanie o pociągnięciu za pomocą klauzul Horna można przeprowadzić w czasie, który jest liniowy w wielkości bazy wiedzy – miła niespodzianka.