Clause (logique)

Une clause en logique booléenne est une conjonction ou une disjonction de littéraux. On parle respectivement de clause conjonctive et de clause disjonctive. Sans précision c'est le plus souvent la clause disjonctive qui est sous-entendue.

En calcul propositionnel, une clause conjonctive est de la forme :

$l_{1}\wedge l_{2}\wedge \cdots \wedge l_{n},$

tandis qu'une clause disjonctive est de la forme :

$l_{1}\vee l_{2}\vee \cdots \vee l_{n},$

où les l_i sont des littéraux, c'est-à-dire des atomes ou des négations d'atomes.

La clause disjonctive vide, c'est-à-dire la disjonction de 0 littéraux, s'évalue toujours à faux. En déduction naturelle, on démontre que la clause vide n'est pas dérivable, ce qui vaut ainsi preuve de la cohérence de ce système d'axiomes.

Voir aussi

• Clause de Horn