{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,6]],"date-time":"2024-09-06T23:07:45Z","timestamp":1725664065454},"publisher-location":"Berlin, Heidelberg","reference-count":24,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540582168"},{"type":"electronic","value":"9783540485735"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1994]]},"DOI":"10.1007\/3-540-58216-9_26","type":"book-chapter","created":{"date-parts":[[2012,2,26]],"date-time":"2012-02-26T15:35:43Z","timestamp":1330270543000},"page":"16-30","source":"Crossref","is-referenced-by-count":1,"title":["Program tactics and logic tactics"],"prefix":"10.1007","author":[{"name":"Mechanized Reasoning Group","sequence":"first","affiliation":[]},{"given":"Fausto","family":"Giunchiglia","sequence":"first","affiliation":[]},{"given":"Paolo","family":"Traverso","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2005,6,2]]},"reference":[{"key":"2_CR1","unstructured":"R.S. Boyer and J.S. Moore. A Computational Logic. Academic Press, 1979. ACM monograph series."},{"key":"2_CR2","doi-asserted-by":"crossref","unstructured":"R.S. Boyer and J.S. More. A theorem prover for a computational logic. In Proceedings of the 10th Conference on Automated Deduction, Lecture Notes in Computer Science 449, Springer-Verlag, pages 1\u201315, 1990.","DOI":"10.1007\/3-540-52885-7_75"},{"key":"2_CR3","first-page":"111","volume-title":"DAI Research Paper No. 349","author":"A. Bundy","year":"1988","unstructured":"A. Bundy. The Use of Explicit Plans to Guide Inductive Proofs. In R. Luck and R. Overbeek, editors, Proc. of the 9th Conference on Automated Deduction, pages 111\u2013120. Springer-Verlag, 1988. Longer version available as DAI Research Paper No. 349, Dept. of Artificial Intelligence, Edinburgh."},{"key":"2_CR4","unstructured":"R. Cartwright and J. McCarthy. Recursive Programs as Functions in a First Order Theory, March 1979. SAIL MEMO AIM-324. Also available as CS Dept. Report No. STAN-CS-79-17."},{"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":"A. Felty. Implementing Tactics and Tacticals in a Higher-Order Logic Programming Language. To appear in: Journal of Automated Reasoning, 1993.","DOI":"10.1007\/BF00881900"},{"key":"2_CR7","doi-asserted-by":"crossref","unstructured":"A. Felty and D. Miller. Specifying Theorem Provers in a Higher-Order Logic Programming Language. In R. Luck and R. Overbeek, editors, Proc. of the 9th Conference on Automated Deduction, pages 61\u201380. Springer-Verlag, 1988.","DOI":"10.1007\/BFb0012823"},{"key":"2_CR8","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 \u2014 University of Genova, Genoa, Italy, 1992."},{"key":"2_CR9","unstructured":"F. Giunchiglia and A. Armando. A Conceptual Architecture for Introspective Systems. Forthcoming IRST-Technical Report, 1993."},{"key":"2_CR10","volume-title":"IRST-Technical Report 9211-21","author":"F. Giunchiglia","year":"1994","unstructured":"F. Giunchiglia and A. Cimatti. Introspective Metatheoretic Reasoning. In Proc. of META-94, Workshop on Metaprogramming in Logic, Pisa, Italy, June 19\u201321, 1994. Also IRST-Technical Report 9211-21, IRST, Trento, Italy."},{"key":"2_CR11","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_CR12","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":"2_CR13","unstructured":"J. Goguen. Higher-order functions considered unnecessary for higher-order programming. In D. A. Turner, editor, Research Topics in Functional Programming, pages 309\u2013351. Addison Wesley, 1990."},{"key":"2_CR14","doi-asserted-by":"crossref","first-page":"69","DOI":"10.1098\/rsta.1992.0026","volume":"339","author":"J. Goguen","year":"1992","unstructured":"J. Goguen, A. Stevens, H. Hilbrdink, and K. Hobley. 2OBJ: a metalogical framework theorem prover based on equational logic. Phil. Trans. R. Soc. Lond., 339:69\u201386, 1992.","journal-title":"Phil. Trans. R. Soc. Lond."},{"key":"2_CR15","unstructured":"J. Goguen, T. Winkler, J. Meseguer, K. Futatsugi, and J. Jouannaud. Introducing OBJ. In J. Goguen, D. Coleman, and R.Gallimore, editors, Applications of algebraic specification using OBJ. Cambridge, 1992."},{"key":"2_CR16","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_CR17","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_CR18","doi-asserted-by":"crossref","unstructured":"D. J. Howe. Computational metatheory in Nuprl. In R. Lusk and R. Overbeek, editors, CADE9, 1988.","DOI":"10.1007\/BFb0012835"},{"key":"2_CR19","volume-title":"Mathematical Theory of Computation","author":"Z. Manna","year":"1974","unstructured":"Z. Manna. Mathematical Theory of Computation. McGraw-Hill, New York, 1974."},{"key":"2_CR20","unstructured":"L. Paulson. Tactics and Tacticals in Cambridge LCF. Technical Report 39, Computer Laboratory, University of Cambridge, 1979."},{"key":"2_CR21","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_CR22","doi-asserted-by":"crossref","first-page":"119","DOI":"10.1016\/0167-6423(83)90008-4","volume":"3","author":"L. C. Paulson","year":"1983","unstructured":"Lawrence C. Paulson. A Higher-Order Implementation of Rewriting. Science of Computer Programming, 3:119\u2013149, 1983.","journal-title":"Science of Computer Programming"},{"key":"2_CR23","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."},{"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","Logic Programming and Automated Reasoning"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-58216-9_26.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,11,17]],"date-time":"2020-11-17T21:18:34Z","timestamp":1605647914000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-58216-9_26"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1994]]},"ISBN":["9783540582168","9783540485735"],"references-count":24,"URL":"https:\/\/doi.org\/10.1007\/3-540-58216-9_26","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[1994]]}}}