Règle d'inférence

Dans un système logique, les régles d'inférence sont les règles qui fondent le processus de déduction, de dérivation ou de démonstration. L'application des règles sur les axiomes du système permet d'en démontrer les théorèmes. Une règle d'inférence est une fonction qui prend un -uplet de formules et rend une formule. Les formules arguments sont appelées « les prémisses » et la formule retournée est appelée la « conclusion ». Les règles d'inférence peuvent également être vues comme des relations liant prémisses et conclusions par lesquelles une conclusion est dite « déductible » ou « dérivable » des prémisses. Si l'ensemble des prémisses est vide, alors la conclusion est appelée un « théorème » ou un « axiome » de la logique. Les règles d'inférences sont en général données dans la forme standard suivante : Prémisse Prémisse Conclusion Cette expression dit que si on se trouve au milieu d'une dérivation logique, où les prémisses ont été déjà obtenues (c'est-à-dire dérivées logiquement des axiomes), alors on peut affirmer que la conclusion est obtenue. Le langage formel utilisé pour décrire les prémisses et la conclusion dépend du système formel ou logique où l'on s'est placé. Dans le cas le plus simple, les formules sont tout simplement des expressions logiques; c'est ainsi le cas pour le modus ponens : A→B ∴B Les règles d'inférence peuvent aussi être formulées de cette manière : un certain nombre de prémisses (peut-être aucune) ; un symbole de dérivation signifiant « infère », « démontre » ou « conclut » ; une conclusion. Cette formulation représente habituellement la vision relationnelle (par opposition à fonctionnelle) d'une règle d'inférence, où le symbole de dérivation représente une relation de démontrabilité existant entre prémisses et conclusion. Les règles d'inférences sont aussi parfois présentées à la manière de cette expression du modus ponens, qui exprime bien la nécessité que les prémisses soient des théorèmes : Si A → B et A, alors B. Les règles d'inférence sont en général formulées comme des « schémas de règles », par l'utilisation de variables universelles.