Automatic synthesis of decision procedures

Predrag Janicic, Alan Bundy

Research output: Chapter in Book/Report/Conference proceedingConference contribution

Abstract

We address the problem of automatic synthesis of decision procedures. We evaluate our ideas on ground arithmetic and linear arithmetic, but the approach can be applied to other domains as well. The approach is well-suited to the proof-planning paradigm. The synthesis mechanism consists of several stages and sub-mechanisms. Our system (adeptus), which we present in this paper, synthesized a decision pro- cedure for ground arithmetic completely automatically and it used some specic 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.
Original languageEnglish
Title of host publicationTowards Mechanized Mathematical Assistants
Subtitle of host publication14th Symposium, Calculemus 2007, 6th International Conference, MKM 2007, Hagenberg, Austria, June 27-30, 2007. Proceedings
PublisherSpringer
Pages80-93
Volume4573
ISBN (Electronic)978-3-540-73086-6
ISBN (Print)978-3-540-73083-5
DOIs
Publication statusPublished - 2007

Publication series

NameLecture Notes in Computer Science
PublisherSpringer Verlag
Volume4573
ISSN (Print)0302-9743

Keywords / Materials (for Non-textual outputs)

  • Decision procedures

Fingerprint

Dive into the research topics of 'Automatic synthesis of decision procedures'. Together they form a unique fingerprint.

Cite this