Un cadre proof-théorique dans lequel les règles d'inférence peuvent s'appliquer à n'importe quelle profondeur à l'intérieur des expressions logiques plutôt qu'au seul niveau racine ; l'inférence profonde favorise des systèmes de preuve symétriques, locaux et souvent plus compacts comme le Calculus of Structures.

Principe

Autoriser l'application de règles à l'intérieur de sous-formules arbitraires : les contextes d'inférence ne sont pas limités au niveau supérieur, ce qui permet des réécritures locales compressant ou symétrisant la structure des preuves, à condition que des propriétés méta (soundness, élimination des coupures) soient préservées par une conception de règles et des contrôles structuraux adéquats.

Démonstration

Dans un système à inférence profonde pour la logique propositionnelle, une règle remplaçant A∨(B∧C) par (A∨B)∧(A∨C) peut s'appliquer à l'intérieur de contextes plus larges, p. ex. X[…], de sorte qu'on réécrit une sous-formule imbriquée directement sans la remonter au niveau supérieur ; cette localité peut donner des dérivations plus courtes que les systèmes en sequent.

Mauvaise application

Permettre naïvement des réécritures internes arbitraires sans restrictions peut briser la terminaison ou la correction (boucles de dérivation ou dérivations d'énoncés non valides) ; concevoir des règles profondes non restreintes pour des logiques à comportement structurel complexe peut produire des cuts non confluents ou non éliminables.

Conséquence

L'inférence profonde fournit souvent des preuves plus courtes et plus symétriques, soutient une localité fine propice au parallélisme et permet des systèmes uniformes pour logiques classiques et non classiques difficiles à représenter de manière compacte en sequent.

Inversion

L'inverse est l'inférence superficielle (systèmes traditionnels en sequent ou en déduction naturelle) où les règles opèrent uniquement au niveau extérieur ; les systèmes superficiels favorisent une lecture opérationnelle claire et des stratégies de normalisation établies mais peuvent produire des preuves plus longues et séquentielles.

Limite

S'applique lorsque les connecteurs logiques et les règles structurelles autorisent des réécritures locales internes et où l'on peut imposer des contrôles méta-théoriques ; ce n'est pas une solution universelle — certains systèmes exigent des contraintes structurelles supplémentaires ou un appareil d'étiquetage pour retrouver des propriétés comme l'élimination des coupures et la décidabilité.

Tension sémantique

Tension entre inférence profonde et calculs en sequent : l'inférence profonde privilégie localité et symétrie au prix d'une méta-théorie plus complexe, tandis que les calculs en sequent mettent l'accent sur la composition modulaire des règles et des preuves de normalisation plus simples ; les deux approches échangent longueur de preuve, clarté et contrôle proof-théorique.

Synthèse

L'Inférence Profonde généralise où et comment les règles s'appliquent à l'intérieur des formules : en autorisant des réécritures locales et profondes on obtient des systèmes de preuve compacts et symétriques qui dévoilent parallélisme et modularité, mais l'approche requiert une conception soignée des règles et des contraintes structurelles pour préserver son sens et ses propriétés.