The problem of reasoning with qualified number restrictions in Description Logics (DLs) has been investigated since the very first research steps in automated reasoning for DLs. Moreover, developing techniques for optimized reasoning with qualified number restrictions and has gained further importance since qualified number restrictions have been added to the forthcoming standard OWL 2 for Semantic Web applications. On the one hand, however, actual DL reasoning techniques, often lack of efficiency in handling those features, especially when the number of restrictions or the values involved are high. On the other hand the manifold problem of reasoning including numerical constraints is a well-established and thoroughly investigate problem in the SMT community, in which a lot of effort is continuously spent in order to enhance the efficiency of reasoning techniques for such kind of problems. In this paper we propose and investigate a novel approach for concept satisfiability in acyclic ALCQ ontologies. The idea is to encode an ALCQ ontology into a formula in Satisfiability Modulo the Theory of Costs (SMT(C)), which is a specific and computationally much cheaper subcase of Linear Arithmetic under the Integers (LA(Z)), and to exploit the power of modern SMT solvers to compute every concept-satisfiability query on a given ontology. We have implemented and tested our approach (called ALCQ2SMT_C) and some optimizations on a wide set of synthesized benchmark formulas, comparing the approach with the main state-of-the-art tools available. Our empirical evaluation confirms the potential of the approach.

Automated Reasoning on TBoxes with Qualified Number Restrictions via SMT / Vescovi, Michele; Sebastiani, Roberto; Haarlsev, Volker. - ELETTRONICO. - (2011), pp. 1-53.

Automated Reasoning on TBoxes with Qualified Number Restrictions via SMT

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

Abstract

The problem of reasoning with qualified number restrictions in Description Logics (DLs) has been investigated since the very first research steps in automated reasoning for DLs. Moreover, developing techniques for optimized reasoning with qualified number restrictions and has gained further importance since qualified number restrictions have been added to the forthcoming standard OWL 2 for Semantic Web applications. On the one hand, however, actual DL reasoning techniques, often lack of efficiency in handling those features, especially when the number of restrictions or the values involved are high. On the other hand the manifold problem of reasoning including numerical constraints is a well-established and thoroughly investigate problem in the SMT community, in which a lot of effort is continuously spent in order to enhance the efficiency of reasoning techniques for such kind of problems. In this paper we propose and investigate a novel approach for concept satisfiability in acyclic ALCQ ontologies. The idea is to encode an ALCQ ontology into a formula in Satisfiability Modulo the Theory of Costs (SMT(C)), which is a specific and computationally much cheaper subcase of Linear Arithmetic under the Integers (LA(Z)), and to exploit the power of modern SMT solvers to compute every concept-satisfiability query on a given ontology. We have implemented and tested our approach (called ALCQ2SMT_C) and some optimizations on a wide set of synthesized benchmark formulas, comparing the approach with the main state-of-the-art tools available. Our empirical evaluation confirms the potential of the approach.
2011
Trento
University of Trento - Dipartimento di Ingegneria e Scienza dell'Informazione
Automated Reasoning on TBoxes with Qualified Number Restrictions via SMT / Vescovi, Michele; Sebastiani, Roberto; Haarlsev, Volker. - ELETTRONICO. - (2011), pp. 1-53.
Vescovi, Michele; Sebastiani, Roberto; Haarlsev, Volker
File in questo prodotto:
File Dimensione Formato  
DISI-11-001_MV_RS_VH.pdf

accesso aperto

Tipologia: Versione editoriale (Publisher’s layout)
Licenza: Tutti i diritti riservati (All rights reserved)
Dimensione 891.45 kB
Formato Adobe PDF
891.45 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/358447
 Attenzione

Attenzione! I dati visualizzati non sono stati sottoposti a validazione da parte dell'ateneo

Citazioni
  • ???jsp.display-item.citation.pmc??? ND
  • Scopus ND
  • ???jsp.display-item.citation.isi??? ND
social impact