Proving theorems based on equivalent transformation using resolution and factoring
Proving theorems based on equivalent transformation using resolution and factoring
复制标题
使用解析和因式分解基于等价变换证明定理
DOI：
10.1109/wict.2012.6409041
复制
发表时间：
2012
期刊：
影响因子：
--
通讯作者：
Ekawit Nantajeewarawat
中科院分区：
文献类型：
--
作者：
K. Akama;Ekawit Nantajeewarawat
提出了一种基于等价变换的定理证明方法。与传统的证明方法相反，我们的证明方法使用保义Skolemization，这需要将函数变量，因此需要一阶公式的扩展。该方法将一阶逻辑中的证明问题转化为一个存在量化合取范式的不可满足性检验问题，通过假设函数变量的隐式全局存在量化和隐式子句合取，可将存在量化合取范式识别为一组扩展子句.扩展子句集的不可满足性检验是通过扩展子句转换的ET规则的连续应用来实现的。针对扩展子句建立了一阶逻辑中归结和因式分解对应的ET规则。
We propose a method for proving theorems based on equivalent transformation (ET). As opposed to conventional proof methods, our proof method uses meaning-preserving Skolemization, which necessitates incorporation of function variables and accordingly requires an extension of first-order formulas. Using the proposed method, a proof problem in first-order logic is converted into a problem of checking unsatisfiability of an existentially quantified conjunctive normal form, which can be identified with a set of extended clauses by assuming implicit global existential quantifications of function variables and implicit clause conjunction. Checking unsatisfiability of a set of extended clauses is realized by successive application of ET rules for transforming extended clauses. ET rules corresponding to resolution and factoring in first-order logic are established for extended clauses.