{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,6]],"date-time":"2024-09-06T23:15:57Z","timestamp":1725664557477},"publisher-location":"Berlin, Heidelberg","reference-count":19,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540587927"},{"type":"electronic","value":"9783540491040"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1994]]},"DOI":"10.1007\/3-540-58792-6_26","type":"book-chapter","created":{"date-parts":[[2012,2,26]],"date-time":"2012-02-26T16:45:24Z","timestamp":1330274724000},"page":"425-439","source":"Crossref","is-referenced-by-count":2,"title":["Introspective metatheoretic reasoning"],"prefix":"10.1007","author":[{"given":"Fausto","family":"Giunchiglia","sequence":"first","affiliation":[]},{"given":"Alessandro","family":"Cimatti","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2005,6,9]]},"reference":[{"key":"26_CR1","unstructured":"D. Basin and R. Constable. Metalogical Frameworks. In Proceedings of the Second Workshop on Logical Frameworks, Edinburgh, Scotland, 1991. To Appear as a chapter in a Cambridge University Press book."},{"key":"26_CR2","unstructured":"R.S. Boyer and J.S. Moore. A Computational Logic. Academic Press, 1979. ACM monograph series."},{"key":"26_CR3","unstructured":"R.S. Boyer and J.S. Moore. Metafunctions: proving them correct and using them efficiently as new proof procedures. In R.S. Boyer and J.S. Moore, editors, The correctness problem in computer science, pages 103\u2013184. Academic Press, 1981."},{"key":"26_CR4","unstructured":"R.L. Constable, S.F. Allen, H.M. Bromley, et al. Implementing Mathematics with the NuPRL Proof Development System. Prentice Hall, 1986."},{"key":"26_CR5","volume-title":"Technical Report 8906-22","author":"F. Giunchiglia","year":"1989","unstructured":"F. Giunchiglia and A. Cimatti. Hgkm Manual \u2014 a revised version. Technical Report 8906-22, IRST, Trento, Italy, 1989."},{"key":"26_CR6","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. Upgraded and extended version forthcoming."},{"key":"26_CR7","volume-title":"Technical Report 92-0010","author":"F. Giunchiglia","year":"1992","unstructured":"F. Giunchiglia. The Getfol Manual \u2014 Getfol version 1. Technical Report 92-0010, DIST-University of Genova, Genoa, Italy, 1992."},{"key":"26_CR8","unstructured":"F. Giunchiglia and A. Smaill. Reflection in constructive and non-constructive automated reasoning. In H. Abramson and M. H. Rogers, editors, Proc. of META-88, Workshop on Metaprogramming in Logic, pages 123\u2013145. MIT Press, 1988. Also IRST-Technical Report 8902-04 and DAI Research Paper 375, University of Edinburgh."},{"key":"26_CR9","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":"26_CR10","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. Submitted for publication to: Journal of Artificial Intelligence."},{"key":"26_CR11","doi-asserted-by":"crossref","unstructured":"F. Giunchiglia and P. Traverso. Program Tactics and Logic Tactics. In Proceedings 5th Intnl. Conference on Logic Programming and Automated Reasoning (LPAR'94), Kiev, Ukraine, July 16\u201321, 1994. Also IRST-Technical Report 9301-01, IRST, Trento, Italy. Presented at the Third International Symposium on Artificial Intelligence and Mathematics, Fort Lauderdale, Florida, January 1994.","DOI":"10.1007\/3-540-58216-9_26"},{"key":"26_CR12","volume-title":"Manual 9109-08","author":"F. Giunchiglia","year":"1991","unstructured":"F. Giunchiglia and R.W. Weyhrauch. Fol User Manual \u2014 Fol version 2. Manual 9109-08, IRST, Trento, Italy, 1991. Also DIST Technical Report 91-0006, DIST, University of Genova."},{"key":"26_CR13","unstructured":"P. N. Johnson-Laird. Mental Models. Cambridge University Press, 1983."},{"key":"26_CR14","unstructured":"Z. Manna and R. Waldinger. The Deductive Synthesis of Imperative LISP Programs. In Sixth National Conference on Artificial Intelligence. AAAI, 1987."},{"key":"26_CR15","doi-asserted-by":"crossref","unstructured":"Z. Manna and R. Waldinger. How to clear a block: A Theory of Plans. Technical Report STAN-CS-87-1141, Department of Computer Science, Stanford University, 1987.","DOI":"10.1007\/BF00247434"},{"key":"26_CR16","doi-asserted-by":"publisher","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":"26_CR17","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":"26_CR18","doi-asserted-by":"crossref","unstructured":"B.C. Smith. Reflection and Semantics in LISP. In Proc. 11th ACM POPL, pages 23\u201335, 1983.","DOI":"10.1145\/800017.800513"},{"issue":"1","key":"26_CR19","doi-asserted-by":"publisher","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. Artificial Intelligence, 13(1):133\u2013176, 1980.","journal-title":"Artificial Intelligence"}],"container-title":["Lecture Notes in Computer Science","Logic Program Synthesis and Transformation \u2014 Meta-Programming in Logic"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-58792-6_26.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,11,17]],"date-time":"2020-11-17T21:24:09Z","timestamp":1605648249000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-58792-6_26"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1994]]},"ISBN":["9783540587927","9783540491040"],"references-count":19,"URL":"https:\/\/doi.org\/10.1007\/3-540-58792-6_26","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[1994]]}}}