A Generic Tableau Prover and its Integration with Isabelle
A Generic Tableau Prover and its Integration with Isabelle
复制标题
通用 Tableau Prover 及其与 Isabelle 的集成
DOI：
10.3217/jucs-005-03-0073
复制
发表时间：
1999
期刊：
影响因子：
--
通讯作者：
Lawrence Charles Paulson
中科院分区：
文献类型：
--
作者：
Lawrence Charles Paulson
一个通用的Tableau证明器已经实现，并与Isabelle(Paulson，1994)集成。与经典的一阶逻辑证明器相比，它有许多扩展，允许它与所提供的任何一组Tableau规则进行推理。它具有更高阶的语法，以便支持用户定义的绑定操作符，如集合论的绑定操作符。统一算法是一阶的，而不是更高阶的，但它包括处理绑定变量的修改。一旦找到证据，就会作为一份战术清单退还给伊莎贝尔。因为伊莎贝尔验证了证据，所以证明者可以为了效率而偷工减料，而不会损害可靠性。例如，证明者可以使用类型信息来指导搜索，而无需完全存储类型信息。类别：F.4、I.1
A generic tableau prover has been implemented and integrated with Isabelle (Paulson, 1994). Compared with classical first-order logic provers, it has numerous extensions that allow it to reason with any supplied set of tableau rules. It has a higherorder syntax in order to support user-defined binding operators, such as those of set theory. The unification algorithm is first-order instead of higher-order, but it includes modifications to handle bound variables. The proof, when found, is returned to Isabelle as a list of tactics. Because Isabelle verifies the proof, the prover can cut corners for efficiency’s sake without compromising soundness. For example, the prover can use type information to guide the search without storing type information in full. Categories: F.4, I.1