Paper Info
Title
Superposition Modulo a Shostak Theory
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.
Year
DOI
Venue
2003
10.1007/978-3-540-45085-6_15
Lecture Notes in Artificial Intelligence
Field
DocType
Volume
Discrete mathematics,Superposition principle,Subroutine,Computer science,Modulo,Algorithm,Coherence (physics),Conjunctive normal form,Critical pair,Operator (computer programming),Semantics
Conference
2741
ISSN
Citations 
PageRank 
0302-9743
3
0.44
References 
Authors
19
4
Name
Order
Citations
PageRank
Harald Ganzinger11513155.21
Thomas Hillenbrand219015.90
Uwe Waldmann330026.30
franz baader4342.97