论文标题
命题遗忘的四种算法
Four algorithms for propositional forgetting
论文作者
论文摘要
比较了四种用于命题遗忘的算法。第一个执行所有可能的分辨率，并删除包含要忘记的变量的子句。第二个通过解决，然后删除在该变量上解决的所有子句来忘记一个变量。第三个输出了要忘记的变量上所有可能的线性分辨率的结果。第四个在回溯搜索过程中从矛盾点产生子句。后者成为赢家，第二个也是第一个在特定案例中扮演的角色。线性分辨率算法在此实现中的性能很差。
Four algorithms for propositional forgetting are compared. The first performs all possible resolutions and deletes the clauses containing a variable to forget. The second forgets a variable at time by resolving and then deleting all clauses that resolve on that variable. The third outputs the result of all possible linear resolutions on the variables to forget. The fourth generates a clause from the points of contradiction during a backtracking search. The latter emerges as the winner, with the second and first having some role in specific cases. The linear resolution algorithm performs poorly in this implementation.
