Ronald Fagin
Journal of the ACM
The resolution principle, an automatic inference technique, is studied as a possible decision procedure for certain classes of first-order formulas. It is shown that most previous resolution strategies do not decide satisfiability even for “simple” solvable classes. Two new resolution procedures are described and are shown to be complete (i.e. semidecision procedures) in the general case and, in addition, to be decision procedures for successively wider classes of first-order formulas. These include many previously studied solvable classes. The proofs that a complete resolution procedure will always halt (without producing the empty clause) when applied to satisfiable formulas in certain classes provide new, and in some cases more enlightening, demonstrations of the solvability of these classes. A technique for constructing a model for a formula shown satisfiable in this way is also described. © 1976, ACM. All rights reserved.
Ronald Fagin
Journal of the ACM
Tushar Deepak Chandra, Sam Toueg
Journal of the ACM
Bing Zhang, Mikio Takeuchi, et al.
ICAIF 2024
Aakash Khochare, Yogesh Simmhan, et al.
eScience 2022