{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,11]],"date-time":"2024-09-11T19:39:01Z","timestamp":1726083541945},"publisher-location":"Cham","reference-count":21,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783030061661"},{"type":"electronic","value":"9783030061678"}],"license":[{"start":{"date-parts":[[2020,1,1]],"date-time":"2020-01-01T00:00:00Z","timestamp":1577836800000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2020]]},"DOI":"10.1007\/978-3-030-06167-8_3","type":"book-chapter","created":{"date-parts":[[2020,5,8]],"date-time":"2020-05-08T00:02:20Z","timestamp":1588896140000},"page":"53-81","update-policy":"http:\/\/dx.doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":0,"title":["Automated Deduction"],"prefix":"10.1007","author":[{"given":"Thierry","family":"Boy de la Tour","sequence":"first","affiliation":[]},{"given":"Ricardo","family":"Caferra","sequence":"additional","affiliation":[]},{"given":"Nicola","family":"Olivetti","sequence":"additional","affiliation":[]},{"given":"Nicolas","family":"Peltier","sequence":"additional","affiliation":[]},{"given":"Camilla","family":"Schwind","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2020,5,8]]},"reference":[{"key":"3_CR1","doi-asserted-by":"publisher","first-page":"2351","DOI":"10.1098\/rsta.2005.1650","volume":"363","author":"H Barendregt","year":"2005","unstructured":"Barendregt H, Wiedijk F (2005) The challenge of computer mathematics. Philos Trans R Soc A 363:2351\u20132375","journal-title":"Philos Trans R Soc A"},{"key":"3_CR2","doi-asserted-by":"crossref","unstructured":"Berardi S, Tatsuta M (2017) Equivalence of inductive definitions and cyclic proofs under arithmetic. In: 32nd annual ACM\/IEEE symposium on logic in computer science, LICS 2017, Reykjavik, Iceland, 20\u201323 June 2017. IEEE Computer Society, pp 1\u201312","DOI":"10.1109\/LICS.2017.8005114"},{"issue":"1\u20134","key":"3_CR3","doi-asserted-by":"publisher","first-page":"333","DOI":"10.1007\/s10817-018-9455-7","volume":"61","author":"JC Blanchette","year":"2018","unstructured":"Blanchette JC, Fleury M, Lammich P, Weidenbach C (2018) A verified SAT solver framework with learn, forget, restart, and incrementality. J Autom Reason 61(1\u20134):333\u2013365","journal-title":"J Autom Reason"},{"key":"3_CR4","doi-asserted-by":"crossref","unstructured":"Bledsoe WW, Loveland DW (eds) (1984) Automated theorem proving: after 25 years. Contemporary mathematics, vol\u00a029. American Mathematical Society, Providence","DOI":"10.1090\/conm\/029"},{"key":"3_CR5","unstructured":"Buss SR (1998) Handbook of proof theory. Studies in logic and the foundations of mathematics. Elsevier Science Publisher, New York"},{"key":"3_CR6","doi-asserted-by":"crossref","unstructured":"Caferra R, Leitsch A, Peltier N (2004) Automated model building. Applied logic (Kluwer), vol\u00a031. Springer (Kluwer), Berlin","DOI":"10.1007\/978-1-4020-2653-9"},{"key":"3_CR7","doi-asserted-by":"crossref","unstructured":"de\u00a0Moura LM, Kong S, Avigad J, van Doorn F, von Raumer J (2015) The lean theorem prover (system description). In: Automated deduction - CADE-25 - 25th international conference on automated deduction, Berlin, Germany, 1\u20137 August 2015, Proceedings, pp 378\u2013388","DOI":"10.1007\/978-3-319-21401-6_26"},{"key":"3_CR8","doi-asserted-by":"crossref","unstructured":"Fitting MC (1983) Proof methods for modal and intuitionistic logics, vol 169. Synthese library. D. Reidel, Dordrecht","DOI":"10.1007\/978-94-017-2794-5"},{"key":"3_CR9","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-4612-2360-3","volume-title":"First-order logic and automated theorem proving","author":"MC Fitting","year":"1996","unstructured":"Fitting MC (1996) First-order logic and automated theorem proving, 2nd edn. Springer, New York","edition":"2"},{"key":"3_CR10","doi-asserted-by":"crossref","unstructured":"Gor\u00e9 R (1999) Tableau methods for modal and temporal logics. Handbook of tableau methods. Kluwer Academic Publishers, Dordrecht, pp 297\u2013396","DOI":"10.1007\/978-94-017-1754-0_6"},{"key":"3_CR11","doi-asserted-by":"publisher","first-page":"67","DOI":"10.1002\/malq.19630090502","volume":"9","author":"SA Kripke","year":"1963","unstructured":"Kripke SA (1963) Semantical analysis of modal logic I, normal propositional calculi. Zeitschr f math Logik u Grundl d Math 9:67\u201396","journal-title":"Zeitschr f math Logik u Grundl d Math"},{"key":"3_CR12","doi-asserted-by":"crossref","unstructured":"Leitsch A (1997) The resolution calculus. Texts in theoretical computer science. Springer, Berlin","DOI":"10.1007\/978-3-642-60605-2"},{"issue":"3","key":"3_CR13","doi-asserted-by":"publisher","first-page":"319","DOI":"10.1023\/A:1006155811656","volume":"24","author":"F Massacci","year":"2000","unstructured":"Massacci F (2000) Single step tableaux for modal logics. J Autom Reason 24(3):319\u2013364","journal-title":"J Autom Reason"},{"key":"3_CR14","doi-asserted-by":"crossref","unstructured":"Reynolds A, Blanchette JC, Cruanes S, Tinelli C (2016) Model finding for recursive functions in SMT. In: Automated reasoning - 8th international joint conference, IJCAR 2016, Coimbra, Portugal, June 27\u2013July 2 2016, Proceedings, pp 133\u2013151","DOI":"10.1007\/978-3-319-40229-1_10"},{"key":"3_CR15","unstructured":"Robinson JA, Voronkov A (2001) Handbook of automated reasoning (2 volumes). Elsevier and MIT Press, Amsterdam and Cambridge"},{"key":"3_CR16","unstructured":"Sch\u00fctte P (1978) Vollst\u00e4ndige Systeme modaler und intuitionistischer Logik. Springer, Berlin"},{"key":"3_CR17","doi-asserted-by":"crossref","unstructured":"Siekmann J, Wrightson G (eds) (1983) Automation of reasoning. Classical papers on computational logic 1957-1967 and 1967-1970, vol 1, 2. Springer, Berlin","DOI":"10.1007\/978-3-642-81955-1"},{"issue":"18","key":"3_CR18","doi-asserted-by":"publisher","first-page":"2015","DOI":"10.1016\/j.artint.2008.09.004","volume":"172","author":"A Sloman","year":"2008","unstructured":"Sloman A (2008) The well-designed young mathematician. Artif Intell 172(18):2015\u20132034","journal-title":"Artif Intell"},{"key":"3_CR19","doi-asserted-by":"crossref","unstructured":"Sutcliffe G (2017) The TPTP problem library and associated infrastructure - from CNF to th0, TPTP v6.4.0. J Autom Reason 59(4):483\u2013502","DOI":"10.1007\/s10817-017-9407-7"},{"key":"3_CR20","unstructured":"Wos L (1988) Automated reasoning: 33 basic research problems. Prentice Hall, Englewood Cliffs"},{"key":"3_CR21","unstructured":"Wos L, Overbeek R, Lusk E, Boyle J (1992) Automated reasoning: introduction and applications. McGraw-Hill, New York"}],"container-title":["A Guided Tour of Artificial Intelligence Research"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-030-06167-8_3","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,9,30]],"date-time":"2023-09-30T20:34:36Z","timestamp":1696106076000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-030-06167-8_3"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2020]]},"ISBN":["9783030061661","9783030061678"],"references-count":21,"URL":"https:\/\/doi.org\/10.1007\/978-3-030-06167-8_3","relation":{},"subject":[],"published":{"date-parts":[[2020]]},"assertion":[{"value":"8 May 2020","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}}]}}