Advertisement
Published in:
2011 | OriginalPaper | Chapter
Automated Reasoning in via SMT
Authors : Volker Haarslev, Roberto Sebastiani, Michele Vescovi
Published in: Automated Deduction – CADE-23
Publisher: Springer Berlin Heidelberg
Activate our intelligent search to find suitable subject content or patents.
Select sections of text to find matching patents with Artificial Intelligence. powered by
Select sections of text to find additional relevant content using AI-assisted search. powered by
Reasoning techniques for qualified number restrictions (QNRs) in Description Logics (DLs) have been investigated in the past but they mostly do not make use of the arithmetic knowledge implied by QNRs. In this paper we propose and investigate a novel approach for concept satisfiability in acyclic
$\mathcal{ALCQ}$
ontologies. It is based on the idea of encoding an
$\mathcal{ALCQ}$
ontology into a formula in Satisfiability Modulo the Theory of Costs (SMT
$(\ensuremath{\mathcal{C}} )$
), which is a specific and computationally much cheaper subcase of Linear Arithmetic under the Integers, and to exploit the power of modern SMT solvers to compute every concept-satisfiability query on a given ontology. We implemented and tested our approach, which includes a very effective individuals-partitioning technique, on a wide set of synthesized benchmark formulas, comparing the approach with the main state-of-the-art DL reasoners available. Our empirical evaluation confirms the potential of the approach.