Superposition with Equivalence Reasoning and Delayed Clause Normal Form Transformation.

Harald Ganzinger, Jrgen Stuber

Browse the full CADE paper archive.