|
Informatics Report Series
|
|
|
|
|
|
|
|
|
| Title:A General Setting for Flexibly Combining and Augmenting Decision Procedures |
| Authors:
Predrag Janicic
; Alan Bundy
|
| Date:Jan 2002 |
| Publication Title:Journal of Automated Reasoning |
| Publisher:Springer Netherlands |
|
Publication Type:Journal Article
Publication Status:Published
|
|
Volume No:28(3)
Page Nos:257-305
|
|
DOI:10.1023/A:1015707001763
ISBN/ISSN:1573-0670
|
- Abstract:
-
The efficient combining and augmenting of decision procedures are often very important for a successful use of theorem provers. There are several schemes for combining and augmenting decision procedures; some of them support handling uninterpreted functions, use of available lemmas, and the like. In this paper we introduce a general setting for describing different schemes for both combining and augmenting decision procedures. This setting is based on the macro inference rules used in different approaches. Some of these rules are abstraction, entailment, congruence closure and lemma invoking. The general setting gives a simple description and the key ideas of one scheme and makes different schemes comparable. Also, it makes easier combining ideas from different schemes. In this paper we describe several schemes via introduced macro inference rules and report on our prototype implementation.
- Copyright:
- 2002 by The University of Edinburgh. All Rights Reserved
- Links To Paper
- No links available
- Bibtex format
- @Article{EDI-INF-RR-0095,
- author = {
Predrag Janicic
and Alan Bundy
},
- title = {A General Setting for Flexibly Combining and Augmenting Decision Procedures},
- journal = {Journal of Automated Reasoning},
- publisher = {Springer Netherlands},
- year = 2002,
- month = {Jan},
- volume = {28(3)},
- pages = {257-305},
- doi = {10.1023/A:1015707001763},
- }
|
