Connection Tableaux with Lazy Paramodulation

It is well-known that the connection refinement of clause tableaux with paramodulation is incomplete (even with weak connections). In this paper, we present a new connection tableau calculus for logic with equality. This calculus is based on a lazy form of paramodulation where parts of the unification step become auxiliary subgoals in a tableau and may be subjected to subsequent paramodulations. Our calculus uses ordering constraints and a certain form of the basicness restriction.

• Type: Conference
• Year: 2006
• Where: CADE
• Authors: Andrey Paskevich
• Keywords: Automated Reasoning, CADE 2006, Clause Tableaux, Unification Step, Weak Connections