{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,7]],"date-time":"2024-09-07T22:38:43Z","timestamp":1725748723722},"publisher-location":"Berlin, Heidelberg","reference-count":14,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783642408847"},{"type":"electronic","value":"9783642408854"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2013]]},"DOI":"10.1007\/978-3-642-40885-4_16","type":"book-chapter","created":{"date-parts":[[2013,9,11]],"date-time":"2013-09-11T11:20:19Z","timestamp":1378898419000},"page":"229-244","source":"Crossref","is-referenced-by-count":0,"title":["Detection of First Order Axiomatic Theories"],"prefix":"10.1007","author":[{"given":"Guillaume","family":"Burel","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Simon","family":"Cruanes","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"16_CR1","unstructured":"Abiteboul, S., Hull, R., Vianu, V.: Foundations of Databases. Addison-Wesley (1995)"},{"issue":"1-2","key":"16_CR2","doi-asserted-by":"publisher","first-page":"217","DOI":"10.1016\/S0747-7171(03)00024-5","volume":"36","author":"J. Avenhaus","year":"2003","unstructured":"Avenhaus, J., Hillenbrand, T., L\u00f6chner, B.: On using ground joinable equations in equational theorem proving. Journal of Symbolic Computation\u00a036(1-2), 217\u2013233 (2003)","journal-title":"Journal of Symbolic Computation"},{"key":"16_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/3-540-60381-6_1","volume-title":"Conditional and Typed Rewriting Systems","author":"L. Bachmair","year":"1995","unstructured":"Bachmair, L., Ganzinger, H.: Associative-commutative superposition. In: Dershowitz, N., Lindenstrauss, N. (eds.) CTRS 1994. LNCS, vol.\u00a0968, pp. 1\u201314. Springer, Heidelberg (1995)"},{"key":"16_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"62","DOI":"10.1007\/3-540-61511-3_69","volume-title":"Automated Deduction - Cade-13","author":"J. Denzinger","year":"1996","unstructured":"Denzinger, J., Schulz, S.: Learning domain knowledge to improve theorem proving. In: McRobbie, M.A., Slaney, J.K. (eds.) CADE 1996. LNCS, vol.\u00a01104, pp. 62\u201376. Springer, Heidelberg (1996)"},{"key":"16_CR5","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"publisher","first-page":"335","DOI":"10.1007\/978-3-540-45085-6_31","volume-title":"Automated Deduction \u2013 CADE-19","author":"H. Ganzinger","year":"2003","unstructured":"Ganzinger, H., Stuber, J.: Superposition with equivalence reasoning and delayed clause normal form transformation. In: Baader, F. (ed.) CADE 2003. LNCS (LNAI), vol.\u00a02741, pp. 335\u2013349. Springer, Heidelberg (2003)"},{"key":"16_CR6","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"publisher","first-page":"232","DOI":"10.1007\/3-540-48660-7_20","volume-title":"Automated Deduction - CADE-16","author":"T. Hillenbrand","year":"1999","unstructured":"Hillenbrand, T., Jaeger, A., L\u00f6chner, B.: System description: Waldmeister \u2013 improvements in performance and ease of use. In: Ganzinger, H. (ed.) CADE 1999. LNCS (LNAI), vol.\u00a01632, pp. 232\u2013236. Springer, Heidelberg (1999)"},{"key":"16_CR7","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"publisher","first-page":"292","DOI":"10.1007\/978-3-540-71070-7_24","volume-title":"Automated Reasoning","author":"K. Korovin","year":"2008","unstructured":"Korovin, K.: iProver \u2013 An Instantiation-Based Theorem Prover for First-Order Logic (System Description). In: Armando, A., Baumgartner, P., Dowek, G. (eds.) IJCAR 2008. LNCS (LNAI), vol.\u00a05195, pp. 292\u2013298. Springer, Heidelberg (2008)"},{"key":"16_CR8","unstructured":"Nieuwenhuis, R., Rubio, A.: Paramodulation-based theorem proving. In: Robinson, J.A., Voronkov, A. (eds.) Handbook of Automated Reasoning. Elsevier, MIT Press (1999)"},{"key":"16_CR9","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"publisher","first-page":"376","DOI":"10.1007\/3-540-45744-5_29","volume-title":"Automated Reasoning","author":"A. Riazanov","year":"2001","unstructured":"Riazanov, A., Voronkov, A.: Vampire 1.1 (System description). In: Gor\u00e9, R.P., Leitsch, A., Nipkow, T. (eds.) IJCAR 2001. LNCS (LNAI), vol.\u00a02083, pp. 376\u2013380. Springer, Heidelberg (2001)"},{"issue":"1","key":"16_CR10","doi-asserted-by":"publisher","first-page":"23","DOI":"10.1145\/321250.321253","volume":"12","author":"J.A. Robinson","year":"1965","unstructured":"Robinson, J.A.: A Machine-Oriented Logic Based on the Resolution Principle. J. ACM\u00a012(1), 23\u201341 (1965)","journal-title":"J. ACM"},{"issue":"2,3","key":"16_CR11","first-page":"111","volume":"15","author":"S. Schulz","year":"2002","unstructured":"Schulz, S.: E - a brainiac theorem prover. AI Commun.\u00a015(2,3), 111\u2013126 (2002)","journal-title":"AI Commun."},{"key":"16_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"33","DOI":"10.1007\/3-540-61464-8_41","volume-title":"Rewriting Techniques and Applications","author":"J. Stuber","year":"1996","unstructured":"Stuber, J.: Superposition theorem proving for abelian groups represented as integer modules. In: Ganzinger, H. (ed.) RTA 1996. LNCS, vol.\u00a01103, pp. 33\u201347. Springer, Heidelberg (1996)"},{"issue":"4","key":"16_CR13","doi-asserted-by":"publisher","first-page":"337","DOI":"10.1007\/s10817-009-9143-8","volume":"43","author":"G. Sutcliffe","year":"2009","unstructured":"Sutcliffe, G.: The TPTP Problem Library and Associated Infrastructure: The FOF and CNF Parts, v3.5.0. Journal of Automated Reasoning\u00a043(4), 337\u2013362 (2009)","journal-title":"Journal of Automated Reasoning"},{"key":"16_CR14","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"publisher","first-page":"514","DOI":"10.1007\/978-3-540-73595-3_38","volume-title":"Automated Deduction \u2013 CADE-21","author":"C. Weidenbach","year":"2007","unstructured":"Weidenbach, C., Schmidt, R.A., Hillenbrand, T., Rusev, R., Topic, D.: System Description: Spass Version 3.0. In: Pfenning, F. (ed.) CADE 2007. LNCS (LNAI), vol.\u00a04603, pp. 514\u2013520. Springer, Heidelberg (2007)"}],"container-title":["Lecture Notes in Computer Science","Frontiers of Combining Systems"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-40885-4_16","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,17]],"date-time":"2019-05-17T05:04:54Z","timestamp":1558069494000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-40885-4_16"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2013]]},"ISBN":["9783642408847","9783642408854"],"references-count":14,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-40885-4_16","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2013]]}}}