Clausule (logica)

In de logica is een clausule (in het Engels: clause) een eindige disjunctie van literalen, dus met de vorm

${\displaystyle l_{0}\vee l_{1}\vee \ldots \vee l_{n}}$

met ${\displaystyle l_{i}}$ voor ${\displaystyle 0\leq i\leq n}$, een literaal.

Een clausule kan ook leeg zijn. Deze is onwaar aangezien een clausule alleen waar is als een of meer literalen waar zijn. De lege clausule wordt met verscheidene symbolen genoteerd, zoals ${\displaystyle \emptyset ,\,\bot }$ of ${\displaystyle \Box }$.

Notatie met verzamelingen

Een clausule wordt soms ook genoteerd als de verzameling van de erin voorkomemde literalen: de clausule ${\displaystyle l_{0}\vee l_{1}\vee \ldots \vee l_{n}}$ wordt genoteerd als ${\displaystyle \{l_{0},l_{1},\ldots ,l_{n}\}}$. Daarbij worden literalen die meerdere keren voorkomen, slechts eenmaal genoteerd. Ook hoeft men geen rekening te houden met de volgorde waarin de literalen staan (of logische wetten toe te passen om de clausule in een bepaalde vorm te krijgen).

Op vergelijkbare wijze wordt een formule in conjunctieve normaalvorm wel genoteerd als een verzameling clausules: ${\displaystyle \{\{p,q,r\},\{s,t,u\}\}}$, met de afspraak dat dit overeenkomt met ${\displaystyle (p\vee q\vee r)\wedge (s\vee t\vee u)}$.

Overzicht

Sommige clausules met een bepaalde vorm hebben een eigen naam:

• Horn-clausule (Horn clause), een clausule met ten hoogste één positieve literaal.
  • Definiete clausule, een Horn clausule met precies één positieve literaal.
  • Doelclausule, een Horn-clausule zonder positieve literalen (deze term wordt met name bij logisch programmeren gebruikt).
• Duale Horn-clausule, een clausule met ten hoogste één negatieve literaal.
• Unit clause, een clausule met één literaal.