Paramodulation without duplication
Christopher S. Lynch · 2002
The resolution (and paramodulation) inference systems are theorem proving procedures for first-order logic (with equality), but they can run exponentially long for subclasses which have polynomial-time decision procedures, as in the case of SLD resolution and the Knuth-Bendix completion procedure, both in the ground case. Specialized methods run in polynomial time, but have not been extended to the full first-order case. We show a form of paramodulation which does not copy literals, which runs in polynomial time for the ground case of the following four subclasses: Horn clauses with any selection rule, any set of unit equalities (this includes completion), equational Horn clauses with a certain selection rule, and conditional narrowing.