David Delahaye

A Strategy Language for Controlled Proof Search

2026 · Electronic Proceedings in Theoretical Computer Science

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 …