Can Full Set-Theoretical Subsumption Semantics in Metamodelled Description Logics Be Captured Within Decidable FOL Fragments?⋆

Abstract

Metamodelling in ontologies enables the structured representation of complex domains by defining relationships between concepts across multiple levels of abstraction. Subsumption, a core relation in hierarchical reasoning, provides a strong foundation for organizing ontological knowledge. In this work, we build on an extended form of higher-order description logic, denoted ℋℐℛ* (ℒ), which supports metamodeling through two semantically ifxed roles: instanceOf and subClassOf. These roles explicitly enforce meta-level constraints, allowing for a richer and more expressive representation of both hierarchical and meta-level concepts. While the logic has four known variants with three shown to be decidable, the decidability of the full set-theoretical semantics of the subClassOf relation for all concepts remains open. This work investigates the decidability of the full set-theoretical semantics of the subClassOf relation for all concepts, denoted as ℋℐℛ(ℒ) for arbitrary base DL, ℒ by seeking to align it with well-established decidable fragments of first-order logic.

Keywords

• eol>Description logics
• Decidable Fragments of FOL
• Metamodelling
• Ontologies

1. Introduction

Ontologies are engineering artifacts that systematically model entities and relationships within a domain, providing a structured framework for representing and understanding its knowledge. By defining concepts, objects, or events and their relationships, ontologies enable consistent communication, reasoning, and interoperability between systems. These frameworks are often formalized using logics, such as description logics (DLs), which allow for representing both extensional (instance-based) and intensional (concept-based) knowledge. For example, the axiom ⊑ asserts that every instance of is also an instance of , while () states that individual is an instance of . The description logic ℛℐ() underpins OWL 2 DL, the Web Ontology Language [ 1, 2 ].

Metamodelling in ontologies enhances semantic representation by allowing concepts and roles to also be treated as individuals, enabling structured modeling of complex domains. For instance, in biological taxonomy, Melman is an instance of Girafa Camelopardalis , which itself can be further classified in the category Taxon. This illustrates how metamodelling supports multi-level classification. OWL 2 introduces punning, a metamodelling technique that permits a name to function simultaneously as an individual, concept, and role, while the reasoner treats each use as semantically distinct [ 3 ]. An important focus in this area involves addressing the constraints required for instantiation and subclass relations, features that standard description logics cannot accommodate. While OWL Full permits restrictions on rdf:type and rdfs:subClassOf, OWL Full is undecidable as demonstrated by Motik [ 4 ]. To address the challenges of metamodelling, various higher-order description logics (DLs) have been proposed, typically grouped by their semantic frameworks. The first group [ 5, 6, 7, 4 ] adopts HiLog-style semantics [ 8 ], utilized in RDF. In this approach, each entity name is treated as an intension—an abstract representation of the entity’s internal meaning. Extensions of concepts and roles are then assigned to these intensions. The second group [ 9, 10, 11 ] is based on Henkin’s general semantics [ 12 ] for higher-order logic. Under this framework, concepts are directly interpreted as sets, meta-concepts as sets of sets, and so on. This stronger semantic foundation provides distinct properties for reasoning.

Kubincová [ 7 ] introduced a decidable higher-order description logic framework, ℋℐℛ* (ℒ), building on and extending the work of Glimm et al. [ 5 ]. In this work, decidability was proved via reduction to ifrst-order ℛℐ, for the following two distinct semantic interpretations: 1. Non-set-theoretical semantics: Under this interpretation, if two concept intensions are related by the meta-level relation subClassOf, then the extension of one concept is included in the extension of the other, i.e., , : subClassOf implies ⊑ , but not necessarily the converse. This semantics was formalized in two variants of the logic: ℋℐℛ (ℛℐ), which applies to named concepts only, and ℋℐℛ (ℛℐ), which generalizes the interpretation to all concepts.

2. Full set-theoretical semantics: Here, the meta-level relation subClassOf is interpreted equivalently

to the subsumption relation, i.e., , : subClassOf if and only if ⊑ . This stricter semantics was applied only to named concepts and is captured in the logic ℋℐℛ (ℛℐ).

These logics enhance expressivity while preserving decidability by incorporating two

ifxed, semantically interpreted roles, instanceOf and subClassOf, to explicitly capture instantiation and subsumption within ontologies. Key features of the framework include: (1) HiLog-style semantics[ 6 ]; (2) typed entity separation: individuals, concepts, and roles are strictly distinguished; (3) flexible typing of concept and role extensions.

In this work, we extend the approach of Kubincová [7] to support metamodeling with full set

theoretical semantics across all concepts. Building on their framework, we introduce a higher-order extension named ℋℐℛ(ℛℐ), which captures intentional and extensional subsumption for all concepts at the meta-level. In this setting, the role subClassOf is semantically interpreted over all concept individuals and defined to correspond to the instance-level implication between the extensions of their respective intensions.

While existing approaches to the decidability of metamodelled description logics have largely relied

on reductions to first-order representations in DL, as demonstrated in works such as [ 6, 7, 10, 5, 13 ], other approaches focus on adapting existing reasoning algorithms for standard description logics to accommodate metamodelling constructs, notably the direct reasoning approach presented in [ 10 ].

Our approach is motivated by the observation that most description logics are semantic fragments of

FOL logic [14], and are often subsumed within known decidable fragments such as the two-variable

fragment FO2 [ 15 ] and the guarded fragment [ 16 ]. We explore whether the decidability of ℋℐℛ(ℒ) can be achieved by seeking to align it to some decidable fragment of FOL. In particular, we examine more expressive and recent decidable fragments such as the three-variable fragment FO−3 [ 17 ], the

Triguarded Fragment (TGF) [18], and Maslov’s class [19]. We present our findings on the applicability

of these fragments to ℋℐℛ(ℒ), highlighting key compatibilities as well as identified limitations.

The main objectives of this work are as follows: • To define the syntax and semantics of a higher-order description logic extended to support full settheoretical subsumption across all concepts. This logic, collectively referred to as ℋℐℛ(ℒ), provides a formal foundation for reasoning about both hierarchical (i.e., subsumption) and instance-level relationships in a metamodelled domain. • To examine the feasibility of reducing reasoning tasks in ℋℐℛ(ℒ) to established decidable fragments of FOL. Specifically, we aim to identify correspondences between the axioms of ℋℐℛ(ℒ) and known decidable fragments of FOL, thereby delineating the logical expressiveness and computational boundaries of the logic.

The structure of this work is organized as follows. Section 1 provides an introduction and discusses related work. In Section 2, we present an overview of some decidable fragments of FOL, which form the basis for our later reductions. Section 3 introduces the decidable higher-order description logic ℋℐℛ(ℛℐ) [ 7, 20 ], and outlines its key semantic features. In Section 4, we focus on the more expressive higher-order extension ℋℐℛ* (ℛℐ), with particular attention to the variant ℋℐℛ(ℒ), whose decidability remains open for arbitrary base logic, . Finally, Section 5 concludes with a summary of our contributions and key findings.

2. First order logic

First-Order Logic (FOL), also known as predicate logic, is a formal system that extends propositional

logic to provide a robust framework for reasoning about objects, their properties, and the relationships between them. Although FOL is generally undecidable, several important fragments of FOL have been shown to be decidable. These fragments restrict the use of variables, quantifiers, or functions in specific ways that ensure decidability while retaining some expressive power. In our research, we investigated some of these decidable fragments, to determine the formal verification of the decidability of our logic. Notations In this work, we use lowercase letters such as , , , etc., to denote variables, and letters such as , , , etc., to denote constants. Terms are either variables, constants, or the result of applying a function symbol to other terms. They denote elements of the domain. Predicate symbols are represented by uppercase letters such as , , , or descriptive names like subClassOf, instanceOf, etc. A predicate of arity forms an atomic formula when applied to terms (e.g., (, )). Universal role (U) refers to the binary predicate U(, ) denoting the set of all pairs of domain elements. Atomic formulas are formulas of the form (1, . . . , ), where is an -ary predicate symbol and 1, . . . , are terms. Formulas are built from atomic formulas using logical connectives (¬, ∧, ∨, →, ↔) and quantifiers ( ∀, ∃). A variable is bound if it appears within the scope of a quantifier. Otherwise, it is free. A formula without free variables is called a sentence. A literal is an atomic formula or its negation. 2.1. Triguarded Fragment Of First Order Logic

The Triguarded fragment (TGF) of first-order logic, introduced by Rudolph and Simkus [ 18], generalizes

both the guarded fragment (GF) [ 21 ] and the two-variable fragment (FO2) [ 21 ]. The finite model theory of TGF has been thoroughly investigated by Kieronski and Rudolph [ 22 ], who provided tight bounds and explored its expressive capacity relative to other decidable fragments.

Definition 1. [ 18 ] The triguarded fragment (TGF) of first-order logic is defined as the smallest set of formulae satisfying the following closure rules: 1. Every atomic formula belongs to TGF. 2. TGF is closed under propositional connectives: if ,

TGF. ∈ TGF, then ¬ , ∧ , and ∨ are also in 3. If is a variable, and is a formula in TGF with |free( )| ≤ 2, then ∀ and ∃ also belong to

TGF. 4. If ¯ is a non-empty tuple of variables, ∈ TGF, is an atomic formula, and free( ) ⊆ free( ), then ∀¯( → ) and ∃¯( ∧ ) also belong to TGF.

The expressiveness of the Triguarded Fragment (TGF) goes beyond both the Guarded Fragment (GF)

and the two-variable fragment (FO2), as exemplified by the following formula, which does not fall into either of those fragments[ 18 ]:

∀ ∀ (1(, ) ∧ 2(, ) → ∃ 3(, , , )) . 2.2. The Guarded Fragment With Universal Role (GFU)

Rudolph and Simkus [18] introduced the Guarded Fragment with Universal Role (GFU), an extension of

the classical Guarded Fragment (GF) designed to capture the expressiveness of the Triguarded Fragment (TGF) while remaining within a guarded syntactic discipline. GFU augments GF by incorporating a built-in binary predicate U ∈ NP, known as the universal role, whose interpretation is fixed as:

U = Δ × Δ for every interpretation .

This means that U relates every pair of domain elements, enabling it to syntactically simulate unguarded

quantification by acting as a universal guard.

Definition 2 ([ 18 ]). GFU is the subset of TGF consisting of formulas that are constructed using only rules (1), (2), and (4) from Definition 1, and which may include atomic formulas involving the predicate U.

The universal role U allows guarded quantification to mimic the flexibility of triguarded quantification.

Specifically, any TGF formula can be transformed into an equivalent GFU formula by replacing each

unguarded quantifier with a quantifier guarded by U.

Proposition 1 ([ 18 ]). For every TGF formula , there exists a GFU formula * that can be computed in polynomial time such that and * are logically equivalent. Furthermore, for any interpretation ℐ and vocabulary NP( ), the interpretations of and * coincide over NP( ) ∪ {U}.

An example is the transformation of the formula in TGF into the following equivalent GFU formula [18]:

∀ ∀ (U(, ) → ((1(, ) ∧ 2(, )) → ∃ 3(, , , ))) Theorem 1 (Complexity [ 22 ]). Deciding satisfiability of TGF and of GFU formulae without equality is N2ExpTime-complete. The problem is NExpTime-complete under the assumption that predicate arities are bounded by a constant.

TGF and GFU thus maintain decidability while ofering greater expressive power. Notably, they also allow the unrestricted use of constants. Although incorporating full equality into logical systems often leads to undecidability, it appears feasible [ 18 ] to include equality atoms of the form = , where is a constant, without afecting the known complexity bounds. This syntactic feature enables the representation of the DL nominals construct.

2.3. FO3 Fragment Of First-Order Logic

− Fiuk and Kieronski [ 17 ] introduced the FO−3 fragment which contains the two-variable fragment FO2 of first-order logic with constants, but without equality, and allowed the use of three variables {, , }. This fragment reach into the area of the FO3 but provide some restrictions on the use of quantifiers pattern such as ∀∀∀, ∀∃∀, and ∀∀∃ which leads to undecidability in FO3.

Definition 3 ([ 17 ]). The set of FO−3 formulas is defined as the smallest set of formulas over variables , , and , satisfying the following closure conditions: 1. Every literal involving at most one variable belongs to FO−3 . 2. FO−3 is closed under conjunction (∧) and disjunction (∨). 3. Let ∈ {, , }. If is a positive Boolean combination of FO−3 formulas and literals, then ∃ is in FO−3 . 4. Let , ′ ∈ {, , } be distinct. If is a positive Boolean combination of FO−3 formulas with free variables contained in {, ′}, and literals involving only and ′, then ∀ is in FO−3 . 5. Let , ′ ∈ {, , } be any variables. If is a positive Boolean combination of FO−3 formulas with at most one free variable, and literals that involve all of , , and , then both ∃ ∀′ and ∀ ∀′ are in FO−3 .

Here, variables and ′ always range over the fixed set {, , }. The key syntactic restriction imposed by Rule (5) is that formulas ending with a universal quantifier and binding subformulas involving all three variables must use positive Boolean combinations where the subformulas have at most one free variable. In contrast, existential quantification in Rule (3), and universal quantification over subformulas with at most two free variables as in Rule (4), are allowed more liberally. As an example, consider the following formula: This belongs to the FO−3 as demonstrated in [ 17 ].

Theorem 2. [ 17 ] FO−3 has the finite (exponential) model property. The finite satisfiability problem ( satisfiability problem) for FO−3 is NExpTime-complete. i.e., 2.4. The Maslov’s Class The Maslov’s class, [ 19, 21 ] is a decidable extension of FO2. Notably, encompasses and generalizes the normal forms of FO2 formulas. The class is defined over the language of first-order logic without equality and without function symbols, but with constants symbols.

Let be a closed formula in negation normal form, and let be a subformula of . The -prefix of is the sequence of quantifiers in that bind the free variables of . A -prefix is said to be a terminal -prefix if it is of the form:

∃1 . . . ∃∀111 . . . , where , ≥ 0 and each ∈ {∃, ∀} for 1 ≤ ≤ . The terminal part is the sufix ∀111 . . . .

If the -prefix contains only existential quantifiers (i.e., of the form ∃1 . . . ∃), then the terminal

-prefix is defined to be the empty sequence.

A closed formula in negation normal form belongs to the class if there exist ≥ 0 universal

quantifiers ∀1, . . . , ∀ in such that for every atomic subformula of , the terminal -prefix of satisfies one of the following conditions:

1. It has length at most 1;

2. It ends with an existential quantifier;

3. It is exactly of the form ∀1∀2 . . . ∀.

As an example, consider the following formula:

∀ ∀ (︀ mwc(, ) → ︀( married(, ) ∧ ∃ (has_child(, ) ∧ has_child(, )))︀ .

This formula belongs to the class since every atomic subformula satisfies one of the above conditions

on terminal prefixes[ 21 ].

Theorem 3. [ 19 ] Every satisfiable formula in admits a finite model of size 2(| |· log | |). Hence, the satisfiability problem for is NExpTime-complete. 3. Instantiation Metamodelling in ℋℐ ℛ( ℛℐ )

Kubincova et al. [20, 7] introduce and investigate the higher-order description logic ℋℐℛ(ℛℐ),

which extends ℛℐ with basic metamodelling capabilities through HiLog-style semantics. In this logic, the metamodelling capability includes the addition of the instanceOf role only (subClassOf role for subsumption not included) for instantiation. Definition 4. [ 20, 7 ] Let = ⊎ ⊎ represent a DL vocabulary such that instanceOf ∈ . The ℋℐℛ(ℛℐ) role expressions are defined as the smallest set constructed inductively to include the expressions listed in the upper part of Table 1, where 0 ∈ ∖ {instanceOf, subClassOf, U}, is an atomic or inverse role, and and are role expressions. Similarly, ℋℐℛ(ℛℐ) descriptions are defined as the smallest set inductively generated to include the expressions in the middle part of Table 1, where ∈ , ∈ , and and are descriptions, with being an atomic or inverse role.

A ℋℐℛ(ℛℐ) knowledge base is a finite set of axioms structured according to the forms shown in the bottom part of Table 1, where , 1, 2 ∈ , and are descriptions, and are atomic or inverse roles, and denotes a role chain.

Definition 5. [ 20, 7 ] An ℋℐℛ interpretation of a DL vocabulary with instanceOf ∈ is a triple ℐ = (Δℐ , · ℐ , · ℰ ) such that: 1. Δℐ = Δℐ ⊎ Δℐ ⊎ Δℐ where Δℐ , Δℐ , Δℐ are pairwise disjoint. 2. ℐ ∈ Δℐ for each ∈ , ℐ ∈ Δℐ for each ∈ , ℐ ∈ Δℐ for each ∈ . 3. For each , ∈ and ̸= (unique role assumption), ℐ ̸= ℐ . 4. ℰ ⊆ Δℐ for each ∈ Δℐ , ℰ ⊆ Δℐ ×

Δℐ for each ∈ Δℐ.

Extensions of role expressions ℰ and descriptions ℰ are inductively defined according to Table 1. Definition 6. [ 20, 7 ] An axiom is satisfied by a ℋℐℛ-interpretation ℐ (ℐ |= ) if ℐ satisfies the respective semantic constraints from Table 1. A ℋℐℛ-interpretation ℐ is a model of (ℐ |= ) if ℐ satisfies every axiom ∈ . A concept is satisfiable in if there exists a model ℐ of such that ℐ ̸= ∅ .

Decidability

Kubincova et. al.[20, 7] showed the decidability of ℋℐℛ(ℛℐ) via reduction to first-order ℛℐ.

Their reduction was based on the work done by Glimm et al.[5]

Definition 7 (First-Order Reduction). [ 7, 20 ] A DL vocabulary with instanceOf ∈ is reduced into a DL vocabulary 1 := (1 , 1, 1 ) where 1 = ⊎ {⊤ , ⊤}, 1 = , and 1 = ⊎ { | ∈ } ⊎ { | ∈ } for fresh names ⊤ , ⊤, , and for all ∈ , ∈ .

A given ℋℐℛ(ℛℐ) knowledge base in is reduced into an ℛℐ knowledge base 1 := Int() ∪ InstSync( ) ∪ Typing( ) ∪ URA( ) in 1, where: • Int() is obtained from by replacing each occurrence of ∈ and ∈ in a nominal or on the left-hand side of a concept or (negative) role assertion by and , respectively. • InstSync( ) consists of axioms ≡ ∃ instanceOf.{} for all ∈ . • Typing( ) consists of axioms ⊤ ⊑ ∀instanceOf.⊤ , ⊤ ⊑ ¬⊤ , : ¬⊤ ⊓ ¬⊤, : ⊤, and : ⊤ for all ∈ , ∈ , and ∈ .

• URA( ) consists of axioms : ¬{} for all pairs of distinct role names , ∈ .

The following theorem holds, and the corollary is implied.

Theorem 4. [ 20, 7 ] For any ℋℐℛ(ℛℐ) knowledge base and any axiom in a common vocabulary , we have |= ⇐⇒ 1 |= Int( ) .

Corollary 1. [ 20, 7 ] Let a ℋℐℛ(ℛℐ) knowledge base be such that only simple roles occur in cardinality restrictions. Concept satisfiability and entailment in a ℋℐℛ(ℛℐ) knowledge base are then decidable in N2ExpTime.

4. Subsumption metamodelling

Kubincová [ 7 ] extended instantiation metamodelling to subsumption metamodelling by introducing a ifxed subClassOf role in ℋℐℛ* (ℛℐ). This allows instanceOf and subClassOf to be used as roles at the meta-level, enabling expressive modeling of hierarchical relationships and supporting automated inference over subclass structures. Kubincová [ 7 ] demonstrated the practical utility of her framework in some domains like biological taxonomy, where complex hierarchies (e.g., Species, Genus, Family) must be precisely represented. ℋℐℛ* (ℛℐ) supports non-set-theoretical subsumption for all concepts and set-theoretical subsumption for named concepts, enhancing the expressivity of DL-based systems beyond conventional capabilities. Subsumption metamodelling has both set-theoretical and non-settheoretical interpretations. In the set-theoretical approach, the relationship subClassOf is explicitly defined by inclusion of the extension of one class within another, based on the suficient condition of subsumption, and the necessary condition focusing on the intended meaning of subClassOf: ∀∀ (∀ (instanceOf(, ) → instanceOf(, )) ↔ subClassOf(, )) .

For non-set-theoretical approaches, subsumption is defined more loosely, focusing on the intended meaning of classes rather than strict set inclusion. It is based on the necessary condition of subsumption:

∀∀ (subClassOf(, ) → ∀ (instanceOf(, ) → instanceOf(, ))) .

Kubincová [ 7 ] demonstrated the decidability of the non-set-theoretical approach for all concepts and the set-theoretical approach for named concepts. Moreso, Kubincova highlighted the practical significance of set-theoretical semantics in managing all-concept subsumptions, noting its essential role in accurately representing complex relationships, particularly in biological taxonomies. The settheoretical semantics for all concepts also enables intuitive and logically sound entailments, such as (1) ⊨ (2), and more complex inferences like (1, 3) ⊨ (4), thereby ensuring that implicit relationships are properly captured within the reasoning framework.

Species ⊑ ∃subClassOf.Genus Family ⊑ ∃subClassOf.Order

Genus ⊑ ∃subClassOf.Family Order ⊑ ∃subClassOf.Kingdom

Species ⊑ ∃subClassOf.Order Zarafa : G. camelopardalis G. camelopardalis : Species

Zarafa : ∃instanceOf.Kingdom (1)

Also, it allows to model that: if every instance of any species is an organism, ∃instanceOf.Species ⊑

Organism, then each species becomes a subconcept of the concept Organism, expressed as Species ⊑

∃subClassOf.{Organism}. 4.1. The description logics ℋℐℛ* (ℛℐ)

Kubincová et al. [7] introduced and proved the decidability of metamodelled description logics under non

set-theoretical subsumption, specifically ℋℐℛ (ℒ) and ℋℐℛ (ℒ), which handle metamodeling for named and all concepts, respectively, where ℒ is any description logic expressive up to ℛℐ.

These variants are also applicable to the logic ℛℐ and satisfy the necessary condition for the

semantics of the subClassOf role. Moreover, they established the decidability of ℋℐℛ (ℒ) for ℒ expressive up to ℛℐ, which extends the approach to set-theoretical subsumption for named concepts and fulfills both the necessary and suficient conditions for interpreting the subClassOf role. 4.2. Set-theoretical subsumption for all concepts, ℋℐℛ(ℛℐ)

Building on the work of Kubincová et al. [7] and adopting a similar nomenclature, we define the

metamodelled description logic ℋℐℛ(ℒ). This logic extends full set-theoretical semantics to all concepts, where ℒ is any logic expressive up to ℛℐ. Additionally, ℋℐℛ(ℒ) enables a unified treatment of the instanceOf and subClassOf relations across multiple meta-levels. Definition 8 (ℋℐℛ Syntax). An ℋℐℛ vocabulary is a DL vocabulary = ⊎ ⊎ such that instanceOf, subClassOf ∈ . The role expressions, concept descriptions, axioms, and knowledge bases of ℋℐℛ(ℛℐ) in are defined identically to their respective ℋℐℛ(ℛℐ) counterparts. Definition 9 (ℋℐℛ Semantics). An ℋℐℛ interpretation of a ℋℐℛ vocabulary is a ℋℐℛ interpretation ℐ = (Δℐ , · ℐ , · ℰ ) where additionally: (a) For all , ∈ Δℐ , (, ) ∈ subClassOf ℐℰ if ℰ ⊆ ℰ .

The extension of ℋℐℛ interpretation to ℋℐℛ(ℛℐ) role expressions and descriptions,

satisfaction of axioms, model, satisfiability, etc., are defined analogously to ℋℐℛ(ℛℐ).

For a fragment ℒ of ℛℐ, ℋℐℛ(ℒ) denotes the respective fragment of ℋℐℛ(ℛℐ).

4.3. Investigating the decidability of ℋℐℛ(ℒ)

This section examines how decidable fragments of FOL could be leveraged to determine the decidability

of interpreting the subClassOf relation set-theoretically for all concepts in ℋℐℛ(ℒ), as defined in

Definition 9, via a translation from description logic (DL) to FOL.

We choose the basic DL ℒ as ℒℋℐ. The choice of ℒℋℐ is due to the fact that most decidable FOL are less expressive than ℛℐ.

Rudolf [23] demonstrated the translation of the ℛℐ description logics to first-order logic with

the translation function . We apply the same translation to the DL ℒℋℐ as demonstrated in Table 2. An ℒℋℐ knowledge base is translated into a first-order theory , where concepts become unary predicates, roles as binary predicates, individuals as constants, and axioms are mapped via the function . Lemma 1. [ 14 ] Let ℒ be a description logic, 1 a knowledge base formulated in ℒ, and an axiom. Then the following equivalence holds:

⇐⇒ where is the first-order theory corresponding to 1 under the translation .

⊨ (), 1 ⊨

For an ℋℐℛ(ℒℋℐ) knowledge base, , we construct a reduced form 1SA as follows (cf. Def. 7):

1SA := 1 ∪ SubClassSync() where

1 := Int() ∪ InstSync( ) ∪ Typing( ) ∪ URA( ), based on the reduction procedure used for ℋℐℛ knowledge [ 7, 20 ]. The SubClassSync(K) axioms consist of: ∃ subClassOf.⊤ ⊑ ⊤ ⊤ ⊑ ∀ subClassOf.⊤ with the full set interpretation of the subClassOf role.

The FOL translation (1SA) of the first-order reduction 1SA except the full set-theoretic semantics of subClassOf is expressible in some decidable fragments of FOL, such as TGF and GFU. In particular, the presence of constants and partial equality ( = ) in TGF and GFU allows for the expression of the

InstSync axioms which require nominals. However, the absence of equality in Maslov’s class and

FO−3 hinders the translation of InstSync into these fragments. This issue can be remedied in Maslov’s class . Instead of equality, nominals in InstSync can be translated using substitution of variables by constants, which are supported in . Yet, FO−3 does not even admit constants.

We now examine the expressibility of the full set-theoretic semantics of subClassOf in some of these decidable fragments of FOL discussed in section 2. In order to achieve the intended semantics, the translation of the subClassOf role is governed by the following bi-conditional: which is given by the forward (→) implication: and the backward (← ) implication given by: ∀ ∀ (subClassOf(, ) ↔ ∀ (instanceOf(, ) → instanceOf(, ))) ∀ ∀ (subClassOf(, ) → ∀ (instanceOf(, ) → instanceOf(, ))) ∀ ∀ (∀ (instanceOf(, ) → instanceOf(, )) → subClassOf(, ))

This is logically equivalent to the following contrapositive form:

∀ ∀ (¬subClassOf(, ) → ∃ (instanceOf(, ) ∧ ¬instanceOf(, )))

The contrapositive of (7) is expressible in both Maslov’s class and the fragment FO−3 . This implies that the backward implication (← ) of (5) is expressible within these fragments. However, it remains uncertain whether the forward implication (→) of (5) can also be expressed in them. Furthermore, it is unclear whether either direction of (5) is expressible in the TGF (Triguarded Fragment) or the GFU (Guarded Fragment with Universal Role). (5) (6) (7) (8) (10) (11) (12) (13) (14) Counterexample Predicate and Axiomatization To facilitate reasoning about violations of the subClassOf relation, we introduce a ternary predicate subClassOfCounterExample. The predicate subClassOfCounterExample(, , ) holds implies that is a counterexample to being a subclass of , i.e., is an instance of but not of . This design is motivated by: • Constructive handling of negation: In fragments like TGF and GFU, direct expression of negated universal implications (e.g., ¬∀(instanceOf(, ) → instanceOf(, ))) is syntactically disallowed. By reifying such negations through a ternary predicate and expressing them using existential quantifiers, we preserve the intended semantics within guarded logic. • Model-theoretic transparency: The counterexample-based semantics aligns well with constructive reasoning approaches and facilitates ontology debugging and explanation by making subclass violations explicit.

This relationship is formally captured by the following axioms:

∀ ∀ (∃ subClassOfCounterExample(, , ) ↔ ¬subClassOf(, )) ∀ ∀ ∀ (subClassOfCounterExample(, , ) ↔ (instanceOf(, ) ∧ ¬instanceOf(, ))) (9)

The forward (→) implication of axiom (8) can be isolated as:

Axiom (10) is logically equivalent to the following formulation:

∀ ∀ (∃ subClassOfCounterExample(, , ) → ¬subClassOf(, )) ∀ ∀ (subClassOf(, ) → ¬(∃ subClassOfCounterExample(, , )))

The backward (← ) implication of axiom (8) is given by:

∀ ∀ (¬subClassOf(, ) → ∃ subClassOfCounterExample(, , ))

The forward (→) of (9) is given by:

∀ ∀ ∀ (subClassOfCounterExample(, , ) → (instanceOf(, ) ∧ ¬instanceOf(, ))) while the backward (← ) implication of (9) is given by: ∀ ∀ ∀ ((instanceOf(, ) ∧ ¬instanceOf(, )) → subClassOfCounterExample(, , ))

While formulas (10)–(13) are expressible within the TGF and GFU fragments, we are not certain formula (14) is expressible in TGF or GFU and thus does not allow for the indirect expression of axiom (5) within these fragments.

4.4. Discussion We analyze the reduction strategy and its translation to some decidable fragments of FOL. Axiom (7), which captures semantic inclusion between universal instance inclusion and the subClassOf relation, is expressible in Maslov’s class and the fragment FO−3 . This confirms that the backward direction (← ) of (5) is expressible in these fragments. However, the expressibility of the forward direction (→) remains unclear. Likewise, it is uncertain whether either direction of (5) is expressible in the TGF or GFU fragments. Nonetheless, the introduction of the subClassOfCounterexample predicate allows for the derivation of (8) and (13), indirectly enabling the backward direction of (5) in TGF and GFU fragments.

Still, the status of (14) remains unresolved, casting doubt on full expressibility in TGF or GFU fragments.

The TGF fragment approximates the expressive power of ℒℋℐ [24]. In contrast, Maslov’s class

corresponds to the description logic ℒ extended with role conjunction, inverse roles, and positive role composition, while explicitly excluding equality. Similarly, the FO−3 fragment [ 21 ] also extends ℒ with constructs comparable to those found in Maslov’s class . Table 3 provides a summary of the semantics of the subClassOf relation with respects to the fragments explored.

5. Conclusion

We have explored the decidability of the higher-order description logic ℋℐℛ(ℒ), instantiated for the base logic ℒℋℐ, which incorporates metamodelling capabilities through semantically fixed roles for instantiation and subsumption. By introducing the ternary predicate subClassOfCounterExample, we captured the counterexample-driven semantics of subclass relations in a form that is partially expressible within the Triguarded Fragment (TGF) and the Guarded Fragment with Universal Role (GFU). Our expressivity analysis demonstrated that these subclass semantics are partially expressible within Maslov’s class and the fragment FO−3 . Consequently, the decidability of the higher-order description logic ℋℐℛ(ℒ) for an arbitrary base logic, ℒ remains an open question.

Acknowledgments

This research was sponsored by the Slovak Republic under the SRDA grant APVV-23-0292 (DyMAX)

and VEGA grant no. 1/0630/25 (eXSec), and it is also based on the work from COST Action CA23147

GOBLIN. Z. Adams was supported by the grant no. UK/1225/2025 awarded by Comenius University in

Bratislava.

Declaration on Generative AI

During the preparation of this work, the authors used Chat-GPT-4 for grammar and spelling check.

After using this tool, the authors reviewed and edited the content as needed and takes full responsibility for the publication’s content.

19th to 22nd, 2021, volume 2954 of CEUR Workshop Proceedings, CEUR-WS.org, 2021. URL: https: //ceur-ws.org/Vol-2954/abstract-21.pdf. [23] S. Rudolph, Foundations of description logics, in: Reasoning Web. Semantic Technologies for the Web of Data - 7th International Summer School 2011, Galway, Ireland, August 23-27, 2011,

Tutorial Lectures, volume 6848 of Lecture Notes in Computer Science, Springer, 2011, pp. 76–136.

doi:10.1007/978-3-642-23032-5\_2. [24] E. Kieronski, A. Malinowski, The triguarded fragment with transitivity, in: LPAR 2020: 23rd

International Conference on Logic for Programming, Artificial Intelligence and Reasoning, Alicante,

Spain, May 22-27, 2020, volume 73 of EPiC Series in Computing, EasyChair, 2020, pp. 334–353. URL:

https://doi.org/10.29007/z359. doi:10.29007/Z359.

References

[1] F. Baader , W. Nutt, Basic description logics , in: F. Baader , D. Calvanese , D. L. McGuinness , D. Nardi , P. F. Patel-Schneider (Eds.), The Description Logic Handbook: Theory , Implementation, and Applications , Cambridge University Press, Cambridge, UK, 2003 , pp. 43 - 95 .

[2] S. Staab , R. Studer (Eds.), Handbook on Ontologies, 2nd ed., Springer Publishing Company, Incorporated, 2009 .

[3] P. Hitzler , M. Krötzsch , S. Rudolph , Foundations of Semantic Web Technologies, Chapman & Hall/CRC, 2009 .

[4] B. Motik , On the properties of metamodeling in OWL , Journal of Logic and Computation 17 ( 2007 ) 617 - 637 .

[5] B. Glimm , S. Rudolph , J. Völker , Integrated metamodeling and diagnosis in OWL 2 , in: Proceedings of the International Semantic Web Conference (ISWC) , 2010 .

[6] M. Homola , J. Kľuka , V. Svátek , M. Vacura , Typed higher-order variant of SROIQ - why not? , in: Proceedings of the 2014 International Workshop on Description Logics (DL) , 2014 .

[7] P. Kubincová , Higher-order description logics for metamodelling , Master's thesis , Comenius University Bratislava, 2016 .

[8] W. Chen , M. Kifer , D. S. Warren , A foundation for higher-order logic programming , Journal of Logic Programming 15 ( 1993 ) 187 - 230 .

[9] L. Badea , Reifying concepts in description logics , in: Proceedings of the 15th International Joint Conference on Artificial Intelligence (IJCAI'97) , 1997 , pp. 142 - 147 .

[10] E. Rohrer , P. Severi , R. Motz , A. Díaz , Metamodelling in an ontology network , in: Proceedings of the 8th International Workshop on Modular Ontologies (WOMO) , CEUR-WS.org , 2014 .

[11] J. Z. Pan , I. Horrocks, G. Schreiber, OWL FA: A metamodeling extension of OWL DL, in: Proceedings of the OWL: Experiences and Directions Workshop (OWLED) , 2005 .

[12] L. Henkin , Completeness in the theory of types , Journal of Symbolic Logic 15 ( 1950 ) 81 - 91 .

[13] G. D. Giacomo , M. Lenzerini , R. Rosati , Higher-order description logics for domain metamodeling , in: Proceedings of the Twenty-Fifth AAAI Conference on Artificial Intelligence (AAAI-11) , AAAI Press, 2011 .

[14] S. Rudolph , Foundations of Description Logics, Technical Report , Karlsruhe Institute of Technology, Germany, 2011 .

[15] E. Grädel , P. G. Kolaitis , M. Y. Vardi , On the decision problem for two-variable first-order logic , Bulletin of Symbolic Logic 3 ( 1997 ) 53 - 69 .

[16] E. Börger , E. Grädel, Y. Gurevich , The Classical Decision Problem , Springer, 1997 .

[17] O. Fiuk , E. Kieronski, Alternating quantifiers in uniform one-dimensional fragments with an excursion into three-variable logic , Journal of Symbolic Logic ( 2024 ).

[18] S. Rudolph , M. Simkus , The triguarded fragment of first-order logic , in: LPAR-22. 22nd International Conference on Logic for Programming , Artificial Intelligence and Reasoning , Awassa, Ethiopia, 16 -21 November 2018 , volume 57 of EPiC Series in Computing, EasyChair, 2018 , pp. 604 - 619 . URL: https://doi.org/10.29007/m8ts. doi: 10 .29007/M8TS.

[19] O. Fiuk , E. Kieronski , V. Michielini , On the complexity of Maslov's class K , in : Proceedings of the 39th Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2024 , Tallinn, Estonia, July 8- 11 , 2024 , ACM, 2024 , pp. 35 : 1 - 35 : 14 . URL: https://doi.org/10.1145/3661814.3662097. doi: 10 .1145/3661814.3662097.

[20] P. Kubincová , J. Kl'uka, M. Homola, Expressive description logic with instantiation metamodelling , in: Proceedings of the Fifteenth International Conference on Principles of Knowledge Representation and Reasoning (KR 2016 ), AAAI Press, Cape Town, South Africa, 2016 , pp. 569 - 579 .

[21] U. Hustadt , R. A. Schmidt , B. Motik , L. Georgieva , A survey of decidable first-order fragments and description logics , Journal on Relational Methods in Computer Science 1 ( 2004 ) 251 - 276 .

[22] E. Kieronski , S. Rudolph , Finite model theory of the triguarded fragment and related logics (extended abstract) , in: Proceedings of the 34th International Workshop on Description Logics (DL 2021 ) part of Bratislava Knowledge September (BAKS 2021 ), Bratislava, Slovakia, September