| 2022 | CADE | Advancing Automated Theorem Proving for the Modal Logics D and S5. | Jens Otten |
| 2021 | TABLEAUX | The nanoCoP 2.0 Connection Provers for Classical, Intuitionistic and Modal Logics. | Jens Otten |
| 2020 | CADE | Equality Preprocessing in Connection Calculi. | Benjamin E. Oliver, Jens Otten |
| 2018 | CADE | Proof Search Optimizations for Non-Clausal Connection Calculi. | Jens Otten |
| 2017 | IJCAI | nanoCoP: Natural Non-clausal Theorem Proving. | Jens Otten |
| 2017 | LPAR | RACCOON: A Connection Reasoner for the Description Logic ALC. | Dimas Melo Filho, Fred Freitas, Jens Otten |
| 2017 | TABLEAUX | Non-clausal Connection Calculi for Non-classical Logics. | Jens Otten |
| 2016 | AI | A Connection Calculus for the Description Logic | Fred Freitas, Jens Otten |
| 2016 | CADE | nanoCoP: A Non-clausal Connection Prover. | Jens Otten |
| 2016 | CADE | Non-clausal Connection-based Theorem Proving in Intuitionistic First-Order Logic. | Jens Otten |
| 2014 | CADE | MleanCoP: A Connection Prover for First-Order Modal Logic. | Jens Otten |
| 2014 | CADE | Problem Libraries for Non-Classical Logics. | Jens Otten, Thomas Raths |
| 2012 | CADE | Implementing Different Proof Calculi for First-order Modal Logics. | Christoph Benzmller, Jens Otten, Thomas Raths |
| 2012 | CADE | The QMLTP Problem Library for First-Order Modal Logics. | Thomas Raths, Jens Otten |
| 2012 | ECAI | Implementing and Evaluating Provers for First-order Modal Logics. | Christoph Benzmller, Jens Otten, Thomas Raths |
| 2012 | LPAR | Implementing Connection Calculi for First-order Modal Logics. | Jens Otten |
| 2011 | TABLEAUX | A Non-clausal Connection Calculus. | Jens Otten |
| 2011 | TABLEAUX | Implementing and Evaluating Theorem Provers for First-Order Modal Logics. | Thomas Raths, Jens Otten |
| 2008 | CADE | leanCoP 2.0and ileanCoP 1.2: High Performance Lean Theorem Proving in Classical and Intuitionistic Logic (System Descriptions). | Jens Otten |
| 2008 | CADE | randoCoP: Randomizing the Proof Search Order in the Connection Calculus. | Thomas Raths, Jens Otten |
| 2005 | TABLEAUX | Clausal Connection-Based Theorem Proving in Intuitionistic First-Order Logic. | Jens Otten |
| 2005 | TABLEAUX | The ILTP Library: Benchmarking Automated Theorem Provers for Intuitionistic Logic. | Thomas Raths, Jens Otten, Christoph Kreitz |
| 1999 | TABLEAUX | linTAP: A Tableau Prover for Linear Logic. | Heiko Mantel, Jens Otten |
| 1997 | CADE | Connection-Based Proof Construction in Linear Logic. | Christoph Kreitz, Heiko Mantel, Jens Otten, Stephan Schmitt |
| 1997 | LOPSTR | A Multi-level Approach to Program Synthesis. | Wolfgang Bibel, Daniel S. Korn, Christoph Kreitz, F. Kurucz, Jens Otten, Stephen Schmitt, G. Stolpmann |
| 1997 | TABLEAUX | ileanTAP: An Intuitionistic Theorem Prover. | Jens Otten |
| 1996 | KI | A Uniform Proof Procedure for Classical and Non-Classical Logics. | Jens Otten, Christoph Kreitz |
| 1996 | TABLEAUX | T-String Unification: Unifying Prefixes in Non-classical Proof Methods. | Jens Otten, Christoph Kreitz |
| 1995 | LOPSTR | Guiding Program Development Systems by a Connection Based Proof Strategy. | Christoph Kreitz, Jens Otten, Stephan Schmitt |
| 1995 | TABLEAUX | A Connection Based Proof Method for Intuitionistic Logic. | Jens Otten |