Informatics Report Series



Related Pages

Report (by Number) Index
Report (by Date) Index
Author Index
Institute Index

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
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.
2002 by The University of Edinburgh. All Rights Reserved
Links To Paper
No links available
Bibtex format
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},

Home : Publications : Report 

Please mail <> with any changes or corrections.
Unless explicitly stated otherwise, all material is copyright The University of Edinburgh