Jens Otten

Publications

This is a selection of papers that appeared in books, journals, and in conference or workshop proceedings. Most of the papers in conference proceedings appeared in Springer's Lecture Notes in Computer Science (LNSC) or Lecture Notes in Artificial Intelligence (LNAI) series.

Most of the theoretical results presented in the following papers have been implemented. The source code of these programs together with more information can be found in the theorem provers section. Please contact me if you have problems downloading a paper.

Contents:

2020 - 2023

  • Proceedings of the International Workshop on Automated Reasoning with Connection Calculi (AReCCa 2023).
    Jens Otten and Wolfgang Bibel.
    CEUR Workshop Proceedings. CEUR-WS.org, 2023.
    (to appear)

  • 20 Years of leanCoP - An Overview of the Provers.
    Jens Otten.
    In J. Otten, Wolfgang Bibel, editors, Automated Reasoning with Connection Calculi, AReCCa 2023, CEUR Workshop Proceedings. CEUR-WS.org, 2023.
    (to appear)

  • Connections: Markov Decision Processes for Classical, Intuitionistic and Modal Connection Calculi.
    Fredrik Rømming, Jens Otten, Sean B. Holden.
    In J. Otten, Wolfgang Bibel, editors, Automated Reasoning with Connection Calculi, AReCCa 2023, CEUR Workshop Proceedings. CEUR-WS.org, 2023.
    (to appear)

  • A Syntax for Connection Proofs.
    Jens Otten and Sean B. Holden.
    In J. Otten, Wolfgang Bibel, editors, Automated Reasoning with Connection Calculi, AReCCa 2023, CEUR Workshop Proceedings. CEUR-WS.org, 2023.
    (to appear)

  • Advancing Automated Theorem Proving for the Modal Logics D and S5.
    Jens Otten.
    In C. Benzmüller, J. Otten, editors, Automated Reasoning in Quantified Non-Classical Logics, ARQNL 2022, CEUR Workshop Proceedings. CEUR-WS.org, 2022. (to appear)

      · modal-DS5-cop_arqnl22.pdf (180 kbytes)

  • Proceedings of the 4th International Workshop on Automated Reasoning in Quantified Non-Classical Logics (ARQNL 2022).
    Christoph Benzmüller and Jens Otten.
    CEUR Workshop Proceedings, volume 3326. CEUR-WS.org, 2022.

  • The nanoCoP 2.0 Connection Provers for Classical, Intuitionistic and Modal Logics.
    Jens Otten.
    In A. Das and S. Negri, editors, Automated Reasoning with Analytic Tableaux and Related Methods, TABLEAUX 2021, LNAI 12842, pages 236-249. © Springer, 2021.

      · nanocop20iM_tab21.pdf (253 kbytes)

    See the nanoCoP, nanoCoP-i and nanoCoP-M homepages for more information.

  • From Schütte's Formal Systems to Modern Automated Deduction.
    Wolfgang Bibel and Jens Otten.
    In R. Kahle, M. Rathjen, editors, The Legacy of Kurt Schütte, pages 217-251. Springer, 2020.

  • Equality Preprocessing in Connection Calculi.
    Benjamin Oliver and Jens Otten
    In P. Fontaine et al., editors, PAAR 2020, CEUR Workshop Proceedings, volume 2752, pages 76-92. CEUR-WS.org, 2020.

      · equality_epicc_paar20.pdf (281 kbytes)

    See the leanCoP-EPICC homepage for more information.

2015 - 2019

  • Converting ALC Connection Proofs into ALC Sequents.
    Eunice Palmeira, Fred Freitas, Jens Otten.
    In H. Barbosa, G. Reis, editors, 6th Workshop on Proof eXchange for Theorem Proving, PxTP 2019. EPTCS, 2019.

      · converting_alc_proofs_pxtp19.pdf (279 kbytes)

  • The Pocket Reasoner - Automatic Reasoning on Small Devices.
    Jens Otten.
    In E. B. Johnsen, I. C. Yu, editors, Norwegian Informatics Conference, NIK 2018. Open Journal Systems, 2018.

      · leancop-ipod_NIK18.pdf (469 kbytes)

    See the leanCoP homepage for more information.

  • Proof Search Optimizations for Non-clausal Connection Calculi.
    Jens Otten.
    In B. Konev, J. Urban, P. Rümmer, editors, Workshop on Practical Aspects of Automated Reasoning, PAAR 2018, CEUR Workshop Proceedings, volume 2162, pages 49-57. CEUR-WS.org, 2018.

      · nanocop11_paar18.pdf (181 kbytes)

    See the nanoCoP homepage for more information.

  • Proceedings of the 3rd International Workshop on Automated Reasoning in Quantified Non-Classical Logics (ARQNL 2018).
    Christoph Benzmüller and Jens Otten.
    CEUR Workshop Proceedings, volume 2095. CEUR-WS.org, 2018.

  • Non-clausal Connection Calculi for Non-classical Logics.
    Jens Otten.
    In R.A. Schmidt and C. Nalon, editors, Automated Reasoning with Analytic Tableaux and Related Methods, TABLEAUX 2017, LNAI 10501, pages 209-227. © Springer, 2017.

      · noncla-nonclass_tab17.pdf (251 kbytes)

    See the nanoCoP-i and nanoCoP-M homepages for more information.

  • nanoCoP: Natural Non-clausal Theorem Proving.
    Jens Otten.
    In C. Sierra, editor, International Joint Conference on Artificial Intelligence, IJCAI 2017, Sister Conference Best Paper Track, pages 4924-4928, ijcai.org, 2017.

      · nanocop_ijcai17.pdf (258 kbytes)

    See the nanoCoP homepage for more information.

  • RACCOON: A Connection Reasoner for the Description Logic ALC.
    Dimas Melo Filho, Fred Freitas, Jens Otten.
    In T. Eiter and D. Sands, editors, Logic for Programming, Artificial Intelligence and Reasoning, LPAR 2017, EPiC 46, pages 200-211. EasyChair, 2017.

      · raccoon_lpar17.pdf (1.6 Mbytes)

  • Advances in Connection-Based Automated Theorem Proving.
    Jens Otten and Wolfgang Bibel.
    In M. Hinchey, J. Bowen, E.-R. Olderog, editors, Provably Correct Systems, NASA Monographs in Systems and Software Engineering, pages 211-241. © Springer, 2017.

  • nanoCoP: A Non-clausal Connection Prover.
    Jens Otten.
    In N. Olivetti and A. Tiwari, editors, Automated Reasoning, IJCAR 2016, LNAI 9706, pages 302-312. © Springer, 2016.

      · nanocop_ijcar16.pdf (207 kbytes)

    See the nanoCoP homepage for more information.

  • Non-clausal Connection-based Theorem Proving in Intuitionistic First-Order Logic.
    Jens Otten.
    In C. Benzmüller, J. Otten, editors, Automated Reasoning in Quantified Non-Classical Logics, ARQNL 2016, CEUR Workshop Proceedings, volume 1770, pages 9-20. CEUR-WS.org, 2016.

      · nanocop-i_arqnl16.pdf (251 kbytes)

  • Proceedings of the 2nd International Workshop on Automated Reasoning in Quantified Non-Classical Logics (ARQNL 2016).
    Christoph Benzmüller and Jens Otten.
    CEUR Workshop Proceedings, volume 1770. CEUR-WS.org, 2016.

  • A Connection Calculus for the Description Logic ALC.
    Fred Freitas and Jens Otten.
    In R. Khoury, C. Drummond, editors, 29th Canadian Conference on Artificial Intelligence, Canadian AI 2016, LNAI 9673, pages 243-256. © Springer, 2016.

      · connect_alc_cai16.pdf (1148 kbytes)

  • Problem Libraries for Non-Classical Logics.
    Jens Otten and Thomas Raths.
    In C. Benzmüller, J. Otten, editors, Automated Reasoning in Quantified Non-Classical Logics, ARQNL 2014, EPiC, volume 33, pages 31-36. EasyChair, 2015.

      · libraries_arqnl14.pdf (141 kbytes)

  • Proceedings of the 1st International Workshop on Automated Reasoning in Quantified Non-Classical Logics (ARQNL 2014).
    Christoph Benzmüller and Jens Otten.
    EPiC, volume 33. EasyChair, 2015.

2010 - 2014

  • MleanCoP: A Connection Prover for First-Order Modal Logic.
    Jens Otten.
    In S. Demri, D. Kapur, C. Weidenbach, editors, Automated Reasoning, IJCAR 2014, LNAI 8562, pages 269-276. © Springer, 2014.

      · mleancop_ijcar14.pdf (202 kbytes)

    See the MleanCoP homepage for more information.

  • Konnektionskalküle für automatisches Beweisen in klassischen und nicht-klassischen Logiken.
    Jens Otten.
    In S. Hölldobler et al., editors, Ausgezeichnete Informatikdissertationen 2013, GI-Edition-Lecture Notes in Informatics (LNI), volume D-14, pages 161-170. Bonner Köllen Verlag, 2014.

  • Implementing and Evaluating Provers for First-order Modal Logics.
    Christoph Benzmüller, Jens Otten, Thomas Raths.
    In L. De Raedt et al., editors, 20th European Conference on Artificial Intelligence, ECAI 2012, pages 163-168. © IOS Press, 2012.

      · modal_ecai12.pdf (295 kbytes)

  • The QMLTP Problem Library for First-order Modal Logics.
    Thomas Raths and Jens Otten.
    In B. Gramlich, D. Miller, U. Sattler, editors, Automated Reasoning, IJCAR 2012, LNAI 7364, pages 454-461. © Springer, 2012.

      · qmltp_ijcar12.pdf (178 kbytes)

    See the QMLTP library homepage for more information.

  • Implementing Connection Calculi for First-order Modal Logics.
    Jens Otten.
    In E. Ternovska, K. Korovin, S. Schulz, editors, International Workshop on the Implementation of Logics, IWIL 2012, EPiC, volume 22, pages 18-32. EasyChair, 2012.

      · mleancop_iwil12.pdf (302 kbytes)
      · mleancop_iwil12.dvi (139 kbytes)

    See the MleanCoP homepage for more information.

  • Implementing Different Proof Calculi for First-order Modal Logics.
    Christoph Benzmüller, Jens Otten, Thomas Raths.
    In P. Fontaine, R. A. Schmidt, S. Schulz, editors, Workshop on Practical Aspects of Automated Reasoning, PAAR 2012, EPiC, volume 21, pages 12-18. EasyChair, 2012.

      · modal_paar12.pdf (200 kbytes)
      · modal_paar12.dvi (56 kbytes)

  • A Non-clausal Connection Calculus.
    Jens Otten.
    In K. Brünnler and G. Metcalfe, editors, Automated Reasoning with Analytic Tableaux and Related Methods, TABLEAUX 2011, LNAI 6793, pages 226-241. © Springer, 2011.

      · concalc_tab11.pdf (336 kbytes)
      · concalc_tab11.dvi (183 kbytes)

  • Evaluating Automated Theorem Provers for First-Order Modal Logics.
    Thomas Raths und Jens Otten.
    In M. Giese, R. Kuznets, editors, International Workshop on First-Order Theorem Proving: TABLEAUX 2011 - Workshops, Tutorials, and Short Papers, Technical Report IAM-11-002, pages 47-63, University of Bern, 2011.

      · modal_ftp11.pdf (413 kbytes)

  • Restricting Backtracking in Connection Calculi.
    Jens Otten.
    AI Communications, volume 23, no. 2-3, pages 159-182. © IOS Press, 2010.

      · restricting_backtracking_aicom10.pdf (289 kbytes)

    See the leanCoP homepage for more information.

  • Specifying and Verifying Organizational Security Properties in First-Order Logic.
    Christoph Brandt, Jens Otten, Christoph Kreitz, Wolfgang Bibel.
    In S. Siegler, N. Wasser, editors, Verification, Induction, Termination Analysis, LNAI 6463, pages 38-53. © Springer, 2010.

      · security_festschrift10.pdf (327 kbytes)

  • Using the TPTP Language for Representing Derivations in Tableau and Connection Calculi.
    Jens Otten and Geoff Sutcliffe.
    In B. Konev, R. A. Schmidt, S. Schulz, editors, Workshop on Practical Aspects of Automated Reasoning, PAAR 2010, EPiC, volume 9, pages 95-105. EasyChair, 2010.

      · cop_syntax_paar10.pdf (192 kbytes)
      · cop_syntax_paar10.dvi (164 kbytes)

2005 - 2009

  • Building a Problem Library for First-Order Modal Logics.
    Thomas Raths and Jens Otten.
    TABLEAUX 2009 Position Papers and Workshop Proceedings, Research Report 387, pages 35-42, University of Oslo, 2009.

      · qmltp_tab09.pdf (140 kbytes)
      · qmltp_tab09.dvi (29 kbytes)

  • leanCoP 2.0 and ileanCoP 1.2: High Performance Lean Theorem Proving in Classical and Intuitionistic Logic.
    Jens Otten.
    In A. Armando, P. Baumgartner, G. Dowek, editors, Automated Reasoning, IJCAR 2008, LNAI 5195, pages 283-291. © Springer, 2008.

      · leancop20_ijcar08.pdf (176 kbytes)
      · leancop20_ijcar08.dvi (50 kbytes)

    See the leanCoP homepage for more information.

  • randoCoP: Randomizing the Proof Search Order in the Connection Calculus.
    Thomas Raths and Jens Otten.
    In B. Konev, R. A. Schmidt, S. Schulz, editors, First International Workshop on Practical Aspects of Automated Reasoning, PAAR 2008, Sydney/Australia, CEUR Workshop Proceedings, volume 373, pages 94-102. CEUR-WS.org, 2008.

      · randocop_paar08.pdf (186 kbytes)

  • The ILTP Problem Library for Intuitionistic Logic.
    Thomas Raths, Jens Otten, Christoph Kreitz.
    Journal of Automated Reasoning, volume 38, no. 1-3, pages 261-271. © Springer, 2007.

      · iltp_jar07.pdf (195 kbytes)
      · iltp_jar07.dvi (43 kbytes)

    See the ILTP library homepage for more information.

  • Clausal Connection-Based Theorem Proving in Intuitionistic First-Order Logic.
    Jens Otten.
    In B. Beckert, editor, Automated Reasoning with Analytic Tableaux and Related Methods, TABLEAUX 2005, LNAI 3702, pages 245-261. © Springer, 2005.

      · ileancop_tab05.pdf (320 kbytes)
      · ileancop_tab05.dvi (87 kbytes)

    See the ileanCoP homepage for more information.

  • The ILTP Library: Benchmarking Automated Theorem Provers for Intuitionistic Logic.
    Thomas Raths, Jens Otten, Christoph Kreitz.
    In B. Beckert, editor, Automated Reasoning with Analytic Tableaux and Related Methods, TABLEAUX 2005, LNAI 3702, pages 333-337. © Springer, 2005.

      · iltp_tab05.pdf (124 kbytes)
      · iltp_tab05.dvi (23 kbytes)

    See the ILTP library homepage for more information.

2000 - 2004

  • leanCoP: Lean Connection-Based Theorem Proving.
    Jens Otten and Wolfgang Bibel.
    Journal of Symbolic Computation, volume 36, pages 139-161. © Elsevier Science, 2003.

      · leancop_jsc.pdf (280 kbytes)
      · leancop_jsc.dvi (94 kbytes)

    See the leanCoP homepage for more information.

  • Matrix-based Constructive Theorem Proving.
    Christoph Kreitz, Jens Otten, Stephan Schmitt, Brigitte Pientka.
    In S. Hölldobler, editor, Intellectics and Computational Logic: Papers in Honor of Wolfgang Bibel, pages 189-205. © Kluwer, 2000.

      · construct_wb60.pdf (191 kbytes)

  • leanCoP: Lean Connection-Based Theorem Proving.
    Jens Otten and Wolfgang Bibel.
    Third International Workshop on First-Order Theorem Proving. Research Report 5/2000, pages 153-159, Universität Koblenz-Landau, 2000.

      · leancop_ftp00.pdf (173 kbytes)
      · leancop_ftp00.dvi (28 kbytes)

    See the leanCoP homepage for more information.

1994 - 1999

  • Connection-based Theorem Proving in Classical and Non-classical Logics.
    Christoph Kreitz and Jens Otten.
    Journal of Universal Computer Science, Special Issue on Integration of Deduction Systems, volume 5, no. 3, pages 88-112. © Springer, 1999.

      · connect_jucs.pdf (366 kbytes)

  • linTAP: A Tableau Prover for Linear Logic.
    Heiko Mantel and Jens Otten.
    In N. Murray, editor, International Conference on Analytic Tableaux and Related Methods, TABLEAUX 1999, LNAI 1617, pages 217-231. © Springer, 1999.

      · lintap_tab99.pdf (327 kbytes)
      · lintap_tab99.dvi (141 kbytes)

    See the linTAP homepage for more information.

  • Compressions and Extensions.
    W. Bibel, S. Brüning, J. Otten, T. Rath, T. Schaub.
    In W. Bibel, P. Schmitt, editors, Automated Deduction - A Basis for Applications, volume 1, chapter 1.5. © Kluwer, 1998.

      · compext_dedu.pdf (307 kbytes)

  • A Multi-Level Approach to Program Synthesis.
    W. Bibel, D. Korn, C. Kreitz, F. Kurucz, J. Otten, S. Schmitt, G. Stolpmann.
    In N. Fuchs, editor, 7th International Workshop on Logic Program Synthesis and Transformation, LOPSTR 1998, LNCS 1463, pages 1-27. © Springer, 1998.

      · multi_lopstr97.pdf (378 kbytes)

  • ileanTAP: An Intuitionistic Theorem Prover.
    Jens Otten.
    In D. Galmiche, editor, International Conference on Automated Reasoning with Analytic Tableaux and Related Methods, TABLEAUX 1997, LNAI 1227, pages 307-312. © Springer, 1997.

      · ileantap_tab97.pdf (171 kbytes)
      · ileantap_tab97.dvi (31 kbytes)

    See the ileanTAP homepage for more information.

  • Connection-Based Proof Construction in Linear Logic.
    Christoph Kreitz, Heiko Mantel, Jens Otten, Stephan Schmitt.
    In W. McCune, editor, 14th International Conference on Automated Deduction, CADE-14, LNAI 1249, pages 207-221. © Springer, 1997.

      · linlogic_cade97.pdf (283 kbytes)
      · linlogic_cade97.dvi (151 kbytes)

  • A Non-Clausal Davis-Putnam Proof Procedure.
    Jens Otten.
    In 15th International Joint Conference on Artificial Intelligence (Poster Session Abstracts), IJCAI-15, Nagoya/Japan, page 82, 1997.

  • Proof Strategies for Intuitionistic Logic.
    Jens Otten.
    In W. Bibel, U. Furbach, R. Hasegawa, M. Stickel, editors, Deduction, Dagstuhl Report 170, pages 14-15, 1997.

  • On the Advantage of a Non-Clausal Davis-Putnam Procedure.
    Jens Otten.
    Technical Report, AIDA-97-1, Technische Hochschule Darmstadt, Intellektik, 1997.

      · ncdp_aida97.pdf (202 kbytes)
      · ncdp_aida97.dvi (52 kbytes)

    See the ncDP homepage for more information.

  • A Uniform Proof Procedure for Classical and Non-Classical Logics.
    Jens Otten and Christoph Kreitz.
    In G. Görz, S. Hölldobler, editors, KI-96: Advances in Artificial Intelligence, LNAI 1137, pages 307-319. © Springer, 1996.

      · uniform_ki96.pdf (285 kbytes)
      · uniform_ki96.dvi (76 kbytes)

  • T-String-Unification: Unifying Prefixes in Non-Classical Proof Methods.
    Jens Otten and Christoph Kreitz.
    In P. Miglioli, U. Moscato, D. Mundici, M. Ornaghi, editors, 5th International Workshop on Theorem Proving with Analytic Tableaux and Related Methods, TABLEAUX 1996, LNAI 1071, pages 244-260. © Springer, 1996.

      · unify_tab96.pdf (286 kbytes)
      · unify_tab96.dvi (79 kbytes)

  • Guiding Program Development Systems by a Connection Based Proof Strategy.
    Christoph Kreitz, Jens Otten, Stephan Schmitt.
    In M. Proietti, editor, 5th International Workshop on Logic Program Synthesis and Transformation, LOPSTR 1996, LNCS 1048, pages 137-151. © Springer, 1996.

      · guide_lopstr95.pdf (261 kbytes)
      · guide_lopstr95.dvi (87 kbytes)

  • A Connection Based Proof Method for Intuitionistic Logic.
    Jens Otten and Christoph Kreitz.
    In P. Baumgartner, R. Hähnle, J. Posegga, editors, 4th International Workshop on Theorem Proving with Analytic Tableaux and Related Methods, TABLEAUX 1995, LNAI 918, pages 122-137. © Springer, 1995.

      · method_tab95.pdf (253 kbytes)
      · method_tab95.dvi (89 kbytes)

  • Connection Based Proof Method for Intuitionistic Logic - Abstract.
    Jens Otten and Ilka Dörnemann.
    In W. Bibel, C. Walther, editors, 11th Annual Meeting of the GI-Fachgruppe Deduktionssysteme, AIDA-94-06, page 21, Technische Hochschule Darmstadt, Intellektik, 1994.