Sciweavers

Share
CADE
2006
Springer

Connection Tableaux with Lazy Paramodulation

12 years 1 months ago
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.
Andrey Paskevich
Added 03 Dec 2009
Updated 03 Dec 2009
Type Conference
Year 2006
Where CADE
Authors Andrey Paskevich
Comments (0)
books