A Strategy Language for Controlled Proof Search
arXiv:2607.12658 · doi:10.4204/EPTCS.448.5
The paper introduces a strategy language for the Pgeon meta‑prover that cleanly separates inference rules from proof search, defining semantics for strategies to enable fair and complete search in semi‑decidable logics, with case studies in first‑order and modal logics.
Abstract
This paper introduces the strategy language of Pgeon, a meta-prover with a clear separation between inference rules and proof search. We give the semantics of strategies as functions over proof states, and of the operators that are used to combine them, allowing for sequential composition, choice, repetition and interleaving of strategies. This language is designed to handle the challenge of fair proof search in semi-decidable logics, where simple depth-first exploration of the proof space is not guaranteed to achieve completeness. We showcase the expressiveness and effectiveness of the approach through case studies in first-order and modal logics.
In Proceedings LFMTP 2026, arXiv:2607.10318