New methods for computing inferences in first order logic

Recent improvements in satisfiability algorithms for propositional logic have made partial instantiation methods for first order predicate logic computationally more attractive. Two such methods have been proposed, one by Jeroslow and a hypergraph method for datalog formulas by Gallo and Rago. The paper shows that they are instances of two general approaches to partial instantiation, and it develops these approaches for a large decidable fragment of first order logic (the ≅≅ fragment).