Klauzula rogu - Horn clause
W logice matematycznej i programowania logicznego , o Klauzula Horna jest logiczną formuły określonej formy regułach jak co daje użyteczne właściwości do zastosowania w programowaniu logicznym, formalnej specyfikacji i teorii modeli . Klauzule Horn zostały nazwane na cześć logika Alfreda Horna , który jako pierwszy wskazał na ich znaczenie w 1951 roku.
Definicja
Klauzula klaksonu jest klauzula (a alternatywą z literałów ) z co najwyżej jednym pozytywny, tzn unnegated , dosłowne.
I odwrotnie, alternatywa literałów z co najwyżej jednym literałem zanegowanym nazywana jest klauzulą dual-horn .
Klauzula Horn z dokładnie jednym pozytywnym literałem jest klauzulą określoną lub ścisłą klauzulą Horn ; klauzula określona bez literałów ujemnych jest klauzulą jednostkową , a klauzula jednostkowa bez zmiennych jest faktem ;. Klauzula Horn bez pozytywnego literału jest klauzulą celu . Zauważ, że pusta klauzula, składająca się z żadnych literałów (co jest odpowiednikiem false ) jest klauzulą celu. Te trzy rodzaje klauzul Horn ilustruje następujący przykład zdaniowy :
| Klauzula typu Horn | Forma alternatywna | Formularz implikacyjny | Czytaj intuicyjnie, jak |
|---|---|---|---|
| Klauzula ostateczna | ¬ p ∨ ¬ q ∨ ... ∨ ¬ t ∨ u | u ← p ∧ q ∧ ... ∧ t | załóżmy, że jeśli p i q oraz ... i t wszystkie są spełnione , wtedy również u zachodzi |
| Fakt | ty | ty ← prawda | Zakładamy, że u posiada |
| Klauzula celu | ¬ p ∨ ¬ q ∨ ... ∨ ¬ t | fałsz ← p ∧ q ∧ ... ∧ t | pokaż, że p i q oraz ... i t wszystkie mają miejsce |
Wszystkie zmienne w klauzuli są niejawnie uniwersalnie kwantyfikowane, a zakresem jest cała klauzula. Na przykład:
- ¬ człowiek ( X ) ∨ śmiertelny ( X )
oznacza:
- ∀X( ¬ człowiek ( X ) ∨ śmiertelny ( X ) )
co jest logicznym odpowiednikiem:
- ∀X ( człowiek ( X ) → śmiertelny ( X ))
Znaczenie
Klauzule Horn odgrywają podstawową rolę w logice konstruktywnej i logice obliczeniowej . Są one ważne w automatycznym dowodzeniu twierdzeń przez rozwiązanie pierwszego rzędu , ponieważ resolwenta dwóch klauzul Horna sama w sobie jest klauzulą Horna, a resolwenta klauzuli celu i klauzuli określonej jest klauzulą celu. Te właściwości klauzul Horna mogą prowadzić do większej skuteczności dowodzenia twierdzenia: klauzula celu jest negacją tego twierdzenia; patrz klauzula Cel w powyższej tabeli. Intuicyjnie, jeśli chcemy udowodnić φ, zakładamy ¬φ (cel) i sprawdzamy, czy takie założenie nie prowadzi do sprzeczności. Jeśli tak, to φ musi zostać utrzymane. W ten sposób mechaniczne narzędzie dowodzenia musi utrzymywać tylko jeden zestaw formuł (założeń), a nie dwa zestawy (założenia i (pod)cele).
Klauzule zdaniowe Horn są również interesujące w złożoności obliczeniowej . Problem znajdowania przypisań prawdziwościowych w celu uczynienia koniunkcji zdań zdaniowych Horna prawdziwymi jest znany jako HORNSAT . Problem ten jest P-zupełny i można go rozwiązać w czasie liniowym . Zauważ, że nieograniczony problem spełnialności logicznej jest problemem NP-zupełnym .
Programowanie logiczne
Klauzule Horn są również podstawą programowania logicznego , gdzie powszechne jest pisanie klauzul określonych w formie implikacji :
- ( p ∧ q ∧ ... ∧ t ) → u
W rzeczywistości rozwiązanie klauzuli celu z klauzulą określoną w celu utworzenia nowej klauzuli celu jest podstawą reguły wnioskowania rozdzielczości SLD , używanej w implementacji języka programowania logicznego Prolog .
W programowaniu logicznym klauzula określona zachowuje się jak procedura redukcji celu. Na przykład klauzula Horn napisana powyżej zachowuje się jak procedura:
- aby pokazać u , pokaż p i pokaż q i ... i pokaż t .
Aby podkreślić to odwrotne użycie klauzuli, często zapisuje się ją w odwrotnej formie:
- u ← ( p ∧ q ∧ ... ∧ t )
W Prologu jest to zapisane jako:
u :- p, q, ..., t.
W programowaniu logicznym obliczenia i ocena zapytań są wykonywane przez reprezentację negacji problemu do rozwiązania jako klauzulę celu. Na przykład problem rozwiązania egzystencjalnie skwantyfikowanej koniunkcji literałów pozytywnych:
- ∃ X ( p ∧ q ∧ ... ∧ t )
jest reprezentowana przez negację problemu (zaprzeczanie, że ma rozwiązanie) i przedstawienie go w logicznie równoważnej formie klauzuli celu:
- ∀ X ( fałsz ← p ∧ q ∧ ... ∧ t )
W Prologu jest to zapisane jako:
:- p, q, ..., t.
Rozwiązanie problemu sprowadza się do wyprowadzenia sprzeczności, którą reprezentuje zdanie puste (lub „fałsz”). Rozwiązaniem problemu jest zastąpienie zmiennych w klauzuli celu terminami, które można wydobyć z dowodu sprzeczności. Używane w ten sposób klauzule celu są podobne do zapytań łączących w relacyjnych bazach danych, a logika klauzuli Horn jest równoważna mocy obliczeniowej z uniwersalną maszyną Turinga .
Notacja Prologu jest w rzeczywistości niejednoznaczna, a termin „klauzula celu” jest czasami używany niejednoznacznie. Zmienne w klauzuli celu można odczytywać jako uniwersalnie lub egzystencjalnie skwantyfikowane, a wyprowadzenie „fałszu” może być zinterpretowane jako wyprowadzenie sprzeczności lub wyprowadzenie pomyślnego rozwiązania problemu do rozwiązania.
Van Emden i Kowalski (1976) zbadali własności modelu teoretycznego klauzul Horna w kontekście programowania logicznego, wykazując, że każdy zestaw określonych klauzul D ma unikalny minimalny model M . Formuła atomowa A jest logicznie implikowana przez D wtedy i tylko wtedy, gdy A jest prawdziwe w M . Wynika z tego, że problem P reprezentowany przez egzystencjalnie skwantyfikowaną koniunkcję literałów dodatnich jest logicznie implikowany przez D wtedy i tylko wtedy, gdy P jest prawdziwe w M . Semantyka modelu minimalnego klauzul Horna stanowi podstawę semantyki modelu stabilnego programów logicznych.