Circumscription is a powerful framework for enabling non-monotonic reasoning in Description Logics (DLs) and other knowledge representation languages based on first-order logic. It is very expressive and rather abstract, which is why it is often used as a host language for defining other non-monotonic formalisms. An alternative approach to obtain a non-monotonic version of a given first-order knowledge representation language is the Equilibrium Logic (EL). For instance, EL allows the generalization of the stable model semantics of logic programs to arbitrary propositional theories and even to arbitrary first-order theories. Recently, DLs with semantics based on EL have been proposed in the context of DL terminologies, but a deeper understanding of this formalism is still missing. The goal of this paper is to clarify the connection been DLs based on EL and DLs based on circumscription, both under the well-known global circumscription and the recently proposed pointwise circumscription. To this end, we first introduce a simple yet powerful extension of circumscribed DLs by attaching to a circumscribed KB an additional set of axioms, which filter out unintended minimal models of the first KB. As we show in this paper, such constrained circumscription is powerful enough to capture DLs under the EL semantics, with global and pointwise minimality. We argue that in some important cases, constrained circumscription is computationally not more expensive than its base variant. Together with the proposed translation, this provides new decidability and complexity results for DLs based on EL semantics.
Description Logics (DLs), as fragments of first-order logic, are monotonic. A prominent research line
on extending DLs with non-monotonic features is given by circumscribed DLs [
Along the line of predicate minimization, another prominent approach is given by Equilibrium
Description Logics (EDLs) [
The main contributions of this work are as follows.
∘ We study the connection between circumscribed DLs and EDLs. Although both are based on predicate
minimization, circumscribed DLs and EDLs are two ‘orthogonal’ formalisms with diferent features, e.g.
varying predicates of circumscribed DLs vs. default negation of EDLs. We show that an EDL knowledge
base can be transformed into a circumscribed knowledge base such that there is a correspondence
between the stable models of the first and a restricted set of models of the second one. Specifically, this
restricted set of models is obtained by filtering out those models satisfying a further set of inclusions.
∘ To formalize such additional restrictions, we propose a hybrid form of circumscription where a
circumscribed knowledge base is paired with a non-circumscribed one. This second knowledge base
acts as a filter over the set of minimal models, allowing further refinement of the selection process
of minimal models. We call this formalism constrained circumscription, as the non-circumscribed
knowledge base constraints the model selection. A similar idea has been used in [
We focus on ℒℋℐ for its expressiveness and recall here the basic notions needed in the following.
We call NC , NR, and NI the mutually disjoint sets of concept names, role names, and individuals. The
expression − is the inverse role of a role name ∈ NR. The syntax of complex concepts in ℒℋℐ
is defined by the grammar := ⊤ | ⊥ | | {} | ¬ | ⊔ | ⊓ | ∃. | ∀., with ∈ NC ,
∈ NR or = − with ∈ NR, and ∈ NI . A TBox is a finite set of concept inclusions and role
inclusions, which are expressions of the form ⊑ and ⊑ , respectively, with and concepts,
and and role names or inverse roles. An expression of the form (), where ∈ NC and ∈ NI ,
is a concept assertion, while an expression of the form (, ) is a role assertion, where ∈ NR. An ABox
is a collection of assertions. A knowledge base (KB) is a pair = (, ), where is an ABox and
is a TBox. Given a KB , we denote with () the set of concept names, role names, and individual
names occurring in . The classical semantics of ℒℋℐ is defined by means of interpretations
ℐ = (Δℐ , · ℐ ) where Δℐ is the domain and · ℐ the interpretation function associating to each ∈ NI a
unique element ℐ ∈ Δℐ , to each ∈ NC a set ℐ ⊆ Δℐ and to each ∈ NR a set ℐ ⊆ Δℐ × Δℐ . The
extension of remaining concept and role expressions in ℒℐ is defined as usual [
We use [
(i) Δℐ = Δ , (ii) ℐ = , for all individuals ∈ , (iii) ℐ = , for all ∈ .
The above definition simply groups interpretations sharing the same domain, interpreting individuals in the same way, and agreeing on the set of predicates in . Note that can be empty. In this case, we simply write ℐ ∼ .
We now formalize the preference relation naturally induced by circumscription patterns. Formally, a circumscription pattern is a triple = (, , ) where , and are mutually disjoint sets of minimized, varying and fixed predicates.
Definition 2 (Preference relation). Given a circumscription pattern = (, , ) and two interpretations ℐ, such that ℐ ∼ , we write: • ℐ ⪯ if ℐ ⊆ , for all ∈ ; • ℐ ≺ , if ℐ ⪯ and ℐ ⊂ for some ∈ .
If the circumscription pattern = (, , ) is such that = ∅, we denote the relations ⪯ and ≺ with the symbols ⊆ and ⊂ , respectively.
Given a KB , a circumscription pattern = (, , ) for is a partition of the predicates occurring in . A KB equipped with a circumscription pattern is called circumscribed and we denote it with Circ (). Given a circumscribed KB, we aim to filter the set of all possible models selecting those where the extension of minimized predicates is the smallest possible. Definition 3. (Minimal model) An interpretation ℐ is a minimal model of Circ (), in symbols ℐ |= Circ (), if ℐ |= and there is no interpretation s.t. |= and ≺ ℐ. We use MM (, ) to denote the set of minimal models of Circ ().
Observe that Definition 2 does not restrict how the extension of may difer in ℐ and and varying predicates do not occur in any of the conditions. Thus, when searching for minimal models, circumscription allows for the reconfiguration of the predicates across the entire model.
In [
(ℐ, ) = ℐ (− )(ℐ, ) = {(, ′) | (′, ) ∈ ℐ } (1 ⊓ 2)(ℐ, ) = 1(ℐ, ) ∩ 2(ℐ, ) ⊤(ℐ, ) = Δℐ (¬)(ℐ, ) = Δℐ ∖
⊥(ℐ, ) = ∅
(1 ⊔ 2)(ℐ, ) = 1(ℐ, ) ∪ 2(ℐ, )
(∃.)(ℐ, ) = { ∈ Δℐ | ∃′ : (, ′) ∈ (ℐ, ) ∧ ′ ∈ (ℐ, )}
(∀.)(ℐ, ) = {︁ ∈ Δℐ | ∀′ : ((,, ′′)) ∈∈ (ℐ,im)pilmiepslie′s∈′∈(ℐ, ) and }︁
classical circumscription, but not always: pointwise circumscription is not able to minimize predicate
participating in a cycle and treats varying predicates diferently. See [
• for all ∈ NC , ℐ ∖ {} = ∖ {}, and • for all ∈ NR, ℐ ∩ (Δ × Δ) = ∩ (Δ ×
Δ), with Δ = Δℐ ∖ {}.
Thus, two interpretations in the relation ∼ ∙ may difer in terms of concept and role names involving one domain element. We now use the relation in Definition 4 to give a pointwise flavor to the preference relation between interpretations of Definition 2.
Definition 5. Assume a circumscription pattern = (, , ) and two interpretations ℐ, such that ℐ ∼ . We write • ℐ ⪯ ∙ , if ℐ ∼ ∙ and ℐ ⪯ ; • ℐ ≺ ∙ , if ℐ ⪯ ∙ and ℐ ⊂ for some ∈ .
Given a circumscription pattern = (, , ) such that = ∅, we denote ⪯ ∙ and ≺ ∙ with ⊆ ∙ and ⊂ ∙ , respectively.
Definition 6. An interpretation ℐ is a pointwise minimal model of Circ (), in symbols ℐ |=∙ Circ (), if ℐ |= and there is no interpretation s.t. |= and ≺ ∙ ℐ. We use PMM (, ) to denote the set of pointwise minimal models of Circ ().
The standard definitions of concept satisfiability, concept subsumption, and concept instances are
adapted to (resp. pointwise) minimal models in the obvious way and can be reduced polynomial one into
the other [
Following [
Definition 7. A Here-and-There (HT) interpretation is a pair (ℐ, ) of interpretations with ℐ ⊆ , with ⊆ NC ∪ NR. The interpretation function · (ℐ, ) is defined in Figure 1.
In general, under the HT semantics predicates do not obey the law of the excluded middle. Already
in the case of propositional HT logic, the formula ∨ ¬ is not a tautology [
As already pointed out in [
Assume a KB = ( , ) and an HT interpretation (ℐ, ). We write: - (ℐ, ) |= ⊑ , if (ℐ, ) ⊆ (ℐ, ) and ⊆ ; - (ℐ, ) |= if ℐ |= and (ℐ, ) |= ⊑ for all ⊑ ∈ .
We can now define stable models of a DL KB.
under fixed predicates , if (i) the HT interpretation ( , ) is a model of , and (ii) there is no ℐ s.t. (ℐ, ) is a model of and ℐ ⊂ .
We denote with SM () the set of all stable models for with fixed predicates . If = ∅, we drop the subscript and write SM ().
Similarly to the approach of this paper, in the stable model semantics of [
In the semantics given in Definition 9, the negation ¬ behaves as negation as failure or default
negation in logic programs: the truth of a negated concept ¬ at a certain domain element in a stable
model intuitively means that the concept could not be proved at such domain element. As already
underlined in [
Classified_Document(1)
User( ℎ) read( ℎ, 1) ∃access_granted_by.Admin ⊑ Has_Read_Permission
Classified_Document ⊓ ¬∀(read)− .Has_Read_Permission ⊑ ⊥ Assume that Admin and access_granted_by are fixed predicates. We derive that all classified documents must be read by someone who has permission to do so. As an efect of ‘ ¬’ behaving as default negation, such permission is not ‘justified’ by the last inclusion above and must come from an Admin. Thus, in every stable model, we derive that John, who is reading the classified document 1, has permission granted by an admin.
In Definition 4 we introduce a relation comparing interpretations that difer only at a single domain element, in terms of concept names and role names involving it. We lift this pointwise comparison to defining pointwise stable models as follows. Recall the definition of ⊆ ∙ and ⊂ ∙ .
Definition 10 (Pointwise Stable Models). Given ⊆ ∪ , an interpretation is a pointwise stable model of a KB under fixed predicates , if (i) the HT interpretation ( , ) is a model of , and (ii) there is no ℐ s.t. (ℐ, ) is a model of and ℐ ⊂ ∙ .
We denote with PSM () the set of all stable models for with fixed predicates . If = ∅, we drop the subscript and write PSM ().
Remark. Pointwise stable models have been already considered for full first-order logic in [
The reasoning tasks of concept satisfiability , subsumption and instance checking can be adapted in the usual way to stable models and pointwise stable models.
We strengthen the undecidability result for ℒℐ of [
able.
In [
is undecidable.
In order to characterize the connection of EDL KBs and circumscribed KBs, we extend circumscription
with constraints. The notion of constraints has been introduced in [
tion ℐ, we say that ℐ is a (pointwise) minimal model of Circ () ∧ , in symbols ℐ |=(∙ ) Circ () ∧ , if ℐ |=(∙ ) Circ () and ℐ |= . We call constraint set the KB .
Compared to [
Example 2. Recall the KB of Example 1. Let us consider ′ ⊆ given by and circumscribed with = {Has_Read_permission} and keeping all the other predicates fixed . Consider the constraint set = {Classified_Document ⊑ ∀(read)− .Has_Read_Permission}. As in Example 1, the inclusion above imposes that whenever a classified document is read, the user reading it has permission to do so. Since the predicate Has_Read_Permission is minimized, in minimal models of ′, any permission must be granted by an Admin. Applying Definition 11, we find that in every minimal model ℐ of Circ (′) ∧ , John got the reading permission from an Admin. Counterintuitively, if we push the constraint set inside the circumscription, i.e. we look for minimal models of Circ (′ ∪ ) we can derive that John has permission to read 1 without the approval of an administrator.
Following [
Theorem 3. Concept satisfiability in circumscribed ℒℋℐ with constraints is NExpTimeNP-complete if all roles are varying.
Filtration has been used in [
ℒℋℐ is in NExpTimeNP.
Expressing Closed Predicates. In DLs with closed predicates [
Intuitively speaking, the extension of a closed predicate is ‘circumscribed’ to instances of given by ABox assertions. Although the underlying principle is close to predicate minimization, DLs with closed predicates and (pointwise) circumscribed DLs are two diferent non-monotonic formalisms and we see no obvious formal translation. On the other hand, constrained circumscription can easily capture DLs with close predicates.
Given a KB = (, ) with a set of closed predicates Σ, let Σ′ = {′ | ∈ Σ}, i.e. we consider a copy of the signature in Σ. Let ′ = {′(⃗) | (⃗) ∈ and ∈ Σ}. We obtain this way a new KB ′ = ( ∪ ′, ). We now define a circumscription pattern for ′ by stating that all predicates in Σ′ are minimized. Since does not contain any occurrence of symbols in Σ′, in a minimal model ℐ′ we will have that each ′ ∈ Σ′ contains only named individuals or pairs of named individuals, whose participation in (′)ℐ is justified by an assertion in ′. To the circumscribed KB Circ (′), we add the set of constraints = { ⊑ ′ | ∈ Σ}. In every model ℐ of Circ (′) ∧ , every element of ℐ is an element of (′)ℐ . In this way, we force to be closed.
Theorem 4. Concept satisfiability w.r.t KBs with closed predicates can be polynomially reduced to concept satisfiability w.r.t. (pointwise) circumscribed KBs with constraints.
The result above almost directly implies that nominals can be simulated using constraints. Indeed this
is already possible via closed predicates: each nominal can be simulated by replacing every occurrence
of with a closed predicate and adding an assertion (). A similar idea has been used in [
Given a KB and a set of fixed predicates, we aim to build a KB ¯ with a circumscription pattern and a set of constraints such that there is a correspondence between stable models of and model of Circ (¯) ∧ up to the original signature. We give a sketch of the translation that we adapted from [18].
The first step of our construction is to simulate HT interpretations. We consider a copy Σ′ of the signature Σ of , which we use to split the ‘here’ and the ‘there’ interpretations. Intuitively speaking, the interpretation of primed predicates corresponds to the interpretations of predicates in the ‘there’ interpretation. We construct the KB ¯ taking the union of two KBs ′ and ⋆. The KB ′ is obtained from by replacing each symbol with its primed counterpart. We use ′ to require that the ‘there’ is a classical model of . The KB ⋆ is obtained by replacing each concept occurring negatively in with ′. This second KB is used to simulate the interpretation of negated concepts in the HT semantics (see Figure 1).
To capture the stable model semantics in the setting of circumscription, we require that all predicates in the original signature of are minimized while all primed predicates are fixed. To synchronize the ‘here’ and the ‘there’, ensuring that the interpretations of primed and non-primed symbols coincide, we introduce constraints of the form ⊑ ′ and ′ ⊑ , for each predicate symbol . These constraints iflter out minimal models that are not stable.
A natural question is: do we really need to rely on constrained circumscription? Circumscription and
Equilibrium Logic are two orthogonal formalisms, as already argued in [
Example 3. Consider the TBox = {¬ ⊑ } with = ∅. It is easy to show that has no stable model. Indeed, given ℐ such that Δℐ = {} and ℐ |= , then ℐ = {}. The interpretation such that Δ = Δℐ and = ∅ is such that ( , ℐ) |= . If we apply (pointwise) circumscription, the most natural option to ‘mimic’ the stable model semantics is to minimize . One can observe that the previous model ℐ of is minimal.
Example 4. Consider the TBox = { ⊑ ⊔ ¬} and assume = {}. We can show that is satisfiable in a stable model of . Indeed, the interpretation ℐ such that Δℐ = {}, ℐ = ℐ = {} is a stable model such that ℐ = ∅. If one considers now (pointwise) circumscription, as before a natural direction is to respect the ‘nature’ of predicates, i.e. keep fixed and minimize . However, assuming that is minimized, it is straightforward to see that there is no minimal model of such that ̸= ∅. The transformation. Given a KB = (, ), let Σ denote the set of all concept names and role names occurring in . We consider a copy of the signature Σ and we denote it with Σ′ = {′| ∈ } ∪ {′| ∈ Σ}. Given a complex concept we denote with ′ the concept over Σ′ obtained globally replacing each predicate symbol in with its primed version. Following [18], we define an operator recursively as follows: • () = , () = , (⊤) = ⊤, (⊥) = ⊥, ({}) = {}, • (¬) = ¬′, (∃.) = ∃. () and (∀.) = ∀. () ⊓ ∀′.′ • ( ∘ ) = () ∘ (), with ∘ ∈ {⊓ , ⊔}.
Given the TBox , we denote with * the resulting TBox, with predicates occurring in Σ ∪ Σ′, obtained applying to all GCIs in , i.e. ⋆ = { () ⊑ ()| ⊑ ∈ }. Observe that the assertions in the ABox can be seen as inclusions in the standard way. It is easy to observe that they are not afected by the transformation. We ⋆ = (, ⋆). We denote with ′ the KB obtained from by replacing each symbol ∈ Σ with its primed counterpart ′ ∈ Σ′.
Given a set Σ of concept names and role names and interpretation , we denote with ′ the interpretation such that Δ = Δ ′ , (′) ′ = for all ∈ Σ. Given an HT interpretation (ℐ, ), we denote with ℐ ∪ ′ the interpretation such that Δℐ∪ ′ = Δℐ = Δ , ℐ∪ ′ = ℐ for all ∈ Σ and ( ′)ℐ∪ ′ = for all ′ ∈ Σ′.
As mentioned at the beginning of this section, we aim to simulate the HT semantics. Roughly speaking, given an HT interpretation, we copy the ‘there’ interpretation using the primed symbols, while unprimed symbols are interpreted as in the ‘here’.
and ⊆ Σ be a set of fixed predicates. Then (ℐ, ) is a HT model of with fixed predicates in if and only if ℐ ∪ ′ is a model of * ∪ ′ ∪ { ⊑ ′ ∈ Σ} ∪ {′ ⊑ | ∈ }.
We now use circumscription to capture stable models. With the following theorem, we formalize the intuitive explanation given at the beginning of this section.
Theorem 5. Assume a KB = (, ) and an interpretation ℐ. Let Σ be the set of predicates occurring in and ⊆ Σ, ℐ ∈ SM () if and only if ℐ ∪ ℐ′ is a model of Circ (* ∪ ′) ∧ , with = { ⊑ ′, ′ ⊑ | ∈ Σ} and = (, ∅, ∪ Σ′) with = Σ ∖ .
Since ′ contains only fixed predicates, alternatively we can add it to the set of constraints. Theorem 5 extends to the case of pointwise EDLs and pointwise circumscribed DLs with constraints. Theorem 6. Assume a KB = (, ) and an interpretation ℐ. Let Σ be the set of predicates occurring in and ⊆ Σ, ℐ ∈ PSM () if and only if ℐ ∪ ℐ′ is a model of Circ∙ (* ∪ ′) ∧ , with = { ⊑ ′, ′ ⊑ | ∈ Σ} and = (, ∅, ∪ Σ′) with = Σ ∖ .
In this paper, we established a translation from Equilibrium DLs (EDLs) and circumscribed DLs with constraints, both under global and pointwise minimization. These two formalisms are interesting on their own and understanding the complexity of one can help in understanding the complexity of the other. Therefore, our future research will follow two main lines. We plan to investigate the expressive power and the computational complexity of EDLs. In particular, we aim to focus on lightweight EDLs in the DL-Lite family. Via the translation of EDLs into circumscribed DLs with constraints, we can refine our investigation by studying the complexity of reasoning in circumscribed DLs with constraints. The preliminary results presented in this paper involve varying predicates, that are not supported in EDLs. We are also interested in identifying syntactic restrictions under which global and pointwise circumscription (with constraints) coincide, inheriting the good computational properties of the latter for both EDLs and pointwise EDLs. Furthermore, we aim to explore the connection between EDLs and DLs based on MKNF [19], and fuzzy DLs under the (3-valued) Gödel semantics [20].
This work was partially supported by the Austrian Science Fund (FWF) project P30873, and by the Wallenberg AI, Autonomous Systems, and Software Program (WASP), funded by the Knut and Alice Wallenberg Foundation. A part of this research was done when Mantas Šimkus was employed at Umeå University, Sweden. [18] D. Pearce, H. Tompits, S. Woltran, Characterising equilibrium logic and nested logic programs:
Reductions and complexity, , Theory Pract. Log. Program. 9 (2009) 565–616. [19] F. M. Donini, D. Nardi, R. Rosati, Description logics of minimal knowledge and negation as failure,
ACM Trans. Comput. Log. 3 (2002) 177–225. [20] F. Bobillo, M. Delgado, J. Gómez-Romero, U. Straccia, Fuzzy description logics under Gödel semantics, International Journal of Approximate Reasoning 50 (2009) 494–514. Special Section on Bayesian Modelling.