Theorem Proving with Abstraction
Theorem Proving with Abstraction
复制标题
抽象定理证明
DOI：
10.1016/0004-3702(81)90015-1
复制
发表时间：
1981
期刊：
影响因子：
--
通讯作者：
D. Plaisted
中科院分区：
文献类型：
--
作者：
D. Plaisted
定义了一类称为抽象的映射，并给出了抽象的例子。这些函数将S的子句集合映射到可能更简单的子句集合T。此外，S的归结证明映射到T的归结证明上。为了寻找S的C子句的证明，只需搜索T的证明并尝试反转抽象映射就可以得到S的C的证明。基于这一思想，我们给出了一些定理证明策略。这些策略中的大多数都是完整的。还提出了一种同时使用多个抽象的方法。这需要在多子句上使用“多子句”，这是文字的多个集合，以及相关联的“m抽象映射”。某些抽象概念特别有趣，因为它们对应于对S小句集合的特定解释。抽象的使用使得支持集策略的优势可以在任意完全的非支持集解析策略中实现。
A class of mappings called abstractions are defined, and examples of abstractions are given. These functions map a set S of clauses onto a possibly simpler set T of clauses. Also, resolution proofs from S map onto possibly simpler resolution proofs from T. In order to search for a proof of a clause C from S, it suffices to search for a proof from T and attempt to invert the abstraction mapping to obtain a proof of C from S. Some theorem proving strategies based on this idea are presented. Most of these strategies are complete. A method of using more than one abstraction at the same time is also presented. This requires the use of ‘multiclauses’, which are multisets of literals, and associated ‘m-abstraction mappings’ on multiclauses. Certain abstractions are especially interesting, because they correspond to particular interpretations of the set S of clauses. The use of abstractions permits the advantages of set-of-support strategies to be realized in arbitrary complete non set-of-support resolution strategies.