{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,5]],"date-time":"2025-10-05T04:13:01Z","timestamp":1759637581708,"version":"3.37.3"},"reference-count":42,"publisher":"Springer Science and Business Media LLC","issue":"4","license":[{"start":{"date-parts":[[2018,6,18]],"date-time":"2018-06-18T00:00:00Z","timestamp":1529280000000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"funder":[{"DOI":"10.13039\/501100000781","name":"European Research Council","doi-asserted-by":"publisher","award":["ProofCert"],"award-info":[{"award-number":["ProofCert"]}],"id":[{"id":"10.13039\/501100000781","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["J Autom Reasoning"],"published-print":{"date-parts":[[2019,12]]},"DOI":"10.1007\/s10817-018-9475-3","type":"journal-article","created":{"date-parts":[[2018,6,17]],"date-time":"2018-06-17T23:45:56Z","timestamp":1529279156000},"page":"857-885","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":9,"title":["A Proof Theory for Model Checking"],"prefix":"10.1007","volume":"63","author":[{"given":"Quentin","family":"Heath","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-0274-4954","authenticated-orcid":false,"given":"Dale","family":"Miller","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2018,6,18]]},"reference":[{"issue":"3","key":"9475_CR1","doi-asserted-by":"publisher","first-page":"297","DOI":"10.1093\/logcom\/2.3.297","volume":"2","author":"J-M Andreoli","year":"1992","unstructured":"Andreoli, J.-M.: Logic programming with focusing proofs in linear logic. J. Logic Comput. 2(3), 297\u2013347 (1992)","journal-title":"J. Logic Comput."},{"key":"9475_CR2","unstructured":"Baelde, D.: A linear approach to the proof-theory of least and greatest fixed points. PhD thesis, Ecole Polytechnique, (2008)"},{"key":"9475_CR3","doi-asserted-by":"publisher","DOI":"10.1145\/2071368.2071370","author":"D Baelde","year":"2012","unstructured":"Baelde, D.: Least and greatest fixed points in linear logic. ACM Trans. Comput. Logic (2012). \n                    https:\/\/doi.org\/10.1145\/2071368.2071370","journal-title":"ACM Trans. Comput. Logic"},{"key":"9475_CR4","unstructured":"Baelde, D., Gacek, A., Miller, D., Nadathur, G., Tiu, A.: The Bedwyr system for model checking over syntactic expressions. In: Pfenning F. (ed.) 21th Conference on Automated Deduction (CADE), number 4603 in Lecture Notes in Artificial Intelligence, pp. 391\u2013397, New York, (2007). Springer"},{"key":"9475_CR5","unstructured":"Baelde, D., Miller, D.: Least and greatest fixed points in linear logic. In: Dershowitz N., Voronkov A. (eds.) International Conference on Logic for Programming and Automated Reasoning (LPAR), volume 4790 of Lecture Notes in Computer Science, pp. 92\u2013106, (2007)"},{"key":"9475_CR6","volume-title":"Principles of model checking","author":"C Baier","year":"2008","unstructured":"Baier, C., Katoen, J.-P.: Principles of model checking. MIT Press, Cambridge (2008)"},{"key":"9475_CR7","doi-asserted-by":"publisher","first-page":"287","DOI":"10.1007\/s10817-016-9380-6","volume":"59","author":"Z Chihani","year":"2017","unstructured":"Chihani, Z., Miller, D., Renaud, F.: A semantic framework for proof evidence. J. Autom. Reason. 59, 287\u2013330 (2017). \n                    https:\/\/doi.org\/10.1007\/s10817-016-9380-6","journal-title":"J. Autom. Reason."},{"key":"9475_CR8","doi-asserted-by":"publisher","first-page":"56","DOI":"10.2307\/2266170","volume":"5","author":"A Church","year":"1940","unstructured":"Church, A.: A formulation of the simple theory of types. J. Symb. Logic 5, 56\u201368 (1940)","journal-title":"J. Symb. Logic"},{"key":"9475_CR9","doi-asserted-by":"publisher","first-page":"293","DOI":"10.1007\/978-1-4684-3384-5_11","volume-title":"Logic and Data Bases","author":"KL Clark","year":"1978","unstructured":"Clark, K.L.: Negation as failure. In: Gallaire, J., Minker, J. (eds.) Logic and Data Bases, pp. 293\u2013322. Plenum Press, New York (1978)"},{"issue":"5","key":"9475_CR10","doi-asserted-by":"publisher","first-page":"654","DOI":"10.1016\/j.apal.2009.07.017","volume":"161","author":"O Delande","year":"2010","unstructured":"Delande, O., Miller, D., Saurin, A.: Proof and refutation in MALL as a game. Ann. Pure Appl. Logic 161(5), 654\u2013672 (2010)","journal-title":"Ann. Pure Appl. Logic"},{"key":"9475_CR11","unstructured":"Emerson, E.\u00a0A.: The beginning of model checking: A personal perspective. In: Grumberg O., Veith H. (eds.) 25 Years of Model Checking\u2013History, Achievements, Perspectives, volume 5000 of Lecture Notes in Computer Science, pp. 27\u201345. Springer, (2008)"},{"key":"9475_CR12","doi-asserted-by":"crossref","unstructured":"Gacek, A., Miller, D., Nadathur, G.: Combining generic judgments with recursive definitions. In Pfenning F. (ed.) 23th Symposium on Logic in Computer Science, pp. 33\u201344. IEEE Computer Society Press (2008)","DOI":"10.1109\/LICS.2008.33"},{"issue":"2","key":"9475_CR13","doi-asserted-by":"publisher","first-page":"241","DOI":"10.1007\/s10817-011-9218-1","volume":"49","author":"A Gacek","year":"2012","unstructured":"Gacek, A., Miller, D., Nadathur, G.: A two-level logic approach to reasoning about computations. J. Autom. Reason. 49(2), 241\u2013273 (2012)","journal-title":"J. Autom. Reason."},{"key":"9475_CR14","first-page":"68","volume-title":"The Collected Papers of Gerhard Gentzen","author":"G Gentzen","year":"1935","unstructured":"Gentzen, G.: Investigations into logical deduction. In: Szabo, M.E. (ed.) The Collected Papers of Gerhard Gentzen, pp. 68\u2013131. North-Holland, Amsterdam (1935)"},{"key":"9475_CR15","unstructured":"Gentzen, G.: New version of the consistency proof for elementary number theory. In Szabo M.\u00a0E. (ed.) Collected Papers of Gerhard Gentzen, pp. 252\u2013286. North-Holland, Amsterdam, 1938. Originally published (1938)"},{"key":"9475_CR16","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1016\/0304-3975(87)90045-4","volume":"50","author":"J-Y Girard","year":"1987","unstructured":"Girard, J.-Y.: Linear logic. Theoret. Comput. Sci. 50, 1\u2013102 (1987)","journal-title":"Theoret. Comput. Sci."},{"key":"9475_CR17","unstructured":"Girard, J.-Y.: Towards a geometry of interaction. In: Categories in Computer Science, volume\u00a092 of Contemporary Mathematics, pp. 69\u2013108. AMS, (1987)"},{"key":"9475_CR18","doi-asserted-by":"publisher","first-page":"255","DOI":"10.1017\/S0960129500001328","volume":"1","author":"J-Y Girard","year":"1991","unstructured":"Girard, J.-Y.: A new constructive logic: classical logic. Math. Struct. Comp. Sci. 1, 255\u2013296 (1991)","journal-title":"Math. Struct. Comp. Sci."},{"key":"9475_CR19","unstructured":"Girard, J.-Y.: A fixpoint theorem in linear logic. An email posting to the mailing list linear@cs.stanford.edu, (1992)"},{"key":"9475_CR20","unstructured":"Heath, Q., Miller, D.: A framework for proof certificates in finite state exploration. In: Kaliszyk C., Paskevich A. (eds.) Proceedings of the Fourth Workshop on Proof eXchange for Theorem Proving, number 186 in Electronic Proceedings in Theoretical Computer Science, pp. 11\u201326. Open Publishing Association, (2015)"},{"issue":"1\u20132","key":"9475_CR21","doi-asserted-by":"publisher","first-page":"107","DOI":"10.1016\/0168-0072(94)00060-G","volume":"75","author":"MI Kanovich","year":"1995","unstructured":"Kanovich, M.I.: Petri nets, Horn programs, Linear Logic and vector games. Ann. Pure Appl. Logic 75(1\u20132), 107\u2013135 (1995)","journal-title":"Ann. Pure Appl. Logic"},{"issue":"46","key":"9475_CR22","doi-asserted-by":"publisher","first-page":"4747","DOI":"10.1016\/j.tcs.2009.07.041","volume":"410","author":"C Liang","year":"2009","unstructured":"Liang, C., Miller, D.: Focusing and polarization in linear, intuitionistic, and classical logics. Theoret. Comput. Sci. 410(46), 4747\u20134768 (2009)","journal-title":"Theoret. Comput. Sci."},{"key":"9475_CR23","volume-title":"Temporal verification of reactive systems: safety","author":"Z Manna","year":"2012","unstructured":"Manna, Z., Pnueli, A.: Temporal verification of reactive systems: safety. Springer, Berlin (2012)"},{"key":"9475_CR24","doi-asserted-by":"publisher","first-page":"91","DOI":"10.1016\/S0304-3975(99)00171-1","volume":"232","author":"R McDowell","year":"2000","unstructured":"McDowell, R., Miller, D.: Cut-elimination for a logic with definitions and induction. Theoret. Comput. Sci. 232, 91\u2013119 (2000)","journal-title":"Theoret. Comput. Sci."},{"issue":"1","key":"9475_CR25","doi-asserted-by":"publisher","first-page":"80","DOI":"10.1145\/504077.504080","volume":"3","author":"R McDowell","year":"2002","unstructured":"McDowell, R., Miller, D.: Reasoning with higher-order abstract syntax in a logical framework. ACM Trans. Comput. Logic 3(1), 80\u2013136 (2002)","journal-title":"ACM Trans. Comput. Logic"},{"issue":"3","key":"9475_CR26","doi-asserted-by":"publisher","first-page":"411","DOI":"10.1016\/S0304-3975(01)00168-2","volume":"294","author":"R McDowell","year":"2003","unstructured":"McDowell, R., Miller, D., Palamidessi, C.: Encoding transition systems in sequent calculus. Theoret. Comput. Sci. 294(3), 411\u2013437 (2003)","journal-title":"Theoret. Comput. Sci."},{"key":"9475_CR27","unstructured":"Miller, D.: Foundational proof certificates. In: Delahaye D., Paleo B.\u00a0W. (eds.) All about Proofs, Proofs for All"},{"key":"9475_CR28","unstructured":"Miller, D., Nigam, V.: Incorporating tables into proofs. In: Duparc J., Henzinger T.\u00a0A. (eds.) CSL 2007: Computer Science Logic, volume 4646 of Lecture Notes in Computer Science, pp. 466\u2013480. Springer, (2007)"},{"key":"9475_CR29","doi-asserted-by":"publisher","first-page":"543","DOI":"10.1016\/j.entcs.2005.11.072","volume":"155","author":"Dale Miller","year":"2006","unstructured":"Miller, D., Saurin, A.: A game semantics for proof search: Preliminary results. In: Proceedings of the Mathematical Foundations of Programming Semantics (MFPS05), number 155 in Electronic Notes in Theoretical Computer Science, pp. 543\u2013563, (2006)","journal-title":"Electronic Notes in Theoretical Computer Science"},{"issue":"4","key":"9475_CR30","doi-asserted-by":"publisher","first-page":"749","DOI":"10.1145\/1094622.1094628","volume":"6","author":"D Miller","year":"2005","unstructured":"Miller, D., Tiu, A.: A proof theory for generic judgments. ACM Trans. Comput. Logic 6(4), 749\u2013783 (2005)","journal-title":"ACM Trans. Comput. Logic"},{"key":"9475_CR31","doi-asserted-by":"publisher","first-page":"194","DOI":"10.1007\/978-3-319-03545-1_13","volume-title":"Certified Programs and Proofs","author":"Dale Miller","year":"2013","unstructured":"Miller, D., Tiu, A.: Extracting proofs from tabled proof search. In: Gonthier G., Norrish M. (eds.) Third International Conference on Certified Programs and Proofs, number 8307 in Lecture Notes in Computer Science, pp. 194\u2013210, Melburne, Australia, (2013). Springer"},{"key":"9475_CR32","volume-title":"Communication and Concurrency","author":"R Milner","year":"1989","unstructured":"Milner, R.: Communication and Concurrency. Prentice-Hall International, Englewood Cliffs (1989)"},{"key":"9475_CR33","doi-asserted-by":"publisher","first-page":"143","DOI":"10.1007\/3-540-63166-6_16","volume-title":"Computer Aided Verification","author":"Y. S. Ramakrishna","year":"1997","unstructured":"Ramakrishna, Y. S., Ramakrishnan, C.\u00a0R., Ramakrishnan, I.\u00a0V., Smolka, S.\u00a0A., Swift, T., Warren, D.\u00a0S.: Efficient model checking using tabled resolution. In: Proceedings of the 9th International Conference on Computer Aided Verification (CAV97), number 1254 in Lecture Notes in Computer Science, pp. 143\u2013154, (1997)"},{"key":"9475_CR34","unstructured":"Ramakrishnan, C.: Model checking with tabled logic programming. ALP News Lett. (2002)"},{"key":"9475_CR35","unstructured":"Sangiorgi, D., Milner, R.: The problem of \u201cweak bisimulation up to\u201d. In: CONCUR, volume 630 of Lecture Notes in Computer Science, pp. 32\u201346. Springer, (1992)"},{"key":"9475_CR36","volume-title":"$$\\pi $$ \u03c0","author":"D Sangiorgi","year":"2001","unstructured":"Sangiorgi, D., Walker, D.: \n                    \n                      \n                    \n                    $$\\pi $$\n                    \n                      \n                        \u03c0\n                      \n                    \n                  -Calculus: A Theory of Mobile Processes. Cambridge University Press, Cambridge (2001)"},{"key":"9475_CR37","unstructured":"Schroeder-Heister, P.: Rules of definitional reflection. In: Vardi M. (ed.) 8th Symposium on Logic in Computer Science, pp. 222\u2013232. IEEE Computer Society Press, IEEE, (1993)"},{"key":"9475_CR38","unstructured":"Schwichtenberg, H.: Proof theory: Some applications ofcut-elimination. In: Barwise J. (ed.) Handbook ofMathematical Logic, volume\u00a090 of Studies in Logic and theFoundations of Mathematics, pp. 739\u2013782. North-Holland,Amsterdam, (1977)"},{"key":"9475_CR39","unstructured":"Tiu, A., Miller, D.: A proof search specification of the \n                    \n                      \n                    \n                    $$\\pi $$\n                    \n                      \n                        \u03c0\n                      \n                    \n                  -calculus. In: 3rd Workshop on the Foundations of Global Ubiquitous Computing, volume 138 of ENTCS, pp. 79\u2013101, (2005)"},{"key":"9475_CR40","doi-asserted-by":"publisher","DOI":"10.1145\/1656242.1656248","author":"A Tiu","year":"2010","unstructured":"Tiu, A., Miller, D.: Proof search specifications of bisimulation and modal logics for the \n                    \n                      \n                    \n                    $$\\pi $$\n                    \n                      \n                        \u03c0\n                      \n                    \n                  -calculus. ACM Trans. Comput. Logic (2010). \n                    https:\/\/doi.org\/10.1145\/1656242.1656248","journal-title":"ACM Trans. Comput. Logic"},{"issue":"4","key":"9475_CR41","doi-asserted-by":"publisher","first-page":"330","DOI":"10.1016\/j.jal.2012.07.007","volume":"10","author":"A Tiu","year":"2012","unstructured":"Tiu, A., Momigliano, A.: Cut elimination for a logic with induction and co-induction. J. Appl. Logic 10(4), 330\u2013367 (2012)","journal-title":"J. Appl. Logic"},{"key":"9475_CR42","unstructured":"Tiu, A., Nadathur, G., Miller, D.: Mixing finite success and finite failure in an automated prover. In: Empirically Successful Automated Reasoning in Higher-Order Logics (ESHOL\u201905), pp. 79\u201398, (2005)"}],"container-title":["Journal of Automated Reasoning"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10817-018-9475-3.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s10817-018-9475-3\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10817-018-9475-3.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,10,4]],"date-time":"2019-10-04T05:05:22Z","timestamp":1570165522000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s10817-018-9475-3"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2018,6,18]]},"references-count":42,"journal-issue":{"issue":"4","published-print":{"date-parts":[[2019,12]]}},"alternative-id":["9475"],"URL":"https:\/\/doi.org\/10.1007\/s10817-018-9475-3","relation":{},"ISSN":["0168-7433","1573-0670"],"issn-type":[{"type":"print","value":"0168-7433"},{"type":"electronic","value":"1573-0670"}],"subject":[],"published":{"date-parts":[[2018,6,18]]},"assertion":[{"value":"16 February 2017","order":1,"name":"received","label":"Received","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"12 June 2018","order":2,"name":"accepted","label":"Accepted","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"18 June 2018","order":3,"name":"first_online","label":"First Online","group":{"name":"ArticleHistory","label":"Article History"}}]}}