Strict General Setting for Building Decision Procedures into Theorem Provers

Predrag Janicic, Alan Bundy

Research output: Chapter in Book/Report/Conference proceedingConference contribution

Abstract / Description of output

The efficient and flexible incorporating of decision procedures into theorem provers is very important for their successful use. There are several approaches for combining and augmenting of decision procedures; some of them support handling uninterpreted functions, congruence closure, lemma invoking etc. In this paper we present a variant of one general setting for building decision procedures into theorem provers (gs framework [18]). That setting is based on macro inference rules motivated by techniques used in different approaches. The general setting enables a simple describing of different combination/augmentation schemes. In this paper, we further develop and extend this setting by an imposed ordering on the macro inference rules. That ordering leads to a "strict setting". It makes implementing and using variants of well-known or new schemes within this framework a very easy task even for a non-expert user. Also, this setting enables easy comparison of different combination/augmentation schemes and combination of their ideas.
Original languageEnglish
Title of host publicationThe 1st International Joint Conference on Automated Reasoning (IJCAR-2001) --- Short Papers
PublisherUniversita degli Studi di Siena, Italia
Number of pages10
Publication statusPublished - 2001


Dive into the research topics of 'Strict General Setting for Building Decision Procedures into Theorem Provers'. Together they form a unique fingerprint.

Cite this