A Resolution Calculus with Shared Literals

Article type: Research Article

Authors: Peltier, Nicolas

Affiliations: Leibniz-IMAG – 46, avenue Félix Viallet, 38031 Grenoble Cedex, France. E-mail: Nicolas.Peltier@imag.fr

Abstract: We present a resolution calculus for first-order logic using a more concise formalism for representing sets of clauses. The idea is to represent the clause set at hand as a Directed Acyclic Graph, which allows one to share common literals instead of duplicating them, thus yielding a much more compact representation of the search space. We define inference rules operating on this language and we prove their soundness and refutational completeness. We also design simplification rules for pruning the search space. Finally we compare our technique with the usual resolution calculus and we prove (using the pigeonhole example) that our method can reduce the length of the proof by an exponential factor (in propositional logic).

Keywords: Resolution, Sharing, Pigeonhole problem

Journal: Fundamenta Informaticae, vol. 76, no. 4, pp. 449-480, 2007