{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,3,19]],"date-time":"2025-03-19T16:11:15Z","timestamp":1742400675922},"publisher-location":"Berlin, Heidelberg","reference-count":27,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540649878"},{"type":"electronic","value":"9783540498018"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1998]]},"DOI":"10.1007\/bfb0055152","type":"book-chapter","created":{"date-parts":[[2006,7,27]],"date-time":"2006-07-27T09:09:13Z","timestamp":1153991353000},"page":"461-478","source":"Crossref","is-referenced-by-count":12,"title":["Case studies in meta-level theorem proving"],"prefix":"10.1007","author":[{"given":"Friedrich W.","family":"von Henke","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Stephan","family":"Pfab","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Holger","family":"Pfeifer","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Harald","family":"Rue\\","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2006,5,27]]},"reference":[{"key":"27_CR1","doi-asserted-by":"crossref","unstructured":"S. F. Allen, R. L. Constable, D. J. Howe, and W. E. Aitken. The Semantics of Reflected Proof. In Proc. 5th Annual IEEE Symposium on Logic in Computer Science, pages 95\u2013105. IEEE CS Press, 1990.","DOI":"10.1109\/LICS.1990.113737"},{"key":"27_CR2","unstructured":"H. R. Anderson. An Introduction to Binary Decision Diagrams. Available at: ftp.id.dtu.dk\/pub\/hra, September 1994."},{"key":"27_CR3","first-page":"18","volume-title":"KI-94 Workshops: Extended Abstracts. Gesellschaft f\u00fcr Informatik e.V","author":"D. A. Basin","year":"1994","unstructured":"D. A. Basin. Beyond Tactic Based Theorem Proving. In J. Kunze and H. Stoyan, editors, KI-94 Workshops: Extended Abstracts. Gesellschaft f\u00fcr Informatik e.V, 1994. 18. Deutsche Jahrestagung f\u00fcr K\u00fcnstliche Intelligenz, Saarbr\u00fccken."},{"key":"27_CR4","unstructured":"D. A. Basin and R. L. Constable. Metalogical Frameworks. Technical Report TR 91-1235, Department of Computer Science, Cornell University, September 1991."},{"key":"27_CR5","first-page":"203","volume-title":"An Inverse of the Evaluation Functional for Typed \u03bb-calculus","author":"U. Berger","year":"1991","unstructured":"U. Berger and H. Schwichtenberg. An Inverse of the Evaluation Functional for Typed \u03bb-calculus. In Proceedings, Sixth Annual IEEE Symposium on Logic in Computer Science, pages 203\u2013211, Amsterdam, The Netherlands, 15\u201318 July 1991. IEEE Computer Society Press."},{"key":"27_CR6","doi-asserted-by":"crossref","unstructured":"S. Boutin. Using Reflection to Build Efficient and Certified Decision Procedures. In M. Abadi and T. Ito, editors, Theoretical Aspects of Computer Software, volume 1281 of Lecture Notes in Computer Science. Springer-Verlag, 1997.","DOI":"10.1007\/BFb0014565"},{"key":"27_CR7","volume-title":"A Computational Logic","author":"R. S. Boyer","year":"1979","unstructured":"R. S. Boyer and J. S. Moore. A Computational Logic. Academic Press, New York, 1979."},{"key":"27_CR8","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, chapter 3. Academic Press, 1981."},{"issue":"3","key":"27_CR9","doi-asserted-by":"publisher","first-page":"293","DOI":"10.1145\/136035.136043","volume":"24","author":"R. E. Bryant","year":"1992","unstructured":"R. E. Bryant. Symbolic Boolean Manipulation with Ordered Binary Decision Diagrams. ACM Computing Surveys, 24(3):293\u2013318, September 1992.","journal-title":"ACM Computing Surveys"},{"key":"27_CR10","unstructured":"R. L. Constable, S. F. Allen, and H. M. Bromley et al. Implementing Mathematics with the Nuprl Proof Development System. Prentice-Hall, 1986."},{"key":"27_CR11","unstructured":"J. Crow, S. Owre, J. Rushby, N. Shankar, and M. Srivas. A Tutorial Introduction to PVS. Presented at WIFT '95: Workshop on Industrial-Strength Formal Specification Techniques, Boca Raton, Florida, April 1995."},{"key":"27_CR12","unstructured":"M. J. C. Gordon and T. F. Melham. Introduction to HOL: A Theorem Proving Environment for Higher-Order Logic. Cambridge University Press, 1993."},{"key":"27_CR13","volume-title":"volume 78 of Lecture Notes in Computer Science","author":"M. J. C. Gordon","year":"1979","unstructured":"M. J. C. Gordon, A. J. R. Milner, and C. P. Wadsworth. Edinburgh LCF: a Mechanized Logic of Computation, volume 78 of Lecture Notes in Computer Science. Springer-Verlag, Berlin, 1979."},{"key":"27_CR14","volume-title":"Technical Report CRC-053","author":"J. Harrison","year":"1995","unstructured":"J. Harrison. Metatheory and Reflection in Theorem Proving: A Survey and Critique. Technical Report CRC-053, SRI Cambridge, Millers Yard, Cambridge, UK, 1995."},{"key":"27_CR15","unstructured":"D. J. Howe. Automating Reasoning in an Implementation of Constructive Type Theory. PhD thesis, Cornell University, 1988. Available as technical report TR 88-925 from the Department of Computer Science, Cornell University."},{"key":"27_CR16","unstructured":"T. B. Knoblock and R. L. Constable. Formalized Metareasoning in Type Theory. In Proceedings of LICS, pages 237\u2013248. IEEE, 1986. Also available as technical report TR 86-742, Department of Computer Science, Cornell University."},{"key":"27_CR17","doi-asserted-by":"crossref","first-page":"97","DOI":"10.1002\/malq.19680140702","volume":"14","author":"G. Kreisel","year":"1968","unstructured":"G. Kreisel and A. L\u00e9vy. Reflection Principles and Their Use for Establishing the Complexity of Axiomatic Systems. Zeitschrift f\u00fcr math. Logik und Grundlagen der Mathematik, Bd. 14:97\u2013142, 1968.","journal-title":"Zeitschrift f\u00fcr math. Logik und Grundlagen der Mathematik"},{"issue":"2","key":"27_CR18","doi-asserted-by":"publisher","first-page":"245","DOI":"10.1145\/357073.357079","volume":"1","author":"G. Nelson","year":"1979","unstructured":"G. Nelson and D. C. Oppen. Simplification by Cooperating Decision Procedures. ACM Transactions on Programming Languages and Systems, 1(2):245\u2013257, October 1979.","journal-title":"ACM Transactions on Programming Languages and Systems"},{"issue":"2","key":"27_CR19","doi-asserted-by":"publisher","first-page":"107","DOI":"10.1109\/32.345827","volume":"21","author":"S. Owre","year":"1995","unstructured":"S. Owre, J. Rushby, N. Shankar, and F. von Henke. Formal Verification for Fault-Tolerant Architectures: Prolegomena to the Design of PVS. IEEE Transactions on Software Engineering, 21(2):107\u2013125, February 1995.","journal-title":"IEEE Transactions on Software Engineering"},{"key":"27_CR20","doi-asserted-by":"crossref","unstructured":"L. C. Paulson. Logic and Computation: Interactive Proof with Cambridge LCF. Number 2 in Cambride Tracts in Theoretical Computer Science. Cambridge University Press, 1987.","DOI":"10.1017\/CBO9780511526602"},{"key":"27_CR21","doi-asserted-by":"crossref","unstructured":"L. C. Paulson. Isabelle: A Generic Theorem Prover, volume 828 of Lecture Notes in Computer Science. Springer-Verlag, 1994.","DOI":"10.1007\/BFb0030541"},{"key":"27_CR22","unstructured":"S. Pfab. Efficient Symbolic Evaluation of Formal Specifications and Its Interrelationship with Theorem Proving. Master's thesis, Universit\u00c4t Ulm, Fakult\u00c4t f\u00fcr Mathematik, January 1998."},{"key":"27_CR23","doi-asserted-by":"crossref","unstructured":"H. Rue\\. Computational Reflection in the Calculus of Constructions and Its Application to Theorem Proving. In J. R. Hindley P. de Groote, editor, Proceedings of Typed Lambda Calculus and Applications (TLCA'97), volume 1210 of Lecture Notes in Computer Science, pages 319\u2013335. Springer-Verlag, April 1997.","DOI":"10.1007\/3-540-62688-3_44"},{"issue":"1","key":"27_CR24","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1145\/2422.322411","volume":"31","author":"R. E. Shostak","year":"1984","unstructured":"R. E. Shostak. Deciding Combinations of Theories. Journal of the ACM, 31(1):1\u201312, 1984.","journal-title":"Journal of the ACM"},{"key":"27_CR25","doi-asserted-by":"crossref","unstructured":"C. Smorynski. Self-Reference and Modal Logic. Springer-Verlag, 1985.","DOI":"10.1007\/978-1-4613-8601-8"},{"key":"27_CR26","doi-asserted-by":"crossref","unstructured":"C. Sprenger. A Verified Model Checker for the Modal \u039c-Calculus in Coq. In B. Steffen, editor, Tools and Algorithms for the Construction and Analysis of Systems, volume 1384 of Lecture Notes in Computer Science. Springer-Verlag, 1998.","DOI":"10.1007\/BFb0054171"},{"key":"27_CR27","doi-asserted-by":"crossref","unstructured":"F. von Henke. An Algebraic Approach to Data Types, Program Verification, and Program Synthesis. In Mathematical Foundations of Computer Science, Proceedings, volume 45 of Lecture Notes in Computer Science. Springer-Verlag, 1976.","DOI":"10.1007\/3-540-07854-1_195"}],"container-title":["Lecture Notes in Computer Science","Theorem Proving in Higher Order Logics"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/BFb0055152","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,4,20]],"date-time":"2019-04-20T08:33:58Z","timestamp":1555749238000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/BFb0055152"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1998]]},"ISBN":["9783540649878","9783540498018"],"references-count":27,"URL":"https:\/\/doi.org\/10.1007\/bfb0055152","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[1998]]}}}