Admissibilité de la Règle de Substitution dans les Systèmes de Preuve Cyclique

Informations Fondamentales

• ID de l'article: 2510.14749
• Titre: Admissibilité de la Règle de Substitution dans les Systèmes de Preuve Cyclique
• Auteurs: Kenji Saotome, Koji Nakazawa (Université de Nagoya)
• Classification: cs.LO (Logique)
• Date de publication: 16 octobre 2025
• Lien de l'article: https://arxiv.org/abs/2510.14749

Résumé

Cet article étudie la question de l'admissibilité de la règle de substitution dans les systèmes de preuve cyclique. La règle de substitution complique l'analyse théorique et augmente le coût computationnel de la recherche de preuve, car chaque séquent peut être la conclusion d'une instance de la règle de substitution. L'admissibilité est donc souhaitable tant sur le plan théorique que pratique. Bien que dans les systèmes non-cycliques l'admissibilité soit généralement prouvée par des transformations de preuve locales, ces transformations peuvent détruire la structure cyclique et ne peuvent pas être appliquées directement. Des recherches antérieures ont suggéré que la règle de substitution n'est probablement pas admissible dans le système de preuve cyclique CLKIDω pour la logique du premier ordre avec prédicats inductifs. Cet article prouve que la règle de substitution est admissible dans CLKIDω en présence de la règle de coupure. Notre approche consiste à dérouler les preuves cycliques en formes infinies, à relever la règle de substitution, puis à rétablir les arêtes pour construire des preuves cycliques sans règle de substitution. Si on restreint la substitution à ne pas introduire de symboles de fonction, ce résultat s'étend à une classe plus large de systèmes, incluant CLKIDω sans coupure et les systèmes de preuve cyclique pour la logique de séparation.

Contexte et Motivation de la Recherche

Définition du Problème

Les preuves cycliques sont une extension des arbres de preuve traditionnels qui introduisent des structures cycliques pour raisonner sur les prédicats définis inductivement. La règle de substitution $\frac{\Gamma \vdash \Delta}{\Gamma[\theta] \vdash \Delta[\theta]}$ (Subst) est introduite dans de nombreux systèmes de preuve cyclique pour faciliter la construction de structures cycliques.

Importance du Problème

1. Aspect théorique: La règle de substitution est toujours applicable, ce qui rend l'analyse des preuves complexe
2. Aspect pratique: L'application sans restriction de la règle de substitution augmente le coût computationnel, car de nombreuses substitutions peuvent être appliquées à chaque étape

Limitations des Approches Existantes

Dans les systèmes de preuve non-cycliques, l'admissibilité de la règle de substitution est généralement établie en deux phases:

1. Phase de relèvement: Déplacer la règle de substitution vers le haut
2. Phase d'élimination: Éliminer la règle de substitution aux axiomes

Cependant, dans les systèmes de preuve cyclique, cette approche fait face à des difficultés fondamentales:

• La phase de relèvement peut détruire la relation bourgeon-compagnon (bud-companion relationship)
• La phase d'élimination ne peut pas éliminer la substitution au niveau des bourgeons

Motivation de la Recherche

Brotherston 1 a posé la question de savoir si la règle de substitution est admissible dans CLKIDω, suggérant que dans le cas général, au moins dans le cadre sans coupure, elle n'est probablement pas admissible. Cet article vise à résoudre ce problème ouvert.

Contributions Fondamentales

1. Résultat théorique principal: Preuve que la règle de substitution est admissible dans CLKIDω en présence de la règle de coupure
2. Résultats étendus: Lorsque la substitution est restreinte à la substitution atomique (ne introduisant pas de symboles de fonction d'arité positive), le résultat s'étend à CLKIDω sans coupure
3. Généralisation d'application: Le résultat s'applique à d'autres systèmes de preuve, tels que les systèmes de preuve cyclique pour la logique de séparation
4. Approche novatrice: Proposition d'une stratégie d'élimination en trois étapes par déroulement infini, relèvement de substitution et reconstruction cyclique

Détails de la Méthode

Définition de la Tâche

Étant donné une preuve Pr+ dans CLKIDω contenant la règle de substitution, construire une preuve Pr- ne contenant pas la règle de substitution, de sorte que les deux prouvent le même séquent.

Architecture de la Méthode Fondamentale

Le processus d'élimination de cet article se divise en deux phases principales:

1. Élimination des Substitutions Composées

Définition:

• Substitution atomique: Substitution où les termes ne contiennent que des variables et des constantes
• Substitution composée: Substitution où les termes contiennent des symboles de fonction d'arité positive

Méthode: Éliminer les substitutions composées par les transformations suivantes:

Γ ⊢ Δ
────────────────────────── (Subst)
Γ[x₁:=t₁,...,xₙ:=tₙ] ⊢ Δ[x₁:=t₁,...,xₙ:=tₙ]

Transformer en utilisant une combinaison de règles de coupure, règles d'égalité et règles de quantificateur existentiel, conservant finalement uniquement les substitutions atomiques.

2. Élimination des Substitutions Atomiques

Ceci est l'innovation fondamentale, contenant trois étapes:

Étape 1: Déroulement Cyclique

• Dérouler la preuve cyclique Pr_var+ en preuve infinie Pr^ω
• Définir le mappage f^ω: Seq(Pr^ω) → Seq(Pr_var+) associant les occurrences de séquents

Étape 2: Relèvement de Substitution

• Construire récursivement la preuve LKIDω Pr^ω_d ne contenant pas la règle de substitution à profondeur d
• Utiliser la propriété d'application de substitution (substitution-application property)

Étape 3: Reconstruction Cyclique

• Construire la pré-preuve CLKIDω Pr- à partir de Pr^ω_d
• Sélectionner les bourgeons et compagnons, en assurant la condition de trace globale

Points d'Innovation Technique

1. Fermeture de Substitution Partielle (Partial-substitution Closure)

Définition 10: Étant donné un ensemble de substitutions Θ et un ensemble de variables X, la fermeture de substitution partielle Cps(Θ,X) est le plus petit ensemble satisfaisant:

• Θ ⊆ Cps(Θ,X)
• Pour θ∈Cps(Θ,X) et x,y∈X: θx→y ∈ Cps(Θ,X)
• Pour θ₁,θ₂∈Cps(Θ,X): θ₁θ₂ ∈ Cps(Θ,X)

Propriété clé: Lorsque restreinte aux substitutions atomiques, la fermeture de substitution partielle est finie.

2. Propriété d'Application de Substitution (Substitution-application Property)

Définition 11: Une règle (R) satisfait la propriété d'application de substitution si pour toute instance de règle et substitution atomique θ, il existe une instance d'application de substitution correspondante, préservant la trace.

Lemme 4: CLKIDω et LKIDω satisfont la propriété d'application de substitution.

3. Préservation de la Condition de Trace Globale

Assurer que la preuve reconstruite satisfait la condition de trace globale par le concept de chemins correspondants:

Définition 12: Pour un chemin (eᵢ) dans Pr-, définir le chemin correspondant (e'ⱼ) dans Pr_var+, de sorte que chaque trace infinie progressante soit préservée.

Configuration Expérimentale

Cet article est un travail purement théorique sans expériences au sens traditionnel. La vérification s'effectue par:

Vérification Théorique

1. Preuve constructive: Prouver l'admissibilité par construction explicite d'algorithmes
2. Analyse de contre-exemples: Analyser les cas où l'admissibilité n'est pas satisfaite sous les conditions restreintes
3. Extension de systèmes: Vérifier l'applicabilité des résultats dans d'autres systèmes

Analyse d'Exemples

L'article fournit des exemples concrets de transformations de preuve:

• Figure 1: Preuve cyclique contenant la règle de substitution
• Figure 3: Preuve infinie après déroulement
• Démonstration de l'élimination de la règle de substitution de la preuve cyclique de N(x) ⊢ E(x)∨O(x)

Résultats Expérimentaux

Résultats Théoriques Principaux

Théorème 2 (Admissibilité de la Règle de Substitution dans CLKIDω): Si Γ ⊢ Δ est prouvable dans CLKIDω, alors il est également prouvable dans CLKIDω sans (Subst).

Théorème 3 (Résultat Renforcé pour les Substitutions Atomiques): Si Pr est une preuve de Γ ⊢ Δ dans CLKIDω et Θ(Pr) ne contient que des substitutions atomiques, alors il existe une preuve sans (Subst) contenant uniquement les règles apparaissant dans Pr.

Résultats Étendus

Théorème 4 (Admissibilité dans les Systèmes sans Coupure): Dans CLKIDω^- (CLKIDω sans coupure), la règle de substitution atomique est admissible.

Théorème 5 (Application à la Logique de Séparation): La règle de substitution est admissible dans CSLω et CSLω^-.

Découvertes Théoriques

1. Rôle clé de la règle de coupure: L'élimination des substitutions composées nécessite la règle de coupure
2. Universalité de la substitution atomique: L'élimination de la substitution atomique s'applique à une classe plus large de systèmes
3. Caractère restrictif des symboles de fonction: L'existence de symboles de fonction est un obstacle clé à l'admissibilité

Travaux Connexes

Directions de Recherche Principales

1. Théorie des preuves cycliques: Travaux fondateurs de Brotherston et al. 1,4,6
2. Recherche de preuve: Recherche pour éviter la recherche heuristique d'hypothèses inductives 2,3,5,11,12
3. Logique de séparation: Applications des preuves cycliques à la logique de séparation 2,7,9

Relation de cet Article avec les Travaux Connexes

• Résout le problème ouvert posé par Brotherston 1
• Étend les travaux de Kimura et al. 7 à un cadre plus général
• Fournit une base théorique pour la recherche de preuve

Avantages de cet Article

1. Première preuve: Première preuve rigoureuse de l'admissibilité de la règle de substitution dans CLKIDω
2. Innovation méthodologique: Propose de nouvelles techniques d'élimination applicables aux structures cycliques
3. Applicabilité large: Les résultats s'appliquent à plusieurs systèmes connexes

Conclusion et Discussion

Conclusions Principales

1. Dans CLKIDω avec la règle de coupure, la règle de substitution est admissible
2. Lorsque restreinte à la substitution atomique, le résultat s'étend aux systèmes sans coupure
3. Ce résultat s'applique à d'autres systèmes importants tels que la logique de séparation

Limitations

1. Dépendance à la coupure: L'élimination des substitutions composées nécessite la règle de coupure
2. Restriction sur les symboles de fonction: Le résultat complètement général nécessite d'exclure les symboles de fonction
3. Complexité de construction: Le processus de construction de preuve est relativement complexe

Directions Futures

1. Ensemble de règles minimal: Étudier l'ensemble minimal de règles permettant toujours l'élimination de la règle de substitution en présence de symboles de fonction
2. Élimination de coupure: Étudier la propriété d'élimination de coupure des systèmes de preuve cyclique par introduction de règles supplémentaires
3. Complexité computationnelle: Analyser la complexité computationnelle de l'élimination de la règle de substitution

Évaluation Approfondie

Points Forts

1. Importance théorique: Résout un problème ouvert important dans ce domaine
2. Innovation méthodologique: Propose de nouvelles techniques applicables aux structures cycliques
3. Rigueur: Preuve rigoureuse et constructive
4. Applicabilité large: Les résultats s'appliquent à plusieurs systèmes connexes
5. Clarté d'exposition: Les détails techniques sont énoncés clairement et faciles à comprendre

Insuffisances

1. Limitations pratiques: La dépendance à la règle de coupure limite les applications pratiques
2. Complexité: Le processus de transformation de preuve est relativement complexe
3. Complétude: Des restrictions subsistent dans le cadre sans coupure

Impact

1. Contribution théorique: Fournit une base théorique importante pour la théorie des preuves cycliques
2. Valeur pratique: Offre une plus grande flexibilité pour l'implémentation de la recherche de preuve cyclique
3. Extensibilité: La méthode peut potentiellement s'appliquer à d'autres systèmes connexes

Scénarios d'Application

1. Preuve automatisée de théorèmes: Améliorer l'efficacité de la recherche de preuve cyclique
2. Vérification de programmes: Applications dans les cadres de vérification tels que la logique de séparation
3. Recherche théorique: Fournir une base pour la recherche ultérieure en théorie des preuves cycliques

Références

L'article cite 19 références connexes, incluant principalement:

1. Travaux fondateurs de Brotherston sur les preuves cycliques
2. Recherche sur l'application des preuves cycliques à la logique de séparation
3. Travaux connexes sur la recherche automatisée de preuve
4. Recherche fondamentale sur l'élimination de coupure et la théorie de la preuve

Cet article apporte une contribution importante à la théorie des preuves cycliques, résolvant un problème ouvert important par des techniques innovantes et jetant les bases pour le développement ultérieur du domaine.