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.


2010 - 2015
  • Advances in Connection-Based Automated Theorem Proving.
    Jens Otten and Wolfgang Bibel.
    In J. Bowen, M. Hinchey, E.-R. Olderog, editors, Provably Correct Systems, © Springer Verlag, 2015. To appear.

  • Automated Reasoning in Quantified Non-Classical Logics (ARQNL 2014).
    Christoph Benzmüller and Jens Otten.
    Workshop Proceedings. EasyChair Proceedings in Computing, 2015.

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

      · mleancop_ijcar14.pdf (202 kbytes)

    See the MleanCoP homepage for more information.

  • Problem Libraries for Non-Classical Logics.
    Jens Otten and Thomas Raths.
    In C. Benzmüller, J. Otten, editors, International Workshop on Automated Reasoning in Quantified Non-Classical Logics, ARQNL 2014, EPiC. EasyChair, 2014.

      · libraries_arqnl14.pdf (141 kbytes)

  • Konnektionskalküle für automatisches Beweisen in klassischen und nicht-klassischen Logiken.
    Jens Otten.
    Ausgezeichnete Informatikdissertationen 2013, GI-Edition-Lecture Notes in Informatics (LNI) 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, International Joint Conference on Automated Reasoning, IJCAR 2012, LNAI 7364, pages 454-461. © Springer Verlag, 2012.

      · qmltp_ijcar12.pdf (178 kbytes)

    See the QMLTP library homepage for more information.

  • Implementing Different Proof Calculi for First-order Modal Logics.
    Christoph Benzmüller, Jens Otten, Thomas Raths.
    In P. Fontaine, R. Schmidt, S. Schulz, editors, International Workshop on Practical Aspects of Automated Reasoning (PAAR-2012), Manchester/UK, 2012.

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

  • 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), Merida/Venezuela, 2012.

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

    See the MleanCoP homepage for more information.

  • 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 Verlag, 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, Bern/Switzerland, 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 Verlag, 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, International Workshop on Practical Aspects of Automated Reasoning (PAAR-2010), Edinburgh/UK, 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 Verlag, 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), CEUR Workshop Proceedings 373, pages 94-102, Sydney/Australia, 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 Verlag, 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 Verlag, 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 Verlag, 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.
    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 Verlag, 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, LNAI 1617, pages 217-231. © Springer Verlag, 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, LNCS 1463, pages 1-27. © Springer Verlag, 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, LNAI 1227, pages 307-312. © Springer Verlag, 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, LNAI 1249, pages 207-221. © Springer Verlag, 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 (IJCAI), Poster Session Abstracts, 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 No. 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 Verlag, 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, LNAI 1071, pages 244-260. © Springer Verlag, 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, LNCS 1048, pages 137-151. © Springer Verlag, 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, LNAI 918, pages 122-137. © Springer Verlag, 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 · 11.11.2016