Extending Consequence-Based Reasoning to SHIQ

Consequence-based calculi are a family of reasoning algorithms for description logics (DLs), and they combine hyper-tableau and resolution in a way that often achieves excellent performance in practice. Up to now, however, they were proposed for either Horn DLs (which do not support disjunction), or for DLs without counting quantifiers. In this paper we present a novel consequence-based calculus for SRIQ— a rich DL that supports both features. This extension is non-trivial since the intermediate consequences that need to be derived during reasoning cannot be captured using DLs themselves. The results of our preliminary performance evaluation suggest the feasibility of our approach in practice.

• Publication year

  2016

• Venue

  Description Logics

• Publication date

  2016-02-14

• Fields of study

  Computer Science

• Identifiers
  arXiv 1602.04498
• External record

  Open on Semantic Scholar

• Source metadata

  Semantic Scholar

• No claims are published for this paper.

• No concepts are published for this paper.

• HermiT: An OWL 2 Reasoner

  2014influential reference
• Coupling Tableau Algorithms for Expressive Description Logics with Completion-Based Saturation Procedures

  2014cited by this paper
• Konclude: System description

  2014influential reference
• Consequence-based and fixed-parameter tractable reasoning in description logics

  2014influential reference
• Consequence-Based Reasoning beyond Horn Ontologies

  2011cited by this paper
• Worst-Case Optimal Reasoning for the Horn-DL Fragments of OWL 1 and 2

  2010influential reference
• Hypertableau Reasoning for Description Logics

  2009cited by this paper
• Consequence-Driven Reasoning for Horn SHIQ Ontologies

  2009cited by this paper
• Deciding expressive description logics in the framework of resolution

  2008cited by this paper
• SRIQ and SROIQ are Harder than SHOIQ

  2008cited by this paper
• RIQ and SROIQ Are Harder than SHOIQ

  2008cited by this paper
• Pellet: A practical OWL-DL reasoner

  2007influential reference
• EXPTIME Tableaux with Global Caching for Description Logics with Transitive Roles, Inverse Roles and Role Hierarchies

  2007cited by this paper
• FaCT++ Description Logic Reasoner: System Description

  2006influential reference
• Pushing the EL Envelope

  2005influential reference
• A Principle for Incorporating Axioms into the First-Order Translation of Modal Formulae

  2003cited by this paper
• Deciding Regular Grammar Logics with Converse Through First-Order Logic

  2003cited by this paper
• The Description Logic Handbook: Theory, Implementation, and Applications

  2003cited by this paper
• The design and implementation of VAMPIRE

  2002cited by this paper
• E – a brainiac theorem prover

  2002cited by this paper
• RACER System Description

  2001cited by this paper
• Resolution Theorem Proving

  2001cited by this paper
• Handbook of Automated Reasoning: Volume 1

  2001cited by this paper
• Resolution-Based Methods for Modal Logics

  2000cited by this paper
• On the Relation of Resolution and Tableaux Proof Systems for Description Logics

  1999cited by this paper
• Term rewriting and all that

  1998influential reference
• Modal Languages and Bounded Fragments of Predicate Logic

  1998cited by this paper
• Two-variable logic with counting is decidable

  1997cited by this paper
• Hyper Tableaux

  1996cited by this paper
• Theorem Proving with Ordering and Equality Constrained Clauses

  1995influential reference
• Proof of proposition 3

  1992cited by this paper
• AND T

  year unknowninfluential reference

• Explaining Reasoning Results for OWL Ontologies with Evee

  2024cites this paper
• Explaining Critical Situations Over Sensor Data Streams Using Proofs and Natural Language

  2024cites this paper
• OWL Reasoners still useable in 2023

  2023influential citation
• On the Eve of True Explainability for OWL Ontologies: Description Logic Proofs with Evee and Evonne

  2022cites this paper
• Dichotomies in Ontology-Mediated Querying with the Guarded Fragment

  2020cites this paper
• The Combined Approach to Query Answering in Horn-ALCHOIQ (Extended Abstract)

  2019cites this paper
• From Horn-SRIQ to Datalog: A Data-Independent Transformation that Preserves Assertion Entailment

  2019cites this paper
• 15 Years of Consequence-Based Reasoning

  2019influential citation
• Suggesting Reasonable Phenotypes to Clinicians

  2019cites this paper
• Consequence-Based Axiom Pinpointing

  2018cites this paper
• Consequence-Based Reasoning for Description Logics with Disjunctions and Number Restrictions

  2018cites this paper
• Consequence-based Reasoning for Description Logics with Disjunction, Inverse Roles, Number Restrictions, and Nominals

  2018influential citation
• From Horn-SRIQ to Datalog: A Data-Independent Transformation that Preserves Assertion Entailment (Extended Version)

  2018cites this paper
• Consequence-based Reasoning for Description Logics with Disjunction, Inverse Roles, and Nominals

  2017influential citation
• Lean Kernels in Description Logics

  2017cites this paper
• Dichotomies in Ontology-Mediated Querying with the Guarded Fragment

  2017cites this paper
• Number Restrictions on Transitive Roles in Description Logics with Nominals

  2017cites this paper
• A Consequence-based Algebraic Calculus for SHOQ

  2017cites this paper
• Pushing the Boundaries of Reasoning About Qualified Cardinality Restrictions

  2017cites this paper
• Optimisation of tableau-based reasoning systems for expressive description logics

  2016influential citation
• Efficient Reasoning for Inconsistent Horn Formulae

  2016cites this paper
• A Saturation-based Algebraic Reasoner for ELQ

  2016cites this paper
• Practical uniform interpolation for expressive description logics

  2015cites this paper
• Pay-As-You-Go Description Logic Reasoning by Coupling Tableau and Saturation Procedures

  2015influential citation