Horn-clausule

In de logica is een Horn-clausule (Engels: Horn clause) een clausule, een disjunctie van literalen, met ten hoogste 1 positieve literaal. Ze zijn vernoemd naar de logicus Alfred Horn, die deze in 1951 behandelde in zijn publicatie "On sentences which are true of direct unions of algebras" in Journal of Symbolic Logic.

Horn-clausules zijn van belang bij logisch programmeren en intuïtionistische logica (ook constructieve logica genoemd).

Varianten

• Een Horn-clausule met precies 1 positieve literaal wordt een definiete clausule genoemd.
• Een Horn-clausule zonder positieve literalen wordt soms een doelclausule genoemd, met name bij logisch programmeren.
• Een Horn-formule is een formule in conjunctieve normaalvorm waarbij alle clausules Horn-clausules zijn. Anders gezegd: het is een conjunctie van Horn-clausules.
• Een duale Horn-clausule is een clausule met ten hoogste 1 negatieve literaal.

Voorbeelden

• Een voorbeeld van een Horn-clausule is:

$\neg p\lor \neg q\vee \cdots \vee \neg t\vee u$

Deze formule kan ook geschreven worden als een implicatie:

$(p\wedge q\wedge \cdots \wedge t)\rightarrow u$

Toepassingen

Bewijzen van stellingen

Horn-clausules zijn relevant bij het automatisch bewijzen van stellingen in resolutie in eerste-ordelogica aangezien de resolutie van twee Horn-clausules een Horn-clausule is. Daarnaast resulteert de resolutie van een doelclausule en een definiete clausule opnieuw in een doelclausule. Bij het automatisch bewijzen van stellingen kan deze eigenschap gebruikt worden om efficiënter stellingen te bewijzen (dit kan door deze te representeren als een doelclausule).

De resolutie van een doelclausule met een definiete clausule om een nieuwe doelclausule te produceren is de basis van SLD-resolutie, die gebruikt wordt om logisch programmeren te implementeren en de programmeertaal Prolog. Bij logisch programmeren gedraagt een Horn clausule zich als een procedure waarbij doelen stuk voor stuk worden bewezen. De eerdergenoemde Horn-clausule kan geschreven als de procedure:

om $u$ aan te tonen, toon aan dat $p$ geldt en toon aan dat $q$ geldt en $\cdots$ en toon aan dat $t$ geldt.

Om dit 'omgekeerde' gebruik van de clausule te benadrukken, wordt deze ook geschreven als:

$u\leftarrow (p\land q\land \cdots \land t)$

De pijl naar links geeft hierbij aan dat $u$ het gevolg is van $p$, $q$, $\ldots$ en $t$.

Horn-vervulbaarheid

Horn-clausules zijn ook relevant in de complexiteitstheorie waarbij het vinden van een toekenning van waar of onwaar aan de atomaire formules om een conjunctie van Horn-clausules waar te maken een P-volledig probleem is. Dit probleem wordt soms HORNSAT genoemd. Dit probleem is de P-versie van het vervulbaarheidsprobleem (SAT) dat een bekend NP-volledig probleem is.

Externe links

• (en) Horn Clause, MathWorld