We explore the relationships between Description Logics and Set Theory. The study is carried on using, on the set-theoretic side, a very rudimentary axiomatic set theory Ω, consisting of only four axioms characterizing binary union, set difference, inclusion, and the power-set. An extension of ALC, dubbed ALCΩ, is defined in which concepts are naturally interpreted as sets living in Ω-models. In ALCΩ not only membership between concepts is allowed—even admitting membership circularity—but also the power-set construct is exploited to add metamodelling capabilities. We investigate translations of ALCΩ into standard description logics as well as a set-theoretic translation. A polynomial encoding of ALCΩ in ALCOI proves the validity of the finite model property as well as an EXPTIME upper bound on the complexity of concept satisfiability. We develop a set-theoretic translation of ALCΩ in the theory Ω, exploiting a technique proposed for translating normal modal and polymodal logics into Ω. Finally, we show that the fragment LCΩ of ALCΩ not admitting roles and individual names, is as expressive as ALCΩ.

Adding the power-set to description logics

Giordano L.;
2020-01-01

Abstract

We explore the relationships between Description Logics and Set Theory. The study is carried on using, on the set-theoretic side, a very rudimentary axiomatic set theory Ω, consisting of only four axioms characterizing binary union, set difference, inclusion, and the power-set. An extension of ALC, dubbed ALCΩ, is defined in which concepts are naturally interpreted as sets living in Ω-models. In ALCΩ not only membership between concepts is allowed—even admitting membership circularity—but also the power-set construct is exploited to add metamodelling capabilities. We investigate translations of ALCΩ into standard description logics as well as a set-theoretic translation. A polynomial encoding of ALCΩ in ALCOI proves the validity of the finite model property as well as an EXPTIME upper bound on the complexity of concept satisfiability. We develop a set-theoretic translation of ALCΩ in the theory Ω, exploiting a technique proposed for translating normal modal and polymodal logics into Ω. Finally, we show that the fragment LCΩ of ALCΩ not admitting roles and individual names, is as expressive as ALCΩ.
File in questo prodotto:
Non ci sono file associati a questo prodotto.

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/11579/111215
Citazioni
  • ???jsp.display-item.citation.pmc??? ND
  • Scopus 2
  • ???jsp.display-item.citation.isi??? 1
social impact