{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,6,12]],"date-time":"2025-06-12T10:43:15Z","timestamp":1749724995415},"reference-count":69,"publisher":"Elsevier BV","issue":"2","license":[{"start":{"date-parts":[[1996,2,1]],"date-time":"1996-02-01T00:00:00Z","timestamp":823132800000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.elsevier.com\/tdm\/userlicense\/1.0\/"},{"start":{"date-parts":[[2013,7,25]],"date-time":"2013-07-25T00:00:00Z","timestamp":1374710400000},"content-version":"vor","delay-in-days":6384,"URL":"https:\/\/www.elsevier.com\/open-access\/userlicense\/1.0\/"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Artificial Intelligence"],"published-print":{"date-parts":[[1996,2]]},"DOI":"10.1016\/0004-3702(95)00002-x","type":"journal-article","created":{"date-parts":[[2002,7,25]],"date-time":"2002-07-25T23:37:38Z","timestamp":1027640258000},"page":"197-241","source":"Crossref","is-referenced-by-count":9,"title":["A metatheory of a mechanized object theory"],"prefix":"10.1016","volume":"80","author":[{"given":"Fausto","family":"Giunchiglia","sequence":"first","affiliation":[]},{"given":"Paolo","family":"Traverso","sequence":"additional","affiliation":[]}],"member":"78","reference":[{"key":"10.1016\/0004-3702(95)00002-X_BIB1","article-title":"Architetture riflessive per la deduzione automatica","author":"Armando","year":"1993"},{"key":"10.1016\/0004-3702(95)00002-X_BIB2","article-title":"Using typed lambda calculus to implement formal systems on a machine","author":"Avron","year":"1989"},{"key":"10.1016\/0004-3702(95)00002-X_BIB3","series-title":"Proceedings Second Workshop on Logical Frameworks","article-title":"Metalogical frameworks","author":"Basin","year":"1991"},{"key":"10.1016\/0004-3702(95)00002-X_BIB4_1","series-title":"AI\u2217IA 1991, 2nd Conference of the Italian Association for Artificial intelligence","first-page":"48","article-title":"Automating meta-theory creation and system extension","author":"Basin","year":"1991"},{"key":"10.1016\/0004-3702(95)00002-X_BIB4_2","unstructured":"also: IRST-Technical Report 9101-04, IRST, Trento."},{"key":"10.1016\/0004-3702(95)00002-X_BIB5","series-title":"Logic Programming","first-page":"153","article-title":"Amalgamating language and meta-language in logic programming","author":"Bowen","year":"1982"},{"key":"10.1016\/0004-3702(95)00002-X_BIB6","series-title":"IEEE Symposium on Logic Programming","first-page":"669","article-title":"A meta-level extension of prolog","author":"Bowen","year":"1985"},{"key":"10.1016\/0004-3702(95)00002-X_BIB7","author":"Boyer","year":"1979"},{"key":"10.1016\/0004-3702(95)00002-X_BIB8","first-page":"103","article-title":"Metafunctions: proving them correct and using them efficiently as new proof procedures","author":"Boyer","year":"1981"},{"key":"10.1016\/0004-3702(95)00002-X_BIB9","series-title":"Proceedings 10th Conference on Automated Deduction","first-page":"1","article-title":"A theorem prover for a computational logic","volume":"449","author":"Boyer","year":"1990"},{"key":"10.1016\/0004-3702(95)00002-X_BIB10_1","series-title":"Proceedings 9th Conference on Automated Deduction","first-page":"111","article-title":"The use of explicit plans to guide inductive proofs","author":"Bundy","year":"1988"},{"key":"10.1016\/0004-3702(95)00002-X_BIB10_2","unstructured":"Longer version available as DAI Research Paper No. 349, Department of Artificial Intelligence, Edinburgh."},{"key":"10.1016\/0004-3702(95)00002-X_BIB11_1","doi-asserted-by":"crossref","first-page":"189","DOI":"10.1016\/0004-3702(81)90010-2","article-title":"Using meta-level inference for selective application of multiple rewrite rules in algebraic manipulation","volume":"16","author":"Bundy","year":"1981","journal-title":"Artif. Intell."},{"key":"10.1016\/0004-3702(95)00002-X_BIB11_2","unstructured":"also: DAI Research Paper 121, Department of Artificial Intelligence, Edinburgh."},{"key":"10.1016\/0004-3702(95)00002-X_BIB12_1","article-title":"Recursive programs as functions in a first order theory","author":"Cartwright","year":"1979","journal-title":"SAIL MEMO AIM-324"},{"key":"10.1016\/0004-3702(95)00002-X_BIB12_2","unstructured":"also: CS Department Report STAN-CS-79-17"},{"key":"10.1016\/0004-3702(95)00002-X_BIB13","author":"Chang","year":"1973"},{"key":"10.1016\/0004-3702(95)00002-X_BIB14","author":"Constable","year":"1986"},{"key":"10.1016\/0004-3702(95)00002-X_BIB15","doi-asserted-by":"crossref","first-page":"259","DOI":"10.2307\/2964649","article-title":"Transfinite recursive progressions of axiomatic theories","volume":"27","author":"Feferman","year":"1962","journal-title":"J. Symbolic Logic"},{"key":"10.1016\/0004-3702(95)00002-X_BIB16","doi-asserted-by":"crossref","first-page":"43","DOI":"10.1007\/BF00881900","article-title":"Implementing tactics and tacticals in a higher-order logic programming language","volume":"11","author":"Felty","year":"1993","journal-title":"J. Autom. Reasoning"},{"key":"10.1016\/0004-3702(95)00002-X_BIB17","article-title":"The GETFOL Manual \u2014 GETFOL version 1","author":"Giunchiglia","year":"1992"},{"key":"10.1016\/0004-3702(95)00002-X_BIB18","article-title":"A conceptual architecture for introspective systems","author":"Giunchiglia","year":"1994"},{"key":"10.1016\/0004-3702(95)00002-X_BIB19","article-title":"HGKM Manual \u2014 a revised version","author":"Giunchiglia","year":"1989"},{"key":"10.1016\/0004-3702(95)00002-X_BIB20_1","series-title":"Proceedings META-94, Workshop on Metaprogramming in Logic","article-title":"Introspective metatheoretic reasoning","author":"Giunchiglia","year":"1994"},{"key":"10.1016\/0004-3702(95)00002-X_BIB20_2","unstructured":"also: Tech. Rept. 9211-21, IRST, Trento."},{"key":"10.1016\/0004-3702(95)00002-X_BIB21","doi-asserted-by":"crossref","first-page":"29","DOI":"10.1016\/0004-3702(94)90037-X","article-title":"Multilanguage hierarchical logics (or: how we can do without modal logics)","volume":"65","author":"Giunchiglia","year":"1994","journal-title":"Artif Intell."},{"key":"10.1016\/0004-3702(95)00002-X_BIB22_1","series-title":"Proceedings META-92, Workshop on Metaprogramming in Logic","first-page":"235","article-title":"Hierarchical meta-logics: intuitions, proof theory and semantics","volume":"649","author":"Giunchiglia","year":"1992"},{"key":"10.1016\/0004-3702(95)00002-X_BIB22_2","unstructured":"also: Tech. Rept. 9101-05, IRST, Trento"},{"key":"10.1016\/0004-3702(95)00002-X_BIB23_1","series-title":"Proceedings META-88, Workshop on Metaprogramming in Logic","first-page":"123","article-title":"Reflection in constructive and non-constructive automated reasoning","author":"Giunchiglia","year":"1988"},{"key":"10.1016\/0004-3702(95)00002-X_BIB23_2","unstructured":"also: Tech. Rept. 8902-04, IRST, Trento and DAI Research Paper 375, University of Edinburgh, Edinburgh"},{"key":"10.1016\/0004-3702(95)00002-X_BIB24_1","series-title":"Proceedings META-90, Workshop on Metaprogramming in Logic","first-page":"306","article-title":"Plan formation and execution in a uniform architecture of declarative metatheories","author":"Giunchiglia","year":"1990"},{"key":"10.1016\/0004-3702(95)00002-X_BIB24_2","unstructured":"also: Tech. Rept. 9003-12, IRST, Trento"},{"key":"10.1016\/0004-3702(95)00002-X_BIB25_1","series-title":"Proceedings 5th International Conference on Logic Programming and Automated Reasoning (LPAR'94)","article-title":"Program tactics and logic tactics","author":"Giunchiglia","year":"1994"},{"key":"10.1016\/0004-3702(95)00002-X_BIB25_2","series-title":"presented at the Third International Symposium on Artificial Intelligence and Mathematics","author":"Giunchiglia","year":"1994"},{"key":"10.1016\/0004-3702(95)00002-X_BIB26_1","series-title":"Meta-Level Architectures and Reflection","first-page":"271","article-title":"A multi-context monotonic axiomatization of inessential non- monotonicity","author":"Giunchiglia","year":"1988"},{"key":"10.1016\/0004-3702(95)00002-X_BIB26_2","unstructured":"also: Tech. Rept. 9105-02, DIST, University of Genova, Genova."},{"key":"10.1016\/0004-3702(95)00002-X_BIB27_1","article-title":"FOL User Manual \u2014 FOL version 2","author":"Giunchiglia","year":"1991"},{"key":"10.1016\/0004-3702(95)00002-X_BIB27_2","unstructured":"also: Tech. Rept. 91 -0006, DIST, University of Genova, Genova."},{"key":"10.1016\/0004-3702(95)00002-X_BIB28","doi-asserted-by":"crossref","first-page":"173","DOI":"10.1007\/BF01700692","article-title":"\u00dcber formal unentscheidbare S\u00e4tze der Principia Mathematica und verwandter Systeme I","volume":"38","author":"G\u00f6del","year":"1931","journal-title":"Monatsh. Math. Phys."},{"key":"10.1016\/0004-3702(95)00002-X_BIB29","series-title":"Research Topics in Functional Programming","first-page":"309","article-title":"Higher-order functions considered unnecessary for higher-order programming","author":"Goguen","year":"1990"},{"key":"10.1016\/0004-3702(95)00002-X_BIB30","doi-asserted-by":"crossref","first-page":"69","DOI":"10.1098\/rsta.1992.0026","article-title":"2OBJ: a metalogical framework theorem prover based on equational logic","volume":"339","author":"Goguen","year":"1992","journal-title":"Phil. Trans. R. Soc. Lond."},{"key":"10.1016\/0004-3702(95)00002-X_BIB31","series-title":"VLSI Specification and Synthesis","article-title":"A proof generating system for higher-order logic","author":"Gordon","year":"1987"},{"key":"10.1016\/0004-3702(95)00002-X_BIB32","article-title":"Edinburgh LCF \u2014 A Mechanized Logic of Computation","volume":"78","author":"Gordon","year":"1979"},{"key":"10.1016\/0004-3702(95)00002-X_BIB33","series-title":"Symposium on Logic in Computer Science","first-page":"194","article-title":"A framework for defining logics","author":"Harper","year":"1971"},{"key":"10.1016\/0004-3702(95)00002-X_BIB34","author":"Harper","year":"1986"},{"key":"10.1016\/0004-3702(95)00002-X_BIB35","series-title":"Proceedings META-88, Workshop on Metaprogramming in Logic","article-title":"Analysis of meta-programs","author":"Hill","year":"1989"},{"key":"10.1016\/0004-3702(95)00002-X_BIB36","article-title":"The G\u00f6del programming language","author":"Hill","year":"1992"},{"key":"10.1016\/0004-3702(95)00002-X_BIB37","doi-asserted-by":"crossref","DOI":"10.1007\/BFb0012835","article-title":"Computational metatheory in Nuprl","author":"Howe","year":"1988"},{"key":"10.1016\/0004-3702(95)00002-X_BIB38","series-title":"The Sixth European Conference on Object-Oriented Programming","article-title":"A reflective model of inheritance","author":"Jagannathan","year":"1992"},{"key":"10.1016\/0004-3702(95)00002-X_BIB39","author":"Kleene","year":"1952"},{"key":"10.1016\/0004-3702(95)00002-X_BIB40","article-title":"Formalized metatheory in type theory","author":"Knoblock","year":"1986"},{"key":"10.1016\/0004-3702(95)00002-X_BIB41","series-title":"Recent Essays on Truth and the Liar Paradox","first-page":"53","article-title":"Outline of a theory of truth","author":"Kripke","year":"1984"},{"key":"10.1016\/0004-3702(95)00002-X_BIB42","author":"Manna","year":"1974"},{"key":"10.1016\/0004-3702(95)00002-X_BIB43","article-title":"Tactics and tacticals in Cambridge LCF","author":"Paulson","year":"1979"},{"key":"10.1016\/0004-3702(95)00002-X_BIB44","doi-asserted-by":"crossref","first-page":"363","DOI":"10.1007\/BF00248324","article-title":"The foundation of a generic theorem prover","volume":"5","author":"Paulson","year":"1989","journal-title":"J. Autom. Reasoning"},{"key":"10.1016\/0004-3702(95)00002-X_BIB45","doi-asserted-by":"crossref","first-page":"119","DOI":"10.1016\/0167-6423(83)90008-4","article-title":"A higher-order implementation of rewriting","volume":"3","author":"Paulson","year":"1983","journal-title":"Sci. Comput. Program."},{"key":"10.1016\/0004-3702(95)00002-X_BIB46","author":"Prawitz","year":"1965"},{"key":"10.1016\/0004-3702(95)00002-X_BIB47","series-title":"Proceedings 11th ACM POPL","first-page":"23","article-title":"Reflection and semantics in LISP","author":"Smith","year":"1983"},{"key":"10.1016\/0004-3702(95)00002-X_BIB48","doi-asserted-by":"crossref","first-page":"141","DOI":"10.1016\/0004-3702(81)90008-4","article-title":"Planning and meta-planning","volume":"16","author":"Stefik","year":"1981","journal-title":"Artif. Intell."},{"key":"10.1016\/0004-3702(95)00002-X_BIB49_1","article-title":"The essence of RUM: theory of the intensional and extensional aspects of LISP-type computation","author":"Talcott","year":"1985"},{"key":"10.1016\/0004-3702(95)00002-X_BIB49_2","unstructured":"also: report STAN-CS-85-1060."},{"key":"10.1016\/0004-3702(95)00002-X_BIB50","author":"Tarski","year":"1956"},{"key":"10.1016\/0004-3702(95)00002-X_BIB51","author":"Van Heijenoort","year":"1967"},{"key":"10.1016\/0004-3702(95)00002-X_BIB52","article-title":"Sintesi ed esecuzione di strategie di prova nella metateoria formale di un dimostratore interattivo","author":"Vigan\u00f2","year":"1994"},{"key":"10.1016\/0004-3702(95)00002-X_BIB53","doi-asserted-by":"crossref","DOI":"10.1007\/3-540-58450-1_60","article-title":"Representing higher-order logic proofs in HOL","author":"von Wright","year":"1994"},{"key":"10.1016\/0004-3702(95)00002-X_BIB54","doi-asserted-by":"crossref","first-page":"133","DOI":"10.1016\/0004-3702(80)90015-6","article-title":"Prolegomena to a theory of mechanized formal reasoning","volume":"13","author":"Weyhrauch","year":"1980","journal-title":"Artif. Intell."},{"key":"10.1016\/0004-3702(95)00002-X_BIB55","series-title":"Proceedings 6th Conference on Automatic Deduction","article-title":"An example of FOL using metatheory. Formalizing reasoning and introducing derived inference rules","author":"Weyhrauch","year":"1982"},{"key":"10.1016\/0004-3702(95)00002-X_BIB56","article-title":"HGKM: a simple implementation","author":"Weyhrauch","year":"1985","journal-title":"FOL working paper 4"},{"key":"10.1016\/0004-3702(95)00002-X_BIB57","first-page":"254","article-title":"A reflective object oriented concurrent language","volume":"441","author":"Yonezawa","year":"1991"}],"container-title":["Artificial Intelligence"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/api.elsevier.com\/content\/article\/PII:000437029500002X?httpAccept=text\/xml","content-type":"text\/xml","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/api.elsevier.com\/content\/article\/PII:000437029500002X?httpAccept=text\/plain","content-type":"text\/plain","content-version":"vor","intended-application":"text-mining"}],"deposited":{"date-parts":[[2019,4,17]],"date-time":"2019-04-17T21:56:55Z","timestamp":1555538215000},"score":1,"resource":{"primary":{"URL":"https:\/\/linkinghub.elsevier.com\/retrieve\/pii\/000437029500002X"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1996,2]]},"references-count":69,"journal-issue":{"issue":"2","published-print":{"date-parts":[[1996,2]]}},"alternative-id":["000437029500002X"],"URL":"https:\/\/doi.org\/10.1016\/0004-3702(95)00002-x","relation":{},"ISSN":["0004-3702"],"issn-type":[{"value":"0004-3702","type":"print"}],"subject":[],"published":{"date-parts":[[1996,2]]}}}