Klauzula Horna (ang. Horn clause) to rodzaj formuły w logice wypowiedzi i logice pierwszego rzędu, w której występuje co najwyżej jedna litera dodatnia (pozytywna), a pozostałe litery, jeśli występują, są negatywne. Nazwa pochodzi od Alfreda Horna, który opisał je w artykule z 1951 roku.

Rodzaje klauzul Horna

Wyróżnia się trzy często spotykane podtypy klauzul Horna:

  • klauzula określona (definite clause) — klauzula zawierająca dokładnie jedną literę dodatnią; ma postać ¬p ∨ ¬q ∨ … ∨ u (czyli u ∨ ¬p ∨ ¬q ∨ … ∨ ¬t). {\displaystyle \neg p\lor \neg q\vee \cdots \vee \neg t\vee u}
  • fakt — klauzula określona bez liter negatywnych (zawierająca tylko literę dodatnią), zwykle traktowana jako bezwarunkowe twierdzenie: u. {\displaystyle u}
  • klauzula celu (goal clause, query) — klauzula zawierająca tylko litery negatywne (żadnej dodatniej); reprezentuje zapytanie lub żądanie dowodu.

Klasyczny zapis i interpretacja kwantyfikatorów

Klauzule Horna w logice pierwszego rzędu standardowo traktuje się jako formuły ze zmiennymi obwiązywanymi uniwersalnie (domyślnie wszystkie zmienne w klauzuli są kwantyfikowane ogółem przy pomocy ∀). Na przykład klauzula

¬ human(X) ∨ mortal(X) {\displaystyle \neg {\text{human}}(X)\lor {\text{mortal}}(X)}

oznacza formalnie

∀X(¬human(X) ∨ mortal(X)) {\displaystyle \forall X(\neg {\text{human}}(X)\lor {\text{mortal}}(X))}

co jest równoważne implikacji

∀X( human(X) → mortal(X) ) {\displaystyle \forall X({\text{human}}(X)\rightarrow {\text{mortal}}(X)).}

Taka reprezentacja jest standardowa w logice i w programowaniu logicznym: litera dodatnia traktowana jest jako wniosek, a litery negatywne jako jego warunki.

Rezolucja, SLD i zastosowania w programowaniu logicznym

Klauzule Horna odgrywają fundamentalną rolę w automatycznym dowodzeniu twierdzeń oraz w programowaniu logicznym. Istotna własność: rezolucja dwóch klauzul Horna znów daje klauzulę Horna, a rezolucja klauzuli celu z klauzulą określoną prowadzi do klauzuli celu — to umożliwia efektywne wnioskowanie.

W praktyce programowania logicznego (np. w Prologu) klauzule określone zapisuje się w postaci implikacji lub w zapisie "odwrotnym" (head ← body):

(p ∧ q ∧ ⋯ ∧ t) → u {\displaystyle (p\wedge q\wedge \cdots \wedge t)\rightarrow u}

albo w notacji używanej w systemach logicznych:

u ← (p ∧ q ∧ ⋯ ∧ t) {\displaystyle u\leftarrow (p\land q\land \cdots \land t)}

W Prologu analogiczna klauzula zapisywana jest jako:

u :- p, q, ..., t.

Interpretacja proceduralna jest następująca: aby udowodnić u (cel), trzeba udowodnić kolejno p, q, …, t. Mechanizm SLD-resolution (Selective Linear Definite clause resolution) wykorzystuje te własności do wykonywania zapytań i rozwiązywania zmiennych w programach Prolog.

Semantyka minimalnego modelu

Van Emden i Kowalski (1976) pokazali ważne własności semantyczne klauzul Horna w kontekście programowania logicznego. Dla dowolnego zbioru klauzul określonych D istnieje jedyny minimalny model M (w sensie zawierania zbiorów atomów) spełniający D. Atom A jest logicznie implikowany przez D wtedy i tylko wtedy, gdy A jest prawdziwy w minimalnym modelu M. Ta minimalna semantyka modelowa stanowi teoretyczną podstawę dla semantyk programów logicznych i rozumienia, co program "zawiera".

Złożoność obliczeniowa i decidowalność

  • W logice zdań (propositional Horn clauses) problem sprawdzenia spełnialności (HORNSAT) jest rozwiązywalny w czasie liniowym i jest problemem P-complete. Oznacza to, że choć trudność jest znacząca, istnieją efektywne algorytmy rozwiązujące HORNSAT.
  • Dla ogólnego problemu satysfakcjonowalności formuł boolowskich (SAT) problem jest NP-complete.
  • Dla logiki pierwszego rzędu problemy ogólnej spełnialności i domknięcia logicznego klauzul Horna bywają niezdecydowane — w ogólności zadania związane z wnioskowaniem w pierwszym rzędzie mogą być nierozstrzygalne.

Zastosowania i uwagi praktyczne

  • Klauzule Horna stanowią podstawę programowania logicznego (np. Prolog, Datalog) i systemów wnioskowania. Dzięki ich strukturze możliwe jest efektywne wykonywanie zapytań i dowodzenie twierdzeń metodami opartymi na rezolucji.
  • Datalog, używany w analizie baz danych i systemach dedukcyjnych, operuje zwykle na podzbiorze klauzul Horna bez funkcji, co gwarantuje decidowalność i często efektywność obliczeniową.
  • W praktycznych implementacjach warto zwracać uwagę na kwestie związane z kolejnością reguł, negacją i strategiami poszukiwania (np. leksykograficzna kolejność prób w Prologu), które wpływają na zachowanie systemu i jego kompletność.

Podsumowanie

Klauzule Horna to prosty, lecz niezwykle użyteczny fragment logiki, łączący dobre własności semantyczne (istnienie minimalnego modelu) z wydajnymi algorytmami wnioskowania. Ich cechy czynią je fundamentem zarówno teoretycznych rozważań o logice i złożoności, jak i praktycznych systemów programowania logicznego, takich jak Prolog.

Klauzule Horna są również podstawą programowania logicznego, gdzie powszechnie pisze się konkretne klauzule w formie implikacji. W rzeczywistości, rozdzielczość klauzuli celu z określoną klauzulą w celu stworzenia nowej klauzuli celu jest podstawą reguły wnioskowania rezolucji SLD, używanej do implementacji programowania logicznego i języka programowania Prolog.

Van Emden i Kowalski (1976) badali teoretyczne właściwości modelu klauzul Horna w kontekście programowania logiki, pokazując, że każdy zestaw zdefiniowanych klauzul D posiada unikalny minimalny model M. Wzór atomowy A jest logicznie implikowany przez D wtedy i tylko wtedy, gdy A jest prawdziwe w M.

Klauzule Propositional Horn są również interesujące w złożoności obliczeniowej, gdzie problem znalezienia przypisania wartości true w celu spełnienia zestawu klauzul propositional Horn (HORNSAT) jest problemem typu P-complete (rozwiązywalnym w czasie liniowym). (Nieograniczony boolejski problem satysfakcji jest jednak problemem NP-complete). Zadawalalność klauzul Horna pierwszego rzędu jest w ogólności niezdecydowana.