Informatics Report Series



Related Pages

Report (by Number) Index
Report (by Date) Index
Author Index
Institute Index

Title:Strict General Setting for Building Decision Procedures into Theorem Provers
Authors: Predrag Janicic ; Alan Bundy
Date:Jan 2001
Publication Title:Procs of ISCAR 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.
2002 by The University of Edinburgh. All Rights Reserved
Links To Paper
No links available
Bibtex format
author = { Predrag Janicic and Alan Bundy },
title = {Strict General Setting for Building Decision Procedures into Theorem Provers},
year = 2001,
month = {Jan},

Home : Publications : Report 

Please mail <> with any changes or corrections.
Unless explicitly stated otherwise, all material is copyright The University of Edinburgh