A General Setting for Flexibly Combining and Augmenting Decision Procedures

Predrag Janicic, Alan Bundy

Research output: Contribution to journalArticlepeer-review

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
Original languageEnglish
Pages (from-to)257-305
JournalJournal of Automated Reasoning
Volume28
Issue number3
DOIs
Publication statusPublished - Jan 2002

Keywords

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

Fingerprint

Dive into the research topics of 'A General Setting for Flexibly Combining and Augmenting Decision Procedures'. Together they form a unique fingerprint.

Cite this