Horn-clausule

In de logica is een Horn-clausule (Engels: Horn clause) een clausule, een disjunctie van literals, met ten hoogste 1 positieve literal. 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 exact 1 positieve literal wordt een definite clause genoemd.
• Een Horn-clausule zonder positieve literals wordt soms een goal clause 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 dual-Horn clause is een clausule met ten hoogste 1 negatieve literal.

Voorbeelden

• Een voorbeeld van een Horn-clausule is:

$\neg p \or \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 goal clause en een definite clause opnieuw in een goal clause. 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 goal clause).

De resolutie van een goal clause met een definite clause om een nieuw goal clause te produceren is de basis van de SLD-resolutie afleidingsregel die gebruikt wordt om logisch programmeren te implementeren en de programmeertaal Prolog. Bij logisch programmeren gedraagt een Horn clausule zich als een procedure waarbij goals 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 \and q \and \cdots \and 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