论文标题
生成压缩组合证明结构 - 一种自动化一阶定理的方法证明
Generating Compressed Combinatory Proof Structures -- An Approach to Automated First-Order Theorem Proving
论文作者
论文摘要
通过组合术语代表一个验证树，该术语还原到树上，使树内的重复形式微妙形式化为组合术语的重复中间。在组合术语的DAG表示中，这些直接因素将其直接转换为共享子图。为了搜索证据，可以列举组合术语，例如clausal tableaux，与与枚举结构的节点相关的公式的统一交织。为了限制搜索空间，枚举可以基于定义为参数化组合术语的证明模式。我们在这里介绍了这种“组合术语为证明结构”的方法，以实现自动化的一阶证明，提出实现和首次实验结果。该方法建立在基于凝结脱离和连接方法的证明结构的术语视图上。它实现了从连接结构微积分已知的功能，到目前为止尚未实现。
Representing a proof tree by a combinator term that reduces to the tree lets subtle forms of duplication within the tree materialize as duplicated subterms of the combinator term. In a DAG representation of the combinator term these straightforwardly factor into shared subgraphs. To search for proofs, combinator terms can be enumerated, like clausal tableaux, interwoven with unification of formulas that are associated with nodes of the enumerated structures. To restrict the search space, the enumeration can be based on proof schemas defined as parameterized combinator terms. We introduce here this "combinator term as proof structure" approach to automated first-order proving, present an implementation and first experimental results. The approach builds on a term view of proof structures rooted in condensed detachment and the connection method. It realizes features known from the connection structure calculus, which has not been implemented so far.
