摘要
The generalized resolution method presented in ref. [1] is a generalization of Robinson’s resolution principle in the first-order logic, which can be applied to a set of nonclausal formulae, i.e. a set of generalized clauses. The method can not only avoid the symbolic redundancy generated from the procedure of transforming a formula into a set of clauses, but also keep the natural description of the problem.
基金
the National Natural Science Foundation of China, the National High Technology Development Program and the National "PanDeng" Program
