{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,4]],"date-time":"2024-09-04T22:02:55Z","timestamp":1725487375176},"publisher-location":"Berlin, Heidelberg","reference-count":15,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540404385"},{"type":"electronic","value":"9783540450139"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2003]]},"DOI":"10.1007\/3-540-45013-0_15","type":"book-chapter","created":{"date-parts":[[2007,7,16]],"date-time":"2007-07-16T12:06:29Z","timestamp":1184587589000},"page":"182-198","source":"Crossref","is-referenced-by-count":1,"title":["Verification in ACL2 of a Generic Framework to Synthesize SAT-Provers"],"prefix":"10.1007","author":[{"given":"F. J.","family":"Mart\u00edn-Mateos","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"J. A.","family":"Alonso","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"M. J.","family":"Hidalgo","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"J. L.","family":"Ruiz-Reina","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2003,6,24]]},"reference":[{"key":"15_CR1","doi-asserted-by":"publisher","first-page":"81","DOI":"10.1016\/S0304-3975(00)00044-X","volume":"266","author":"G. Aguilera","year":"2001","unstructured":"G. Aguilera, I.P. de Guzman, M. Ojeda-Aciego and A. Valverde. Reductions for non-clausal theorem proving. Theoretical Computer Science 266, pages 81\u2013112. Elsevier, 2001.","journal-title":"Theoretical Computer Science"},{"issue":"2","key":"15_CR2","doi-asserted-by":"publisher","first-page":"227","DOI":"10.1016\/0304-3975(90)90139-9","volume":"74","author":"M. Bezem","year":"1990","unstructured":"M. Bezem. Completeness of resolution revisited. Theoretical Computer Science 74, no. 2, pages 227\u2013237, 1990.","journal-title":"Theoretical Computer Science"},{"key":"15_CR3","unstructured":"R. S. Boyer and J S. Moore. A Computational Logic. Academic Press, 1979."},{"key":"15_CR4","unstructured":"J. Caldwell. Decidability Extracted: Synthesizing \u201cCorrect-by-Construction\u201d Decision Procedures from Constuctive Proofs. PhD thesis, Cornell University, 1998"},{"key":"15_CR5","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"188","DOI":"10.1007\/3-540-09510-1_15","volume-title":"Proceedings of the Sixth International Colloquium on Automata, Languages and Programming","author":"N. Dershowitz","year":"1979","unstructured":"N. Dershowitz and Z. Manna. Proving Termination with Multiset Orderings. In Proceedings of the Sixth International Colloquium on Automata, Languages and Programming, LNCS 71, pages 188\u2013202. Springer-Verlag, 1979."},{"key":"15_CR6","doi-asserted-by":"crossref","DOI":"10.1007\/978-1-4684-0357-2","volume-title":"First-Order Logic and Automated Theorem Proving","author":"M.C. Fitting","year":"1990","unstructured":"M.C. Fitting. First-Order Logic and Automated Theorem Proving. Springer-Verlag, New York, 1990."},{"key":"15_CR7","unstructured":"J.H. Gallier. Logic for Computer Science, Foundations of Automatic Theorem Proving. Harper and Row Publishers, 1986."},{"key":"15_CR8","doi-asserted-by":"crossref","unstructured":"M. Kaufmann, P. Manolios, and J S. Moore. Computer-Aided Reasoning: An Approach. Kluwer Academic Publishers, 2000.","DOI":"10.1007\/978-1-4615-4449-4"},{"key":"15_CR9","unstructured":"F.J. Martin-Mateos, J.A. Alonso, M.J. Hidalgo, and J.L. Ruiz-Reina. A Generic Instantiation Tool and a Case Study: A Generic Multiset Theory, 2002."},{"key":"15_CR10","unstructured":"F.J. Martin-Mateos. Teoria computacional (en ACL2) sobre calculos proposicionales. PhD thesis, University of Seville, 2002."},{"key":"15_CR11","unstructured":"J.L. Ruiz-Reina. Una teoria computacional acerca de la logica ecuacional. PhD thesis, University of Seville, 2001."},{"key":"15_CR12","unstructured":"J.L. Ruiz-Reina, J.A. Alonso, M.J. Hidalgo, and F.J. Martin. Multiset Relations: a Tool for Proving Termination. In Second ACL2 Workshop, Technical Report TR-00-29, Computer Science Departament, University of Texas, 2000."},{"key":"15_CR13","unstructured":"J.L. Ruiz-Reina, J.A. Alonso, M.J. Hidalgo, and F.J. Martin. Mechanical verification of a rule-based unification algorithm in the Boyer-Moore theorem prover. In Proceedings AGP\u201999, Joint Conference on Declarative Programming, L\u2019Aquila (Italia), 1999."},{"key":"15_CR14","doi-asserted-by":"crossref","DOI":"10.1007\/978-3-642-86718-7","volume-title":"First-Order Logic","author":"R.M. Smullyan","year":"1968","unstructured":"R.M. Smullyan. First-Order Logic. Springer-Verlag: Heidelberg, Germany, 1968."},{"issue":"1\u20132","key":"15_CR15","doi-asserted-by":"publisher","first-page":"277","DOI":"10.1023\/A:1006351428454","volume":"24","author":"H. Zhang","year":"2000","unstructured":"H. Zhang and M.E. Stickel. Implementing the Davis-Putnam method Journal of Automated Reasoning, 24(1\u20132):277\u2013296, 2000.","journal-title":"Journal of Automated Reasoning"}],"container-title":["Lecture Notes in Computer Science","Logic Based Program Synthesis and Transformation"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-45013-0_15","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,4,30]],"date-time":"2019-04-30T23:21:56Z","timestamp":1556666516000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-45013-0_15"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2003]]},"ISBN":["9783540404385","9783540450139"],"references-count":15,"URL":"https:\/\/doi.org\/10.1007\/3-540-45013-0_15","relation":{},"ISSN":["0302-9743"],"issn-type":[{"type":"print","value":"0302-9743"}],"subject":[],"published":{"date-parts":[[2003]]}}}