Clause de Horn

En logique, en particulier en calcul propositionnel, une clause de Horn est une clause comportant au plus un littéral positif. Il existe donc trois types de clauses de Horn : celles qui comportent un littéral positif et au moins un littéral négatif, appelées clauses de Horn strictes ; celles qui comportent un littéral positif et aucun littéral négatif, appelées clauses de Horn positives ; celles qui ne comportent que des littéraux négatifs, appelées clauses de Horn négatives. De plus toute clause de Horn est de la forme (qui peut aussi s'écrire sous la forme ) . Les clauses de Horn forment un sous–ensemble des formes normales disjonctives dans lesquelles un seul terme est positif. La dénomination « clause de Horn » vient du nom du logicien Alfred Horn qui, le premier, met en évidence l’intérêt de telles clauses en 1951 dans l’article « On sentences which are true of direct unions of algebras » publié dans le Journal of Symbolic Logic, numéro 16, pages 14 à 21. Que peut–on représenter avec des clauses de Horn ? Les clauses de Horn strictes énonçant sont équivalentes à . Intuitivement, elles représentent des règles « si ... alors ... » et permettent de déduire de nouveaux faits à partir de faits existants ; Les clauses de Horn positives sont appelées faits. Il s’agit en effet de variables propositionnelles qui représentent intuitivement des propositions élémentaires qui sont soit vraies soit fausses. Par exemple, « L'épice est une drogue » est un fait ; Les clauses de Horn négatives représentent des buts à atteindre, i.e. des questions. En effet, si l’on veut prouver , alors q est le but de la résolution. Or on peut se ramener, via le principe de déduction en appliquant une technique d’inconsistance, à . La clause est une clause de Horn négative qui modélise bien le but à atteindre. Les formes normales composées de clauses de Horn sont un cas particulier de formes normales pour lesquelles on connait des méthodes de résolution efficaces. En effet le problème de la satisfiabilité d’un ensemble de clauses de Horn — aussi appelé HORN–SAT — est dans la classe P et complet pour cette classe.

À propos de ce résultat

Cette page est générée automatiquement et peut contenir des informations qui ne sont pas correctes, complètes, à jour ou pertinentes par rapport à votre recherche. Il en va de même pour toutes les autres pages de ce site. Veillez à vérifier les informations auprès des sources officielles de l'EPFL.

Concepts associés (9)

Cours associés (1)

Séances de cours associées (11)

CS-550: Formal verification

We introduce formal verification as an approach for developing highly reliable systems. Formal verification finds proofs that computer systems work under all relevant scenarios. We will learn how to u

En logique mathématique, la règle de résolution ou principe de résolution de Robinson est une règle d'inférence logique qui généralise le modus ponens. Cette règle est principalement utilisée dans les systèmes de preuve automatiques, elle est à la base du langage de programmation logique Prolog. La règle du modus ponens s'écrit et se lit : de p et de "p implique q", je déduis q. On peut réécrire l'implication "p implique q" comme "p est faux ou q est vraie". Ainsi, la règle du modus ponens s'écrit .

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 : tandis qu'une clause disjonctive est de la forme : où les li 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.

Moteurs d'inférence : Clauses de résolution et de corne CS-330: Artificial intelligence

Couvre les moteurs d'inférence basés sur la résolution, les clauses Horn, le filtrage et l'unification de l'intelligence artificielle.

Étapes d'élimination des quantificateurs pour Presburger Arithmetic CS-550: Formal verification

Explore les étapes d'élimination des quantificateurs pour Presbourger Arithmetic, en mettant l'accent sur les techniques permettant de simplifier et d'éliminer efficacement les quantificateurs.

Proposition de résolution CS-550: Formal verification

Explore l'exhaustivité dans la logique propositionnelle, la résolution sur les clauses, la forme conjonctive, la résolution unitaire, les solveurs SAT et la génération de preuves.