{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,8,31]],"date-time":"2025-08-31T10:36:07Z","timestamp":1756636567869,"version":"3.37.3"},"reference-count":51,"publisher":"Springer Science and Business Media LLC","issue":"1","license":[{"start":{"date-parts":[[2016,10,18]],"date-time":"2016-10-18T00:00:00Z","timestamp":1476748800000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["J Autom Reasoning"],"published-print":{"date-parts":[[2017,1]]},"DOI":"10.1007\/s10817-016-9391-3","type":"journal-article","created":{"date-parts":[[2016,10,18]],"date-time":"2016-10-18T16:12:07Z","timestamp":1476807127000},"page":"149-179","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":25,"title":["Soundness and Completeness Proofs by Coinductive Methods"],"prefix":"10.1007","volume":"58","author":[{"given":"Jasmin Christian","family":"Blanchette","sequence":"first","affiliation":[]},{"given":"Andrei","family":"Popescu","sequence":"additional","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0001-7982-2768","authenticated-orcid":false,"given":"Dmitriy","family":"Traytel","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2016,10,18]]},"reference":[{"key":"9391_CR1","volume-title":"A Course in Mathematical Logic","author":"JL Bell","year":"1977","unstructured":"Bell, J.L., Machover, M.: A Course in Mathematical Logic. North-Holland, Amsterdam (1977)"},{"key":"9391_CR2","unstructured":"Berghofer, S.: First-order logic according to fitting. In: Klein, G., Nipkow, T., Paulson, L. (eds.) Archive of Formal Proofs. http:\/\/www.isa-afp.org\/entries\/FOL-Fitting.shtml (2007)"},{"key":"9391_CR3","doi-asserted-by":"crossref","unstructured":"Bertot, Y.: Filters on coinductive streams, an application to Eratosthenes\u2019 sieve. In: Urzyczyn, P. (ed.) TLCA 2005, LNCS, vol. 3461, pp. 102\u2013115. Springer (2005)","DOI":"10.1007\/11417170_9"},{"key":"9391_CR4","doi-asserted-by":"crossref","unstructured":"Blanchette, J.C., B\u00f6hme, S., Popescu, A., Smallbone, N.: Encoding monomorphic and polymorphic types. In: Piterman, N., Smolka, S. (eds.) TACAS 2013, LNCS, vol. 7795, pp. 493\u2013507. Springer (2013)","DOI":"10.1007\/978-3-642-36742-7_34"},{"key":"9391_CR5","doi-asserted-by":"crossref","unstructured":"Blanchette, J.C., Fleury, M., Weidenbach, C.: A verified SAT solver framework with learn, forget, restart, and incrementality. In: Olivetti, N., Tiwari, A. (eds.) IJCAR 2016, LNCS, vol. 9706. Springer (2016)","DOI":"10.1007\/978-3-319-40229-1_4"},{"key":"9391_CR6","doi-asserted-by":"crossref","unstructured":"Blanchette, J.C., H\u00f6lzl, J., Lochbihler, A., Panny, L., Popescu, A., Traytel, D.: Truly modular (co)datatypes for Isabelle\/HOL. In: Klein, G., Gamboa, R. (eds.) ITP 2014, LNCS, vol. 8558, pp. 93\u2013110. Springer (2014)","DOI":"10.1007\/978-3-319-08970-6_7"},{"key":"9391_CR7","doi-asserted-by":"crossref","unstructured":"Blanchette, J.C., Popescu, A.: Mechanizing the metatheory of Sledgehammer. In: Fontaine, P., Ringeissen, C., Schmidt, R.A. (eds.) FroCoS\u00a02013, LNCS, vol. 8152, pp. 245\u2013260. Springer (2013)","DOI":"10.1007\/978-3-642-40885-4_17"},{"key":"9391_CR8","unstructured":"Blanchette, J.C., Popescu, A., Traytel, D.: Abstract completeness. In: Klein, G., Nipkow, T., Paulson, L. (eds.) Archive of Formal Proofs. http:\/\/www.isa-afp.org\/entries\/Abstract_Completeness.shtml (2014)"},{"key":"9391_CR9","doi-asserted-by":"crossref","unstructured":"Blanchette, J.C., Popescu, A., Traytel, D.: Unified classical logic completeness\u2014a coinductive pearl. In: Demri, S., Kapur, D., Weidenbach, C. (eds.) IJCAR 2014, LNCS, vol. 8562, pp. 46\u201360. Springer (2014)","DOI":"10.1007\/978-3-319-08587-6_4"},{"key":"9391_CR10","unstructured":"Blanchette, J.C., Popescu, A., Traytel, D.: Formal development associated with this paper. http:\/\/people.inf.ethz.ch\/trayteld\/compl-journal-devel.tgz (2015)"},{"key":"9391_CR11","doi-asserted-by":"crossref","unstructured":"Blanchette, J.C., Popescu, A., Traytel, D.: Foundational extensible corecursion: a proof assistant perspective. In: Fisher, K., Reppy, J.H. (eds.) ICFP 2015, pp. 192\u2013204. ACM (2015)","DOI":"10.1145\/2784731.2784732"},{"key":"9391_CR12","doi-asserted-by":"crossref","unstructured":"Brotherston, J.: Cyclic proofs for first-order logic with inductive definitions. In: Beckert, B. (ed.) TABLEAUX 2005, LNCS, vol. 3702, pp. 78\u201392. Springer (2005)","DOI":"10.1007\/11554554_8"},{"key":"9391_CR13","unstructured":"Brotherston, J.: Sequent calculus proof systems for inductive definitions. Ph.D. thesis, University of Edinburgh (2006)"},{"key":"9391_CR14","doi-asserted-by":"crossref","unstructured":"Brotherston, J., Bornat, R., Calcagno, C.: Cyclic proofs of program termination in separation logic. In: Necula, G.C., Wadler, P. (eds.) POPL 2008, pp. 101\u2013112. ACM (2008)","DOI":"10.1145\/1328438.1328453"},{"key":"9391_CR15","doi-asserted-by":"crossref","unstructured":"Brotherston, J., Distefano, D., Petersen, R.L.: Automated cyclic entailment proofs in separation logic. In: Bj\u00f8rner, N., Sofronie-Stokkermans, V. (eds.) CADE-23, LNCS, vol. 6803, pp. 131\u2013146. Springer (2011)","DOI":"10.1007\/978-3-642-22438-6_12"},{"key":"9391_CR16","doi-asserted-by":"crossref","unstructured":"Brotherston, J., Gorogiannis, N., Petersen, R.L.: A generic cyclic theorem prover. In: Jhala, R., Igarashi, A. (eds.) APLAS 2012, LNCS, vol. 7705, pp. 350\u2013367. Springer (2012)","DOI":"10.1007\/978-3-642-35182-2_25"},{"key":"9391_CR17","doi-asserted-by":"crossref","unstructured":"Brotherston, J., Simpson, A.: Complete sequent calculi for induction and infinite descent. In: LICS 2007, pp. 51\u201362. IEEE Computer Society (2007)","DOI":"10.1109\/LICS.2007.16"},{"issue":"1","key":"9391_CR18","doi-asserted-by":"crossref","first-page":"39","DOI":"10.1016\/j.tcs.2005.09.061","volume":"351","author":"A Ciaffaglione","year":"2006","unstructured":"Ciaffaglione, A., Gianantonio, P.D.: A certified, corecursive implementation of exact real numbers. Theor. Comput. Sci. 351(1), 39\u201351 (2006)","journal-title":"Theor. Comput. Sci."},{"key":"9391_CR19","volume-title":"Institution-Independent Model Theory. Studies in Universal Logic","author":"R Diaconescu","year":"2008","unstructured":"Diaconescu, R.: Institution-Independent Model Theory. Studies in Universal Logic. Birkh\u00e4user, Basel (2008)"},{"key":"9391_CR20","doi-asserted-by":"crossref","DOI":"10.1007\/978-1-4612-2360-3","volume-title":"First-Order Logic and Automated Theorem Proving. Graduate Texts in Computer Science","author":"M Fitting","year":"1996","unstructured":"Fitting, M.: First-Order Logic and Automated Theorem Proving. Graduate Texts in Computer Science, 2nd edn. Springer, Berlin (1996)","edition":"2"},{"key":"9391_CR21","volume-title":"Fairness. Texts and Monographs in Computer Science","author":"N Francez","year":"1986","unstructured":"Francez, N.: Fairness. Texts and Monographs in Computer Science. Springer, Berlin (1986)"},{"key":"9391_CR22","volume-title":"Logic for Computer Science: Foundations of Automatic Theorem Proving. Computer Science and Technology","author":"JH Gallier","year":"1986","unstructured":"Gallier, J.H.: Logic for Computer Science: Foundations of Automatic Theorem Proving. Computer Science and Technology. Harper & Row, New York (1986)"},{"key":"9391_CR23","unstructured":"G\u00f6del, K.: \u00dcber die Vollst\u00e4ndigkeit des Logikkalk\u00fcls. Ph.D. thesis, Universit\u00e4t Wien (1929)"},{"volume-title":"Introduction to HOL: A Theorem Proving Environment for Higher Order Logic","year":"1993","key":"9391_CR24","unstructured":"Gordon, M.J.C., Melham, T.F. (eds.): Introduction to HOL: A Theorem Proving Environment for Higher Order Logic. Cambridge University Press, Cambridge (1993)"},{"key":"9391_CR25","doi-asserted-by":"crossref","unstructured":"Haftmann, F., Nipkow, T.: Code generation via higher-order rewrite systems. In: Blume, M., Kobayashi, N., Vidal, G. (eds.) FLOPS 2010, LNCS, vol. 6009, pp. 103\u2013117. Springer (2010)","DOI":"10.1007\/978-3-642-12251-4_9"},{"key":"9391_CR26","first-page":"100","volume-title":"Handbook of Automated Reasoning","author":"R H\u00e4hnle","year":"2001","unstructured":"H\u00e4hnle, R.: Tableaux and related methods. In: Robinson, A., Voronkov, A. (eds.) Handbook of Automated Reasoning, vol. I, pp. 100\u2013178. Elsevier, Amsterdam (2001)"},{"key":"9391_CR27","doi-asserted-by":"crossref","unstructured":"Harrison, J.: Formalizing basic first order model theory. In: Grundy, J., Newey, M.C. (eds.) TPHOLs \u201998, LNCS, vol. 1479, pp. 153\u2013170. Springer (1998)","DOI":"10.1007\/BFb0055135"},{"key":"9391_CR28","unstructured":"Ilik, D.: Constructive completeness proofs and delimited control. Ph.D. thesis, \u00c9cole polytechnique (2010)"},{"key":"9391_CR29","first-page":"222","volume":"62","author":"B Jacobs","year":"1997","unstructured":"Jacobs, B., Rutten, J.: A tutorial on (co)algebras and (co)induction. Bull. Eur. Assoc. Theor. Comput. Sci. 62, 222\u2013259 (1997)","journal-title":"Bull. Eur. Assoc. Theor. Comput. Sci."},{"key":"9391_CR30","doi-asserted-by":"crossref","unstructured":"Kaplan, D.: Review of Kripke (1959) [32]. J. Symb. Log. 31, 120\u2013122 (1966)","DOI":"10.2307\/2270649"},{"key":"9391_CR31","volume-title":"Mathematical Logic","author":"SC Kleene","year":"1967","unstructured":"Kleene, S.C.: Mathematical Logic. Wiley, London (1967)"},{"issue":"1","key":"9391_CR32","doi-asserted-by":"crossref","first-page":"1","DOI":"10.2307\/2964568","volume":"24","author":"S Kripke","year":"1959","unstructured":"Kripke, S.: A completeness theorem in modal logic. J. Symb. Log. 24(1), 1\u201314 (1959)","journal-title":"J. Symb. Log."},{"issue":"4","key":"9391_CR33","doi-asserted-by":"crossref","first-page":"405","DOI":"10.2307\/421172","volume":"2","author":"JL Krivine","year":"1996","unstructured":"Krivine, J.L.: Une preuve formelle et intuitionniste du th\u00e9or\u00e8me de compl\u00e9tude de la logique classique. Bull. Symb. Log. 2(4), 405\u2013421 (1996)","journal-title":"Bull. Symb. Log."},{"key":"9391_CR34","unstructured":"Margetson, J., Ridge, T.: Completeness theorem. In: Klein, G., Nipkow, T., Paulson, L. (eds.) Archive of Formal Proofs. http:\/\/www.isa-afp.org\/entries\/Completeness.shtml (2004)"},{"issue":"1","key":"9391_CR35","doi-asserted-by":"crossref","first-page":"3","DOI":"10.1016\/S0304-3975(97)00143-6","volume":"192","author":"R Mayr","year":"1998","unstructured":"Mayr, R., Nipkow, T.: Higher-order rewrite systems and their confluence. Theor. Comput. Sci. 192(1), 3\u201329 (1998)","journal-title":"Theor. Comput. Sci."},{"key":"9391_CR36","doi-asserted-by":"crossref","unstructured":"Nakata, K., Uustalu, T., Bezem, M.: A proof pearl with the fan theorem and bar induction: walking through infinite trees with mixed induction and coinduction. In: Yang, H. (ed.) APLAS 2011, LNCS, vol. 7078, pp. 353\u2013368. Springer (2011)","DOI":"10.1007\/978-3-642-25318-8_26"},{"key":"9391_CR37","first-page":"247","volume-title":"Acts of Knowledge: History, Philosophy and Logic: Essays Dedicated to G\u00f6ran Sundholm","author":"S Negri","year":"2009","unstructured":"Negri, S.: Kripke completeness revisited. In: Primiero, G., Rahman, S. (eds.) Acts of Knowledge: History, Philosophy and Logic: Essays Dedicated to G\u00f6ran Sundholm, pp. 247\u2013282. College Publications, London (2009)"},{"key":"9391_CR38","doi-asserted-by":"crossref","DOI":"10.1007\/978-3-319-10542-0","volume-title":"Concrete Semantics: With Isabelle\/HOL","author":"T Nipkow","year":"2014","unstructured":"Nipkow, T., Klein, G.: Concrete Semantics: With Isabelle\/HOL. Springer, Berlin (2014)"},{"key":"9391_CR39","doi-asserted-by":"crossref","unstructured":"Nipkow, T., Paulson, L.C., Wenzel, M.: Isabelle\/HOL: A\u00a0Proof Assistant for Higher-Order Logic, LNCS, vol. 2283. Springer (2002)","DOI":"10.1007\/3-540-45949-9"},{"key":"9391_CR40","doi-asserted-by":"crossref","unstructured":"Petria, M.: An institutional version of G\u00f6del\u2019s completeness theorem. In: CALCO 2007, pp. 409\u2013424 (2007)","DOI":"10.1007\/978-3-540-73859-6_28"},{"key":"9391_CR41","doi-asserted-by":"crossref","unstructured":"Pfenning, F.: Review of \u201cJean H. Gallier: Logic for Computer Science, Harper & Row, New York 1986\u201d [22]. J. Symb. Log. 54(1), 288\u2013289 (1989)","DOI":"10.2307\/2275035"},{"key":"9391_CR42","doi-asserted-by":"crossref","unstructured":"Ridge, T., Margetson, J.: A mechanically verified, sound and complete theorem prover for first order logic. In: Hurd, J., Melham, T.F. (eds.) TPHOLs 2005, LNCS, vol. 3603, pp. 294\u2013309. Springer (2005)","DOI":"10.1007\/11541868_19"},{"key":"9391_CR43","doi-asserted-by":"crossref","unstructured":"Ro\u015fu, G.: Equality of streams is a $$\\Pi _2^0$$ \u03a0 2 0 -complete problem. In: Reppy, J.H., Lawall, J.L. (eds.) ICFP \u201906. ACM (2006)","DOI":"10.1145\/1159803.1159827"},{"key":"9391_CR44","doi-asserted-by":"crossref","unstructured":"Ro\u015fu, G.: An effective algorithm for the membership problem for extended regular expressions. In: Seidl, H. (ed.) FoSSaCS 2007, LNCS, vol. 4423, pp. 332\u2013345. Springer (2007)","DOI":"10.1007\/978-3-540-71389-0_24"},{"key":"9391_CR45","doi-asserted-by":"crossref","unstructured":"Rutten, J.J.M.M.: Automata and coinduction (an exercise in coalgebra). In: Sangiorgi, D., de\u00a0Simone, R. (eds.) CONCUR \u201998, LNCS, vol. 1466, pp. 194\u2013218. Springer (1998)","DOI":"10.1007\/BFb0055624"},{"key":"9391_CR46","doi-asserted-by":"crossref","unstructured":"Rutten, J.J.M.M.: Regular expressions revisited: a coinductive approach to streams, automata, and power series. In: Backhouse, R.C., Oliveira, J.N. (eds.) MPC 2000, LNCS, vol. 1837, pp. 100\u2013101. Springer (2000)","DOI":"10.1007\/10722010_7"},{"key":"9391_CR47","doi-asserted-by":"crossref","first-page":"358","DOI":"10.1016\/S1571-0661(04)80972-1","volume":"45","author":"JJMM Rutten","year":"2001","unstructured":"Rutten, J.J.M.M.: Elements of stream calculus (an extensive exercise in coinduction). Electron. Notes Theor. Comput. Sci. 45, 358\u2013423 (2001)","journal-title":"Electron. Notes Theor. Comput. Sci."},{"key":"9391_CR48","doi-asserted-by":"crossref","unstructured":"Schlichtkrull, A.: Formalization of the resolution calculus for first-order logic. In: Blanchette, J.C., Merz, S. (eds.) ITP 2016, LNCS, vol. 9807. Springer (2016)","DOI":"10.1007\/978-3-319-43144-4_21"},{"issue":"3","key":"9391_CR49","doi-asserted-by":"crossref","first-page":"199","DOI":"10.2478\/v10037-012-0023-z","volume":"20","author":"JJ Schl\u00f6der","year":"2012","unstructured":"Schl\u00f6der, J.J., Koepke, P.: The G\u00f6del completeness theorem for uncountable languages. Formaliz. Math. 20(3), 199\u2013203 (2012)","journal-title":"Formaliz. Math."},{"key":"9391_CR50","doi-asserted-by":"crossref","unstructured":"Traytel, D., Popescu, A., Blanchette, J.C.: Foundational, compositional (co)datatypes for higher-order logic: category theory applied to theorem proving. In: LICS 2012, pp. 596\u2013605. IEEE Computer Society (2012)","DOI":"10.1109\/LICS.2012.75"},{"key":"9391_CR51","doi-asserted-by":"crossref","DOI":"10.1017\/CBO9781139168717","volume-title":"Basic Proof Theory","author":"AS Troelstra","year":"2000","unstructured":"Troelstra, A.S., Schwichtenberg, H.: Basic Proof Theory, 2nd edn. Cambridge University Press, Cambridge (2000)","edition":"2"}],"container-title":["Journal of Automated Reasoning"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10817-016-9391-3.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s10817-016-9391-3\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10817-016-9391-3.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,9,14]],"date-time":"2019-09-14T15:07:03Z","timestamp":1568473623000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s10817-016-9391-3"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2016,10,18]]},"references-count":51,"journal-issue":{"issue":"1","published-print":{"date-parts":[[2017,1]]}},"alternative-id":["9391"],"URL":"https:\/\/doi.org\/10.1007\/s10817-016-9391-3","relation":{},"ISSN":["0168-7433","1573-0670"],"issn-type":[{"type":"print","value":"0168-7433"},{"type":"electronic","value":"1573-0670"}],"subject":[],"published":{"date-parts":[[2016,10,18]]}}}