This is selection of papers that appeared in books and journals, in conference proceedings, or as technical reports. Most of the papers in conference proceedings have been published within Springer's Lecture Notes in Computer Science (LNSC) or Lecture Notes in Artificial Intelligence (LNAI).

Most parts 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 for more information or if you have problems downloading a paper.

• 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, pp. 38-53. © Springer Verlag, 2010.

    · security_festschrift10.pdf (327 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.
  
  

• 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)
  
  

• 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)
  
  

• 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 Non-Clausal Connection Calculus.
  Jens Otten.
  In K. Brünnler and G. Metcalfe, editor, 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)
  
  

• 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)
  
  

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

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

• 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 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)
  
  

• 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)
  
  

• 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)
  
  

• 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)
  
  

• 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)
  
  

• A Non-Clausal Davis-Putnam Proof Procedure.
  Jens Otten.
  In 15th International Joint Conference on Artificial Intelligence (Poster Session Abstracts), 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.
  
  

• Ein konnektionenorientiertes Beweisverfahren für intuitionistische Logik.
  Jens Otten.
  Master Thesis, Technische Hochschule Darmstadt, Intellektik, 1995.

    · intu_diplom.pdf (683 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.