Autodescriptivity: Beware! - Chris Brink; Ingrid Rewitzky; Renate A. Schmidt (Comput. J., 1991)

Terminological Representation, Natural Language & Relation Algebra. - Renate A. Schmidt (GWAI, 1992)

Editorial: The Possibility of Generating True Conjectures. - Hans Jürgen Ohlbach; Renate A. Schmidt (J. Log. Comput., 1993)

Peirce Algebras. - Chris Brink; Katarina Britz; Renate A. Schmidt (Formal Aspects Comput., 1994)

Resolution is a Decision Procedure for Many Propositional Modal Logics. - Renate A. Schmidt (Advances in Modal Logic, 1996)

On Evaluating Decision Procedures for Modal Logic. - Ullrich Hustadt; Renate A. Schmidt (IJCAI (1), 1997)

Functional Translation and Second-Order Frame Properties of Modal Logics. - Hans Jürgen Ohlbach; Renate A. Schmidt (J. Log. Comput., 1997)

Optimised modal translation and resolution. - Renate A. Schmidt (1997)

Decidability by unrefined resolution for propositional modal logics. - Renate A. Schmidt (RelMiCS, 1998)

A Resolution-Based Decision Procedure for Extensions of K4. - Harald Ganzinger; Ullrich Hustadt; Christoph Meyer 001; Renate A. Schmidt (Advances in Modal Logic, 1998)

Issues of Decidability for Description Logics in the Framework of Resolution. - Ullrich Hustadt; Renate A. Schmidt (FTP (LNCS Selection), 1998)

E-Unification for Subsystems of S4. - Renate A. Schmidt (RTA, 1998)

Simplification and Backjumping in Modal Tableau. - Ullrich Hustadt; Renate A. Schmidt (TABLEAUX, 1998)

Maslov's Class K Revisited. - Ullrich Hustadt; Renate A. Schmidt (CADE, 1999)

MSPASS: Subsumption Testing with SPASS. - Ullrich Hustadt; Renate A. Schmidt; Christoph Weidenbach (Description Logics, 1999)

On the Relation of Resolution and Tableaux Proof Systems for Description Logics. - Ullrich Hustadt; Renate A. Schmidt (IJCAI, 1999)

An empirical analysis of modal theorem provers. - Ullrich Hustadt; Renate A. Schmidt (J. Appl. Non Class. Logics, 1999)

Decidability by Resolution for Propositional Modal Logics. - Renate A. Schmidt (J. Autom. Reason., 1999)

Deciding Fluted Logic with Resolution. - Renate A. Schmidt (ARW, 2000)

A Resolution Decision Procedure for Fluted Logic. - Renate A. Schmidt; Ullrich Hustadt (CADE, 2000)

Verification within the KARO Agent Theory. - Ullrich Hustadt; Clare Dixon; Renate A. Schmidt; Michael Fisher 001; John-Jules Ch. Meyer; Wiebe van der Hoek (FAABS, 2000)

Normal Forms and Proofs in Combined Modal and Temporal Logics. - Ullrich Hustadt; Clare Dixon; Renate A. Schmidt; Michael Fisher 001 (FroCoS, 2000)

MSPASS: Modal Reasoning by Translation and First-Order Resolution. - Ullrich Hustadt; Renate A. Schmidt (TABLEAUX, 2000)

Resolution-Based Methods for Modal Logics. - Ullrich Hustadt; Hans de Nivelle; Renate A. Schmidt (Log. J. IGPL, 2000)

Computational Space Efficiency and Minimal Model Generation for Guarded Formulae. - Lilia Georgieva; Ullrich Hustadt; Renate A. Schmidt (LPAR, 2001)

Reasoning about agents in the KARO framework. - Ullrich Hustadt; Clare Dixon; Renate A. Schmidt; Michael Fisher 001; John-Jules Ch. Meyer; Wiebe van der Hoek (TIME, 2001)

Combining Dynamic Logic with Doxastic Modal Logics. - Renate A. Schmidt; Dmitry Tishkovsky (Advances in Modal Logic, 2002)

A New Clausal Class Decidable by Hyperresolution. - Lilia Georgieva; Ullrich Hustadt; Renate A. Schmidt (CADE, 2002)

On the relationship between decidable fragments, non-classical logics, and description logics. - Lilia Georgieva; Ullrich Hustadt; Renate A. Schmidt (Description Logics, 2002)

Multi-agent Logics of Dynamic Belief and Knowledge. - Renate A. Schmidt; Dmitry Tishkovsky (JELIA, 2002)

Scientific Benchmarking with Temporal Logic Decision Procedures. - Ullrich Hustadt; Renate A. Schmidt (KR, 2002)

Using Resolution for Testing Modal Satisfiability and Building Models. - Ullrich Hustadt; Renate A. Schmidt (J. Autom. Reason., 2002)

SCAN Is Complete for All Sahlqvist Formulae. - Valentin Goranko; Ullrich Hustadt; Renate A. Schmidt; Dimiter Vakarelov (RelMiCS, 2003)

Mechanised Reasoning and Model Generation for Extended Modal Logics. - Renate A. Schmidt; Ullrich Hustadt (Theory and Applications of Relational Structures as Knowledge Instruments, 2003)

Two Proof Systems for Peirce Algebras. - Renate A. Schmidt; Ewa Orlowska; Ullrich Hustadt (RelMiCS, 2003)

A Principle for Incorporating Axioms into the First-Order Translation of Modal Formulae. - Renate A. Schmidt; Ullrich Hustadt (CADE, 2003)

Hyperresolution for guarded formulae. - Lilia Georgieva; Ullrich Hustadt; Renate A. Schmidt (J. Symb. Comput., 2003)

Multi-Agent Dynamic Logics with Informational Test. - Renate A. Schmidt; Dmitry Tishkovsky (Ann. Math. Artif. Intell., 2004)

Interactions between Knowledge, Action and Commitment within Agent Dynamic Logic. - Renate A. Schmidt; Dmitry Tishkovsky; Ullrich Hustadt (Stud Logica, 2004)

Deciding Monodic Fragments by Temporal Resolution. - Ullrich Hustadt; Boris Konev; Renate A. Schmidt (CADE, 2005)

Investigating Finite Models of Non-classical Logics with Relation Algebra and RelView. - Rudolf Berghammer; Renate A. Schmidt (Theory and Applications of Relational Structures as Knowledge Instruments, 2006)

Developing Modal Tableaux and Resolution Methods via First-Order Resolution. - Renate A. Schmidt (Advances in Modal Logic, 2006)

Computational modal logic. - Ian Horrocks 001; Ullrich Hustadt; Ulrike Sattler; Renate A. Schmidt (Handbook of Modal Logic, 2007)

System Description: SpassVersion 3.0. - Christoph Weidenbach; Renate A. Schmidt; Thomas Hillenbrand; Rostislav Rusev; Dalibor Topic (CADE, 2007)

Deciding ALBO with Tableau. - Renate A. Schmidt; Dmitry Tishkovsky (Description Logics, 2007)

Using Tableau to Decide Expressive Description Logics with Role Negation. - Renate A. Schmidt; Dmitry Tishkovsky (ISWC/ASWC, 2007)

The axiomatic translation principle for modal logic. - Renate A. Schmidt; Ullrich Hustadt (ACM Trans. Comput. Log., 2007)

Second-Order Quantifier Elimination - Foundations, Computational Aspects and Applications. - Dov M. Gabbay; Renate A. Schmidt; Andrzej Szalas (College Publications, 2008)

A General Tableau Method for Deciding Description Logics, Modal Logics and Related First-Order Fragments. - Renate A. Schmidt; Dmitry Tishkovsky (IJCAR, 2008)

Improved Second-Order Quantifier Elimination in Modal Logic. - Renate A. Schmidt (JELIA, 2008)

Relations and Kleene Algebras in Computer Science. - Renate A. Schmidt; Georg Struth (J. Log. Algebraic Methods Program., 2008)

On combinations of propositional dynamic logic and doxastic modal logics. - Renate A. Schmidt; Dmitry Tishkovsky (J. Log. Lang. Inf., 2008)

A new methodology for developing deduction methods. - Renate A. Schmidt (Ann. Math. Artif. Intell., 2009)

A Tableau Method for Checking Rule Admissibility in S4. - Sergey Babenyshev; Vladimir V. Rybakov; Renate A. Schmidt; Dmitry Tishkovsky (M4M, 2009)

Simulation and Synthesis of Deduction Calculi. - Renate A. Schmidt (M4M, 2009)

Empirically successful computerized reasoning. - Renate A. Schmidt; Geoff Sutcliffe; Stephan Schulz 001 (J. Appl. Log., 2009)

A Comparison of Solvers for Propositional Dynamic Logic. - Ullrich Hustadt; Renate A. Schmidt (PAAR@IJCAR, 2010)

Special issue on practical aspects of automated reasoning. - Boris Konev; Renate A. Schmidt; Stephan Schulz 001 (AI Commun., 2010)

Synthesising Terminating Tableau Calculi for Relational Logics - (Invited Paper). - Renate A. Schmidt (RAMiCS, 2011)

METTEL textsc{Met hspace{-.5pt}TeL}: A Tableau Prover with Logic-Independent Inference Engine. - Dmitry Tishkovsky; Renate A. Schmidt; Mohammad Khodadadi (TABLEAUX, 2011)

Automated Synthesis of Tableau Calculi - Renate A. Schmidt; Dmitry Tishkovsky (Log. Methods Comput. Sci., 2011)

A Tableau Calculus for Minimal Modal Model Generation. - Fabio Papacchini; Renate A. Schmidt (M4M/LAMAS, 2011)

Preface: Special Issue of Selected Extended Papers of CADE-22. - Renate A. Schmidt; Brigitte Pientka (J. Autom. Reason., 2011)

Synthesising and Implementing Tableau Calculi for Interrogative Epistemic Logics. - Stefan Minica; Mohammad Khodadadi; Renate A. Schmidt; Dmitry Tishkovsky (PAAR@IJCAR, 2012)

MetTeL2: Towards a Tableau Prover Generation Platform. - Dmitry Tishkovsky; Renate A. Schmidt; Mohammad Khodadadi (PAAR@IJCAR, 2012)

An Abstract Tableau Calculus for the Description Logic SHOI Using Unrestricted Blocking and Rewriting. - Mohammad Khodadadi; Renate A. Schmidt; Dmitry Tishkovsky (Description Logics, 2012)

The Tableau Prover Generator MetTeL2. - Dmitry Tishkovsky; Renate A. Schmidt; Mohammad Khodadadi (JELIA, 2012)

Labelled Tableaux for Temporal Logic with Cardinality Constraints. - Clare Dixon; Boris Konev; Renate A. Schmidt; Dmitry Tishkovsky (SYNASC, 2012)

The Ackermann approach for modal logic, correspondence theory and second-order reduction. - Renate A. Schmidt (J. Appl. Log., 2012)

First-Order Resolution Methods for Modal Logics. - Renate A. Schmidt; Ullrich Hustadt (Programming Logics, 2013)

A Refined Tableau Calculus with Controlled Blocking for the Description Logic SHOI. - Mohammad Khodadadi; Renate A. Schmidt; Dmitry Tishkovsky (Description Logics, 2013)

Uniform Interpolation of -Ontologies Using Fixpoints. - Patrick Koopmann; Renate A. Schmidt (FroCos, 2013)

Computing Minimal Models Modulo Subset-Simulation for Modal Logics. - Fabio Papacchini; Renate A. Schmidt (FroCos, 2013)

Forgetting Concept and Role Symbols in $ mathcal{ALCH}$ -Ontologies. - Patrick Koopmann; Renate A. Schmidt (LPAR, 2013)

A Refined Tableau Calculus with Controlled Blocking for the Description Logic. - Mohammad Khodadadi; Renate A. Schmidt; Dmitry Tishkovsky (TABLEAUX, 2013)

Implementation and Evaluation of Forgetting in ALC-Ontologies. - Patrick Koopmann; Renate A. Schmidt (WoMO, 2013)

Refinement in the Tableau Synthesis Framework - Dmitry Tishkovsky; Renate A. Schmidt (CoRR, 2013)

Satisfiability problem for modal logic with global counting operators coded in binary is NExpTime-complete. - Michal Zawidzki; Renate A. Schmidt; Dmitry Tishkovsky (Inf. Process. Lett., 2013)

Tableau Development for a Bi-intuitionistic Tense Logic. - John G. Stell; Renate A. Schmidt; David E. Rydeheard (RAMiCS, 2014)

Axiomatic and Tableau-Based Reasoning for Kt(H, R). - Renate A. Schmidt; John G. Stell; David E. Rydeheard (Advances in Modal Logic, 2014)

Count and Forget: Uniform Interpolation of $ mathcal{SHQ}$ -Ontologies. - Patrick Koopmann; Renate A. Schmidt (IJCAR, 2014)

Terminating Minimal Model Generation Procedures for Propositional Modal Logics. - Fabio Papacchini; Renate A. Schmidt (IJCAR, 2014)

Forgetting and Uniform Interpolation for ALC-Ontologies with ABoxes. - Patrick Koopmann; Renate A. Schmidt (Description Logics, 2014)

Using tableau to decide description logics with full role negation and identity. - Renate A. Schmidt; Dmitry Tishkovsky (ACM Trans. Comput. Log., 2014)

Uniform Interpolation and Forgetting for ALC Ontologies with ABoxes. - Patrick Koopmann; Renate A. Schmidt (AAAI, 2015)

Saturated-Based Forgetting in the Description Logic SIF. - Patrick Koopmann; Renate A. Schmidt (Description Logics, 2015)

Concept Forgetting for ALCOI-Ontologies using an Ackermann Approach. - Yizheng Zhao; Renate A. Schmidt (Description Logics, 2015)

LETHE: Saturation-Based Reasoning for Non-Standard Reasoning Tasks. - Patrick Koopmann; Renate A. Schmidt (ORE, 2015)

Concept Forgetting in ALCOI -Ontologies Using an Ackermann Approach. - Yizheng Zhao; Renate A. Schmidt (ISWC (1), 2015)

Modal Tableau Systems with Blocking and Congruence Closure. - Renate A. Schmidt; Uwe Waldmann (TABLEAUX, 2015)

Forgetting Concept and Role Symbols in ALCOIH mu+( top, sqcap)-Ontologies. - Yizheng Zhao; Renate A. Schmidt (Description Logics, 2016)

Forgetting Concept and Role Symbols in ALCOIHµ+(∇, ⊓)-Ontologies. - Yizheng Zhao; Renate A. Schmidt (IJCAI, 2016)

Lifting QBF Resolution Calculi to DQBF. - Olaf Beyersdorff; Leroy Chew; Renate A. Schmidt; Martin Suda 001 (Electron. Colloquium Comput. Complex., 2016)

A bi-intuitionistic modal logic: Foundations and automation. - John G. Stell; Renate A. Schmidt; David E. Rydeheard (J. Log. Algebraic Methods Program., 2016)

Role Forgetting for ALCOQH(universal role)-Ontologies Using an Ackermann-Based Approach. - Yizheng Zhao; Renate A. Schmidt (IJCAI, 2017)

A Preliminary Comparison of the Forgetting Solutions Computed using SCAN, LETHE and FAME. - Ruba Alassaf; Renate A. Schmidt (SOQE, 2017)

Forgetting-Based Abduction in ALC. - Warren Del-Pinto; Renate A. Schmidt (SOQE, 2017)

Rule Refinement for Semantic Tableau Calculi. - Dmitry Tishkovsky; Renate A. Schmidt (TABLEAUX, 2017)

FAME: An Automated Tool for Semantic Forgetting in Expressive Description Logics. - Yizheng Zhao; Renate A. Schmidt (IJCAR, 2018)

The FAME Family: A Family of Reasoning Tools for Forgetting in Expressive Description Logics. - Yizheng Zhao; Hao Feng; Ruba Alassaf; Warren Del-Pinto; Renate A. Schmidt (Description Logics, 2018)

On Concept Forgetting in Description Logics with Qualified Number Restrictions. - Yizheng Zhao; Renate A. Schmidt (IJCAI, 2018)

Methods and Metrics for Knowledge Base Engineering and Integration. - Giorgos Stoilos; David Geleta; Szymon Wartak; Sheldon Hall; Mohammad Khodadadi; Yizheng Zhao; Ghadah Alghamdi; Renate A. Schmidt (WOP@ISWC, 2018)

ABox Abduction via Forgetting in ALC (Long Version). - Warren Del-Pinto; Renate A. Schmidt (CoRR, 2018)

ABox Abduction via Forgetting in ALC. - Warren Del-Pinto; Renate A. Schmidt (AAAI, 2019)

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 (AAAI, 2019)

Automating Automated Reasoning - The Case of Two Generic Automated Reasoning Tools. - Yoni Zohar; Dmitry Tishkovsky; Renate A. Schmidt; Anna Zamansky (Description Logic, Theory Combination, and All That, 2019)

FAME(Q): An Automated Tool for Forgetting in Description Logics with Qualified Number Restrictions. - Yizheng Zhao; Renate A. Schmidt (CADE, 2019)

Modularity Meets Forgetting: A Case Study with the SNOMED CT Ontology. - Jieying Chen 001; Ghadah Alghamdi; Renate A. Schmidt; Dirk Walther 002; Yongsheng Gao 005 (Description Logics, 2019)

Tracking Logical Difference in Industrial-Scale Ontologies. - Yizheng Zhao; Ghadah Alghamdi; Renate A. Schmidt; Hao Feng; Giorgos Stoilos; Damir Juric; Mohammad Khodadadi (Description Logics, 2019)

Extending Forgetting-Based Abduction Using Nominals. - Warren Del-Pinto; Renate A. Schmidt (FroCos, 2019)

DLS-Forgetter: An Implementation of the DLS Forgetting Calculus for First-Order Logic. - Ruba Alassaf; Renate A. Schmidt (GCAI, 2019)

Ontology Extraction for Large Ontologies via Modularity and Forgetting. - Jieying Chen 001; Ghadah Alghamdi; Renate A. Schmidt; Dirk Walther 002; Yongsheng Gao 005 (K-CAP, 2019)

Deduction Beyond Satisfiability (Dagstuhl Seminar 19371). - Carsten Fuhs; Philipp Rümmer; Renate A. Schmidt; Cesare Tinelli (Dagstuhl Reports, 2019)

Reinterpreting Dependency Schemes: Soundness Meets Incompleteness in DQBF. - Olaf Beyersdorff; Joshua Blinkhorn; Leroy Chew; Renate A. Schmidt; Martin Suda 001 (J. Autom. Reason., 2019)

A Practical Approach to Forgetting in Description Logics with Nominals. - Yizheng Zhao; Renate A. Schmidt; Yuejie Wang; Xuanming Zhang; Hao Feng (AAAI, 2020)

Deciding the Loosely Guarded Fragment and Querying Its Horn Fragment Using Resolution. - Sen Zheng 001; Renate A. Schmidt (AAAI, 2020)

Querying the Guarded Fragment via Resolution (Extended Abstract). - Sen Zheng 001; Renate A. Schmidt (PAAR+SC²@IJCAR, 2020)

Protege-TS: An OWL Ontology Term Selection Tool. - Ian Hyland; Renate A. Schmidt (Description Logics, 2020)

UI-FAME: A Deductive Forgetting Tool for Creating Views of ALC-TBoxes. - Xuan Wu; Chang Lu; Yizheng Zhao; Renate A. Schmidt; Hao Feng (Description Logics, 2020)

Signature-Based Abduction for Expressive Description Logics. - Patrick Koopmann; Warren Del-Pinto; Sophie Tourret; Renate A. Schmidt (KR, 2020)

Querying Guarded Fragments via Resolution. - Sen Zheng 001; Renate A. Schmidt (CoRR, 2020)

Signature-Based Abduction for Expressive Description Logics - Technical Report. - Patrick Koopmann; Warren Del-Pinto; Sophie Tourret; Renate A. Schmidt (CoRR, 2020)

Blocking and Other Enhancements for Bottom-Up Model Generation Methods. - Peter Baumgartner 001; Renate A. Schmidt (J. Autom. Reason., 2020)

Tracking Semantic Evolutionary Changes in Large-Scale Ontological Knowledge Bases. - Zhao Liu; Chang Lu; Ghadah Alghamdi; Renate A. Schmidt; Yizheng Zhao (CIKM, 2021)

Concept Description and Definition Extraction for the ANEMONE System. - David Toluhi; Renate A. Schmidt; Bijan Parsia (EMAS@AAMAS, 2021)

Semantic Forgetting in Expressive Description Logics. - Mostafa Sakr; Renate A. Schmidt (FroCoS, 2021)

Upwardly Abstracted Definition-Based Subontologies. - Ghadah Alghamdi; Renate A. Schmidt; Warren Del-Pinto; Yongsheng Gao 005 (K-CAP, 2021)

Resolution-Based Uniform Interpolation for Multi-Agent Modal Logic Kn. - Ruba Alassaf; Renate A. Schmidt; Uli Sattler (SOQE@KR, 2021)

Integrated Deduction (Dagstuhl Seminar 21371). - Maria Paola Bonacina; Philipp Rümmer; Renate A. Schmidt (Dagstuhl Reports, 2021)

Saturation-Based Uniform Interpolation for Multi-Modal Logics. - Ruba Alassaf; Renate A. Schmidt; Uli Sattler (AiML, 2022)

Advances and Challenges in the Development and Application of Forgetting Tools (invited talk abstract). - Renate A. Schmidt (ARQNL@IJCAR, 2022)

Fine-Grained Forgetting for the Description Logic ALC. - Mostafa Sakr; Renate A. Schmidt (Description Logics, 2022)

Knowledge Extraction Based on Forgetting and Subontology Generation (DL Invited Talk Abstract). - Renate A. Schmidt (Description Logics, 2022)

Extracting Subontologies from SNOMED CT. - Warren Del-Pinto; Renate A. Schmidt; Yongsheng Gao 005 (ESWC (Satellite Events), 2022)

Focus Set Semantic Differences. - Ghadah Abdulrahman S. Alghamdi; Renate A. Schmidt; Yongsheng Gao 005 (K-CAP, 2023)

International Patient Summary Terminology. - Warren Del-Pinto; Renate A. Schmidt; Yongsheng Gao 005; Ghadah Alghamdi; Alejandro Lopez Osornio; Suzy Roy (MedInfo, 2023)

Saturation-Based Boolean Conjunctive Query Answering and Rewriting for the Guarded Quantification Fragments. - Sen Zheng 001; Renate A. Schmidt (J. Autom. Reason., 2023)

Computing Witnesses Using the SCAN Algorithm. - Fabian Achammer; Stefan Hetzl; Renate A. Schmidt (CADE, 2025)

Uniform Interpolation and Forgetting for Large-Scale Ontologies with Application to Semantic Difference in SNOMED CT. - Yizheng Zhao; Junyi Zhang; Renate A. Schmidt (CADE, 2025)

Computing Witnesses Using the SCAN Algorithm (Extended Preprint). - Fabian Achammer; Stefan Hetzl; Renate A. Schmidt (CoRR, 2025)