AI 中文总结
介绍用于受控证明搜索的Pgeon策略语言，其语义基于证明状态函数及组合运算符，能应对半可判定逻辑公平证明搜索挑战，通过一阶和模态逻辑案例研究展示了该方法的表现力与有效性。
AI 中文摘要
本文介绍了Pgeon的策略语言，Pgeon是一个推理规则和证明搜索明确分离的元证明器。我们将策略的语义定义为证明状态上的函数，以及用于组合它们的运算符的语义，允许策略进行顺序组合、选择、重复和交错。该语言旨在应对半可判定逻辑中公平证明搜索的挑战，在这种逻辑中，简单的深度优先搜索证明空间不能保证达到完备性。我们通过一阶逻辑和模态逻辑的案例研究展示了该方法的表现力和有效性。
英文摘要
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.
CommentsIn Proceedings LFMTP 2026, arXiv:2607.10318
Journal refEPTCS 448, 2026, pp. 58-64
