{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,6]],"date-time":"2024-09-06T23:01:23Z","timestamp":1725663683518},"publisher-location":"Berlin, Heidelberg","reference-count":24,"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_37","type":"book-chapter","created":{"date-parts":[[2012,2,26]],"date-time":"2012-02-26T12:40:22Z","timestamp":1330260022000},"page":"11-22","source":"Crossref","is-referenced-by-count":2,"title":["Building and executing proof strategies in a formal metatheory"],"prefix":"10.1007","author":[{"given":"Alessandro","family":"Armando","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Alessandro","family":"Cimatti","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Luca","family":"Vigan\u00f2","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2005,6,3]]},"reference":[{"key":"2_CR1","doi-asserted-by":"crossref","unstructured":"A. Armando and E. Giunchiglia. Embedding Complex Decision Procedures inside an Interactive Theorem Prover. Annals of Artificial Intelligence and Mathematics, 8(3\u20134), 1993. In press.","DOI":"10.1007\/BF01530803"},{"issue":"2","key":"2_CR2","doi-asserted-by":"crossref","first-page":"193","DOI":"10.1145\/322248.322249","volume":"28","author":"P.B. Andrews","year":"1981","unstructured":"P.B. Andrews. Theorem Proving via General Matings. Journal of the ACM, 28(2):193\u2013214, 1981.","journal-title":"Journal of the ACM"},{"issue":"4","key":"2_CR3","first-page":"633","volume":"28","author":"W. Bibel","year":"1981","unstructured":"W. Bibel. On Matrices with Connections. Journal of the A CM, 28(4):633\u2013645, 1981.","journal-title":"Journal of the A CM"},{"key":"2_CR4","unstructured":"R.S. Boyer and J.S. Moore. A Computational Logic. Academic Press, 1979. ACM monograph series."},{"key":"2_CR5","unstructured":"R.L. Constable, S.F. Allen, H.M. Bromley, et al. Implementing Mathematics with the NuPRL Proof Development System. Prentice Hall, 1986."},{"key":"2_CR6","doi-asserted-by":"crossref","unstructured":"N.G. deBruijn. The mathematical language automath. In Symposium in Automatic Demonstration, Lecture Notes in Mathematics, volume Vol. 125, pages 29\u201361. Springer-Verlag, 1970.","DOI":"10.1007\/BFb0060623"},{"key":"2_CR7","unstructured":"F. Giunchiglia and A. Armando. A Conceptual Architecture for Introspective Systems. Forthcoming IRST-Technical Report, 1993."},{"key":"2_CR8","volume-title":"Technical Report 9107-05","author":"F. Giunchiglia","year":"1991","unstructured":"F. Giunchiglia and A. Cimatti. HGKM User Manual \u2014 HGKM version 2. Technical Report 9107-05, DIST \u2014 University of Genova, Genova, Italy, 1991."},{"key":"2_CR9","volume-title":"Technical Report 9211-21","author":"F. Giunchiglia","year":"1992","unstructured":"F. Giunchiglia and A. Cimatti. Introspective Metatheoretic Reasoning. Technical Report 9211-21, IRST, Trento, Italy, 1992."},{"key":"2_CR10","volume-title":"Technical Report 9211-22","author":"F. Giunchiglia","year":"1992","unstructured":"F. Giunchiglia and A. Cimatti. Introspective Metatheoretic Theorem Proving. Technical Report 9211-22, IRST, Trento, Italy, 1992."},{"key":"2_CR11","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."},{"key":"2_CR12","unstructured":"M.J. Gordon, R. Milner, L. Morris, and C. Wadsworth. A Metalanguage for Interactive Proof in LCF. CSR report series CSR-16-77, Department of Artificial Intelligence, Dept. of Computer Science, University of Edinburgh, 1977."},{"key":"2_CR13","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":"2_CR14","first-page":"111","volume-title":"IRST-Technical Report 9012-03","author":"F. Giunchiglia","year":"1991","unstructured":"F. Giunchiglia and P. Traverso. Reflective reasoning with and between a declarative metatheory and the implementation code. In Proc. of the 12th International Joint Conference on Artificial Intelligence, pages 111\u2013117, Sydney, 1991. Also IRST-Technical Report 9012-03, IRST, Trento, Italy."},{"key":"2_CR15","volume-title":"GETFOL User Manual \u2014 GETFOL version 1. Manual 9109-09","author":"F. Giunchiglia","year":"1991","unstructured":"F. Giunchiglia and P. Traverso. GETFOL User Manual \u2014 GETFOL version 1. Manual 9109-09, IRST, Trento, Italy, 1991. Also MRG-DIST Technical Report 9107-01, DIST, University of Genova."},{"key":"2_CR16","volume-title":"Technical Report 9211-24","author":"F. Giunchiglia","year":"1992","unstructured":"F. Giunchiglia and P. Traverso. A Metatheory of a Mechanized Object Theory. Technical Report 9211-24, IRST, Trento, Italy, 1992."},{"key":"2_CR17","volume-title":"Technical Report 9301-01","author":"F. Giunchiglia","year":"1993","unstructured":"F. Giunchiglia and P. Traverso. Program tactics and logic tactics. Technical Report 9301-01, IRST, Trento, Italy, 1993."},{"key":"2_CR18","first-page":"190","volume-title":"IRST-Technical Report 9211-18","author":"F. Giunchiglia","year":"1992","unstructured":"F. Giunchiglia, P. Traverso, A. Cimatti, and P. Pecchiari. A System for Multi-Level Reasoning. In A. Yonozawa and B.C. Smith, editors, Proc. IMSA '92 International Workshop on Reflection and Meta-level Architecture, pages 190\u2013195, Tokyo, 1992. Also IRST-Technical Report 9211-18, IRST, Trento, Italy."},{"key":"2_CR19","doi-asserted-by":"crossref","first-page":"90","DOI":"10.1145\/357084.357090","volume":"2","author":"Z. Manna","year":"1980","unstructured":"Z. Manna and R. Waldinger. A deductive approach to program synthesis. ACM Transactions on Programming Languages and Systems, 2:90\u2013121, 1980.","journal-title":"ACM Transactions on Programming Languages and Systems"},{"key":"2_CR20","doi-asserted-by":"crossref","first-page":"363","DOI":"10.1007\/BF00248324","volume":"5","author":"L. Paulson","year":"1989","unstructured":"L. Paulson. The Foundation of a Generic Theorem Prover. Journal of Automated Reasoning, 5:363\u2013396, 1989.","journal-title":"Journal of Automated Reasoning"},{"key":"2_CR21","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":"2_CR22","doi-asserted-by":"crossref","first-page":"23","DOI":"10.1145\/321250.321253","volume":"12","author":"A. Robinson","year":"1965","unstructured":"A. Robinson. A Machine oriented Logic Based on the resolution principle. Journal of the ACM, 12:23\u201341, 1965.","journal-title":"Journal of the ACM"},{"key":"2_CR23","doi-asserted-by":"crossref","unstructured":"C. Walther. Argument-Bounded Algorithms as a Basis for Automated Termination Proofs. In Proc. of the 9th Conference on Automated Deduction, 1988.","DOI":"10.1007\/BFb0012861"},{"issue":"1","key":"2_CR24","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."}],"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_37.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,11,17]],"date-time":"2020-11-17T21:10:53Z","timestamp":1605647453000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-57292-9_37"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1993]]},"ISBN":["9783540572923","9783540480389"],"references-count":24,"URL":"https:\/\/doi.org\/10.1007\/3-540-57292-9_37","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[1993]]}}}