Une disjonction de littéraux (atomes ou leurs négations) traitée comme une unité syntaxique unique, couramment utilisée dans la forme normale conjonctive (FNC) et comme objet de base pour les procédures de preuve par résolution et les solveurs SAT.

Principe

Une clause encode la contrainte selon laquelle au moins un de ses littéraux doit être vrai ; représenter des formules comme des ensembles de clauses (FNC) permet l'application uniforme des opérations de résolution et de propagation d'unités.

Démonstration

Considérons la clause (¬P ∨ Q ∨ R) et la clause unité (P). Leur résolution produit le résolvant (Q ∨ R). Dans une réfutation par résolution, des étapes successives de résolution sur des clauses peuvent aboutir à la clause vide, indiquant l'insatisfaisabilité.

Mauvaise application

Considérer une clause comme équivalente à une implication dans des contextes où la portée des variables ou les quantificateurs importent (logique du premier ordre) sans renommage, ou appliquer la résolution à des formules non normalisées en FNC, ce qui peut conduire à des erreurs.

Conséquence

Considérer le savoir comme un ensemble de clauses permet des techniques algorithmiques efficaces (propagation d'unités, littéraux surveillés, DPLL/CDCL pour SAT et preuves par résolution) et une représentation modulaire des contraintes propositionnelles.

Inversion

Le point de vue dual est la conjonction de littéraux (un cube) ou le traitement de formules complètes plutôt que de clauses normalisées ; revenir à la structure formulelle arbitraire peut améliorer la lisibilité mais perd l'uniformité exploitée par les algorithmes de résolution.

Limite

Une clause est une forme syntaxique spécifique (disjonction finie de littéraux) ; elle s'applique en contexte propositionnel et au premier ordre (avec variables et quantificateurs implicites) après normalisation et renommage appropriés, et exclut la structure booléenne imbriquée arbitraire sauf si normalisée.

Tension sémantique

La tension existe entre la représentation compacte et adaptée au calcul par clauses et les représentations au niveau des formules qui conservent plus directement la structure et le sens syntaxiques ; les clauses favorisent le calcul tandis que les formules favorisent l'interprétation humaine.

Synthèse

Une clause est une unité syntaxique normalisée — une disjonction finie de littéraux — utilisée pour exprimer des contraintes en FNC particulièrement adaptées à la résolution et aux algorithmes SAT, au prix d'une perte relative de richesse syntaxique.