Superposition modulo a Shostak Theory

Harald Ganzinger, Thomas Hillenbrand, and Uwe Waldmann

In Franz Baader, editor, Automated Deduction - CADE-19, 19th International Conference on Automated Deduction, LNAI 2741, pages 182-196, Miami Beach, FL, USA, July 28-August 2, 2003. Springer-Verlag.

Abstract: We investigate superposition modulo a Shostak theory T in order to facilitate reasoning in the amalgamation of T and a free theory F. Free operators occur naturally for instance in program verification problems when abstracting over subroutines. If their behaviour in addition can be specified axiomatically, much more of the program semantics can be captured. Combining the Shostak-style components for deciding the clausal validity problem with the ordering and saturation techniques developed for equational reasoning, we derive a refutationally complete calculus on mixed ground clauses which result for example from CNF transforming arbitrary universally quantified formulae. The calculus works modulo a Shostak theory in the sense that it operates on canonizer normalforms. For the Shostak solvers that we study, coherence comes for free: no coherence pairs need to be considered.


Previous | Up | Next
Uwe Waldmann <uwe@mpi-inf.mpg.de>, 2004-01-07.
Imprint | Data Protection