A Strategy Language for Controlled Proof Search

Résumé Technique : Un langage de stratégie pour la recherche de preuves contrôlée

Énoncé du Problème
Dans le raisonnement automatisé, la complétude statique d'un calcul logique (l'existence d'une preuve pour tout théorème) ne garantit pas la complétude dynamique d'un prouveur (la capacité à trouver réellement cette preuve). Dans les logiques semi-décidables, les règles d'inférence peuvent générer une infinité de successeurs. Si une stratégie de recherche de preuve emploie une exploration biaisée — telle qu'une approche naïve en profondeur qui privilégie indéfiniment une branche — elle peut reporter indéfiniment des inférences pertinentes, échouant ainsi à découvrir des preuves valides même lorsqu'elles existent. Ce problème est particulièrement aigu dans les cadres comme Pgeon, qui séparent les règles d'inférence des stratégies de recherche de preuve, car la conception de la politique d'exploration devient un déterminant critique du succès.

Méthodologie
L'article introduit un langage de stratégie formel pour Pgeon, un méta-prouveur qui compile des spécifications déclaratives de calculs logiques en prouveurs exécutables. Le changement méthodologique central consiste à modéliser la recherche de preuve non pas comme une relation entre états, mais comme l'énumération d'états de preuve via des flux (streams).

1. Sémantique Formelle : Un état de preuve ($\Sigma$) est traité comme un arbre de preuve partiellement construit. Une stratégie est définie comme une fonction $s: \Sigma \to \text{Str}(\Sigma)$, associant un état à un flux (fini ou infini) d'états successeurs. Cela rend le non-déterminisme explicite :

   • Un flux vide représente un échec.
   • Un flux contenant un seul élément représente un succès déterministe.
   • Un flux avec plusieurs éléments représente un embranchement non déterministe.
   • Des flux infinis représentent des règles pouvant générer un nombre illimité de successeurs.

2. Combinateurs : Le langage fournit un ensemble d'opérateurs pour composer ces stratégies, distinguant l'exploration biaisée (profondeur) de l'exploration équitable (entrelacement) :

   • Composition Séquentielle ($;$) : Applique une stratégie aux résultats d'une autre.
   • Choix Biaisé à Gauche ($\parallel$) : Tente la première stratégie ; si elle échoue (flux vide), elle retombe sur la seconde.
   • Composition Séquentielle Équitable ($\&;$) : Entrelace les résultats des applications séquentielles en utilisant la diagonalisation ($\triangle$), garantissant que si un résultat est atteignable en étapes finies, il sera finalement exploré.
   • Choix Équitable ($\&|$) : Entrelace équitablement les résultats de deux stratégies alternatives.
   • Répétition ($*$) : Définie comme un point fixe inférieur via la composition séquentielle équitable ($\mu X. \text{id} \&; (s \&; X)$), assurant que toutes les profondeurs d'itération finies sont explorées plutôt que de procéder strictement en profondeur.

3. Opérations Primitives : Le langage inclut des règles primitives ($r$) et un opérateur d'application exhaustive ($r!$) qui applique une règle à toutes les correspondances admissibles dans un état.

Contributions Clés

• Sémantique de Flux Compositionnelle : L'article fournit une algèbre compositionnelle pour les combinateurs de stratégie où l'espace de recherche est réifié comme un objet de premier ordre (un flux). Cela permet de raisonner sur l'équité et l'énumération indépendamment des détails d'implémentation tels que la discipline de pile ou les continuations.
• Mécanismes d'Équité : En introduisant des opérateurs d'entrelacement basés sur la diagonalisation ($\&;$ et $\&|$), le cadre traite le problème de "starvation" (famine) où des branches infinies empêchent la découverte de preuves finies.
• Langage de Stratégie Formel pour Pgeon : Le travail formalise la composante de stratégie du cadre Pgeon, en abstrayant le flux de contrôle de la recherche de preuve en un langage déclaratif.

Résultats et Études de Cas
L'article démontre l'expressivité et l'efficacité de l'approche à travers deux études de cas :

1. Logique du Premier Ordre (LK) : Les auteurs traitent l'interaction entre la clôture (unification) et la saturation de règles. Une stratégie naïve d'application répétée de règles échoue souvent à trouver des preuves car elle s'engage dans des instanciations spécifiques trop tôt. La stratégie proposée, $(\odot^* \&; (\alpha \parallel \delta \parallel \beta \parallel \gamma!)^*)^*$, utilise la composition équitable pour entrelacer les tentatives de clôture avec la saturation de règles. Cela garantit que différents choix d'unification sont explorés à travers toutes les profondeurs de recherche, empêchant le système de rester bloqué dans des boucles d'instanciation infinies tout en manquant une dérivation de clôture.

2. Logique Modale (S4) : Dans S4, la règle non déterministe $\theta$ (retrait arbitraire de formules) est nécessaire pour permettre l'application de la règle modale S4 mais risque de rejeter des formules nécessaires à la clôture. Une utilisation non contrôlée de $\theta$ mène à des impasses. Les auteurs proposent une stratégie combinée $\theta^* \&; \text{S4}$, qui explore toutes les manières de retirer des formules pour permettre les applications de S4 de façon équitable. Ceci est intégré dans une stratégie plus large $((\alpha \parallel \beta \parallel T)^*; (\theta^* \&; \text{S4}))^*$, garantissant que si une application réussie de S4 nécessite un sous-ensemble spécifique de formules retirées, cette configuration est finalement atteinte sans famine.

Signification
L'article affirme que cette approche offre une fondation principled et modulaire pour spécifier et analyser les procédures de recherche de preuves. En séparant les règles d'inférence des stratégies de recherche et en fournissant un langage formel avec une sémantique compositionnelle, le cadre permet l'exploration systématique des espaces de recherche dans les logiques semi-décidables. Il démontre que la complétude dynamique peut être atteinte même lorsque des stratégies naïves en profondeur échouent, en gérant explicitement l'équité par l'entrelacement de flux. Ce travail permet de raisonner sur les procédures de recherche de preuve à un niveau abstrait, indépendamment de l'implémentation spécifique du prouveur.