{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,6]],"date-time":"2024-09-06T23:01:18Z","timestamp":1725663678455},"publisher-location":"Berlin, Heidelberg","reference-count":12,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540572923"},{"type":"electronic","value":"9783540480389"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1993]]},"DOI":"10.1007\/3-540-57292-9_36","type":"book-chapter","created":{"date-parts":[[2012,2,26]],"date-time":"2012-02-26T12:40:09Z","timestamp":1330260009000},"page":"1-10","source":"Crossref","is-referenced-by-count":1,"title":["Proving formulas through reduction to decidable classes"],"prefix":"10.1007","author":[{"given":"Mauro","family":"Manzo","sequence":"first","affiliation":[]},{"given":"Enrico","family":"Giunchiglia","sequence":"additional","affiliation":[]},{"given":"Alessandro","family":"Armando","sequence":"additional","affiliation":[]},{"given":"Paolo","family":"Pecchiari","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2005,6,3]]},"reference":[{"key":"1_CR1","volume-title":"Technical Report 9204-01","author":"F. Giunchiglia","year":"1992","unstructured":"F. Giunchiglia. The GETFOL Manual \u2014 GETFOL version 1. Technical Report 9204-01, DIST \u2014 University of Genova, Genoa, Italy, 1992. Forthcoming IRST-Technical Report."},{"issue":"1","key":"1_CR2","doi-asserted-by":"crossref","first-page":"133","DOI":"10.1016\/0004-3702(80)90015-6","volume":"13","author":"R.W. Weyhrauch","year":"1980","unstructured":"R.W. Weyhrauch. Prolegomena to a Theory of Mechanized Formal Reasoning. Artif. Intell., 13(1):133\u2013176, 1980.","journal-title":"Artif. Intell."},{"key":"1_CR3","doi-asserted-by":"crossref","unstructured":"M.J. Gordon, A.J. Milner, and C.P. Wadsworth. Edinburgh LCF \u2014 A mechanized logic of computation, volume 78 of Lecture Notes in Computer Science. Springer Verlag, 1979.","DOI":"10.1007\/3-540-09724-4"},{"key":"1_CR4","volume-title":"Natural Deduction \u2014 A proof theoretical study","author":"D. Prawitz","year":"1965","unstructured":"D. Prawitz. Natural Deduction \u2014 A proof theoretical study. Almquist and Wiksell, Stockholm, 1965."},{"key":"1_CR5","volume-title":"Technical Report 9205-01","author":"A. Armando","year":"1992","unstructured":"A. Armando and E. Giunchiglia. Embedding Complex Decision Procedures inside an Interactive Theorem Prover. Technical Report 9205-01, DIST, University of Genova, Genova, Italy, 1992."},{"key":"1_CR6","first-page":"83","volume":"11","author":"R.S. Boyer","year":"1988","unstructured":"R.S. Boyer and J.S. More. Integrating decision procedures into heuristic theorem provers: A case study of linear arithmetic. Machine Intelligence, 11:83\u2013124, 1988.","journal-title":"Machine Intelligence"},{"key":"1_CR7","unstructured":"A. Bundy, A. Smaill, and J. Hesketh. Turning eureka steps into calculations in automatic program synthesis. In S.L.H. Clarke, editor, Proceedings of UK IT 90, pages 221\u20136, 1990. Also available from Edinburgh University as DAI Research Paper no. 448."},{"key":"1_CR8","first-page":"607","volume-title":"Extended version available as DAI Research Paper 359","author":"F. Giunchiglia","year":"1988","unstructured":"F. Giunchiglia and E. Giunchiglia. Building complex derived inference rules: a decider for the class of prenex universal-existential formulas. In Proc. 7th European Conference on Artificial Intelligence, pages 607\u2013609, 1988. Extended version available as DAI Research Paper 359, Dept. of Artificial Intelligence, Edinburgh."},{"key":"1_CR9","volume-title":"Technical Report 9107-03","author":"F. Giunchiglia","year":"1991","unstructured":"F. Giunchiglia, A. Armando, A. Cimatti, E. Giunchiglia P. Pecchiari, L. Serafini, A. Simpson, and P. Traverso. GETFOL Programmer Manual \u2014 GETFOL version 1. Technical Report 9107-03, DIST \u2014 University of Genova, Genova, Italy, 1991."},{"key":"1_CR10","volume-title":"Proceedings 5th Irish Conference on Artificial Intelligence and Cognitive Science","author":"A. Armando","year":"1992","unstructured":"A. Armando, E. Giunchiglia, and P. Traverso. From Propositional Deciders to First Order Deciders: a Structured Approach to the Decision Problem. In Proceedings 5th Irish Conference on Artificial Intelligence and Cognitive Science, Limerick, Ireland, 1992. Springer Verlag. Also IRST-Technical Report 9208-07, IRST, Trento, Italy."},{"key":"1_CR11","doi-asserted-by":"crossref","unstructured":"G. Huet and D.C. Oppen. Equations and rewrite rules: a survey. In R. Book, editor, Formal languages: perspectives and open problems Academic Press, 1980. Presented at the conference on formal language theory, Santa Barbara, 1979. Available from SRI International as technical report CSL-111.","DOI":"10.1016\/B978-0-12-115350-2.50017-8"},{"key":"1_CR12","doi-asserted-by":"crossref","first-page":"191","DOI":"10.1007\/BF02432151","volume":"2","author":"F.J. Pelletier","year":"1986","unstructured":"F.J. Pelletier. Seventy-Five Problems for Testing Automatic Theorem Provers. Journal of Automated Reasoning, 2:191\u2013216, 1986. See also Errata Corrige in Journal of Automated Reasoning, 4:235\u2013236, 1988.","journal-title":"Journal of Automated Reasoning"}],"container-title":["Lecture Notes in Computer Science","Advances in Artificial Intelligence"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-57292-9_36.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,11,17]],"date-time":"2020-11-17T21:10:52Z","timestamp":1605647452000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-57292-9_36"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1993]]},"ISBN":["9783540572923","9783540480389"],"references-count":12,"URL":"https:\/\/doi.org\/10.1007\/3-540-57292-9_36","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[1993]]}}}