Reasoning techniques for qualified number restrictions (QNRs) in De- scription 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 pro- pose and investigate a novel approach for concept satisfiability in acyclic ALCQ ontologies. It is based on the idea of encoding an ALCQ ontology into a for- mula in Satisfiability Modulo the Theory of Costs (SMT ( C ) ), which is a specific and computationally much cheaper subcase of Linear Arithmetic under the Inte- gers, 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

Automated Reasoning in ALCQ via SMT

Sebastiani, Roberto;Vescovi, Michele
2011-01-01

Abstract

Reasoning techniques for qualified number restrictions (QNRs) in De- scription 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 pro- pose and investigate a novel approach for concept satisfiability in acyclic ALCQ ontologies. It is based on the idea of encoding an ALCQ ontology into a for- mula in Satisfiability Modulo the Theory of Costs (SMT ( C ) ), which is a specific and computationally much cheaper subcase of Linear Arithmetic under the Inte- gers, 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
2011
In proc. International Conference on Automated Deduction
Berlin
Springer
V., Haarslev; Sebastiani, Roberto; Vescovi, Michele
File in questo prodotto:
File Dimensione Formato  
cade11.pdf

Solo gestori archivio

Tipologia: Post-print referato (Refereed author’s manuscript)
Licenza: Tutti i diritti riservati (All rights reserved)
Dimensione 203.18 kB
Formato Adobe PDF
203.18 kB Adobe PDF   Visualizza/Apri

I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione

Utilizza questo identificativo per citare o creare un link a questo documento: https://hdl.handle.net/11572/89116
Citazioni
  • ???jsp.display-item.citation.pmc??? ND
  • Scopus 8
  • ???jsp.display-item.citation.isi??? 6
social impact