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

Documents

Original languageEnglish
Title of host publicationThe 1st International Joint Conference on Automated Reasoning (IJCAR-2001) --- Short Papers
PublisherUniversita degli Studi di Siena, Italia
Pages86-95
Number of pages10
StatePublished - 2001

Abstract

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