Connection tableaux with lazy paramodulation (Q928656): Difference between revisions

Up to now, no competitive theorem prover for first-order logic with equality is known which is based on the tableau calculus. The present paper presents such a calculus. It starts with connection tableaux and transforms the equality symbol into an uninterpreted predicate symbol and constraints, similar to [\textit{L. Bachmair, H. Ganzinger} and \textit{A. Voronkov}, Lect. Notes Comput. Sci. 1421, 175--190 (1998; Zbl 0926.03006)]. As a refinement, paramodulation is restricted to be lazy and basic, as in [\textit{L. Bachmair, H. Ganzinger, C. Lynch} and \textit{W. Snyder}, Inf. Comput. 121, No. 2, 172--192 (1995; Zbl 0833.68115)]. The calculus is proved to be sound and complete. Unfortunately, no implementation is available and so no comparison with saturation-based provers is possible.