TY - GEN
T1 - A Framework for the Flexible Integration of a Class of Decision Procedures into Theorem Provers
AU - Bundy,Alan
AU - Janicic,P.
AU - Green,I.
PY - 1999
Y1 - 1999
N2 - 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 applications 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 exibly integrate decision procedures into heuristic theorem provers. In this paper we address such problems and describe a framework for the exible integration of decision procedures into other proof methods. The proposed framework 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 instantiation of this framework within the Clam proof-planning system, to which it is well suited. We report on some results using this implementation.
AB - 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 applications 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 exibly integrate decision procedures into heuristic theorem provers. In this paper we address such problems and describe a framework for the exible integration of decision procedures into other proof methods. The proposed framework 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 instantiation of this framework within the Clam proof-planning system, to which it is well suited. We report on some results using this implementation.
KW - theorem proving
KW - decision procedures
KW - integrating decsion procedures
KW - quantifier elimination
U2 - 10.1007/3-540-48660-7_9
DO - 10.1007/3-540-48660-7_9
M3 - Conference contribution
SN - 978-3-540-66222-8
T3 - Lecture Notes in Computer Science
SP - 127
EP - 141
BT - Automated Deduction — CADE-16
PB - Springer-Verlag GmbH
ER -