Bedwyr系统用于在句法表达式上进行模型检测
摘要：Bedwyr：一种逻辑编程的一般化方法，允许直接对可能包含绑定的句法表达式进行模型检查。这个用OCaml编写的系统是对证明搜索理论的两个最新进展的直接实现。第一个是将有限的成功和有限的失败都捕捉在序列推理中，通过合并允许探索固定点的定义的推理规则。因此，这样一个序列推理中的证明搜索可以捕捉简单的模型检查问题，以及操作语义中的may和must行为。第二个是直接支持高阶抽象语法，使用术语级的λ绑定和∇量词。这些特性允许直接对包含绑定变量的表达式进行推理。
作者：David Baelde, Andrew Gacek, Dale Miller, Gopalan Nadathur, and Alwen Tiu
论文ID：cs/0702116
分类：Logic in Computer Science
分类简称：cs.LO
提交时间：2008-04-25