Jens Otten
   Senior Researcher
University of Oslo  

Welcome!
Publications
Theorem Provers
Contact
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 have been published 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.


2015 - 2017
  • 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. EasyChair, 2017. (to appear)

  • Advances in Connection-Based Automated Theorem Proving.
    Jens Otten and Wolfgang Bibel.
    In J. Bowen, M. Hinchey, 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.

1995 - 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.


Jens Otten · Institutt for informatikk · University of Oslo · 01.01.2017