L'inférence est le mécanisme général par lequel on déduit de nouvelles propositions à partir de propositions existantes selon l'ensemble de règles d'une logique ; elle précise comment les conclusions découlent des prémisses dans un formalisme donné.

Principe

Appliquer des règles de transformation qui préservent la relation de correction (vérité, validité, probabilité, etc.) par rapport à la sémantique choisie, de sorte que les formules dérivées soient justifiées par les prémisses et les règles.

Démonstration

À partir des prémisses « Tous les humains sont mortels » et « Socrate est humain », appliquer l'instanciation universelle puis modus ponens pour inférer « Socrate est mortel » ; en logique propositionnelle, déduire B à partir de A→B et A par modus ponens.

Mauvaise application

Utiliser une règle d'inférence en dehors de ses préconditions (par exemple affirmer le conséquent en logique classique) ou transposer des principes classiques dans une logique non compatible, produisant des conclusions invalides.

Conséquence

Bien appliquée, l'inférence produit des chaînes d'énoncés justifiés permettant preuves, raisonnement automatique, calcul des conséquences et propagation de contraintes dans un système formel.

Inversion

La perspective inverse consiste à traiter des conclusions comme hypothèses et à inférer les prémisses (abduction) ou à inverser la direction du raisonnement (recherche de preuve en arrière) ; cela contraste avec l'application inférentielle directe.

Limite

Ici, l'inférence se réfère à une déduction formelle régie par des règles dans des systèmes syntaxiques ou sémantiques ; elle exclut la généralisation inductive informelle sauf si elle est formalisée dans une logique probabiliste ou inductive.

Tension sémantique

Il existe une tension entre la dérivabilité syntaxique (ce qui peut être prouvé par des règles) et l'entailment sémantique (ce qui est vrai dans tous les modèles) ; une formule peut être sémantiquement conséquence sans être prouvable dans un système incomplet.

Synthèse

L'inférence est la transformation régie par des règles qui convertit des prémisses en conclusions sous contraintes explicites de correction ; elle constitue le noyau opérationnel reliant prémisses, règles et conclusions dans la construction de preuves et le raisonnement automatique.