A Resolution Calculus with Shared Literals

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).

• Type: Journal
• Year: 2007
• Where: FUIN
• Authors: Nicolas Peltier
• Keywords: Directed Acyclic Graph, FUIN 2007, Search Space, first-order Logic