1. Research with MATF
  2. MATF
  3. Research outputs
Please use this identifier to cite or link to this item: https://research.matf.bg.ac.rs/handle/123456789/519
DC FieldValueLanguage
dc.contributor.authorJaničić, Predragen_US
dc.contributor.authorBundy, Alanen_US
dc.date.accessioned2022-08-13T10:14:43Z-
dc.date.available2022-08-13T10:14:43Z-
dc.date.issued2007-01-01-
dc.identifier.isbn9783540730835-
dc.identifier.issn03029743en
dc.identifier.urihttps://research.matf.bg.ac.rs/handle/123456789/519-
dc.description.abstractWe 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.en
dc.relation.ispartofLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)en_US
dc.titleAutomatic synthesis of decision procedures: A case study of ground and linear arithmeticen_US
dc.typeConference Paperen_US
dc.relation.publicationInternational Conference on Mathematical Knowledge Management Symposium on the Integration of Symbolic Computation and Mechanized Reasoning MKM 2007 - Towards Mechanized Mathematical Assistantsen_US
dc.identifier.doi10.1007/978-3-540-73086-6_7-
dc.identifier.scopus2-s2.0-38049081003-
dc.identifier.urlhttps://api.elsevier.com/content/abstract/scopus_id/38049081003-
dc.contributor.affiliationInformatics and Computer Scienceen_US
dc.relation.firstpage80en_US
dc.relation.lastpage93en_US
dc.relation.volume4573 LNAIen_US
item.fulltextNo Fulltext-
item.openairecristypehttp://purl.org/coar/resource_type/c_18cf-
item.cerifentitytypePublications-
item.grantfulltextnone-
item.openairetypeConference Paper-
crisitem.author.deptInformatics and Computer Science-
crisitem.author.orcid0000-0001-8922-4948-
Appears in Collections:Research outputs
Show simple item record

Page view(s)

15
checked on Dec 24, 2024

Google ScholarTM

Check

Altmetric

Altmetric


Items in DSpace are protected by copyright, with all rights reserved, unless otherwise indicated.