{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,4,10]],"date-time":"2026-04-10T11:02:59Z","timestamp":1775818979538,"version":"3.50.1"},"publisher-location":"Berlin, Heidelberg","reference-count":28,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783540710691","type":"print"},{"value":"9783540710707","type":"electronic"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"DOI":"10.1007\/978-3-540-71070-7_23","type":"book-chapter","created":{"date-parts":[[2008,8,29]],"date-time":"2008-08-29T09:56:30Z","timestamp":1220003790000},"page":"283-291","source":"Crossref","is-referenced-by-count":33,"title":["leanCoP 2.0 and ileanCoP 1.2: High Performance Lean Theorem Proving in Classical and Intuitionistic Logic (System Descriptions)"],"prefix":"10.1007","author":[{"given":"Jens","family":"Otten","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"23_CR1","doi-asserted-by":"crossref","first-page":"31","DOI":"10.1007\/978-94-011-3488-0_2","volume-title":"Automated Reasoning: Essays in Honor of Woody Bledsoe","author":"O. Astrachan","year":"1991","unstructured":"Astrachan, O., Loveland, D.: METEORs: High Performance Theorem Provers Using Model Elimination. In: Bledsoe, W.W., Boyer, S. (eds.) Automated Reasoning: Essays in Honor of Woody Bledsoe, pp. 31\u201360. Kluwer, Amsterdam (1991)"},{"key":"23_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"793","DOI":"10.1007\/3-540-58156-1_62","volume-title":"Automated Deduction - CADE-12","author":"B. Beckert","year":"1994","unstructured":"Beckert, B., Posegga, J.: lean TA P: Lean Tableau-Based Theorem Proving. In: Bundy, A. (ed.) CADE 1994. LNCS, vol.\u00a0814, pp. 793\u2013797. Springer, Heidelberg (1994)"},{"key":"23_CR3","doi-asserted-by":"publisher","first-page":"844","DOI":"10.1145\/182.183","volume":"26","author":"W. Bibel","year":"1983","unstructured":"Bibel, W.: Matings in Matrices. Commun. ACM\u00a026, 844\u2013852 (1983)","journal-title":"Commun. ACM"},{"key":"23_CR4","doi-asserted-by":"crossref","unstructured":"Bibel, W.: Automated Theorem Proving. Vieweg, Wiesbaden (1987)","DOI":"10.1007\/978-3-322-90102-6"},{"key":"23_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"783","DOI":"10.1007\/3-540-58156-1_60","volume-title":"Automated Deduction - CADE-12","author":"W. Bibel","year":"1994","unstructured":"Bibel, W., Br\u00fcning, S., Egly, U., Rath, T.: KoMeT. In: Bundy, A. (ed.) CADE 1994. LNCS, vol.\u00a0814, pp. 783\u2013787. Springer, Heidelberg (1994)"},{"key":"23_CR6","first-page":"88","volume":"5","author":"C. Kreitz","year":"1999","unstructured":"Kreitz, C., Otten, J.: Connection-based Theorem Proving in Classical and Non-classical Logics. Journal of Universal Computer Science\u00a05, 88\u2013112 (1999)","journal-title":"Journal of Universal Computer Science"},{"key":"23_CR7","doi-asserted-by":"publisher","first-page":"183","DOI":"10.1007\/BF00244282","volume":"8","author":"R. Letz","year":"1992","unstructured":"Letz, R., Schumann, J., Bayerl, S., Bibel, W.: SETHEO: A High-Performance Theorem Prover. Journal of Automated Reasoning\u00a08, 183\u2013212 (1992)","journal-title":"Journal of Automated Reasoning"},{"key":"23_CR8","doi-asserted-by":"publisher","first-page":"297","DOI":"10.1007\/BF00881947","volume":"13","author":"R. Letz","year":"1994","unstructured":"Letz, R., Mayr, K., Goller, C.: Controlled Integration of the Cut Rule into Connection Tableaux Calculi. Journal of Automated Reasoning\u00a013, 297\u2013337 (1994)","journal-title":"Journal of Automated Reasoning"},{"key":"23_CR9","doi-asserted-by":"publisher","first-page":"2015","DOI":"10.1016\/B978-044450813-3\/50030-8","volume-title":"Handbook of Automated Reasoning","author":"R. Letz","year":"2001","unstructured":"Letz, R., Stenz, G.: Model Elimination and Connection Tableau Procedures. In: Robinson, A., Voronkov, A. (eds.) Handbook of Automated Reasoning, pp. 2015\u20132114. Elsevier, Amsterdam (2001)"},{"key":"23_CR10","doi-asserted-by":"publisher","first-page":"236","DOI":"10.1145\/321450.321456","volume":"15","author":"D. Loveland","year":"1968","unstructured":"Loveland, D.: Mechanical Theorem-Proving by Model Elimination. Journal of the ACM\u00a015, 236\u2013251 (1968)","journal-title":"Journal of the ACM"},{"key":"23_CR11","doi-asserted-by":"crossref","unstructured":"McCune, W.: Otter 3.0 Reference Manual and Guide. Technical report ANL-94\/6, Argonne National Laboratory (1994)","DOI":"10.2172\/10129052"},{"key":"23_CR12","unstructured":"McCune, W.: Release of Prover9. In: Mile High Conference on Quasigroups, Loops and Nonassociative Systems, Technical report, Denver (2005)"},{"key":"23_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"307","DOI":"10.1007\/BFb0027422","volume-title":"Automated Reasoning with Analytic Tableaux and Related Methods","author":"J. Otten","year":"1997","unstructured":"Otten, J.: ileanT AP: An Intuitionistic Theorem Prover. In: Galmiche, D. (ed.) TABLEAUX 1997. LNCS, vol.\u00a01227, pp. 307\u2013312. Springer, Heidelberg (1997)"},{"key":"23_CR14","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"publisher","first-page":"245","DOI":"10.1007\/11554554_19","volume-title":"Automated Reasoning with Analytic Tableaux and Related Methods","author":"J. Otten","year":"2005","unstructured":"Otten, J.: Clausal Connection-Based Theorem Proving in Intuitionistic First-Order Logic. In: Beckert, B. (ed.) TABLEAUX 2005. LNCS (LNAI), vol.\u00a03702, pp. 245\u2013261. Springer, Heidelberg (2005)"},{"key":"23_CR15","unstructured":"Otten, J.: Restricting Backtracking in Connection Calculi. Technical report, Institut f\u00fcr Informatik, University of Potsdam (2008)"},{"key":"23_CR16","doi-asserted-by":"publisher","first-page":"139","DOI":"10.1016\/S0747-7171(03)00037-3","volume":"36","author":"J. Otten","year":"2003","unstructured":"Otten, J., Bibel, W.: leanCoP: Lean Connection-based Theorem Proving. Journal of Symbolic Computation\u00a036, 139\u2013161 (2003)","journal-title":"Journal of Symbolic Computation"},{"key":"23_CR17","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"244","DOI":"10.1007\/3-540-61208-4_16","volume-title":"Theorem Proving with Analytic Tableaux and Related Methods","author":"J. Otten","year":"1996","unstructured":"Otten, J., Kreitz, C.: T-String-Unification: Unifying Prefixes in Non-classical Proof Methods. In: Miglioli, P., Moscato, U., Ornaghi, M., Mundici, D. (eds.) TABLEAUX 1996. LNCS, vol.\u00a01071, pp. 244\u2013260. Springer, Heidelberg (1996)"},{"key":"23_CR18","unstructured":"Raths, T., Otten, J.: randoCoP: Randomizing the Proof Search Order in the Connection Calculus. Technical report, Institut f\u00fcr Informatik, University of Potsdam (2008)"},{"key":"23_CR19","doi-asserted-by":"publisher","first-page":"261","DOI":"10.1007\/s10817-006-9060-z","volume":"38","author":"T. Raths","year":"2007","unstructured":"Raths, T., Otten, J., Kreitz, C.: The ILTP Problem Library for Intuitionistic Logic. Journal of Automated Reasoning\u00a038, 261\u2013271 (2007)","journal-title":"Journal of Automated Reasoning"},{"key":"23_CR20","doi-asserted-by":"publisher","first-page":"619","DOI":"10.1093\/logcom\/2.5.619","volume":"2","author":"D. Sahlin","year":"1992","unstructured":"Sahlin, D., Franzen, T., Haridi, S.: An Intuitionistic Predicate Logic Theorem Prover. Journal of Logic and Computation\u00a02, 619\u2013656 (1992)","journal-title":"Journal of Logic and Computation"},{"key":"23_CR21","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"publisher","first-page":"421","DOI":"10.1007\/3-540-45744-5_34","volume-title":"Automated Reasoning","author":"S. Schmitt","year":"2001","unstructured":"Schmitt, S., Lorigo, L., Kreitz, C., Nogin, A.: JProver: Integrating Connection-based Theorem Proving into Interactive Proof Assistants. In: Gor\u00e9, R.P., Leitsch, A., Nipkow, T. (eds.) IJCAR 2001. LNCS (LNAI), vol.\u00a02083, pp. 421\u2013426. Springer, Heidelberg (2001)"},{"key":"23_CR22","doi-asserted-by":"publisher","first-page":"353","DOI":"10.1007\/BF00297245","volume":"4","author":"M. Stickel","year":"1988","unstructured":"Stickel, M.: A Prolog Technology Theorem Prover: Implementation by an Extended Prolog Compiler. Journal of Automated Reasoning\u00a04, 353\u2013380 (1988)","journal-title":"Journal of Automated Reasoning"},{"key":"23_CR23","first-page":"71","volume":"21","author":"G. Sutcliffe","year":"2008","unstructured":"Sutcliffe, G.: The CADE-21 Automated Theorem Proving System Competition. AI Communications\u00a021, 71\u201381 (2008)","journal-title":"AI Communications"},{"key":"23_CR24","doi-asserted-by":"publisher","first-page":"177","DOI":"10.1023\/A:1005806324129","volume":"21","author":"G. Sutcliffe","year":"1998","unstructured":"Sutcliffe, G., Suttner, C.: The TPTP Problem Library. Journal of Automated Reasoning\u00a021, 177\u2013203 (1998)","journal-title":"Journal of Automated Reasoning"},{"key":"23_CR25","doi-asserted-by":"publisher","first-page":"21","DOI":"10.1007\/s10817-006-9032-3","volume":"37","author":"J. Urban","year":"2006","unstructured":"Urban, J.: MPTP 0.2: Design, Implementation, and Initial Experiments. Journal of Automated Reasoning\u00a037, 21\u201343 (2006)","journal-title":"Journal of Automated Reasoning"},{"key":"23_CR26","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"2","DOI":"10.1007\/3-540-61511-3_65","volume-title":"Automated Deduction - Cade-13","author":"T. Tammet","year":"1996","unstructured":"Tammet, T.: A Resolution Theorem Prover for Intuitionistic Logic. In: McRobbie, M.A., Slaney, J.K. (eds.) CADE 1996. LNCS, vol.\u00a01104, pp. 2\u201316. Springer, Heidelberg (1996)"},{"key":"23_CR27","doi-asserted-by":"publisher","first-page":"1487","DOI":"10.1016\/B978-044450813-3\/50024-2","volume-title":"Handbook of Automated Reasoning","author":"A. Waaler","year":"2001","unstructured":"Waaler, A.: Connections in Nonclassical Logics. In: Robinson, A., Voronkov, A. (eds.) Handbook of Automated Reasoning, pp. 1487\u20131578. Elsevier, Amsterdam (2001)"},{"key":"23_CR28","volume-title":"Automated Deduction in Nonclassical Logics","author":"L. Wallen","year":"1990","unstructured":"Wallen, L.: Automated Deduction in Nonclassical Logics. MIT Press, Cambridge (1990)"}],"container-title":["Lecture Notes in Computer Science","Automated Reasoning"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-540-71070-7_23.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,11,19]],"date-time":"2020-11-19T05:15:11Z","timestamp":1605762911000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-540-71070-7_23"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[null]]},"ISBN":["9783540710691","9783540710707"],"references-count":28,"URL":"https:\/\/doi.org\/10.1007\/978-3-540-71070-7_23","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[]}}