A Maximal-Literal Unit Strategy for Horn Clauses
A Maximal-Literal Unit Strategy for Horn Clauses
复制标题
Horn 子句的最大字面单元策略
DOI：
--
复制
发表时间：
1990
期刊：
影响因子：
--
通讯作者：
N. Dershowitz
中科院分区：
文献类型：
--
作者：
N. Dershowitz
给出了一种新的正单位定理证明方法。它使用一项排序来限制副调制到方程的潜在极大边。完备性是用证明排序来表示的。
A new positive-unit theorem-proving procedure for equational Horn clauses is presented. It uses a term ordering to restrict paramodulation to potentially maximal sides of equations. Completeness is shown using proof orderings.