{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,7,4]],"date-time":"2025-07-04T20:21:53Z","timestamp":1751660513157,"version":"3.41.0"},"publisher-location":"Cham","reference-count":20,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783319669014"},{"type":"electronic","value":"9783319669021"}],"license":[{"start":{"date-parts":[[2017,1,1]],"date-time":"2017-01-01T00:00:00Z","timestamp":1483228800000},"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":[[2017]]},"DOI":"10.1007\/978-3-319-66902-1_19","type":"book-chapter","created":{"date-parts":[[2017,8,29]],"date-time":"2017-08-29T11:34:20Z","timestamp":1504006460000},"page":"311-327","source":"Crossref","is-referenced-by-count":3,"title":["Cyclic Proofs with Ordering Constraints"],"prefix":"10.1007","author":[{"given":"Sorin","family":"Stratulat","sequence":"first","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2017,8,30]]},"reference":[{"key":"19_CR1","doi-asserted-by":"crossref","first-page":"739","DOI":"10.1016\/S0049-237X(08)71120-0","volume-title":"Handbook of Mathematical Logic","author":"P Aczel","year":"1977","unstructured":"Aczel, P.: An introduction to inductive definitions. In: Barwise, J. (ed.) Handbook of Mathematical Logic, pp. 739\u2013782. North Holland, Amsterdam (1977)"},{"key":"19_CR2","doi-asserted-by":"crossref","DOI":"10.1017\/CBO9781139172752","volume-title":"Term Rewriting and All That","author":"F Baader","year":"1998","unstructured":"Baader, F., Nipkow, T.: Term Rewriting and All That. Cambridge University Press, Cambridge (1998)"},{"key":"19_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"337","DOI":"10.1007\/3-540-44881-0_24","volume-title":"Rewriting Techniques and Applications","author":"G Barthe","year":"2003","unstructured":"Barthe, G., Stratulat, S.: Validation of the JavaCard platform with implicit induction techniques. In: Nieuwenhuis, R. (ed.) RTA 2003. LNCS, vol. 2706, pp. 337\u2013351. Springer, Heidelberg (2003). doi: 10.1007\/3-540-44881-0_24"},{"issue":"2","key":"19_CR4","doi-asserted-by":"crossref","first-page":"189","DOI":"10.1007\/BF00881856","volume":"14","author":"A Bouhoula","year":"1995","unstructured":"Bouhoula, A., Rusinowitch, M.: Implicit induction in conditional theories. J. Autom. Reason. 14(2), 189\u2013235 (1995)","journal-title":"J. Autom. Reason."},{"key":"19_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"102","DOI":"10.1007\/3-540-58156-1_8","volume-title":"Automated Deduction \u2014 CADE-12","author":"F Bronsard","year":"1994","unstructured":"Bronsard, F., Reddy, U.S., Hasker, R.W.: Induction using term orderings. In: Bundy, A. (ed.) CADE 1994. LNCS, vol. 814, pp. 102\u2013117. Springer, Heidelberg (1994). doi: 10.1007\/3-540-58156-1_8"},{"key":"19_CR6","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"78","DOI":"10.1007\/11554554_8","volume-title":"Automated Reasoning with Analytic Tableaux and Related Methods","author":"J Brotherston","year":"2005","unstructured":"Brotherston, J.: Cyclic proofs for first-order logic with inductive definitions. In: Beckert, B. (ed.) TABLEAUX 2005. LNCS (LNAI), vol. 3702, pp. 78\u201392. Springer, Heidelberg (2005). doi: 10.1007\/11554554_8"},{"key":"19_CR7","unstructured":"Brotherston, J.: Sequent calculus proof systems for inductive definitions. Ph.D. thesis, University of Edinburgh, November 2006"},{"key":"19_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"350","DOI":"10.1007\/978-3-642-35182-2_25","volume-title":"Programming Languages and Systems","author":"J Brotherston","year":"2012","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, Heidelberg (2012). doi: 10.1007\/978-3-642-35182-2_25"},{"issue":"6","key":"19_CR9","doi-asserted-by":"crossref","first-page":"1177","DOI":"10.1093\/logcom\/exq052","volume":"21","author":"J Brotherston","year":"2011","unstructured":"Brotherston, J., Simpson, A.: Sequent calculi for induction and infinite descent. J. Logic Comput. 21(6), 1177\u20131216 (2011)","journal-title":"J. Logic Comput."},{"key":"19_CR10","doi-asserted-by":"crossref","first-page":"176","DOI":"10.1007\/BF01201353","volume":"39","author":"G Gentzen","year":"1935","unstructured":"Gentzen, G.: Untersuchungen \u00fcber das logische Schlie\u00dfen. I. Mathematische Zeitschrift 39, 176\u2013210 (1935)","journal-title":"I. Mathematische Zeitschrift"},{"issue":"3","key":"19_CR11","doi-asserted-by":"crossref","first-page":"408","DOI":"10.1145\/377978.377993","volume":"2","author":"O Kupferman","year":"2001","unstructured":"Kupferman, O., Vardi, M.: Weak alternating automata are not that weak. ACM Trans. Comput. Logic (TOCL) 2(3), 408\u2013429 (2001)","journal-title":"ACM Trans. Comput. Logic (TOCL)"},{"key":"19_CR12","unstructured":"Michel, M.: Complementation is more difficult with automata on infinite words. Technical report, CNET (1988)"},{"key":"19_CR13","doi-asserted-by":"crossref","DOI":"10.1017\/CBO9780511527340","volume-title":"Structural Proof Theory","author":"S Negri","year":"2001","unstructured":"Negri, S., von Plato, J.: Structural Proof Theory. Cambridge University Press, Cambridge (2001)"},{"issue":"2","key":"19_CR14","doi-asserted-by":"crossref","first-page":"53","DOI":"10.1023\/A:1023251327012","volume":"30","author":"M Rusinowitch","year":"2003","unstructured":"Rusinowitch, M., Stratulat, S., Klay, F.: Mechanical verification of an ideal incremental ABR conformance algorithm. J. Autom. Reason. 30(2), 53\u2013177 (2003)","journal-title":"J. Autom. Reason."},{"key":"19_CR15","doi-asserted-by":"crossref","unstructured":"Stratulat, S.: A unified view of induction reasoning for first-order logic. In: Voronkov, A. (ed.) Turing-100 (The Alan Turing Centenary Conference). EPiC Series, vol. 10, pp. 326\u2013352. EasyChair (2012)","DOI":"10.29007\/nsx4"},{"key":"19_CR16","doi-asserted-by":"crossref","unstructured":"Stratulat, S.: Structural vs. cyclic induction: a report on some experiments with Coq. In: SYNASC International Symposium on Symbolic and Numeric Algorithms for Scientific Computing, pp. 27\u201334. IEEE Computer Society (2016)","DOI":"10.1109\/SYNASC.2016.018"},{"issue":"Part 1","key":"19_CR17","doi-asserted-by":"crossref","first-page":"209","DOI":"10.1016\/j.jsc.2016.07.014","volume":"80","author":"S Stratulat","year":"2017","unstructured":"Stratulat, S.: Mechanically certifying formula-based Noetherian induction reasoning. J. Symb. Comput. 80(Part 1), 209\u2013249 (2017)","journal-title":"J. Symb. Comput."},{"issue":"2","key":"19_CR18","doi-asserted-by":"crossref","first-page":"146","DOI":"10.1137\/0201010","volume":"1","author":"R Tarjan","year":"1972","unstructured":"Tarjan, R.: Depth-first search and linear graph algorithms. SIAM J. Comput. 1(2), 146\u2013160 (1972)","journal-title":"SIAM J. Comput."},{"key":"19_CR19","unstructured":"The Coq development team: The Coq Reference Manual. INRIA (2017)"},{"issue":"1","key":"19_CR20","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1093\/jigpal\/12.1.1","volume":"12","author":"C-P Wirth","year":"2004","unstructured":"Wirth, C.-P.: Descente infinie + deduction. Logic J. IGPL 12(1), 1\u201396 (2004)","journal-title":"Logic J. IGPL"}],"container-title":["Lecture Notes in Computer Science","Automated Reasoning with Analytic Tableaux and Related Methods"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-66902-1_19","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,25]],"date-time":"2025-06-25T05:11:35Z","timestamp":1750828295000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-66902-1_19"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2017]]},"ISBN":["9783319669014","9783319669021"],"references-count":20,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-66902-1_19","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2017]]}}}