A Strategy Language for Controlled Proof Search

Technical Summary: A Strategy Language for Controlled Proof Search

Problem Statement
In automated reasoning, the static completeness of a logical calculus (the existence of a proof for any theorem) does not guarantee the dynamic completeness of a prover (the ability to actually find that proof). In semi-decidable logics, inference rules can generate infinitely many successors. If a proof search strategy employs unfair exploration—such as a naive depth-first approach that indefinitely prioritizes one branch—it may postpone relevant inferences forever, failing to discover valid proofs even when they exist. This issue is particularly acute in frameworks like Pgeon, which separate inference rules from proof-search strategies, as the design of the exploration policy becomes a critical determinant of success.

Methodology
The paper introduces a formal strategy language for Pgeon, a meta-prover framework that compiles declarative specifications of logical calculi into executable provers. The core methodological shift is modeling proof search not as a relation between states, but as the enumeration of proof states via streams.

1. Formal Semantics: A proof state ($\Sigma$) is treated as a partially constructed proof tree. A strategy is defined as a function $s: \Sigma \to \text{Str}(\Sigma)$, mapping a state to a stream (finite or infinite) of successor states. This makes non-determinism explicit:

   • An empty stream represents failure.
   • A singleton stream represents deterministic success.
   • A stream with multiple elements represents non-deterministic branching.
   • Infinite streams represent rules that can generate unboundedly many successors.

2. Combinators: The language provides a set of operators to compose these strategies, distinguishing between biased (depth-first) and fair (interleaved) exploration:

   • Sequential Composition ($;$): Applies one strategy to the results of another.
   • Left-biased Choice ($\parallel$): Attempts the first strategy; if it fails (empty stream), it falls back to the second.
   • Fair Sequential Composition ($\&;$): Interleaves the results of sequential applications using diagonalization ($\triangle$), ensuring that if a result is reachable in finite steps, it is eventually explored.
   • Fair Choice ($\&|$): Fairly interleaves the results of two alternative strategies.
   • Repetition ($*$): Defined as a least fixpoint using fair sequential composition ($\mu X. \text{id} \&; (s \&; X)$), ensuring that all finite iteration depths are explored rather than proceeding strictly depth-first.

3. Primitive Operations: The language includes primitive rules ($r$) and an exhaustive application operator ($r!$) that applies a rule to all admissible matches in a state.

Key Contributions

• Compositional Stream Semantics: The paper provides a compositional algebra for strategy combinators where the search space is reified as a first-class object (a stream). This allows for reasoning about fairness and enumeration independently of implementation details like stack discipline or continuations.
• Fairness Mechanisms: By introducing diagonalization-based interleaving operators ($\&;$ and $\&|$), the framework addresses the "starvation" problem where infinite branches prevent the discovery of finite proofs.
• Formal Strategy Language for Pgeon: The work formalizes the strategy component of the Pgeon framework, abstracting the control flow of proof search into a declarative language.

Results and Case Studies
The paper demonstrates the expressiveness and effectiveness of the approach through two case studies:

1. First-Order Logic (LK): The authors address the interaction between closure (unification) and rule saturation. A naive strategy of repeated rule application often fails to find proofs because it commits to specific instantiations too early. The proposed strategy, $(\odot^* \&; (\alpha \parallel \delta \parallel \beta \parallel \gamma!)^*)^*$, uses fair composition to interleave closure attempts with rule saturation. This ensures that different unification choices are explored across all search depths, preventing the system from getting stuck in infinite instantiation loops while missing a closing derivation.

2. Modal Logic (S4): In S4, the non-deterministic rule $\theta$ (arbitrary removal of formulas) is necessary to enable the application of the modal rule S4 but risks discarding formulas needed for closure. An uncontrolled use of $\theta$ leads to dead ends. The authors propose a combined strategy $\theta^* \&; \text{S4}$, which explores all ways of removing formulas to enable S4 applications fairly. This is integrated into a larger strategy $((\alpha \parallel \beta \parallel T)^*; (\theta^* \&; \text{S4}))^*$, ensuring that if a successful application of S4 requires a specific subset of removed formulas, that configuration is eventually reached without starvation.

Significance
The paper claims that this approach offers a principled and modular foundation for specifying and analyzing proof-search procedures. By separating inference rules from search strategies and providing a formal language with compositional semantics, the framework allows for the systematic exploration of search spaces in semi-decidable logics. It demonstrates that dynamic completeness can be achieved even when naive depth-first strategies fail, by explicitly managing fairness through stream interleaving. The work enables reasoning about proof-search procedures at an abstract level, independent of the specific implementation of the prover.