Abstract

A counter-example contradicting Theorem 4.2 in [4] is given, thus showing that the proof of the decidability of the PVD=g class that is presented in [4] is incorrect. Then, we give a new decidability proof for a non-trivial extension of PVD=g the so-called 'PVDE' class. The new proof is based on refinements of the paramodulation calculus. Detailed proofs of the refutational completeness of this refinement and of the termination of this calculus on PVDE are provided.We show that the other results presented in [4] concerning model building can be preserved, and even extended to PVDE, i.e. we present an algorithm for extracting models from saturated clause sets. The building process can be seen as a refinement of the one given in [4]