Please use this identifier to cite or link to this item: https://research.matf.bg.ac.rs/handle/123456789/523
Title: A general setting for flexibly combining and augmenting decision procedures
Authors: Janičić, Predrag 
Bundy, Alan
Affiliations: Informatics and Computer Science 
Keywords: Augmentation of decision procedures;Combining decision procedures;Decision procedures;Theorem proving
Issue Date: 1-Jan-2002
Journal: Journal of Automated Reasoning
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.
URI: https://research.matf.bg.ac.rs/handle/123456789/523
ISSN: 01687433
DOI: 10.1023/A:1015707001763
Appears in Collections:Research outputs

Show full item record

SCOPUSTM   
Citations

10
checked on Dec 21, 2024

Page view(s)

15
checked on Dec 24, 2024

Google ScholarTM

Check

Altmetric

Altmetric


Items in DSpace are protected by copyright, with all rights reserved, unless otherwise indicated.