{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,1,29]],"date-time":"2024-01-29T21:08:03Z","timestamp":1706562483465},"reference-count":32,"publisher":"Springer Science and Business Media LLC","issue":"2","license":[{"start":{"date-parts":[[1996,9,1]],"date-time":"1996-09-01T00:00:00Z","timestamp":841536000000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Ann Math Artif Intell"],"published-print":{"date-parts":[[1996,9]]},"DOI":"10.1007\/bf02127970","type":"journal-article","created":{"date-parts":[[2005,9,14]],"date-time":"2005-09-14T17:08:51Z","timestamp":1126717731000},"page":"235-259","source":"Crossref","is-referenced-by-count":2,"title":["Program tactics and logic tactics"],"prefix":"10.1007","volume":"17","author":[{"given":"Fausto","family":"Giunchiglia","sequence":"first","affiliation":[]},{"given":"Paolo","family":"Traverso","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"BF02127970_CR1","unstructured":"A. Armando,Architetture Riflessive per la Deduzione Automatica, Ph.D. Thesis, DIST \u2014 University of Genoa (1993)."},{"key":"BF02127970_CR2","unstructured":"D. Basin and R. Constable, Metalogical frameworks,Proceedings of the Second Workshop on Logical Frameworks, Edinburgh, Scotland (1991). To appear as a chapter in a Cambridge University Press book."},{"key":"BF02127970_CR3","unstructured":"R.S. Boyer and J.S. Moore,A Computational Logic, ACM monograph series (Academic Press, 1979)."},{"key":"BF02127970_CR4","unstructured":"R.S. Boyer and J.S. Moore, Metafunctions: proving them correct and using them efficiently as new proof procedures, in:The Correctness Problem in Computer Science, eds. R.S. Boyer and J.S. Moore (Academic Press, 1981) pp. 103\u2013184."},{"key":"BF02127970_CR5","doi-asserted-by":"crossref","unstructured":"R.S. Boyer and J.S. Moore, A theorem prover for a computational logic,Proceedings of the 10th Conference on Automated Deduction, Lecture Notes in Computer Science 449 (Springer-Verlag, 1990) pp. 1\u201315.","DOI":"10.1007\/3-540-52885-7_75"},{"key":"BF02127970_CR6","doi-asserted-by":"crossref","unstructured":"A. Bundy. The use of explicit plans to guide inductive proofs,Proc. of the 9th Conference on Automated Deduction, eds. R. Luck and R. Overbeek (Springer-Verlag, 1988) pp. 111\u2013120. Longer version available as DAI Research Paper No. 349, Dept. of Artificial Intelligence, Edinburgh.","DOI":"10.1007\/BFb0012826"},{"key":"BF02127970_CR7","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":"BF02127970_CR8","unstructured":"R.L. Constable, S.F. Allen, H.M. Bromley et al.,Implementing Mathematics with the NuPRL Proof Development System (Prentice-Hall, 1986)."},{"key":"BF02127970_CR9","doi-asserted-by":"crossref","first-page":"43","DOI":"10.1007\/BF00881900","volume":"11","author":"A. Felty","year":"1993","unstructured":"A. Felty, Implementing tactics and tacticals in a higher-order logic programming language,Journal of Automated Reasoning 11(1993) 43\u201381.","journal-title":"Journal of Automated Reasoning"},{"key":"BF02127970_CR10","doi-asserted-by":"crossref","unstructured":"A. Felty and D. Howe, Tactic theorem proving with refinement tree proofs and metavariables,Proc. of the 12th Conference on Automated Deduction, ed. A. Bundy (Springer-Verlag, 1994) pp. 605\u2013619.","DOI":"10.1007\/3-540-58156-1_44"},{"key":"BF02127970_CR11","doi-asserted-by":"crossref","unstructured":"A. Felty and D. Miller, Specifying theorem provers in a higher-order logic programming language,Proc. of the 9th Conference on Automated Deduction, eds. R. Luck and R. Overbeek (Springer-Verlag, 1988) pp. 61\u201380.","DOI":"10.1007\/BFb0012823"},{"key":"BF02127970_CR12","series-title":"Technical Report","volume-title":"The GETFOL Manual \u2014 GETFOL version 1","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":"BF02127970_CR13","unstructured":"F. Giunchiglia and A. Armando, A conceptual architecture for introspective systems, Forthcoming IRST-Technical Report (1993)."},{"key":"BF02127970_CR14","series-title":"Technical Repot","volume-title":"HGKM Manual \u2014 a revised version","author":"F. Giunchiglia","year":"1989","unstructured":"F. Giunchiglia and A. Cimatti, HGKM Manual \u2014 a revised version, Technical Repot 8906-22, IRST, Trento, Italy (1989)."},{"key":"BF02127970_CR15","unstructured":"F. Giunchiglia and A. Cimatti, Introspective metatheoretic reasoning,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":"BF02127970_CR16","unstructured":"F. Giunchiglia and P. Traverso, Reflective reasoning with and between a declarative metatheory and the implementation code,Proc. of the 12th International Joint Conference on Artificial Intelligence, Sydney (1991) pp. 111\u2013117. Also IRST-Technical Report 9012-03, IRST, Trento, Italy."},{"key":"BF02127970_CR17","doi-asserted-by":"crossref","first-page":"197","DOI":"10.1016\/0004-3702(95)00002-X","volume":"80","author":"F. Giunchiglia","year":"1996","unstructured":"F. Giunchiglia and P. Traverso, A metatheory of a mechanized object theory,Artificial Intelligence 80 (1996) 197\u2013241. Also IRST-Technical Report 9211-24, IRST, Trento, Italy (1992).","journal-title":"Artificial Intelligence"},{"key":"BF02127970_CR18","unstructured":"J. Goguen, Higher-order functions considered unnecessary for higher-order programming,Research Topics in Functional Programming, ed. D.A. Turner (Addison-Wesley, 1990) pp. 309\u2013351."},{"key":"BF02127970_CR19","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 (1992) 69\u201386.","journal-title":"Phil. Trans. R. Soc. Lond."},{"key":"BF02127970_CR20","unstructured":"J. Goguen, T. Winkler, J. Meseguer, K. Futatsugi and J. Jouannaud, Introducing OBJ, in:Applications of Algebraic Specification Using OBJ, eds. J. Goguen, D. Coleman and R. Gallimore (Cambridge, 1992)."},{"key":"BF02127970_CR21","doi-asserted-by":"crossref","unstructured":"M.J. Gordon, A.J. Milner and C.P. Wadsworth,Edinburgh LCF \u2014 A Mechanized Logic of Computation, Lecture Notes in Computer Science 78 (Springer-Verlag, 1979).","DOI":"10.1007\/3-540-09724-4"},{"key":"BF02127970_CR22","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":"BF02127970_CR23","doi-asserted-by":"crossref","unstructured":"D.J. Howe, Computational metatheory in Nuprl, in:CADE9, eds. R. Lusk and R. Overbeek (1988).","DOI":"10.1007\/BFb0012835"},{"key":"BF02127970_CR24","doi-asserted-by":"crossref","unstructured":"M. Kerber and M. Kohlhase, A mechanization of strong kleene logic for partial functions,Proc. of the 12th Conference on Automated Deduction, ed. A. Bundy (Springer-Verlag, 1994) pp. 371\u2013385.","DOI":"10.1007\/3-540-58156-1_26"},{"key":"BF02127970_CR25","volume-title":"Mathematical Theory of Computation","author":"Z. Manna","year":"1974","unstructured":"Z. Manna,Mathematical Theory of Computation (McGraw-Hill, New York, 1974)."},{"key":"BF02127970_CR26","unstructured":"E. Melis, A model of analogy-driven proof-plan construction,Proc. of the 14th International Joint Conference on Artificial Intelligence (1995)."},{"key":"BF02127970_CR27","unstructured":"L. Paulson, Tactics and tacticals in Cambridge LCF, Technical Report 39, Computer Laboratory, University of Cambridge (1979)."},{"key":"BF02127970_CR28","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 (1989) 363\u2013396.","journal-title":"Journal of Automated Reasoning"},{"key":"BF02127970_CR29","doi-asserted-by":"crossref","unstructured":"L. Paulson, Designing a theorem prover, in:Handbook of Logic in Computer Science, Vol. II, eds. S. Abramsky, D. Gabbay and T.S.E. Maibaum (Oxford University Press, 1992) pp. 416\u2013475.","DOI":"10.1093\/oso\/9780198537618.003.0004"},{"key":"BF02127970_CR30","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 Wiskell, Stockholm, 1965)."},{"key":"BF02127970_CR31","series-title":"Technical Report","volume-title":"Representing higher-order logic proofs in HOL","author":"J. Wright von","year":"1994","unstructured":"J. von Wright, Representing higher-order logic proofs in HOL, Technical Report jan-18-94, Abo Akademi University, Turku, Finland (1994)."},{"issue":"1","key":"BF02127970_CR32","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,Artificial Intelligence 13(1) (1980) 133\u2013176.","journal-title":"Artificial Intelligence"}],"container-title":["Annals of Mathematics and Artificial Intelligence"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/BF02127970.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/BF02127970\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/BF02127970","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,1,29]],"date-time":"2024-01-29T20:15:55Z","timestamp":1706559355000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/BF02127970"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1996,9]]},"references-count":32,"journal-issue":{"issue":"2","published-print":{"date-parts":[[1996,9]]}},"alternative-id":["BF02127970"],"URL":"https:\/\/doi.org\/10.1007\/bf02127970","relation":{},"ISSN":["1012-2443","1573-7470"],"issn-type":[{"value":"1012-2443","type":"print"},{"value":"1573-7470","type":"electronic"}],"subject":[],"published":{"date-parts":[[1996,9]]}}}