Klauzula Horna — definicja i zastosowania w logice i programowaniu (Prolog)

Klauzula Horna — przystępne wyjaśnienie, przykłady i zastosowania w logice i Prologu. Poznaj definicję, typy (fakt, cel), rozwiązywanie i praktyczne wykorzystanie.

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).
• fakt — klauzula określona bez liter negatywnych (zawierająca tylko literę dodatnią), zwykle traktowana jako bezwarunkowe twierdzenie: 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)

oznacza formalnie

∀X(¬human(X) ∨ mortal(X))

co jest równoważne implikacji

∀X( human(X) → 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

albo w notacji używanej w systemach logicznych:

u ← (p ∧ q ∧ ⋯ ∧ 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.

Pytania i odpowiedzi

P: Co to jest klauzula rogowa?

P: Kto pierwszy je opisał?

P: Co to jest klauzula definitywna?

P: Co to jest fakt?

P: Co to jest klauzula celu?

P: Jak działają zmienne w przypadkach niepropozycyjnych?

Szukaj według litery