{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,12,13]],"date-time":"2025-12-13T23:00:58Z","timestamp":1765666858814},"publisher-location":"Berlin, Heidelberg","reference-count":16,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783642033582"},{"type":"electronic","value":"9783642033599"}],"license":[{"start":{"date-parts":[[2009,1,1]],"date-time":"2009-01-01T00:00:00Z","timestamp":1230768000000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2009]]},"DOI":"10.1007\/978-3-642-03359-9_12","type":"book-chapter","created":{"date-parts":[[2009,8,19]],"date-time":"2009-08-19T21:46:12Z","timestamp":1250718372000},"page":"147-163","source":"Crossref","is-referenced-by-count":16,"title":["Formalizing the Logic-Automaton Connection"],"prefix":"10.1007","author":[{"given":"Stefan","family":"Berghofer","sequence":"first","affiliation":[]},{"given":"Markus","family":"Reiter","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"12_CR1","unstructured":"Basin, D., Friedrich, S.: Combining WS1S and HOL. In: Gabbay, D., de Rijke, M. (eds.) Frontiers of Combining Systems 2. Studies in Logic and Computation, vol.\u00a07, pp. 39\u201356. Research Studies Press\/Wiley (2000)"},{"key":"12_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"24","DOI":"10.1007\/3-540-45842-5_2","volume-title":"Types for Proofs and Programs","author":"S. Berghofer","year":"2002","unstructured":"Berghofer, S., Nipkow, T.: Executing higher order logic. In: Callaghan, P., Luo, Z., McKinna, J., Pollack, R. (eds.) TYPES 2000. LNCS, vol.\u00a02277, p. 24. Springer, Heidelberg (2002)"},{"key":"12_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"30","DOI":"10.1007\/3-540-61064-2_27","volume-title":"Trees in Algebra and Programming - CAAP \u201996","author":"A. Boudet","year":"1996","unstructured":"Boudet, A., Comon, H.: Diophantine equations, Presburger arithmetic and finite automata. In: Kirchner, H. (ed.) CAAP 1996. LNCS, vol.\u00a01059, pp. 30\u201343. Springer, Heidelberg (1996)"},{"key":"12_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"515","DOI":"10.1007\/BFb0014565","volume-title":"Theoretical Aspects of Computer Software","author":"S. Boutin","year":"1997","unstructured":"Boutin, S.: Using reflection to build efficient and certified decision procedures. In: Ito, T., Abadi, M. (eds.) TACS 1997. LNCS, vol.\u00a01281, pp. 515\u2013529. Springer, Heidelberg (1997)"},{"key":"12_CR5","doi-asserted-by":"publisher","first-page":"33","DOI":"10.1007\/s10817-008-9101-x","volume":"41","author":"A. Chaieb","year":"2008","unstructured":"Chaieb, A., Nipkow, T.: Proof synthesis and reflection for linear arithmetic. Journal of Automated Reasoning\u00a041, 33\u201359 (2008)","journal-title":"Journal of Automated Reasoning"},{"key":"12_CR6","volume-title":"Proof, Language, and Interaction: Essays in Honor of Robin Milner","author":"R.L. Constable","year":"2000","unstructured":"Constable, R.L., Jackson, P.B., Naumov, P., Uribe, J.: Constructively formalizing automata theory. In: Plotkin, G., Stirling, C., Tofte, M. (eds.) Proof, Language, and Interaction: Essays in Honor of Robin Milner. MIT Press, Cambridge (2000)"},{"key":"12_CR7","unstructured":"Harrison, J.: Metatheory and reflection in theorem proving: A survey and critique. Technical Report CRC-053, SRI Cambridge (1995), \n                    \n                      http:\/\/www.cl.cam.ac.uk\/users\/jrh\/papers\/reflect.dvi.gz"},{"key":"12_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"311","DOI":"10.1007\/BFb0028022","volume-title":"Computer Science Logic","author":"N. Klarlund","year":"1998","unstructured":"Klarlund, N.: Mona & Fido: The logic-automaton connection in practice. In: Nielsen, M. (ed.) CSL 1997. LNCS, vol.\u00a01414, pp. 311\u2013326. Springer, Heidelberg (1998)"},{"key":"12_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"589","DOI":"10.1007\/11814771_48","volume-title":"Automated Reasoning","author":"A. Krauss","year":"2006","unstructured":"Krauss, A.: Partial recursive functions in higher-order logic. In: Furbach, U., Shankar, N. (eds.) IJCAR 2006. LNCS, vol.\u00a04130, pp. 589\u2013603. Springer, Heidelberg (2006)"},{"key":"12_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"173","DOI":"10.1007\/978-3-540-74591-4_14","volume-title":"Theorem Proving in Higher Order Logics","author":"Y. Minamide","year":"2007","unstructured":"Minamide, Y.: Verified decision procedures on context-free grammars. In: Schneider, K., Brandt, J. (eds.) TPHOLs 2007. LNCS, vol.\u00a04732, pp. 173\u2013188. Springer, Heidelberg (2007)"},{"key":"12_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/BFb0055126","volume-title":"Theorem Proving in Higher Order Logics","author":"T. Nipkow","year":"1998","unstructured":"Nipkow, T.: Verified lexical analysis. In: Grundy, J., Newey, M. (eds.) TPHOLs 1998. LNCS, vol.\u00a01479, pp. 1\u201315. Springer, Heidelberg (1998)"},{"key":"12_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"18","DOI":"10.1007\/978-3-540-71070-7_3","volume-title":"Automated Reasoning","author":"T. Nipkow","year":"2008","unstructured":"Nipkow, T.: Linear quantifier elimination. In: Armando, A., Baumgartner, P., Dowek, G. (eds.) IJCAR 2008. LNCS, vol.\u00a05195, pp. 18\u201333. Springer, Heidelberg (2008)"},{"key":"#cr-split#-12_CR13.1","unstructured":"Nishihara, T., Minamide, Y.: Depth first search. In: Klein, G., Nipkow, T., Paulson, L. (eds.) The Archive of Formal Proofs,                                           http:\/\/afp.sf.net\/entries\/Depth-First-Search.shtml                                                           (June 2004);"},{"key":"#cr-split#-12_CR13.2","unstructured":"Formal proof development"},{"key":"12_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"162","DOI":"10.1007\/3-540-44464-5_13","volume-title":"Advances in Computing Science - ASIAN 2000","author":"K.N. Verma","year":"2000","unstructured":"Verma, K.N., Goubault-Larrecq, J., Prasad, S., Arun-Kumar, S.: Reflecting BDDs in Coq. In: He, J., Sato, M. (eds.) ASIAN 2000. LNCS, vol.\u00a01961, pp. 162\u2013181. Springer, Heidelberg (2000)"},{"key":"12_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/3-540-46419-0_1","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"P. Wolper","year":"2000","unstructured":"Wolper, P., Boigelot, B.: On the construction of automata from linear arithmetic constraints. In: Schwartzbach, M.I., Graf, S. (eds.) TACAS 2000. LNCS, vol.\u00a01785, pp. 1\u201319. Springer, Heidelberg (2000)"}],"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\/978-3-642-03359-9_12","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,3,9]],"date-time":"2019-03-09T08:37:52Z","timestamp":1552120672000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-03359-9_12"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2009]]},"ISBN":["9783642033582","9783642033599"],"references-count":16,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-03359-9_12","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2009]]}}}