Search

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). [ABSTRACT FROM AUTHOR]

A method is proposed to construct decision procedures for various subclasses of first-order logic with equality. We define a notion of complexity of first-order terms and equations, and we propose semantic and syntactic criteria ensuring that existing refinements of the paramodulation calculus terminate on the considered clause sets. These refinements use reduction orderings, selection functions and simplification rules. Since they are sound and refutationally complete, the corresponding classes of formulae are decidable. Moreover, the automatic extraction of models from saturated clause sets is also possible. A discussion and detailed comparisons with existing works in the field are provided, together with numerous examples and some undecidability results. [ABSTRACT FROM AUTHOR]