Renate A. Schmidt

Uli Sattler

Proceedings of the Advances in Modal Logic, AiML 2022, Rennes, France, 2022

2021

Integrated Deduction (Dagstuhl Seminar 21371).

[BibT_eX]

[DOI]

Maria Paola Bonacina

Philipp Rümmer

Dagstuhl Reports, 2021

Resolution-Based Uniform Interpolation for Multi-Agent Modal Logic Kn.

[BibT_eX]

[DOI]

Uli Sattler

Proceedings of the Second Workshop on Second-Order Quantifier Elimination and Related Topics (SOQE 2021) associated with the 18th International Conference on Principles of Knowledge Representation and Reasoning (KR 2021), 2021

Upwardly Abstracted Definition-Based Subontologies.

[BibT_eX]

[DOI]

Proceedings of the K-CAP '21: Knowledge Capture Conference, 2021

Semantic Forgetting in Expressive Description Logics.

[BibT_eX]

[DOI]

Mostafa Sakr

Proceedings of the Frontiers of Combining Systems - 13th International Symposium, 2021

Concept Description and Definition Extraction for the ANEMONE System.

[BibT_eX]

[DOI]

David Toluhi

Bijan Parsia

Proceedings of the Engineering Multi-Agent Systems - 9th International Workshop, 2021

Tracking Semantic Evolutionary Changes in Large-Scale Ontological Knowledge Bases.

[BibT_eX]

[DOI]

Proceedings of the CIKM '21: The 30th ACM International Conference on Information and Knowledge Management, Virtual Event, Queensland, Australia, November 1, 2021

2020

Blocking and Other Enhancements for Bottom-Up Model Generation Methods.

[BibT_eX]

[DOI]

Peter Baumgartner

J. Autom. Reason., 2020

Signature-Based Abduction for Expressive Description Logics - Technical Report.

[BibT_eX]

[DOI]

CoRR, 2020

Querying Guarded Fragments via Resolution.

[BibT_eX]

[DOI]

Sen Zheng

CoRR, 2020

Signature-Based Abduction for Expressive Description Logics.

[BibT_eX]

[DOI]

Proceedings of the 17th International Conference on Principles of Knowledge Representation and Reasoning, 2020

UI-FAME: A Deductive Forgetting Tool for Creating Views of ALC-TBoxes.

[BibT_eX]

[DOI]

Proceedings of the 33rd International Workshop on Description Logics (DL 2020) co-located with the 17th International Conference on Principles of Knowledge Representation and Reasoning (KR 2020), 2020

Protege-TS: An OWL Ontology Term Selection Tool.

[BibT_eX]

[DOI]

Ian Hyland

Querying the Guarded Fragment via Resolution (Extended Abstract).

[BibT_eX]

[DOI]

Sen Zheng

Proceedings of the Joint Proceedings of the 7th Workshop on Practical Aspects of Automated Reasoning (PAAR) and the 5th Satisfiability Checking and Symbolic Computation Workshop (SC-Square) Workshop, 2020

Deciding the Loosely Guarded Fragment and Querying Its Horn Fragment Using Resolution.

[BibT_eX]

[DOI]

Sen Zheng

Proceedings of the Thirty-Fourth AAAI Conference on Artificial Intelligence, 2020

A Practical Approach to Forgetting in Description Logics with Nominals.

[BibT_eX]

[DOI]

Proceedings of the Thirty-Fourth AAAI Conference on Artificial Intelligence, 2020

2019

Reinterpreting Dependency Schemes: Soundness Meets Incompleteness in DQBF.

[BibT_eX]

[DOI]

J. Autom. Reason., 2019

Deduction Beyond Satisfiability (Dagstuhl Seminar 19371).

[BibT_eX]

[DOI]

Dagstuhl Reports, 2019

Ontology Extraction for Large Ontologies via Modularity and Forgetting.

[BibT_eX]

[DOI]

Proceedings of the 10th International Conference on Knowledge Capture, 2019

DLS-Forgetter: An Implementation of the DLS Forgetting Calculus for First-Order Logic.

[BibT_eX]

[DOI]

Proceedings of the GCAI 2019. Proceedings of the 5th Global Conference on Artificial Intelligence, 2019

Extending Forgetting-Based Abduction Using Nominals.

[BibT_eX]

[DOI]

Proceedings of the Frontiers of Combining Systems - 12th International Symposium, 2019

Tracking Logical Difference in Industrial-Scale Ontologies.

[BibT_eX]

[DOI]

Proceedings of the 32nd International Workshop on Description Logics, 2019

Modularity Meets Forgetting: A Case Study with the SNOMED CT Ontology.

[BibT_eX]

[DOI]

Proceedings of the 32nd International Workshop on Description Logics, 2019

FAME(Q): An Automated Tool for Forgetting in Description Logics with Qualified Number Restrictions.

[BibT_eX]

[DOI]

Proceedings of the Automated Deduction - CADE 27, 2019

Automating Automated Reasoning - The Case of Two Generic Automated Reasoning Tools.

[BibT_eX]

[DOI]

Proceedings of the Description Logic, Theory Combination, and All That, 2019

Tracking Logical Difference in Large-Scale Ontologies: A Forgetting-Based Approach.

[BibT_eX]

[DOI]

Proceedings of the Thirty-Third AAAI Conference on Artificial Intelligence, 2019

ABox Abduction via Forgetting in ALC.

[BibT_eX]

[DOI]

Proceedings of the Thirty-Third AAAI Conference on Artificial Intelligence, 2019

2018

ABox Abduction via Forgetting in ALC (Long Version).

[BibT_eX]

[DOI]

CoRR, 2018

Methods and Metrics for Knowledge Base Engineering and Integration.

[BibT_eX]

[DOI]

Proceedings of the 9th Workshop on Ontology Design and Patterns (WOP 2018) co-located with 17th International Semantic Web Conference (ISWC 2018), 2018

On Concept Forgetting in Description Logics with Qualified Number Restrictions.

[BibT_eX]

[DOI]

Proceedings of the Twenty-Seventh International Joint Conference on Artificial Intelligence, 2018

The FAME Family: A Family of Reasoning Tools for Forgetting in Expressive Description Logics.

[BibT_eX]

[DOI]

Proceedings of the 31st International Workshop on Description Logics co-located with 16th International Conference on Principles of Knowledge Representation and Reasoning (KR 2018), Tempe, Arizona, US, October 27th - to, 2018

FAME: An Automated Tool for Semantic Forgetting in Expressive Description Logics.

[BibT_eX]

[DOI]

Proceedings of the Automated Reasoning - 9th International Joint Conference, 2018

2017

Rule Refinement for Semantic Tableau Calculi.

[BibT_eX]

[DOI]

Proceedings of the Automated Reasoning with Analytic Tableaux and Related Methods, 2017

Forgetting-Based Abduction in ALC.

[BibT_eX]

[DOI]

Proceedings of the Workshop on Second-Order Quantifier Elimination and Related Topics (SOQE 2017), 2017

A Preliminary Comparison of the Forgetting Solutions Computed using SCAN, LETHE and FAME.

[BibT_eX]

[DOI]

Proceedings of the Workshop on Second-Order Quantifier Elimination and Related Topics (SOQE 2017), 2017

Role Forgetting for ALCOQH(universal role)-Ontologies Using an Ackermann-Based Approach.

[BibT_eX]

[DOI]

Proceedings of the Twenty-Sixth International Joint Conference on Artificial Intelligence, 2017

2016

A bi-intuitionistic modal logic: Foundations and automation.

[BibT_eX]

[DOI]

John G. Stell

David E. Rydeheard

J. Log. Algebraic Methods Program., 2016

Lifting QBF Resolution Calculi to DQBF.

[BibT_eX]

[DOI]

Electron. Colloquium Comput. Complex., 2016

Forgetting Concept and Role Symbols in ALCOIHµ+(∇, ⊓)-Ontologies.

[BibT_eX]

[DOI]

Proceedings of the Twenty-Fifth International Joint Conference on Artificial Intelligence, 2016

Forgetting Concept and Role Symbols in ALCOIH\mu+(\top, \sqcap)-Ontologies.

[BibT_eX]

[DOI]

Proceedings of the 29th International Workshop on Description Logics, 2016

2015

Modal Tableau Systems with Blocking and Congruence Closure.

[BibT_eX]

[DOI]

Uwe Waldmann

Proceedings of the Automated Reasoning with Analytic Tableaux and Related Methods, 2015

Concept Forgetting in ALCOI -Ontologies Using an Ackermann Approach.

[BibT_eX]

[DOI]

Proceedings of the Semantic Web - ISWC 2015, 2015

LETHE: Saturation-Based Reasoning for Non-Standard Reasoning Tasks.

[BibT_eX]

[DOI]

Proceedings of the Informal Proceedings of the 4th International Workshop on OWL Reasoner Evaluation (ORE-2015) co-located with the 28th International Workshop on Description Logics (DL 2015), 2015

Concept Forgetting for ALCOI-Ontologies using an Ackermann Approach.

[BibT_eX]

[DOI]

Proceedings of the 28th International Workshop on Description Logics, 2015

Saturated-Based Forgetting in the Description Logic SIF.

[BibT_eX]

[DOI]

Proceedings of the 28th International Workshop on Description Logics, 2015

Uniform Interpolation and Forgetting for ALC Ontologies with ABoxes.

[BibT_eX]

[DOI]

Proceedings of the Twenty-Ninth AAAI Conference on Artificial Intelligence, 2015

2014

Using tableau to decide description logics with full role negation and identity.

[BibT_eX]

[DOI]

ACM Trans. Comput. Log., 2014

Forgetting and Uniform Interpolation for ALC-Ontologies with ABoxes.

[BibT_eX]

[DOI]

Proceedings of the Informal Proceedings of the 27th International Workshop on Description Logics, 2014

Terminating Minimal Model Generation Procedures for Propositional Modal Logics.

[BibT_eX]

[DOI]

Fabio Papacchini

Proceedings of the Automated Reasoning - 7th International Joint Conference, 2014

Count and Forget: Uniform Interpolation of $\mathcal{SHQ}$ -Ontologies.

[BibT_eX]

[DOI]

Proceedings of the Automated Reasoning - 7th International Joint Conference, 2014

Axiomatic and Tableau-Based Reasoning for Kt(H, R).

[BibT_eX]

[DOI]

John G. Stell

David E. Rydeheard

Proceedings of the Advances in Modal Logic 10, 2014

Tableau Development for a Bi-intuitionistic Tense Logic.

[BibT_eX]

[DOI]

John G. Stell

David E. Rydeheard

Proceedings of the Relational and Algebraic Methods in Computer Science, 2014

2013

Satisfiability problem for modal logic with global counting operators coded in binary is NExpTime-complete.

[BibT_eX]

[DOI]

Michal Zawidzki

Inf. Process. Lett., 2013

Refinement in the Tableau Synthesis Framework

[BibT_eX]

[DOI]

CoRR, 2013

Implementation and Evaluation of Forgetting in ALC-Ontologies.

[BibT_eX]

[DOI]

Proceedings of the 7th International Workshop on Modular Ontologies co-located with the 12th International Conference on Logic Programming and Non-monotonic Reasoning (LPNMR 2013), 2013

A Refined Tableau Calculus with Controlled Blocking for the Description Logic.

[BibT_eX]

[DOI]

Proceedings of the Automated Reasoning with Analytic Tableaux and Related Methods, 2013

Forgetting Concept and Role Symbols in $\mathcal{ALCH}$ -Ontologies.

[BibT_eX]

[DOI]

Proceedings of the Logic for Programming, Artificial Intelligence, and Reasoning, 2013

Computing Minimal Models Modulo Subset-Simulation for Modal Logics.

[BibT_eX]

[DOI]

Fabio Papacchini

Proceedings of the Frontiers of Combining Systems, 2013

Uniform Interpolation of -Ontologies Using Fixpoints.

[BibT_eX]

[DOI]

Proceedings of the Frontiers of Combining Systems, 2013

A Refined Tableau Calculus with Controlled Blocking for the Description Logic SHOI.

[BibT_eX]

[DOI]

Proceedings of the Informal Proceedings of the 26th International Workshop on Description Logics, Ulm, Germany, July 23, 2013

First-Order Resolution Methods for Modal Logics.

[BibT_eX]

[DOI]

Proceedings of the Programming Logics - Essays in Memory of Harald Ganzinger, 2013

2012

The Ackermann approach for modal logic, correspondence theory and second-order reduction.

[BibT_eX]

[DOI]

J. Appl. Log., 2012

Labelled Tableaux for Temporal Logic with Cardinality Constraints.

[BibT_eX]

[DOI]

Proceedings of the 14th International Symposium on Symbolic and Numeric Algorithms for Scientific Computing, 2012

The Tableau Prover Generator MetTeL2.

[BibT_eX]

[DOI]

Proceedings of the Logics in Artificial Intelligence - 13th European Conference, 2012

An Abstract Tableau Calculus for the Description Logic SHOI Using Unrestricted Blocking and Rewriting.

[BibT_eX]

[DOI]

Proceedings of the 2012 International Workshop on Description Logics, 2012

MetTeL2: Towards a Tableau Prover Generation Platform.

[BibT_eX]

[DOI]

Proceedings of the Third Workshop on Practical Aspects of Automated Reasoning, 2012

Synthesising and Implementing Tableau Calculi for Interrogative Epistemic Logics.

[BibT_eX]

[DOI]

Proceedings of the Third Workshop on Practical Aspects of Automated Reasoning, 2012

2011

Preface: Special Issue of Selected Extended Papers of CADE-22.

[BibT_eX]

[DOI]

Brigitte Pientka

J. Autom. Reason., 2011

A Tableau Calculus for Minimal Modal Model Generation.

[BibT_eX]

[DOI]

Fabio Papacchini

Proceedings of the 7th Workshop on Methods for Modalities, 2011

Automated Synthesis of Tableau Calculi

[BibT_eX]

[DOI]

Log. Methods Comput. Sci., 2011

METTEL\textsc{Met\hspace{-.5pt}TeL}: A Tableau Prover with Logic-Independent Inference Engine.

[BibT_eX]

[DOI]

Proceedings of the Automated Reasoning with Analytic Tableaux and Related Methods, 2011

Synthesising Terminating Tableau Calculi for Relational Logics - (Invited Paper).

[BibT_eX]

[DOI]

Proceedings of the Relational and Algebraic Methods in Computer Science, 2011

2010

Special issue on practical aspects of automated reasoning.

[BibT_eX]

[DOI]

Boris Konev

Stephan Schulz

AI Commun., 2010

A Comparison of Solvers for Propositional Dynamic Logic.

[BibT_eX]

[DOI]

Proceedings of the 2nd Workshop on Practical Aspects of Automated Reasoning, 2010

2009

Empirically successful computerized reasoning.

[BibT_eX]

[DOI]

Geoff Sutcliffe

Stephan Schulz

J. Appl. Log., 2009

Simulation and Synthesis of Deduction Calculi.

[BibT_eX]

[DOI]

Proceedings of the 6th Workshop on Methods for Modalities, 2009

A Tableau Method for Checking Rule Admissibility in S4.

[BibT_eX]

[DOI]

Proceedings of the 6th Workshop on Methods for Modalities, 2009

A new methodology for developing deduction methods.

[BibT_eX]

[DOI]

Ann. Math. Artif. Intell., 2009

2008

On combinations of propositional dynamic logic and doxastic modal logics.

[BibT_eX]

[DOI]

J. Log. Lang. Inf., 2008

Relations and Kleene Algebras in Computer Science.

[BibT_eX]

[DOI]

Georg Struth

J. Log. Algebraic Methods Program., 2008

Improved Second-Order Quantifier Elimination in Modal Logic.

[BibT_eX]

[DOI]

Proceedings of the Logics in Artificial Intelligence, 11th European Conference, 2008

A General Tableau Method for Deciding Description Logics, Modal Logics and Related First-Order Fragments.

[BibT_eX]

[DOI]

Proceedings of the Automated Reasoning, 4th International Joint Conference, 2008

Second-Order Quantifier Elimination - Foundations, Computational Aspects and Applications.

[BibT_eX]

[DOI]

Dov M. Gabbay

Andrzej Szalas

Studies in logic : Mathematical logic and foundations 12, College Publications, ISBN: 978-1-904987-56-7, 2008

2007

The axiomatic translation principle for modal logic.

[BibT_eX]

[DOI]

ACM Trans. Comput. Log., 2007

Using Tableau to Decide Expressive Description Logics with Role Negation.

[BibT_eX]

[DOI]

Proceedings of the Semantic Web, 2007

Deciding ALBO with Tableau.

[BibT_eX]

[DOI]

Proceedings of the 2007 International Workshop on Description Logics (DL2007), 2007

System Description: SpassVersion 3.0.

[BibT_eX]

[DOI]

Proceedings of the Automated Deduction, 2007

Computational modal logic.

[BibT_eX]

[DOI]

Proceedings of the Handbook of Modal Logic., 2007

2006

Developing Modal Tableaux and Resolution Methods via First-Order Resolution.

[BibT_eX]

[DOI]

Proceedings of the Advances in Modal Logic 6, 2006

Investigating Finite Models of Non-classical Logics with Relation Algebra and RelView.

[BibT_eX]

[DOI]

Rudolf Berghammer

Proceedings of the Theory and Applications of Relational Structures as Knowledge Instruments II, 2006

2005

Deciding Monodic Fragments by Temporal Resolution.

[BibT_eX]

[DOI]

Boris Konev

Proceedings of the Automated Deduction, 2005

2004

Interactions between Knowledge, Action and Commitment within Agent Dynamic Logic.

[BibT_eX]

[DOI]

Stud Logica, 2004

Multi-Agent Dynamic Logics with Informational Test.

[BibT_eX]

[DOI]

Ann. Math. Artif. Intell., 2004

2003

Hyperresolution for guarded formulae.

[BibT_eX]

[DOI]

J. Symb. Comput., 2003

A Principle for Incorporating Axioms into the First-Order Translation of Modal Formulae.

[BibT_eX]

[DOI]

Proceedings of the Automated Deduction - CADE-19, 19th International Conference on Automated Deduction Miami Beach, FL, USA, July 28, 2003

Two Proof Systems for Peirce Algebras.

[BibT_eX]

[DOI]

Ewa Orlowska

Proceedings of the Relational and Kleene-Algebraic Methods in Computer Science: 7th International Seminar on Relational Methods in Computer Science and 2nd International Workshop on Applications of Kleene Algebra, 2003

Mechanised Reasoning and Model Generation for Extended Modal Logics.

[BibT_eX]

[DOI]

Proceedings of the Theory and Applications of Relational Structures as Knowledge Instruments, 2003

SCAN Is Complete for All Sahlqvist Formulae.

[BibT_eX]

[DOI]

2002

Using Resolution for Testing Modal Satisfiability and Building Models.

[BibT_eX]

[DOI]

J. Autom. Reason., 2002

Scientific Benchmarking with Temporal Logic Decision Procedures.

[BibT_eX]

Proceedings of the Eights International Conference on Principles and Knowledge Representation and Reasoning (KR-02), 2002

Multi-agent Logics of Dynamic Belief and Knowledge.

[BibT_eX]

[DOI]

Proceedings of the Logics in Artificial Intelligence, European Conference, 2002

On the relationship between decidable fragments, non-classical logics, and description logics.

[BibT_eX]

[DOI]

Proceedings of the 2002 International Workshop on Description Logics (DL2002), 2002

A New Clausal Class Decidable by Hyperresolution.

[BibT_eX]

[DOI]

Proceedings of the Automated Deduction, 2002

Combining Dynamic Logic with Doxastic Modal Logics.

[BibT_eX]

[DOI]

Proceedings of the Advances in Modal Logic 4, papers from the fourth conference on "Advances in Modal logic," held in Toulouse, France, 30 September, 2002

2001

Reasoning about agents in the KARO framework.

[BibT_eX]

[DOI]

Proceedings of the Eigth International Symposium on Temporal Representation and Reasoning, 2001

Computational Space Efficiency and Minimal Model Generation for Guarded Formulae.

[BibT_eX]

[DOI]

Proceedings of the Logic for Programming, 2001

2000

Resolution-Based Methods for Modal Logics.

[BibT_eX]

[DOI]

Hans de Nivelle

Log. J. IGPL, 2000

MSPASS: Modal Reasoning by Translation and First-Order Resolution.

[BibT_eX]

[DOI]

Proceedings of the Automated Reasoning with Analytic Tableaux and Related Methods, 2000

Normal Forms and Proofs in Combined Modal and Temporal Logics.

[BibT_eX]

[DOI]

Proceedings of the Frontiers of Combining Systems, 2000

Verification within the KARO Agent Theory.

[BibT_eX]

[DOI]

Proceedings of the Formal Approaches to Agent-Based Systems, First International Workshop, 2000

A Resolution Decision Procedure for Fluted Logic.

[BibT_eX]

[DOI]

Proceedings of the Automated Deduction, 2000

Deciding Fluted Logic with Resolution.

[BibT_eX]

[DOI]

Proceedings of the Seventh Workshop on Automated Reasoning, 2000

1999

Decidability by Resolution for Propositional Modal Logics.

[BibT_eX]

[DOI]

J. Autom. Reason., 1999

An empirical analysis of modal theorem provers.

[BibT_eX]

[DOI]

J. Appl. Non Class. Logics, 1999

On the Relation of Resolution and Tableaux Proof Systems for Description Logics.

[BibT_eX]

[DOI]

Proceedings of the Sixteenth International Joint Conference on Artificial Intelligence, 1999

MSPASS: Subsumption Testing with SPASS.

[BibT_eX]

[DOI]

Christoph Weidenbach

Proceedings of the 1999 International Workshop on Description Logics (DL'99), Linköping, Sweden, July 30, 1999

Maslov's Class K Revisited.

[BibT_eX]

[DOI]

Proceedings of the Automated Deduction, 1999

1998

Simplification and Backjumping in Modal Tableau.

[BibT_eX]

[DOI]

Proceedings of the Automated Reasoning with Analytic Tableaux and Related Methods, 1998

E-Unification for Subsystems of S4.

[BibT_eX]

[DOI]

Proceedings of the Rewriting Techniques and Applications, 9th International Conference, 1998

Issues of Decidability for Description Logics in the Framework of Resolution.

[BibT_eX]

[DOI]

Proceedings of the Automated Deduction in Classical and Non-Classical Logics, 1998

A Resolution-Based Decision Procedure for Extensions of K4.

[BibT_eX]

Proceedings of the Advances in Modal Logic 2, 1998

Decidability by unrefined resolution for propositional modal logics.

[BibT_eX]

Proceedings of the Participants Copies for Relational Methods in Logic, 1998

1997

Optimised modal translation and resolution.

[BibT_eX]

[DOI]

PhD thesis, 1997

Functional Translation and Second-Order Frame Properties of Modal Logics.

[BibT_eX]

[DOI]

Hans Jürgen Ohlbach

J. Log. Comput., 1997

On Evaluating Decision Procedures for Modal Logic.

[BibT_eX]

[DOI]

Proceedings of the Fifteenth International Joint Conference on Artificial Intelligence, 1997

1996

Resolution is a Decision Procedure for Many Propositional Modal Logics.

[BibT_eX]

Proceedings of the Advances in Modal Logic 1, 1996

1994

Peirce Algebras.

[BibT_eX]

[DOI]

Chris Brink

Katarina Britz

Formal Aspects Comput., 1994

1993

Editorial: The Possibility of Generating True Conjectures.

[BibT_eX]

[DOI]

Hans Jürgen Ohlbach

J. Log. Comput., 1993

1992

Terminological Representation, Natural Language & Relation Algebra.

[BibT_eX]

[DOI]

Proceedings of the GWAI-92: Advances in Artificial Intelligence, 16th German Conference on Artificial Intelligence, Bonn, Germany, August 31, 1992

1991

Autodescriptivity: Beware!

[BibT_eX]

Chris Brink

Ingrid Rewitzky