{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,4]],"date-time":"2024-09-04T23:58:42Z","timestamp":1725494322057},"publisher-location":"Berlin, Heidelberg","reference-count":18,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540662228"},{"type":"electronic","value":"9783540486602"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1999]]},"DOI":"10.1007\/3-540-48660-7_23","type":"book-chapter","created":{"date-parts":[[2007,11,9]],"date-time":"2007-11-09T15:53:07Z","timestamp":1194623587000},"page":"267-281","source":"Crossref","is-referenced-by-count":6,"title":["On Explicit Reflection in Theorem Proving and Formal Verification"],"prefix":"10.1007","author":[{"given":"Sergei N.","family":"Artemov","sequence":"first","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2002,5,17]]},"reference":[{"key":"23_CR1","doi-asserted-by":"publisher","first-page":"95","DOI":"10.1109\/LICS.1990.113737","volume-title":"Proceedings of the Fifth Annual Symposium on Logic in Computer Science","author":"S. Allen","year":"1990","unstructured":"Allen, S., Constable R., Howe D., Aitken W.: The Semantics of Reflected Proofs. In: Proceedings of the Fifth Annual Symposium on Logic in Computer Science, Los Alamitos, CA, USA, IEEE Computer Society Press (1990) 95\u2013107."},{"key":"23_CR2","unstructured":"Artemov, S.: Extensions of Theories by the Reflection Principles and the Corresponding Modal Logics. Ph.D. Thesis (in Russian). Moscow (1979)"},{"key":"23_CR3","first-page":"14","volume":"702","author":"S. Artemov","year":"1993","unstructured":"Artemov, S., Strassen, T.: The Basic Logic of Proofs. In.: Lecture Notesi in Computer Science. Vol. 702. Springer-Verlag (1993) 14\u201328.","journal-title":"The Basic Logic of Proofs"},{"key":"23_CR4","doi-asserted-by":"publisher","first-page":"29","DOI":"10.1016\/0168-0072(94)90007-8","volume":"67","author":"A. S","year":"1994","unstructured":"Artemov, S.: Logic of Proofs. Annals of Pure and Applied Logic 67 (1994) 29\u201359","journal-title":"Annals of Pure and Applied Logic"},{"key":"23_CR5","unstructured":"Artemov, S.: Operational Modal Logic. Technical Report MSI 95-29, Cornell University (1995)"},{"key":"23_CR6","unstructured":"Artemov, S.: Explicit Provability: the Intended Semantics for Intuitionistic and Modal Logic. Technical Report CFIS 98-10, Cornell University (1998)"},{"key":"23_CR7","unstructured":"Boolos, G.: The Unprovability of Consistency: An Essay in Modal Logic. Cambridge University Press (1979)"},{"key":"23_CR8","doi-asserted-by":"publisher","first-page":"217","DOI":"10.1016\/0898-1221(79)90044-0","volume":"5","author":"D. M","year":"1979","unstructured":"Davis, M., Schwartz, J.: Metamathematical Extensibility for Theorem Verifiers and Proof Checkers. Computers and Mathematics with Applications 5 (1979) 217\u2013230","journal-title":"Computers and Mathematics with Applications"},{"key":"23_CR9","doi-asserted-by":"crossref","first-page":"35","DOI":"10.4064\/fm-49-1-35-92","volume":"49","author":"F. S","year":"1960","unstructured":"Feferman, S.: Arithmetization of Metamathematics in a General Setting. Fundamenta Mathematicae 49 (1960) 35\u201392","journal-title":"Fundamenta Mathematicae"},{"key":"23_CR10","doi-asserted-by":"publisher","first-page":"259","DOI":"10.2307\/2964649","volume":"27","author":"F. S","year":"1962","unstructured":"Feferman, S.: Transfinite Recursive Progressions of Axiomatic Theories. Journal of Symbolic Logic 27 (1962) 259\u2013316","journal-title":"Journal of Symbolic Logic"},{"key":"23_CR11","unstructured":"Harrison, J.: Metatheory and Reflection in Theorem Proving: A Survey and Critique. University of Cambridge (1995) \n                    http:\/\/www.dcs.glasgow.ac.uk\/~tfm\/hol-bib.html\\#H"},{"key":"23_CR12","first-page":"237","volume-title":"Proceedings of the First Annual Symposium on Logic in Computer Science","author":"T Knoblock","year":"1986","unstructured":"Knoblock, T., Constable, R.: Formalized Metareasoning in Type Theory. In: Proceedings of the First Annual Symposium on Logic in Computer Science. Cambridge, MA, USA, IEEE Computer Society Press (1986) 237\u2013248"},{"key":"23_CR13","doi-asserted-by":"publisher","first-page":"97","DOI":"10.1002\/malq.19680140702","volume":"14","author":"K. G","year":"1968","unstructured":"Kreisel, G., Levy, A.: Reflection Principles and Their Use for Establishing the Complexity of Axiomatic Systems. Zeitschrift f\u00fcr Mathematische Logik und Grundlagen der Mathematik 14 (1968) 97\u2013142","journal-title":"Zeitschrift f\u00fcr Mathematische Logik und Grundlagen der Mathematik"},{"key":"23_CR14","series-title":"Lect Notes Comput Sci","first-page":"140","volume-title":"On Extensibility of Proof Checkers","author":"P. R","year":"1995","unstructured":"Pollack, R.: On Extensibility of Proof Checkers. Lecture Notes in Computer Science, Vol. 996.,Springer-Verlag, Berlin Heidelberg New York (1995) 140\u2013161"},{"key":"23_CR15","doi-asserted-by":"crossref","unstructured":"Smorynski, C.: The Incompleteness Theorems. In: Barwise, J (ed.): Handbook of Mathematical Logic, Vol. 4. North-Holland, Amsterdam (1977) 821\u2013865","DOI":"10.1016\/S0049-237X(08)71123-6"},{"key":"23_CR16","doi-asserted-by":"crossref","DOI":"10.1007\/978-1-4613-8601-8","volume-title":"Self-Reference and Modal Logic","author":"C. Smorynski","year":"1985","unstructured":"C. Smorynski, C.: Self-Reference and Modal Logic. Springer-Verlag, Berlin (1985)"},{"key":"23_CR17","unstructured":"A.S. Troelstra, A.S., van Dalen, D.: Constructivism in Mathematics. An Introduction, Vol. 1, Amsterdam; North Holland (1988)"},{"key":"23_CR18","doi-asserted-by":"publisher","first-page":"161","DOI":"10.1112\/plms\/s2-45.1.161","volume":"45","author":"T. A","year":"1939","unstructured":"Turing, A.: Systems of Logics Based on Ordinals. Proceedings of the London Mathematical Society, Ser. 2, Vol. 45(1939) 161\u2013228","journal-title":"Proceedings of the London Mathematical Society"}],"container-title":["Lecture Notes in Computer Science","Automated Deduction \u2014 CADE-16"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-48660-7_23","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,2,25]],"date-time":"2019-02-25T03:37:12Z","timestamp":1551065832000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-48660-7_23"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1999]]},"ISBN":["9783540662228","9783540486602"],"references-count":18,"URL":"https:\/\/doi.org\/10.1007\/3-540-48660-7_23","relation":{},"ISSN":["0302-9743"],"issn-type":[{"type":"print","value":"0302-9743"}],"subject":[],"published":{"date-parts":[[1999]]}}}