Règle de résolutionEn 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 .
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 : 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.
DatalogDatalog est un langage de requête et de règles pour les bases de données déductives. Il correspond à un sous ensemble de Prolog. Ses origines remontent aux débuts de la programmation logique. Datalog a la syntaxe suivante.
Problème SATvignette|Une instance du Sudoku peut être transformée en une formule de logique propositionnelle à satisfaire. Une assignation des variables propositionnelles donne une grille complétée. En informatique théorique, le problème SAT ou problème de satisfaisabilité booléenne est le problème de décision, qui, étant donné une formule de logique propositionnelle, détermine s'il existe une assignation des variables propositionnelles qui rend la formule vraie. Ce problème est important en théorie de la complexité.
