Horn-Klausul

En Horn-klausul är en logisk disjunktion av bokstäver där högst en av bokstäverna är positiv och alla andra är negativa. Den är uppkallad efter Alfred Horn som beskrev dem i en artikel 1951.

En Horn-klausul med exakt en positiv bokstavlig mening är en bestämd klausul, en bestämd klausul utan negativa bokstavliga meningar kallas ibland för ett "faktum", och en Horn-klausul utan en positiv bokstavlig mening kallas ibland för en målklausul. Dessa tre typer av Horn-klausuler illustreras i följande exempel på en proposition:

bestämd sats: ¬ p ∨ ¬ q ∨ ⋯ ∨ ¬ t ∨ u {\\displaystyle \neg p\lor \neg q\vee \cdots \vee \neg t\vee u} $\neg p\lor \neg q\vee \cdots \vee \neg t\vee u$

faktum: u {\displaystyle u} $u$

målklausul: ¬ p ∨ ¬ q ∨ ⋯ ∨ ¬ t {\displaystyle \neg p\lor \neg q\vee \cdots \vee \neg t} $\neg p\lor \neg q\vee \cdots \vee \neg t$

I det icke-propositionella fallet är alla variabler i en sats implicit universellt kvantifierade med räckvidd för hela satsen. Till exempel:

¬ människa ( X ) ∨ dödlig ( X ) {\displaystyle \neg {\text{human}}(X)\lor {\text{mortal}}(X)} $\neg {\text{human}}(X)\lor {\text{mortal}}(X)$

står för:

∀ X ( ¬ mänsklig ( X ) ∨ dödlig ( X ) ) {\displaystyle \forall X(\neg {\text{human}}(X)\lor {\text{mortal}}(X))} $\forall X(\neg {\text{human}}(X)\lor {\text{mortal}}(X))$

vilket är logiskt likvärdigt med:

∀ X ( människa ( X ) → dödlig ( X ) ) . {\displaystyle \forall X({\text{human}}(X)\rightarrow {\text{mortal}}(X)). } $\forall X({\text{human}}(X)\rightarrow {\text{mortal}}(X)).$

Hornklausuler spelar en grundläggande roll inom konstruktiv logik och beräkningslogik. De är viktiga för automatiserad teoremprövning genom första ordningens upplösning, eftersom upplösaren av två Horn-klausuler i sig själv är en Horn-klausul, och upplösaren av en målklausul och en bestämd klausul är en målklausul. Dessa egenskaper hos Horn-klausuler kan leda till större effektivitet när det gäller att bevisa en sats (representerad som negationen av en målklausul).

Hornklausuler ligger också till grund för logisk programmering, där det är vanligt att skriva bestämda klausuler i form av en implikation:

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

Upplösningen av en målklausul med en bestämd klausul för att skapa en ny målklausul ligger till grund för SLD-upplösningsregeln, som används för att genomföra logisk programmering och programmeringsspråket Prolog.

I logisk programmering fungerar en bestämd klausul som en målreduktionsprocedur. Till exempel beter sig Horn-klausulen ovan som en procedur:

att visa u {\displaystyle u} $u$ , visa p {\displaystyle p} $p$ och visa q {\displaystyle q} och ⋯ {\displaystyle \cdots } $\cdots$ och visa t {\displaystyle t} $t$ .

För att betona denna bakåtriktade användning av klausulen skrivs den ofta i bakåtriktad form:

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

I Prolog skrivs detta som:

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

Prolog-notationen är faktiskt tvetydig, och termen "målklausul" används ibland också på ett tvetydigt sätt. Variablerna i en målklausul kan tolkas som universellt eller existentiellt kvantifierade, och att härleda "false" kan tolkas antingen som att härleda en motsägelse eller som att härleda en lyckad lösning av det problem som skall lösas.

Van Emden och Kowalski (1976) undersökte de modellteoretiska egenskaperna hos Horn-klausuler i samband med logisk programmering och visade att varje uppsättning bestämda klausuler D har en unik minimimodell M. En atomformel A är logiskt implicerad av D om och endast om A är sann i M. D innebär att ett problem P som representeras av en existentiellt kvantifierad konjunktion av positiva bokstäver är logiskt implicerad av D om och endast om P är sann i M. Den minimala modellsemantiken för Horn-klausuler utgör grunden för den stabila modellsemantiken för logiska program.

Propositionella Horn-klausuler är också av intresse för beräkningskomplexitet, där problemet med att hitta sanningsvärden som gör en konjunktion av propositionella Horn-klausuler sann är ett P-komplett problem (som faktiskt kan lösas på linjär tid), ibland kallat HORNSAT. (Det obegränsade Boolska uppfyllbarhetsproblemet är dock ett NP-komplett problem). Tillfredsställelse av Horn-klausuler av första ordningen är oavgörbar.

Frågor och svar

F: Vad är en hornklausul?

S: En Horn-klausul är en logisk disjunktion av bokstäver där högst en av bokstäverna är positiv och alla andra är negativa.

Fråga: Vem beskrev dem först?

Svar: Alfred Horn beskrev dem för första gången i en artikel 1951.

Fråga: Vad är en bestämd sats?

Svar: En Horn-klausul med exakt en positiv bokstavsdel kallas en bestämd klausul.

Fråga: Vad är ett faktum?

Svar: En bestämd sats utan några negativa bokstavsord kallas ibland för ett "faktum".

Fråga: Vad är en målklausul?

Svar: En Horn-sats utan en positiv bokstavsdel kallas ibland för en mål-sats.

F: Hur fungerar variabler i icke-propositionella fall?

S: I icke-propositionella fall är alla variabler i en klausul implicit universellt kvantifierade med räckvidd för hela klausulen. Detta innebär att de gäller för varje del av påståendet.

F: Vilken roll spelar Horn-klausuler i konstruktiv logik och beräkningslogik? S: Hornklausuler spelar en viktig roll i automatiserad teoremprövning med hjälp av första ordningens upplösning, eftersom upplösningen mellan två Hornklausuler eller mellan en målklausul och en bestämd klausul kan användas för att skapa större effektivitet när man bevisar något som representeras som negationen av dess målklausul. De används också som grund för logiska programmeringsspråk som Prolog, där de beter sig som målreduktionsprocedurer.