| 2026 | KR | Do Transformers Learn What Theory Predicts? Knowledge Representation-Guided Mechanistic Verification via Causal Abstraction. | Chang Lu, Renate A. Schmidt, Yizheng Zhao |
| 2025 | CADE | Computing Witnesses Using the SCAN Algorithm. | Fabian Achammer, Stefan Hetzl, Renate A. Schmidt |
| 2025 | CADE | Uniform Interpolation and Forgetting for Large-Scale Ontologies with Application to Semantic Difference in SNOMED CT. | Yizheng Zhao, Junyi Zhang, Renate A. Schmidt |
| 2025 | CIKM | OntoLDiff: A Highly Efficient System for Tracking Logical Difference in Large-Scale Ontologies. | Yizheng Zhao, Renate A. Schmidt |
| 2025 | TABLEAUX | Refined Tableau Systems for Some Modal Logics of Confluence. | Kiana Samadpour Motalebi, Renate A. Schmidt, Cludia Nalon |
| 2022 | AiML | Saturation-Based Uniform Interpolation for Multi-Modal Logics. | Ruba Alassaf, Renate A. Schmidt, Uli Sattler |
| 2022 | CADE | Advances and Challenges in the Development and Application of Forgetting Tools (invited talk abstract). | Renate A. Schmidt |
| 2021 | CIKM | Tracking Semantic Evolutionary Changes in Large-Scale Ontological Knowledge Bases. | Zhao Liu, Chang Lu, Ghadah Alghamdi, Renate A. Schmidt, Yizheng Zhao |
| 2021 | EMAS | Concept Description and Definition Extraction for the ANEMONE System. | David Toluhi, Renate A. Schmidt, Bijan Parsia |
| 2021 | KR | Resolution-Based Uniform Interpolation for Multi-Agent Modal Logic K | Ruba Alassaf, Renate A. Schmidt, Uli Sattler |
| 2020 | AAAI | A Practical Approach to Forgetting in Description Logics with Nominals. | Yizheng Zhao, Renate A. Schmidt, Yuejie Wang, Xuanming Zhang, Hao Feng |
| 2020 | AAAI | Deciding the Loosely Guarded Fragment and Querying Its Horn Fragment Using Resolution. | Sen Zheng, Renate A. Schmidt |
| 2020 | CADE | Querying the Guarded Fragment via Resolution (Extended Abstract). | Sen Zheng, Renate A. Schmidt |
| 2020 | KR | Signature-Based Abduction for Expressive Description Logics. | Patrick Koopmann, Warren Del-Pinto, Sophie Tourret, Renate A. Schmidt |
| 2019 | AAAI | ABox Abduction via Forgetting in ALC. | Warren Del-Pinto, Renate A. Schmidt |
| 2019 | AAAI | Tracking Logical Difference in Large-Scale Ontologies: A Forgetting-Based Approach. | Yizheng Zhao, Ghadah Alghamdi, Renate A. Schmidt, Hao Feng, Giorgos Stoilos, Damir Juric, Mohammad Khodadadi |
| 2019 | CADE | FAME(Q): An Automated Tool for Forgetting in Description Logics with Qualified Number Restrictions. | Yizheng Zhao, Renate A. Schmidt |
| 2018 | CADE | FAME: An Automated Tool for Semantic Forgetting in Expressive Description Logics. | Yizheng Zhao, Renate A. Schmidt |
| 2018 | IJCAI | On Concept Forgetting in Description Logics with Qualified Number Restrictions. | Yizheng Zhao, Renate A. Schmidt |
| 2017 | IJCAI | Role Forgetting for ALCOQH(universal role)-Ontologies Using an Ackermann-Based Approach. | Yizheng Zhao, Renate A. Schmidt |
| 2017 | TABLEAUX | Rule Refinement for Semantic Tableau Calculi. | Dmitry Tishkovsky, Renate A. Schmidt |
| 2016 | IJCAI | Forgetting Concept and Role Symbols in ALCOIH | Yizheng Zhao, Renate A. Schmidt |
| 2016 | SAT | Lifting QBF Resolution Calculi to DQBF. | Olaf Beyersdorff, Leroy Chew, Renate A. Schmidt, Martin Suda |
| 2015 | AAAI | Uniform Interpolation and Forgetting for ALC Ontologies with ABoxes. | Patrick Koopmann, Renate A. Schmidt |
| 2015 | TABLEAUX | Modal Tableau Systems with Blocking and Congruence Closure. | Renate A. Schmidt, Uwe Waldmann |
| 2014 | AiML | Axiomatic and Tableau-Based Reasoning for Kt(H, R). | Renate A. Schmidt, John G. Stell, David E. Rydeheard |
| 2014 | CADE | Count and Forget: Uniform Interpolation of $\mathcal{SHQ}$ -Ontologies. | Patrick Koopmann, Renate A. Schmidt |
| 2014 | CADE | Terminating Minimal Model Generation Procedures for Propositional Modal Logics. | Fabio Papacchini, Renate A. Schmidt |
| 2013 | LPAR | Forgetting Concept and Role Symbols in $\mathcal{ALCH}$ -Ontologies. | Patrick Koopmann, Renate A. Schmidt |
| 2013 | TABLEAUX | A Refined Tableau Calculus with Controlled Blocking for the Description Logic. | Mohammad Khodadadi, Renate A. Schmidt, Dmitry Tishkovsky |
| 2012 | CADE | Synthesising and Implementing Tableau Calculi for Interrogative Epistemic Logics. | Stefan Minica, Mohammad Khodadadi, Renate A. Schmidt, Dmitry Tishkovsky |
| 2012 | CADE | MetTeL | Dmitry Tishkovsky, Renate A. Schmidt, Mohammad Khodadadi |
| 2012 | JELIA | The Tableau Prover Generator MetTeL2. | Dmitry Tishkovsky, Renate A. Schmidt, Mohammad Khodadadi |
| 2012 | SYNASC | Labelled Tableaux for Temporal Logic with Cardinality Constraints. | Clare Dixon, Boris Konev, Renate A. Schmidt, Dmitry Tishkovsky |
| 2011 | TABLEAUX | METTEL\textsc{Met\hspace{-.5pt}TeL}: A Tableau Prover with Logic-Independent Inference Engine. | Dmitry Tishkovsky, Renate A. Schmidt, Mohammad Khodadadi |
| 2010 | CADE | A Comparison of Solvers for Propositional Dynamic Logic. | Ullrich Hustadt, Renate A. Schmidt |
| 2009 | TABLEAUX | Automated Synthesis of Tableau Calculi. | Renate A. Schmidt, Dmitry Tishkovsky |
| 2008 | CADE | A General Tableau Method for Deciding Description Logics, Modal Logics and Related First-Order Fragments. | Renate A. Schmidt, Dmitry Tishkovsky |
| 2008 | JELIA | Improved Second-Order Quantifier Elimination in Modal Logic. | Renate A. Schmidt |
| 2007 | CADE | System Description: SpassVersion 3.0. | Christoph Weidenbach, Renate A. Schmidt, Thomas Hillenbrand, Rostislav Rusev, Dalibor Topic |
| 2006 | AiML | Developing Modal Tableaux and Resolution Methods via First-Order Resolution. | Renate A. Schmidt |
| 2006 | CADE | Blocking and Other Enhancements for Bottom-Up Model Generation Methods. | Peter Baumgartner, Renate A. Schmidt |
| 2005 | CADE | Deciding Monodic Fragments by Temporal Resolution. | Ullrich Hustadt, Boris Konev, Renate A. Schmidt |
| 2003 | CADE | A Principle for Incorporating Axioms into the First-Order Translation of Modal Formulae. | Renate A. Schmidt, Ullrich Hustadt |
| 2002 | AiML | Combining Dynamic Logic with Doxastic Modal Logics. | Renate A. Schmidt, Dmitry Tishkovsky |
| 2002 | CADE | A New Clausal Class Decidable by Hyperresolution. | Lilia Georgieva, Ullrich Hustadt, Renate A. Schmidt |
| 2002 | JELIA | Multi-agent Logics of Dynamic Belief and Knowledge. | Renate A. Schmidt, Dmitry Tishkovsky |
| 2002 | KR | Scientific Benchmarking with Temporal Logic Decision Procedures. | Ullrich Hustadt, Renate A. Schmidt |
| 2001 | LPAR | Computational Space Efficiency and Minimal Model Generation for Guarded Formulae. | Lilia Georgieva, Ullrich Hustadt, Renate A. Schmidt |
| 2001 | TIME | Reasoning about agents in the KARO framework. | Ullrich Hustadt, Clare Dixon, Renate A. Schmidt, Michael Fisher, John-Jules Ch. Meyer, Wiebe van der Hoek |
| 2000 | CADE | A Resolution Decision Procedure for Fluted Logic. | Renate A. Schmidt, Ullrich Hustadt |
| 2000 | TABLEAUX | MSPASS: Modal Reasoning by Translation and First-Order Resolution. | Ullrich Hustadt, Renate A. Schmidt |
| 1999 | CADE | Maslov's Class K Revisited. | Ullrich Hustadt, Renate A. Schmidt |
| 1999 | IJCAI | On the Relation of Resolution and Tableaux Proof Systems for Description Logics. | Ullrich Hustadt, Renate A. Schmidt |
| 1998 | AiML | A Resolution-Based Decision Procedure for Extensions of K4. | Harald Ganzinger, Ullrich Hustadt, Christoph Meyer, Renate A. Schmidt |
| 1998 | TABLEAUX | Simplification and Backjumping in Modal Tableau. | Ullrich Hustadt, Renate A. Schmidt |
| 1997 | IJCAI | On Evaluating Decision Procedures for Modal Logic. | Ullrich Hustadt, Renate A. Schmidt |
| 1996 | AiML | Resolution is a Decision Procedure for Many Propositional Modal Logics. | Renate A. Schmidt |
| 1992 | KI | Terminological Representation, Natural Language & Relation Algebra. | Renate A. Schmidt |