Översikt

En Horn-klausul är en speciell form av logisk klausul som innehåller högst en positiv bokstavlig sats (literal) och eventuellt flera negativa. Begreppet introducerades av Alfred Horn 1951 och utgör en viktig klass i både propositionell och predikatlogik. Horn-klausuler är lättare att behandla algoritmiskt än allmänna klausuler, eftersom vissa slutledningsoperationer bevarar formen hos Horn-klausuler och därmed ger effektivare bevisprocedurer.

{\displaystyle \neg p\lor \neg q\vee \cdots \vee \neg t\vee u}

Definition och vanliga typer

Formellt kan en Horn-klausul beskrivas som en disjunktion av literaler där som mest en är positiv. Med andra ord är en Horn-klausul av formen ¬p ∨ ¬q ∨ ... ∨ u, där u kan vara frånvarande. Det finns tre vanliga underkategorier:

  • Bestämd klausul (definite clause): innehåller exakt en positiv literal, till exempel ¬p ∨ ¬q ∨ u. I logisk programmering skrivs detta ofta som en implikation (p ∧ q ∧ ... → u) eller i bakåtriktad form u :- p, q, ... . {\displaystyle u}
  • Faktum (fact): en klausul som endast är en positiv literal, exempelvis u; detta representerar ett grundläggande påstående utan villkor. {\displaystyle \neg p\lor \neg q\vee \cdots \vee \neg t}
  • Målklausul eller goal-clause: en Horn-klausul utan positiva literaler, alltså en ren konjunktion av nekande literaler eller, om man tar negationen, ett mål som skall bevisas. Sådana klausuler används ofta för att uttrycka frågor eller negationer av mål som ska visas. {\displaystyle \neg {\text{human}}(X)\lor {\text{mortal}}(X)}

Formella samband och kvantifiering

I predikatlogik antas variabler i en Horn-klausul vanligtvis vara universellt kvantifierade över hela satsen. Till exempel är en klausul ¬human(X) ∨ mortal(X) ekvivalent med ∀X (human(X) → mortal(X)). På så sätt kan Horn-klausuler enkelt uttrycka regler av typen "om villkor så slutsats" som är centrala för deduktiva system. {\displaystyle \forall X(\neg {\text{human}}(X)\lor {\text{mortal}}(X))} {\displaystyle \forall X({\text{human}}(X)\rightarrow {\text{mortal}}(X)).}

Historik och teoretisk utveckling

Alfred Horn formulerade ursprungligen dessa klausuler i mitten av 1900-talet. Sedan dess har Horn-klausuler fått stor betydelse, framför allt efter arbeten som visade deras praktiska och modellteoretiska egenskaper. Ett framträdande resultat är Van Emden och Kowalskis analys från 1976 som visar att en mängd bestämda klausuler alltid har en entydig minimal modell: den minsta mängd atomära fakta som gör alla klausuler sanna. Detta ger en tydlig semantisk grund för hur logiska program ska tolkas och ligger bakom senare semantiker för mer avancerade programtyper. {\displaystyle (p\wedge q\wedge \cdots \wedge t)\rightarrow u}

Tillämpningar i logisk programmering och automatisk slutledning

Horn-klausuler är själva ryggraden i logisk programmering. I praktiska system skrivs regler ofta som bestämda klausuler och körs genom målorienterad slutledning. Prolog, ett av de mest kända logiska programmeringsspråken, använder bestämda klausuler och SLD-upplösning (Selective Linear Definite clause resolution) för att reducera mål till enklare delmål tills ett faktum uppnås eller ett misslyckande konstateras. Denna mekanism bygger direkt på att upplösning mellan Horn-klausuler ger en ny Horn-klausul, vilket bevarar problemets struktur under beräkningen. {\displaystyle u} {\displaystyle p} q

Algoritmiska och komplexitetsrelaterade aspekter

Ur beräkningssynpunkt är beslutet om satisfierbarhet för propositionella Horn-klausuler betydligt enklare än för allmän satisfierbarhet. Problemet HORNSAT (saker som gör en konjunktion av propositionella Horn-klausuler sann) kan lösas i linjär tid och klassificeras som P-komplett i komplexitetsteori. Detta står i kontrast mot det allmänna Booleska satisfierbarhetsproblemet (SAT) som är NP-komplett. För första ordningens Horn-klausuler blir situationen annorlunda: satisfierbarhetsproblem och härledbarhet är i allmänhet mer komplicerade och i många fall oavgörbara. {\displaystyle \cdots }

Viktiga egenskaper och skillnader

Några egenskaper som särskiljer Horn-klausuler från mer generella klausuler är:

  • Bevarandet under upplösning: upplösaren av två Horn-klausuler är fortfarande en Horn-klausul, vilket möjliggör effektiva slutledningsprocedurer.
  • Existensen av en minimal modell för uppsättningar av bestämda klausuler, vilket ger en entydig semantisk tolkning av program bestående av sådana klausuler.
  • Lättare algoritmisk hantering i propositionella fall (linjär tid) jämfört med allmän SAT.

Trots dessa fördelar finns begränsningar: Horn-klausuler kan inte uttrycka alla Booleska funktioner eller logiska samband utan att falla utanför Horn-formen, och när man går upp i uttryckskraft (till exempel genom att lägga till fri användning av negation i huvudledet) förloras många av de effektiva egenskaperna.

Praktiska exempel och vidare läsning

Som konkret exempel kan man tänka sig ett enkelt regelsystem för arvsrelation: "Om X är en människa så är X dödlig" kan skrivas som en bestämd klausul och behandlas av en Prolog-motor för att härleda individuella påståenden. För vidare teknisk fördjupning kan man läsa om disjunktioner och deras roll i logik via disjunktion, om principerna för logisk programmering, och om implementeringar i språk som Prolog. För komplexitetsrelaterade jämförelser se vidare SAT-problemet och klassificeringen av svårighetsgrad i NP-teori. {\displaystyle t} {\displaystyle u\leftarrow (p\land q\land \cdots \land t)}