Definition

En Horn-klausul er en disjunktion af literaler, hvor højst én af literalerne er positiv. Med andre ord må en Horn-klausul indeholde nul eller ét positivt atom, mens resten (hvis nogen) er negationer af atomære formler. Navnet stammer fra Alfred Horn, som beskrev denne form i 1951.

Formelt er en literal enten et atom A eller dennes negation ¬A. En Horn-klausul kan derfor skrives som

bestemt sætning: ¬ p ∨ ¬ q ∨ ⋯ ∨ ∨ ¬ t ∨ u {\displaystyle \neg p\lor \neg q\vee \cdots \vee \neg t\vee u} {\displaystyle \neg p\lor \neg q\vee \cdots \vee \neg t\vee u}

Typer af Horn-klausuler

  • Bestemt klausul (definite clause): én positiv literal og nul eller flere negative literaler. Ofte skrevet som implication (p ∧ q ∧ … ∧ t) → u.
  • Faktum: en bestemt klausul uden negative literaler, altså blot et positivt atom (u i eksemplet nedenfor).
  • Målklausul (goal clause eller clause mål): en Horn-klausul uden positiv literal; dvs. kun negative literaler. Sådanne bruges ofte som forespørgsler eller mål i bevisprocedurer.

faktum: u {\displaystyle u} {\displaystyle u}

målsætningsklausul: ¬ p ∨ ¬ q ∨ ∨ ⋯ ∨ ¬ t {\displaystyle \neg p\lor \neg q\vee \cdots \vee \neg t} {\displaystyle \neg p\lor \neg q\vee \cdots \vee \neg t}

Førsteordens Horn-klausuler og kvantificering

I førsteordenslogik er variabler i en klausul typisk implicit universelt kvantificerede over hele klausulen. For eksempel kan en førsteordens Horn-klausul skrives som:

¬ menneske ( X ) ∨ dødelig ( X ) {\displaystyle \neg {\text{human}}(X)\lor {\text{mortal}}(X)} {\displaystyle \neg {\text{human}}(X)\lor {\text{mortal}}(X)}

Dette står for

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

hvilket logisk svarer til implikationen

∀ X ( menneske ( X ) → dødelig ( X ) ) . {\displaystyle \forall X({\text{human}}(X)\rightarrow {\text{mortal}}(X)). } {\displaystyle \forall X({\text{human}}(X)\rightarrow {\text{mortal}}(X)).}

Horn-klausulers rolle i logik og automatiseret bevisførelse

Horn-klausuler er centrale i konstruktiv logik og beregningslogik. En væsentlig effektivitetsegenskab er, at resolventen af to Horn-klausuler igen er en Horn-klausul. Desuden er resolventen af en målklausul og en bestemt klausul en målklausul. Disse bevarelsesegenskaber er grundlaget for effektive bevisprocedurer, fordi de tillader specialiserede opløsningsalgoritmer (f.eks. SLD-opløsning) som undgår eksplosionen i kompleksitet, der kan opstå i fuld førsteordensopløsning.

Horn-klausuler i logisk programmering

Horn-klausuler udgør det syntaktiske grundlag for logisk programmering, og særligt for sproget Prolog. En bestemt klausul skrives ofte i implicationsform:

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

Fra et implementeringssynspunkt fungerer en bestemt klausul som en målreduktionsprocedure: for at bevise u skal man bevise p, q, …, t. Denne bagudrettede søgning (backward chaining) er netop hvad SLD-opløsning gør — opløsning af en målklausul med en bestemt klausul producerer en ny målklausul, og processen fortsættes, indtil målet er opfyldt eller ingen flere opløsninger er mulige.

I logisk programmering skriver man ofte klausuler i bagudvendt form:

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

I Prolog skrives dette som:

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

Bemærk at Prolog-notationen i praksis er tvetydig med hensyn til kvantificering: i førsteordenslogik er variabler i en klausul universelt kvantificerede, mens en forespørgsel (et mål) typisk behandles som at der søges efter eksistentielle bindingsmuligheder (variable som skal instansieres for at opfylde målet).

Semantik: minimale modeller og Herbrand-model

Van Emden og Kowalski (1976) viste vigtige modelteoretiske egenskaber for sæt af definitive (bestemte) klausuler. Hvert sæt D af definitive klausuler har en entydig minimal model M (den mindst mulig model i forståelsen af sættets sande atomformler). En atom A er logisk impliceret af D netop når A er sand i denne minimale model M. For logisk programmering svarer denne model ofte til den mindste Herbrand-model.

Dette betyder også, at et problem P, repræsenteret som en eksistentielt kvantificeret konjunktion af positive literaler, er logisk impliceret af D netop når P er sand i M. Den minimale modelsemantik for Horn-klausuler er desuden grundlag for videre semantiske tilgange (f.eks. stable model semantics og well-founded semantics), som håndterer negation og ikke-monotone aspekter i logiske programmer.

Kompleksitet og beslutbarhed

Propositionelle Horn-klausuler har gunstige kompleksitetsegenskaber: satisfiability-problemet for propositionelle Horn-formler (ofte kaldet HORNSAT) er i P og kan løses i lineær tid (f.eks. ved en baglæns kædetrækning eller ved unit propagation). Faktisk er HORNSAT P-komplet, hvilket betyder, at det er et typisk problem i klassen P med hensyn til (parallel) kompleksitet.

Til sammenligning er det generelle Booleske tilfredsstillelsesproblem SAT NP-komplet. Tilfredsstillelse for Horn-klausuler i første ordens logik er generelt ikke afgørlig (uudsigeligt), fordi førsteordenslogik i almindelighed fører til uafgørlighed.

Praktiske konsekvenser og anvendelser

  • Effektiv automatiseret bevisførelse: Horn-fragmentets bevarelsesegenskaber gør det muligt at bygge hurtige og målrettede opløsningsprocedurer (SLD), som anvendes i Prolog-implementeringer.
  • Logisk programmering: mange programmer og videnbaser skrives naturligt som sæt af Horn-klausuler (regler og facts), hvilket gør udtrækning af fakta og forespørgsler effektiv.
  • Databasesystemer: visse databaseforespørgsler (f.eks. Datalog) kan udtrykkes ved Horn-klausuler, og evalueres effektivt ved fixpunktberegning.

Eksempel på brug i Prolog

Givet klausulen

at vise u {\displaystyle u}{\displaystyle u} , vise p {\displaystyle p}{\displaystyle p} og vise q {\displaystyle q}q og ⋯ {\displaystyle \cdots } {\displaystyle \cdots }og show t {\displaystyle t} {\displaystyle t}

kan Prolog-syntaksen u :- p, q, ..., t. bruges til at angive reglen, og en forespørgsel ?- u. vil forsøge at reducere målet til underordnede mål p, q, …, t ved SLD-opløsning.

Afsluttende bemærkninger

Horn-klausuler udgør et fleksibelt og beregningsvenligt fragment af logikken, med stærke forbindelser til praktiske systemer som Prolog, Datalog og enkelte databaseoptimeringsmetoder. Deres formelle egenskaber — bevarelsen ved opløsning, eksistensen af en unik minimal model for definitive programmer og effektiviteten af HORNSAT — forklarer den udbredte anvendelse i både teori og praksis.