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.

• Type: Conference
• Year: 2007
• Where: MKM
• Authors: Predrag Janicic, Alan Bundy
• Keywords: Automatic Synthesis, Decision Procedures, MKM 2007, Synthesis Mechanism