Êtes-vous un étudiant de l'EPFL à la recherche d'un projet de semestre?
Travaillez avec nous sur des projets en science des données et en visualisation, et déployez votre projet sous forme d'application sur Graph Search.
Concept
Clause de Horn
Résumé
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.
Source officielle
À 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.
Cours associés (1)
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