Paper Info
Title
A Rewrite Rule Based Framework for Combining Decision Procedures
Abstract
A rewrite rule based framework for combining decision procedures for universally quantified theories is proposed. It builds on the key ideas of Shostak's combination approach. A distinctive feature of the proposed framework is that its soundness and completeness can be easily established. Furthermore, the framework has the desired property of being efficient (by avoiding duplication of equality reasoning in all decision procedures) as well as generating canonical forms as in Shostak's combination framework. It thus enables tight integration of decision procedures with equational and inductive reasoning based on rewriting.
Year
DOI
Venue
2002
10.1007/3-540-45988-X_8
FroCos
Keywords
Field
DocType
tight integration,distinctive feature,inductive reasoning,equality reasoning,proposed framework,combining decision procedures,decision procedure,combination approach,key idea,rewrite rule,combination framework,canonical form
Inductive reasoning,Discrete mathematics,Rewrite rule,Computer science,Disjunctive normal form,Algorithm,Canonical form,Distinctive feature,Rewriting,Soundness,Completeness (statistics)
Conference
ISBN
Citations 
PageRank 
3-540-43381-3
7
0.60
References 
Authors
23
1
Name
Order
Citations
PageRank
Deepak Kapur12282235.00