用于语法表达式模型检验的Bedwyr系统
The Bedwyr system for model checking over syntactic expressions
摘要：
Bedwyr是逻辑编程的一种推广，它允许直接对可能包含绑定的语法表达式进行模型检验。这个系统是用OCaml编写的，是证明搜索理论中两个最新进展的直接实现。第一个是集中在这样一个事实，即有限的成功和有限的失败都可以捕获在微积分通过纳入推理规则的定义，允许不动点进行探索。因此，证明搜索在这样一个演算可以捕捉简单的模型检验问题，以及可能和必须行为的操作语义。第二个是使用术语级$λ$绑定器和$\nabla$量词直接支持高阶抽象语法。这些功能允许直接在包含绑定变量的表达式上进行推理。
英文摘要：
Bedwyr is a generalization of logic programming that allows model checking directly on syntactic expressions possibly containing bindings. This system, written in OCaml, is a direct implementation of two recent advances in the theory of proof search. The first is centered on the fact that both finite success and finite failure can be captured in the sequent calculus by incorporating inference rules for definitions that allow fixed points to be explored. As a result, proof search in such a sequent calculus can capture simple model checking problems as well as may and must behavior in operational semantics. The second is that higher-order abstract syntax is directly supported using term-level $λ$-binders and the $\nabla$ quantifier. These features allow reasoning directly on expressions containing bound variables.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
