Sciweavers

MKM
2007
Springer

Automatic Synthesis of Decision Procedures: A Case Study of Ground and Linear Arithmetic

14 years 5 months ago
Automatic Synthesis of Decision Procedures: A Case Study of Ground and Linear Arithmetic
We address the problem of automatic synthesis of decision procedures. Our synthesis mechanism consists of several stages and submechanisms and is well-suited to the proof-planning paradigm. The system (adeptus), that we present in this paper, synthesised a decision procedure for ground arithmetic completely automatically and it used some specific method generators in generating a decision procedure for linear arithmetic, in only a few seconds of cpu time. We believe that this approach can lead to automated assistance in constructing decision procedures and to more reliable implementations of decision procedures.
Predrag Janicic, Alan Bundy
Added 08 Jun 2010
Updated 08 Jun 2010
Type Conference
Year 2007
Where MKM
Authors Predrag Janicic, Alan Bundy
Comments (0)