Edinburgh Research Explorer

A General Setting for Flexibly Combining and Augmenting Decision Procedures

Research output: Contribution to journalArticle

Related Edinburgh Organisations

Documents

Original languageEnglish
Pages (from-to)257-305
JournalJournal of Automated Reasoning
Volume28
Issue number3
DOIs
StatePublished - Jan 2002

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.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

    Research areas

  • theorem proving, decision procedures, combining decision procedures, augmenting decision procedures

Download statistics

No data available

ID: 400386