Règle de résolution | EPFL Graph Search

Ê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 GraphSearch.

Découvrez-en plus sur les applications Graph.

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 . La règle de résolution, elle, généralise la règle du modus ponens car elle s'applique sur des clauses quelconques. Une clause est une formule qui est une disjonction (un "ou") de littéraux (une proposition atomique ou une proposition atomique précédée d'une négation). Par exemple est une clause avec deux littéraux ("non p" et "q"). Ainsi, en logique propositionnelle, la règle de résolution s'écrit : Autrement dit, étant donné deux clauses et , on en déduit . La formule déduite, c'est-à-dire est appelé résolvant de et . Bien sûr, l'application de la règle est donnée à permutation près des littéraux. Par exemple : où dénote la contradiction (clause vide). En logique des prédicats les formules atomiques sont de la forme où est un symbole de prédicat et les sont des termes composés de constantes, de variables et de symboles de fonctions. La règle de résolution en logique des prédicats est similaire à la règle de résolution en logique propositionnelle mais les formules atomiques partagées par deux clauses ne doivent pas être identiques mais unifiables. Deux formules atomiques sont unifiables s'il existe une substitution des variables par des termes qui rend les deux formules identiques (voir unification). Par exemple : est une application de la règle de résolution en logique des prédicats. Elle se lit : de "P(a)" et de "(pour tout x) non P(x) ou Q(x)", je déduis "Q(a)". Ici, la formule atomique et la formule atomique sont unifiables avec la substitution . Plus généralement, la règle de résolution en logique des prédicats est : où est un unificateur principal des formules atomiques et .

À 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 (24)

Cours associés (4)

Séances de cours associées (27)

Méthode des tableaux

vignette|200px|Représentation graphique d'un tableau propositionnel partiellement construit En théorie de la démonstration, les tableaux sémantiques sont une méthode de résolution du problème de la décision pour le calcul des propositions et les logiques apparentées, ainsi qu'une méthode de preuve pour la logique du premier ordre. La méthode des tableaux peut également déterminer la satisfiabilité des ensembles finis de formules de diverses logiques. C'est la méthode de preuve la plus populaire pour les logiques modales (Girle 2000).

Unification

vignette|Unifier deux termes, c'est les rendre identiques en remplaçant les variables. En informatique et en logique, l'unification est un processus algorithmique qui, étant donnés deux termes, trouve une substitution qui appliquée aux deux termes les rend identiques. Par exemple, et peuvent être rendus identiques par la substitution et , qui donne quand on l'applique à chacun de ces termes le terme .

Skolem normal form

In mathematical logic, a formula of first-order logic is in Skolem normal form if it is in prenex normal form with only universal first-order quantifiers. Every first-order formula may be converted into Skolem normal form while not changing its satisfiability via a process called Skolemization (sometimes spelled Skolemnization). The resulting formula is not necessarily equivalent to the original one, but is equisatisfiable with it: it is satisfiable if and only if the original one is satisfiable.

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

EE-431: Advanced VLSI design

In this project-based course, students collect hands-on experience with designing full-custom digital VLSI circuits in dynamic logic. They learn to carry out the design and optimization on transistor

CS-330: Artificial intelligence

Introduction aux techniques de l'Intelligence Artificielle, complémentée par des exercices de programmation qui montrent les algorithmes et des exemples de leur application à des problèmes pratiques.

Coq: Introduction

Présente Coq, couvrant la définition des propositions, la démonstration des théorèmes, et l'utilisation de tactiques.

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.

Mise à niveau des dalles: calcul d'épaisseur ENV-140: Fundamentals of geomatics MOOC: Éléments de Géomatique

Couvre les principes de nivellement et de calcul de l'épaisseur de la dalle et de la hauteur du plafond.