Edinburgh Research Explorer

Strict General Setting for Building Decision Procedures into Theorem Provers

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

Related Edinburgh Organisations


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


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.

Download statistics

No data available

ID: 7553331