Please use this identifier to cite or link to this item: https://research.matf.bg.ac.rs/handle/123456789/511
Title: A framework for the flexible integration of a class of decision procedures into theorem provers
Authors: Janičić, Predrag 
Bundy, Alan
Green, Ian
Affiliations: Informatics and Computer Science 
Issue Date: 1-Jan-1999
Related Publication(s): International Conference on Automated Deduction CADE 1999
Journal: Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Abstract: 
The role of decision procedures is often essential in theorem proving. Decision procedures can reduce the search space of heuristic components of a prover and increase its abilities. However, in some ap­plications only a small number of conjectures fall within the scope of the available decision procedures. Some of these conjectures could in an informal sense fall ‘just outside’ that scope. In these situations a problem arises because lemmas have to be invoked or the decision procedure has to communicate with the heuristic component of a theorem prover. This problem is also related to the general problem of how to flexibly integrate decision procedures into heuristic theorem provers. In this paper we ad­dress such problems and describe a framework for the flexible integration of decision procedures into other proof methods. The proposed frame­work can be used in different theorem provers, for different theories and for different decision procedures. New decision procedures can be simply ‘plugged-in’ to the system. As an illustration, we describe an instantia­tion of this framework within the Clam proof-planning system, to which it is well suited. We report on some results using this implementation.
URI: https://research.matf.bg.ac.rs/handle/123456789/511
ISBN: 3540662227
ISSN: 03029743
DOI: 10.1007/3-540-48660-7_9
Appears in Collections:Research outputs

Show full item record

SCOPUSTM   
Citations

5
checked on Dec 21, 2024

Page view(s)

8
checked on Dec 24, 2024

Google ScholarTM

Check

Altmetric

Altmetric


Items in DSpace are protected by copyright, with all rights reserved, unless otherwise indicated.