Please use this identifier to cite or link to this item:
https://research.matf.bg.ac.rs/handle/123456789/519| Title: | Automatic synthesis of decision procedures: A case study of ground and linear arithmetic | Authors: | Janičić, Predrag Bundy, Alan |
Affiliations: | Informatics and Computer Science | Issue Date: | 1-Jan-2007 | Related Publication(s): | International Conference on Mathematical Knowledge Management Symposium on the Integration of Symbolic Computation and Mechanized Reasoning MKM 2007 - Towards Mechanized Mathematical Assistants | Journal: | Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) | Abstract: | 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. © Springer-Verlag Berlin Heidelberg 2007. |
URI: | https://research.matf.bg.ac.rs/handle/123456789/519 | ISBN: | 9783540730835 | ISSN: | 03029743 | DOI: | 10.1007/978-3-540-73086-6_7 |
| Appears in Collections: | Research outputs |
Show full item record
Items in DSpace are protected by copyright, with all rights reserved, unless otherwise indicated.