The deployment of Knowledge Representation and Reasoning technologies in aeronautics applications poses two primary challenges: achieving suficient expressivity to capture complex domain knowledge and executing reasoning tasks eficiently while minimizing memory usage and computational overhead. An efective strategy for achieving the necessary expressivity involves integrating two fundamental KRR concepts: Description Logics(DLs) and Logic Programming(LP). The main objective of this thesis is to select a unified semantics for integrating DLs and LP, with a particular focus on its applicability and adaptability to the aeronautics domain. The chosen language will be studied in the context of representative aeronautics use cases, identifying challenges that arise during its adaptation. Based on these findings, the thesis will propose appropriate extensions to the unified semantics. Furthermore, an optimized reasoner will be developed with respect to the extended semantics. Finally, comprehensive user manuals and guidelines will be provided to assist knowledge engineers in modeling and implementing various aeronautics use cases using the proposed language.
The aeronautics industry is recognized as a safety-critical domain, which implies that system malfunctions can have safety consequences. Therefore, software systems used in this industry must exhibit reliable, robust, and explainable characteristics to prevent such outcomes. Additionally, many software systems in this field operate on resource-constrained hardware, such as microcontrollers. In this context, knowledge representation and reasoning (KRR) systems hold significant promise because they enable systems to produce transparent and explainable decisions. With the assistance of domain experts, knowledge specific to aeronautics applications can be captured using formal representation languages, such as ontologies. This knowledge contains critical operational information and is integrated with real-time data to make timely decisions through logical reasoning. However, adapting the KRR system to the aeronautics domain presents several significant challenges. These challenges include ensuring suficient expressivity to encapsulate all complex domain knowledge and efectively executing necessary reasoning tasks with limited computational resources and minimal latency.
An efective strategy for tackling the expressivity challenge is the integration of rules and ontologies, which is a well-explored area of research. Ontologies, generally grounded in Description Logics (DLs), operate under the open-world assumption (OWA), which means that the absence of information does not imply its negation. They are used to encapsulate general domain knowledge through concepts and their relationships [1]. Conversely, Logic Programming (LP) rules operate under the closed-world assumption (CWA), which presumes that what is not known to be true is considered false. These rules are utilized to represent knowledge through if-then relationships [2]. Owing to their complementary characteristics, the integration of DLs and LP rules enhances the expressiveness of the resultant KRR, which is termed a hybrid knowledge base.
Motivation: To build an efective reasoning system that integrates DLs and LP, it is essential to adopt a suitable semantics that harmoniously combines the strengths of both paradigms. This hybrid semantics must integrate the strengths of both DLs and LP while ensuring semantic compatibility between them. Also, a reasoner must be implemented that is both sound and complete with respect to the chosen semantics to perform query answering answering. While query answering, the reasoner should exhibit strong performance characteristics, particularly low latency for query responses and high throughput for handling large volumes of data. Finally, to ensure broad applicability, especially in embedded or resource-constrained environments, the implementation should be optimized for minimal resource consumption, enabling lightweight and eficient operation even on platforms such as micro-controllers. Use Case: We present a use case in the aeronautics domain that necessitates the integration of DLs with LP rules. We propose a system known as the NOTAM-Aware Reasoning System (NARS). Prior to a flight’s departure, pilots must manually review all Notices to Airmen(NOTAM), which are oficial advisories that convey time-sensitive changes such as runway closures, airspace restrictions, or technical malfunctions, to ensure that the flight plan remains consistent with real-world. A NOTAM message typically contains crucial information, including what is afected—such as runways, airspace, or environmental changes—the location, validity time period, and the authority issuing the notice. All of these details are essential for helping pilots to plan their flights safely. For example, if a NOTAM indicates that the arrival runway, the specific runway designated for landing a flight at a given time, is closed during the scheduled landing period. In this case, the pilot must first identify the issue while reviewing hundreds of NOTAMs, and then plan the flight accordingly. Several agencies assist pilots in this review process. This manual verification and decision-making process is both time-consuming and susceptible to human error. NARS addresses this problem by reviewing NOTAMs and suggesting updates to the pilot when it detects real-world changes afecting the flight plan. The knowledge base for NARS can be constructed using a hybrid KRR system. On the DL side, static and hierarchical domain knowledge, such as airport infrastructure, diferent types of runways, and airspace zones can be represented. This structured knowledge provides a formal vocabulary to describe entities and their relationships-for example, stating that "a runway is part of an airport". In contrast, LP handles dynamic knowledge, which is encoded as conditional if-then rules. For instance, a rule might specify that "if a runway is closed during the scheduled landing time, then an alternate runway should be proposed"; or "if critical equipment at an airport is out of service, the flight operations team must be notified".
Section 2 presents existing approaches for combining DLs and LP, along with a brief justification for the selected formalism. Section 3 outlines the research plan with a timeline. Sections 4 and 5 introduce the chosen language, Hybrid MKNF, and its reasoner, NoHr, followed by a performance evaluation. Section 6 discusses the limitations of the current Hybrid MKNF framework based on the use case. Section 7 presents the results achieved so far, Section 8 outlines the ongoing work, and Section 9 proposes future research directions.
In general, three main approaches exist for combining DLs with LP: loose integration, tight integration, and full integration [3]. Each of these integration strategies can be based on one of two major semantics: well-founded [4] or answer set semantics [5].In loose integration, a DL ontology and LP rules are treated as distinct components, with an interface enabling controlled knowledge exchange. A prominent approach in this category is DL-Programs, which have been extensively studied under both answer set semantics [6] and well-founded semantics [7]. Knowledge exchange in DL-Programs is realized exclusively through external operators, i.e., additional constructors that mediate interaction between the DL ontology and the rule component. These operators necessitate supplementary rules, thereby increasing the language’s complexity for knowledge engineers. For example, consider the DL axiom stating that a flight with an open arrival runway is an on-time flight:
(
Rwy(rw1).
To represent the default assumption that all runways are open unless explicitly known to be closed, we
define a DL-Program rule:
opnRwy() ← DL[Rwy](), not DL[CldRwy]().
(
The only reasoning task in DL-Programs is model checking, that is, verifying whether a given interpretation satisfies the axioms and rules of the knowledge base.Then the computed model is stored in a database for query answering. However, this approach is not memory-eficient, as it requires computing and storing the full model. Nonetheless, DL-programs ofer the benefit of integrating with external data sources, such as Python programs or relational databases. An extended language known as HEX [8], along with its corresponding reasoner, DLV-Hex [9], supports this integration. Moreover, the DReW system [10] provides an optimized DL-Program reasoner by exploiting Datalog-rewritable DLs such as ℒℒ+ [11] and ℛℰ ℒ [12]. An alternative loose integration approach, known as F-Logic#, combines F-Logic with DL ontologies [13].
In tight integration, reasoning is performed with respect to an integrated model that simultaneously satisfies both the DL ontology and the LP rules. Formally, such a model is defined as = ∪ , where is a model of the DL ontology and is a model of the LP program. The construction of begins with a candidate DL model . Using , the grounded LP program is simplified in two steps. First, any rule whose body contains DL atoms that evaluate to false in is discarded, since such rules cannot be satisfied. Second, for the remaining rules, DL atoms that evaluate to true in are removed from the body, as they are already satisfied. This yields a residual LP program that no longer contains DL atoms. A model of this simplified program is then computed under either answer set or well-founded semantics. The procedure is repeated for each possible DL model , producing a corresponding LP model in each case. Several hybrid languages have been proposed in the literature to realize this notion of tight integration. Notably, R-Hybrid KB [14] and DL+Log [15] are founded on answer set semantics, while HD-Rule is based on well-founded semantics [16]. Furthermore, an extension of DL+Log has been introduced, which incorporates closed-world predicates within a DL ontology, leading to the creation of clopen knowledge base [17]. Additionally, Resilient Logic Programs (RLP) have been proposed to merge both tight and loose integration, where loose integration shares only logical consequences between DL and LP, while tight integration enables knowledge sharing between individual models [18]. In tight integration, even when employing well-founded semantics, numerous possible models may exist, complicating the reasoning process. Consequently, constructing a practical reasoner under these conditions is challenging. Additionally, the knowledge engineer must possess an understanding of individual models of DLs to generate the corresponding rule program due to the model-based integration between DL and LP, further complicating the knowledge engineering process.
In full integration, a singular unifying non-monotonic formalism is defined to encapsulate both the semantics of DLs and LP. Several non-monotonic extensions of first-order logic have been proposed, including default logic, epistemic logic, defeasible logic, and circumscription. Ideally, selecting one of these extensions to integrate both DL and rules constitutes the fundamental concept of this approach. In Full Integration, we encountered on works grounded in Minimal Knowledge and Negationas-a-failure(MKNF), Open-Answer Set Programming (OASP) [19], and Defeasible Logics [20]. We intentionally excluded a significant array of research that merge DLs with first-order rules, such as SWRL [21], AL-Log [22], Carin [23], due to their lack of closed-world reasoning capabilities. Given the undecidability of OASP, several decidable variants have been proposed. These include the F-Hybrid Knowledge Base, which integrates ℋ DL with a finite set of Forest Logic Programs (FLP) [ 24]. These programs allow only unary and binary predicates and adhere to the forest-model property. Additionally, the G-Hybrid Knowledge Base combines ℒℛ−{≤} with a finite set of ASP rules that comply with the guardness restriction, wherein each rule contains a guarded predicate, and all variables within the rules must appear in that predicate [25]. In this context, Hybrid MKNF ofers a more general and expressive formalism that integrates DLs and LP [26], as it is based on a unified language that seamlessly combines both paradigms.
Selection: In loose integration approaches such as DL-Programs and F-Logic#, information exchange from LP rules to the DL component is managed through additional operators. This process can be very complex for knowledge engineers, especially when dealing with large knowledge bases. Furthermore, reasoning often requires computing the entire model to answer queries, leading to high memory consumption. Consequently, any update to the knowledge base necessitates recomputing the model from scratch, making this approach impractical for the aeronautics domain. Similarly, in tight integration systems, as discussed earlier, multiple models may exist—even under well-founded semantics. This multiplicity complicates the construction of eficient reasoners. Moreover, among tight integration languages, only HD-Rules supports top-down query answering; other languages rely on answer set semantics and focus solely on model computation as their reasoning task. This again results in high memory usage. A further limitation of HD-Rules is that information flow is only supported from DL to LP, not vice versa, which restricts their applicability. Therefore, languages based on these methodologies are not ideal for the aeronautics domain. In the case of full integration, as in certain fragments of open answer set programming, strong syntactic restrictions are imposed to guarantee decidability. However, these restrictions introduce significant overhead in knowledge engineering. Considering these limitations, Hybrid MKNF emerges as a more general and expressive semantics combining DL and LP in a unified framework. Due to these reasons, we chose Hybrid MKNF as the KRR approach best suited for the aeronautics domain.
The research began with a comprehensive study of the theoretical foundations of LP, including diferent types of LP rules, various semantics (such as stable model and well-founded semantics), and associated reasoning tools. A similar study was conducted for DLs, covering their syntax, semantics, reasoning algorithms, and existing implementations. This stage was referred to as the Foundation Phase. Following this, we explored existing research on the integration of DLs and LP. We first identified general approaches used to unify their semantics and then analyzed the main languages proposed in each category. This extensive literature review constituted the Survey Phase, during which we studied the theoretical foundations, strengths, and limitations of each approach.
Based on insights from the survey, we proceeded to select a hybrid language that was most suitable for the aeronautics domain. We implemented simple aeronautics use cases using diferent hybrid knowledge representation languages to support the selection process. The selection was guided by three key factors: combining the strengths of DL and LP with bidirectional information exchange, supporting eficient knowledge engineering (i.e., imposes minimal syntactic restrictions, while remaining accessible and comprehensible to knowledge engineers), and enabling the development of an optimized reasoner for eficient query answering. After reviewing the benefits and limitations of existing languages, we chose Hybrid MKNF because it provided a more general and expressive framework that integrates DLs and LP. Moreover, it supported a well-founded semantics, which enabled the implementation of eficient top-down query answering. This process formed the Selection Phase. Once the language was chosen, we moved to the Experimentation Phase. In this phase, we evaluated the availability and performance of existing reasoners for the selected language and implemented more complex aeronautics use cases to assess its practical suitability. Based on the results from experimentation, we propose optimization strategies to improve the eficiency of existing Hybrid MKNF reasoner implementations. We will also identify additional expressivity requirements emerging from these use cases. To address these needs, we will propose extensions to the chosen Hybrid MKNF framework. The main features of these extensions will include classical negation, allowing explicit representation of negative knowledge in the LP component. A complete theoretical study, including semantics, computation methodology, and query answering algorithms, is currently being conducted as part of ongoing work. Other proposed extensions will include integrity constraints, enabling knowledge engineers to enforce conditions on query answers, and date-and-time reasoning, which will be essential for handling NOTAMs, each of which has a start and end time, ensuring that decisions respect these constraints. Additionally, we will enable the reasoner to generate justifications for each query answer. The timeline of my research, reflecting both the current plan and the results achieved so far, is illustrated in figure 1.
We chose Hybrid MKNF as the knowledge representation language to DLs and LP for the aeronautics domain. We now provide a detailed overview of Hybrid MKNF. The Hybrid MKNF, as introduced in [26], is based on the logic of Minimal Knowledge and Negation as a Failure (MKNF), an extension of first-order logic that incorporates two modal operators, namely K and not originally described in [27]. The K operator denotes knowledge known by the system, whereas the not operator signifies knowledge not known by the system, functioning analogously to default negation in logic programming and facilitating closed-world reasoning. A Hybrid MKNF under well-founded semantics, = (, ) where O is a DL ontology and P is the set of MKNF rules of the form [28]: ←
1, . . . , , 1, . . . , .
where , for 1 ≤ ≤ , and for 1 ≤ ≤ are first-order atoms. The rule (
OpnRwy ⊑ Rwy CldRwy ⊓ OpnRwy ⊑ ⊥ CldRwy() ← NOTAM(), affdBy(, ), Rwy( ), opStat(, closed).
OpnRwy() ← Rwy(), CldRwy().
recommendDelay() ← Flight(), hasDepartureAirport(, ), OpnAirport( ). (
Rule (
∀( Rwy() ← OpnRwy()). (
Truth evaluation of first-order atoms with modal operators, in relation to the three-valued MKNF model, proceeds as follows. An atomic formula (1, . . . , ) is evaluated as true under a first-order interpretation if the tuple (1 , . . . , ) is an element of the interpretation of the predicate in , denoted ; formally, if (1 , . . . , ) ∈ . Otherwise, the formula is evaluated as false when (1 , . . . , ) ∈/ . The implication 1 ⊃ 2 is evaluated as true if the truth value of 2 is greater than or equal to that of 1 with respect to the order < < , and false otherwise. The truth value of is true if evaluates to true in all interpretations in , false if evaluates to false in some interpretation in ⊆ , and undefined otherwise. Similarly, not is true if is false in some interpretation in ⊆ , false if is true in all interpretations in , and undefined otherwise [28].
An MKNF interpretation pair (, ) satisfies a closed MKNF formula , denoted (, ) |= , if and only if (, )( ) = , meaning that all rules within evaluate to true under this interpretation. An MKNF interpretation pair (, ) is considered a three-valued MKNF model for a formula if it satisfies two key conditions. First, it must satisfy the formula itself. Second, it must be minimal in the sense that one cannot extend or to larger interpretation pairs that still satisfy . The only three-valued model of 1:M = {{Rwy(rw1),OpnRwy(rw1)},{Rwy(rw1),OpnRwy(rw1),CldRwy(rw1)}},N = {{Rwy(rw1),OpnRwy(rw1)}}.
Consider an MKNF formula . A partial three-valued MKNF model (, ) is called the well-founded
model of if and only if, for every other three-valued MKNF model (1, 1) of , the relation
(1, 1) ⪰ (, ) holds, meaning 1 ⊆ and 1 ⊇ . For every MKNF formula there exist only
one well-founded three-valued model.
4.2. Query Answering
The alternating fixed-point method provides a bottom-up strategy for computing the three-valued,
wellfounded model of a Hybrid MKNF knowledge base [28]. Initially, this model must be computed using
the proposed bottom-up approach. Once computed, it can be stored in a database for querying purposes.
However, this method is impractical for large knowledge bases, particularly when only specific parts of
information are relevant. To address this issue, a query answering algorithm called SLG(O) resolution
has been proposed, which is both sound and complete with respect to the well-founded Hybrid MKNF
model. SLG(O) resolution is a goal-directed query answering that employs SLG resolution to manage
LP rules, where O acts as the oracle responsible for handling queries related to the DL component
[30]. The resolution process begins with a query that is matched against the rule head, subsequently
generating new subgoals derived from the body of that rule. When a subgoal corresponds to a DL atom,
the system invokes the DL oracle to determine whether the atom is entailed by DL. Throughout the
process, tabling is used to store the intermediate results, thereby preventing infinite loops and ensuring
termination. Before implementing the SLG(O) resolution, a knowledge-based doubling step must be
conducted to align with the bottom-up computation of the well-founded MKNF model [30]. Consider
= (, ) be a Hybrid MKNF knowledge base and in [30] introduce new predicates and
for each predicate appearing in , and then constructively define:
1. by substituting each concepts or role in by ; and
2. by transforming each rule of form (
i ← ii(a) ← ii(b) ← 1, . . . , , 1, . . . , and either, 1, . . . , , 1, . . . , , if is a DL concept or role; or 1, . . . , , 1, . . . , otherwise.
The doubled Hybrid MKNF knowledge base is defined as = (, , ). In this transformation, each original predicate in the knowledge base is paired with two predicates, and , where indicates the non-falsity of . In addition, a new predicate , semantically equivalent to the classical negation ¬, is introduced. This predicate prevents the derivation of when ¬ is entailed in the ontology. To enforce this, not is added to the body of every rule, with as its head, ensuring that can only be inferred when ¬ is not supported by the ontology. This transformation process is called a semi-negative transformation. It aids in verifying MKNF consistency by identifying cases where is true but is not. In such instances, because is true and is false, it follows that ¬ is entailed by DL ontology O, leading to inconsistency.
An existing implementation of Hybrid MKNF is the NoHr reasoner. NoHr employs SLG(O) resolution, which fundamentally translates the doubled Hybrid MKNF knowledge base into logic programming rules [31]. This method facilitates eficient reasoning through query answering using XSB Prolog. Specifically, the doubled Hybrid MKNF knowledge base, represented as = (, , ), is converted into a semantically equivalent form: = (∅, ∪ ), where is the doubled logic program, and is the DL ontology translated into equivalent set of rules, followed by knowledge base doubling. The NoHr reasoner employs two distinct translation methodologies to convert DL into rules. First, a classification algorithm is used to deduce subsumption relationships, which are then translated into LP rules[32]. For classification, NoHr integrates three existing DL reasoners: ELK, Hermit, and Konclude, with Hermit and Konclude supporting more expressive DL constructors. Second, for the QL profile, a direct translation method was applied to convert DL axioms into Logic Programs without the need for prior classification[ 33]. We chose to focus on the classification-based translation with HermiT reasoner, as it supports more expressive DL constructors than the QL. The various steps involved in the NoHr reasoner with classification-based translator are illustrated in figure 2.
Consider DL axioms (
Rwy() ← OpnRwy().
Rwy() ← OpnRwy(), NRwy().
(
The combination of knowledge base doubling and semi-negative transformation enables a
paraconsistent-like behavior in the NoHR reasoner, allowing reasoning to continue even when parts of
the knowledge base are inconsistent by isolating and reasoning over consistent fragments. In a Hybrid
MKNF knowledge base, inconsistencies occur when both an atom and its classical negation ¬ are
derivable. For example, consider adding the two assertions OpnRwy(rw1) and cldRwy(rw1).
According to DL axiom (
OpnRwy(1) ← NOpnRwy(1).
CldRwy(1) ← NCldRwy(1).
(18) (19)
OpnRwy(1).
CldRwy(1).
Using rule (
Below, we outline the consistency resolving techniques employed by the NoHr reasoner. Consider a conjunctive query of the form: () ← 1, 2, . . . , , 1, 2, . . . , where 1, 2, . . . , , 1, 2, . . . , represent the conjunction of predicates being queried within the context of a Hybrid MKNF framework. To address the paraconsistent feature, the query is transformed into two distinct queries: () ← 1, 2, . . . , , 1, 2, . . . , and () ← 1, 2, . . . , , 1, 2, . . . , . Consistent answers were identified by querying the prolog engine with: () ∧ () While Inconsistent answers were determined using: () ∧ (). This approach enables the system to manage contradictions by distinguishing between consistent and inconsistent results, to ensure that contradictions do not invalidate the reasoning process.
Evaluation: A thorough evaluation of the NoHr reasoner is crucial for its deployment in aeronautics, where real-time performance and reliability are essential. Key evaluation criteria include: (i) identifying the supported DL constructors to aid ontology modeling; (ii) measuring preprocessing time for ontologies and rules, to assess readiness after updates or reboots; (iii) analyzing query response latency, which must remain under one second due to safety-critical requirements; and (iv) assessing resource usage, as the reasoner may run on devices with limited memory and CPU capacity.
To analyze the preprocessing delay of the DL component, we utilized the OWL2Bench benchmark, which is an extension of LUBM dataset designed to generate DL ontologies of varying sizes across four OWL profiles: EL, QL, RL, and DL[ 34]. We use this benchmark to evaluate the DL part with the NoHr reasoner. For the logic program component, we employed the benchmark provided by the NoHr reasoner, which generates "n" number of rules based on an associated DL ontology. For each DL ontology generated from the OWL2Benchmark, utilizing the rule benchmark provided by the NoHR reasoner, rules are generated in quantities of 10, 100, 1,000, 10,000, and 25,000. The rule benchmark is available here:https://github.com/NoHRReasoner/NoHR/tree/master/nohr-benchmark and OWL2Bench is available here:https://github.com/kracr/owl2bench. For query evaluation, we used the set of queries provided with the LUBM benchmark, making minor modifications to match the structure and vocabulary of the DL ontologies generated by the OWL2Bench benchmark. These were then converted into equivalent queries compatible with a prolog engine. Queries are available here for reference:https://swat.cse.lehigh.edu/projects/lubm/queries-sparql.txt.To evaluate memory consumption and CPU utilization, we use ontology files containing varying numbers of axioms. The measurements focus exclusively on the query answering phase of the NoHR reasoner. Evaluation Summary: During the ontology preprocessing phase, a considerable amount of time is devoted to ontology classification and XSB loading, both of which are significantly afected by the number of DL axioms (figure 2). In the rule processing stage, the XSB loading time is directly proportional to the size of the translated ontology (figure 4). During preprocessing, we also noted increased memory usage and CPU utilization, both of which were correlated with the size of the knowledge base (figure 3). Once preprocessing is complete, query answering with XSB-Prolog becomes highly eficient, particularly for selective queries that filter results based on specific conditions and return only a small subset of answers (figure 5). However, we observed a noticeable decline in the performance of queries that required reasoning over recursive rules. Certain DL constructors, such as Equivalence Relationships and Transitive Properties, are translated into recursive rules, which significantly afect performance. Furthermore, elevated memory usage persisted in the query-answering phase (figure 5 and figure 7).
The primary objective of this thesis is to develop a KRR system tailored for the aeronautics domain. We have selected Hybrid MKNF under well-founded semantics from existing state-of-the-art approaches due to its strong reasoning capabilities and a prototype reasoner is already available. The next step is to adapt this framework for practical use in aeronautics context and to propose necessary extensions to enhance the feature of Hybrid MKNF. The following paragraph analyzes the main challenges involved in adapting Hybrid MKNF to meet these real-world requirements.
Problem 1: The NoHr reasoner is an existing system based on Hybrid MKNF under well-founded semantics. However, our evaluation shows that it consumes significant computational resources, which can limit its applicability in resource-constrained environments,which may restrict its practical use in aeronautics applications. To make it suitable for this domain, further optimization techniques are essential to enhance its performance and ensure eficient, reliable reasoning in real-world aeronautical environments.
Problem 2: One missing feature is the explicit representation of negative knowledge within the logic programming component of Hybrid MKNF. Consider the following use case: A runway is operational only if there is no NOTAM indicating that it is closed, and no obstacle is present on the runway. This can be initially represented by the following MKNF rule: OpnRwy(X) ← Rwy(X), ob(A,X), CldRwy(X). (20) However, due to the safety-critical nature of aeronautics, the predicate ob(A,X) which indicate that there exist an obstacle for a runway X in an airport A, carries particular importance. Using not operator with ob(A,X) to infer that a runway is operational introduces safety concerns because it relies on the absence of evidence rather than explicit confirmation. Such assumptions are unacceptable in this domain. Instead, we must explicitly verify that the runway is free of obstacles, thereby enhancing the reliability of the system. One way to achieve this is by replacing the not operator with classical negation denoted as ¬.
Classical negation can be incorporated into existing Hybrid MKNF semantics via syntactic transformation for unary and binary predicates. For a unary predicate , we introduce a new concept with the axiom ≡ ¬ in DL, allowing to stand for the classical negation of within rules. For a binary predicate , a corresponding predicate is created, and the disjointness axiom ⊓ ⊑ ⊥ enforces that represents the classical negation of . However, this approach requires additional knowledge engineering and is limited to unary and binary predicates. Extending the rule component with classical negation enhances expressiveness, simplifies knowledge engineering, and facilitates the modeling of critical scenarios, such as the one illustrated above. After the extension of classical negation , the rule (20) can be rewritten as: OpnRwy(X) ← Rwy(X), ¬ob(A,X), CldRwy(X). (21) Problem 3: Another crucial feature currently lacking is the capability to represent integrity constraints within the knowledge base and enforce them during query answering. Consider NARS use case, many NOTAMs are incomplete or invalid. A NOTAM may lack crucial information such as location, efective time, or activity description. These incomplete NOTAMs must be excluded from the reasoning process to avoid producing misleading or inconsistent conclusions. To handle this, we formally define the conditions that constitute a valid NOTAM and represent them as integrity constraints in the knowledge base. This allows the reasoning engine to automatically detect and disregard invalid NOTAMs before any inference or query answering is performed.
Problem 4: Providing justifications for all decisions derived from Hybrid MKNF reasoning is vital, especially given the safety-critical nature of aeronautics. It is essential to develop formal methods that can provide clear and reliable explanations for each query answering result, capabilities that are currently unavailable.
As a first step, we began addressing the problems explained in Section 4 by leveraging existing stateof-the-art methods. Optimizing a reasoner for hybrid MKNF, while proposing extensions such as classical negation and integrity constraints, involves substantial theoretical work. Therefore, as an initial approach, we proposed extensions based on syntactic transformations, allowing us to solve these problems within the existing semantics and provide an initial solution.
Handling Classical Negation: A syntactic transformation inspired from [35, 36], We extend Hybrid
MKNF knowledge bases = (, ) to support classical negation in P by replacing each negated
atom ¬ with a fresh predicate ′ and adding constraints ⊥ ← , ′ to ensure consistency. This
leads to a modified knowledge base, ′ = (, ′ ∪ ) where ′ is updated program by replacing
the classically negated atoms and constraints in the form ⊥ ← , ′.Subsequently, knowledge base
doubling and semi-negative transformation are applied as described in [30], resulting in the doubled
knowledge base ′ = (, , ′ ∪ ), as outlined below:
1. is obtained by substituting each predicate in with ;
2. is derived by transforming each rule of the form (
We hypothesize that this syntactic transformation maintains semantic equivalence, consistent with the existing state of the art. A formal explanation and theoretical study, including proof, are ongoing and planned as part of future work. This transformation enables the use of existing Hybrid MKNF query answering methods. After the knowledge base doubling, we can use consistent and inconsistent query answering with the steps defined in Section 5.
Consider the Hybrid MKNF knowledge base = (, ), where contains an assertion Rwy(rw1) and includes rules (21) and a fact: ¬ob(ifbo,rw1) . These rules can be transformed into the following rules as per the syntactic transformation, resulting in the modified knowledge base ′ = (, ′ ∪ ) as shown below(only logic programming part is provided): OpnRwy(X) ← Rwy(), ob′(, ), CldRwy().
⊥ ← ob(, ), ob′(, ).
ob′( , 1).
After knowledge base doubling and semi-negative transformation we get ′ = (, , ′ ∪ ): (22) (23) (24) (25) (26) opnRwy(X) ← rwy(), ob′(, ), cldRwy().
opnRwy() ← rwy(), ob′ (, ), cldRwy(), NopnRwy(). Nob(, ) ← ob′(, ). Nob′(, ) ← ob(, ).
(27) (28)
ob′( , 1). (29) ob′ ( , 1) ← Nob′( , 1). (30)
After applying all transformations, we obtain the modified knowledge base ′ = (, , ′ ∪ ),where all occurrences of classical negation within the rules are syntactically eliminated. By adding the assertion rwy(rw1), we can infer opnRwy(rw1) because there is an explicit negative fact indicating the absence of an obstacle, specifically ¬ob(lfbo,rw1), and no closure is indicated. Now, consider a scenario of inconsistency where an additional assertion ob(lfbo,rw1) is introduced, which also needs to be doubled. In this case, ob(lfbo,rw1) becomes inconsistent because both the atom and its classical negation are simultaneously true. In such a situation, the rules defined in (27) and (28) ensure that both Nob(, ) and ob′(, ) are inferred to be true. Consequently, due to the semi-negative transformation, both ob′ ( , 1) and ob( , 2) are inferred as false. This allows to detect that atom ob(lfbo,rw1), along with its duplicate ob′(lfbo,rw2), is inconsistent. Recall that an atom is considered consistently true only if both and its duplicate are true. Then consistent and inconsistent query answering mechanism described earlier can be used to correctly handle such situations and provide only consistent answers.
Integrity Constraints: A syntactic approach to enforcing integrity constraints is also proposed, inspired by [37, 38] on using classical negation [39]. The idea is to treat any data that violates a specified condition as inconsistent. For example, if a NOTAM message lacks essential information such as a start or end time, it should be considered invalid. This can be captured with a rule that states: ¬Notam() ← Notam(), hasStartTime(, ). (31) This rule means that if a NOTAM exists, but we cannot find any associated start time or end time, then its negation is derived, creating an inconsistency. When this happens, both the original NOTAM and its negation coexist in the knowledge base. During consistent query answering, such inconsistent atoms are filtered out(see Section 5).
Optimize Resource Consumption: NoHr operates by translating a Hybrid MKNF knowledge base into an equivalent logic program, using a sequence of transformation algorithms(figure 1). This logic program is then executed by the XSB-Prolog engine to perform query answering. To mitigate memory consumption, we propose using NoHr exclusively during a preprocessing phase to generate the transformed logic program. During system operation, only the resulting logic program is executed independently with a prolog engine such XSB-Prolog or SWI-Prolog. This approach significantly reduces runtime memory usage while maintaining the reasoning capabilities, as the live system no longer depends on the full NoHr infrastructure.We can also integrate the syntactic approach proposed for combining classical negation with integrity constraints into this. The architecture of the proposed work flow is available in figure 8:
The syntactic approach outlined above provides a straightforward means of incorporating classical negation into an LP while enabling reuse of the NoHR reasoner. However, this approach remains heuristic in nature, and a more rigorous account of the semantics, supported by formal proofs, is required. Our next objective is therefore to define a formal semantics for the extended Hybrid MKNF framework, with particular emphasis on the truth evaluation of modal operators involving classically negated atoms, such as ¬ and not ¬, within the context of a three-valued model.
Building on this foundation, we will introduce a bottom-up computational methodology that generalizes the existing alternating fixpoint approach to compute the extended (, ) partition, which incorporates both positive and classically negated literals. We will formally prove that the resulting partition is sound and complete with respect to the extended well-founded semantics. Subsequently, we will develop a query answering algorithm extending the SLG(O) resolution method discussed in Section 3.2 of [30]. This algorithm will employ knowledge base doubling and semi-negative transformation techniques to identify inconsistencies and filter out contradictory atoms during query evaluation, thereby ensuring paraconsistent reasoning capabilities. We will also provide a formal proof that the proposed query answering procedure is sound and complete with respect to the extended well-founded (, ) partition. Finally, we will implement the extended query answering algorithm for specific DLs.
The theoretical contributions, including the formal semantics, computational methodology, and query answering algorithm, will be submitted as a full paper. In parallel, we will submit the implementation results, focusing on query answering over specific DLs, as a short paper to the Automated Reasoning Conference 2026, whose submission deadline is expected around January or February.
This section outlines the upcoming steps following the completion of the current task—extending the hybrid MKNF framework with classical negation. Once this work is finalized and the results are submitted to a conference, We will select the next objective from the list below to pursue. The objectives are presented in order of priority, with the first being the most immediate focus after the current phase. The scope of these objective will be carried within the phd objective or beyond depends on the time. Explore rule engines: Our goal is to construct a practical reasoner capable of running eficiently on resource-constrained devices. Currently, reasoning is performed by translating a hybrid MKNF knowledge base into a Prolog program with tabling, using XSB-Prolog for query answering. However, by restricting the syntax, we can identify several useful subsets of hybrid MKNF, enabling the use of a wider range of solvers and also facilitating the development of lightweight, practical reasoners. For instance, DLs can be integrated with definite logic programs—programs consisting only of positive rules—and with stratified programs, where predicates are organized into layers (strata) such that no predicate depends negatively on itself, either directly or indirectly. Additionally, reasoning can be extended to unrestricted, unstratified programs without such constraints. In the cases of definite logic programs and stratified programs, there are existing solvers such as I-DLV 1, Trealla Prolog2, Tau-Prolog 3 which are more lightweight. We will formally define these syntactic subsets of Hybrid MKNF and conduct a detailed evaluation of various rule engines applicable to each subset. In addition to this, we aim to identify lightweight solvers that ofer practical performance benefits for constrained environments. This objective enables knowledge engineers to select a reasoner that best aligns with the specific requirements of the application.
Explanation: Another important objective is to develop a formal theory for explaining the reasoning process in Hybrid MKNF. Provenance, a concept in logic programming, has been widely used to generate justifications for query answering results[ 40]. Inspired by this approach, we will propose an extension of provenance techniques to Hybrid MKNF knowledge bases under the well-founded semantics. Paraconsistent Semantics: Extending Hybrid MKNF with classical negation introduces potential inconsistencies. A paraconsistent semantics for Hybrid MKNF under the well-founded semantics has already been proposed [41], but no implementation currently supports it. Extending this semantics to accommodate classical negation within the LP component, and devising a sound and complete query answering algorithm for the extended framework, constitute important directions for future research, particularly given their practical relevance in safety-critical domains such as aeronautics. 1https://dlv.demacs.unical.it/i-dlv 2https://github.com/trealla-prolog/trealla 3https://tau-prolog.org/ Date-and-Time Reasoning: Another important research direction is the integration of date-and-time reasoning within the reasoner. For instance, in the NARS use case, NOTAM messages are associated with a start and end time. Therefore, the reasoner must take these date-and-time constraints into account when performing inference.
I express my sincere thanks to my supervisors: Christophe REY(Université Clermont-Auvergne), Florence DE GRANCEY(Thales), Victor CHARPENAY(Ecole des Mines de Saint-Étienne), and Farouk TOUMANI(Université Clermont-Auvergne) for their guidance and assistance thus far. This research is jointly funded by Thales and National Association of Research and Technology(ANRT),France.
During the preparation of this work, the author(s) used ChatGPT (OpenAI, GPT-4) to assist with grammar and spelling correction, as well as to improve clarity and readability. After using this tool, the author(s) reviewed and edited the content as needed and take full responsibility for the final version of the manuscript. [16] W. Drabent, J. Henriksson, J. Maluszynski, Hd-rules: A hybrid system interfacing prolog with dl-reasoners, in: Applications of Logic Programming to the Web, 2007. [17] L. Bajraktari, M. Ortiz, M. imkus, Combining rules and ontologies into clopen knowledge bases, in: AAAI Conference, 2018. URL: https://api.semanticscholar.org/CorpusID:19234928. [18] S. Lukumbuzya, M. Ortiz, M. imkus, Resilient logic programs: Answer set programs challenged by ontologies, in: AAAI Conference on Artificial Intelligence, 2020. [19] S. Heymans, D. V. Nieuwenborgh, D. Vermeir, Open answer set programming for the semantic web, J. Appl. Log. 5 (2007) 144–169. URL: https://api.semanticscholar.org/CorpusID:7957259. [20] G. Antoniou, A. Bikakis, Dr-prolog: A system for defeasible reasoning with rules and ontologies on the semantic web, IEEE Transactions on Knowledge and Data Engineering 19 (2007). URL: https://api.semanticscholar.org/CorpusID:14844582. [21] H. Lan, Swrl : A semantic web rule language combining owl and ruleml, , 2004. URL: https: //api.semanticscholar.org/CorpusID:207974723. [22] F. Donini, M. Lenzerini, D. Nardi, Al-log: Integrating datalog and description logics, Journal of
Intelligent Information Systems 10 (1999). doi:10.1023/A:1008687430626. [23] Combining horn rules and description logics in carin, Artificial Intelligence 104 (1998) 165–209. [24] C. Feier, S. Heymans, Hybrid reasoning with forest logic programs, in: Extended Semantic Web
Conference, 2009. URL: https://api.semanticscholar.org/CorpusID:11089946. [25] S. Heymans, L. Predoiu, C. Feier, J. de Bruijn, D. V. Nieuwenborgh, G-hybrid knowledge bases, 2003. URL: https://api.semanticscholar.org/CorpusID:9440798. [26] B. Motik, R. Rosati, A faithful integration of description logics with logic programming, in:
Proceedings of the 20th IJCAI, IJCAI’07, 2007. [27] V. Lifschitz, Nonmonotonic databases and epistemic queries, in: Proceedings of the 12th International Joint Conference on Artificial Intelligence - Volume 1, IJCAI’91, 1991. [28] M. Knorr, J. J. Alferes, P. Hitzler, Local closed world reasoning with description logics under the well-founded semantics, Artif. Intell. 175 (2011) 1528–1554. [29] B. Motik, R. Rosati, Reconciling description logics and rules, J. ACM 57 (2008). URL: https: //doi.org/10.1145/1754399.1754403. doi:10.1145/1754399.1754403. [30] J. J. Alferes, M. Knorr, T. Swift, Query-driven procedures for hybrid mknf knowledge bases, ArXiv abs/1007.3515 (2010). URL: https://api.semanticscholar.org/CorpusID:3126629. [31] V. Kasalica, Nohr: An overview, KI - Knstliche Intelligenz (2020) 1–7. URL: https://api.
semanticscholar.org/CorpusID:212408100. [32] V. Ivanov, M. Knorr, J. Leite, A query tool for el with non-monotonic rules, in: International
Workshop on the Semantic Web, 2013. URL: https://api.semanticscholar.org/CorpusID:16285536. [33] N. Costa, M. Knorr, J. Leite, Next step for nohr: Owl 2 ql, in: International Workshop on the
Semantic Web, 2015. URL: https://api.semanticscholar.org/CorpusID:41958726. [34] G. Singh, S. K. Bhatia, R. Mutharaju, Owl2bench: A benchmark for owl 2 reasoners, in: International
Workshop on the Semantic Web, 2020. URL: https://api.semanticscholar.org/CorpusID:226229397. [35] V. Lifschitz, D. Pearce, A. Valverde, Strongly equivalent logic programs, ACM Trans. Comput. Logic 2 (2001) 526–541. URL: https://doi.org/10.1145/383779.383783. doi:10.1145/383779.383783. [36] J. Alferes, L. Pereira, T. Przymusinski, ’classical’ negation in nonmonotonic reasoning and logic programming, J. Autom. Reasoning 20 (1998) 107–142. doi:10.1023/A:1005900924623. [37] S. Flesca, S. Greco, E. Zumpano, Active integrity constraints, PPDP ’04, Association for Computing
Machinery, New York, NY, USA, 2004, p. 98–107. [38] L. e. a. Cruz-Filipe, Active integrity constraints: From theory to implementation, in: Knowledge
Discovery, Knowledge Engineering and Knowledge Management, Cham, 2016, pp. 399–420. [39] J. Chomicki, G. Saake, P. Godfrey, J. Grant, J. Gryz, J. Minker, Integrity constraints: Semantics and applications (1998). [40] C. V. Damásio, A. Analyti, G. Antoniou, Justifications for logic programming, in: International
Conference on Logic Programming and Non-Monotonic Reasoning, 2013. [41] T. Kaminski, Eficient paraconsistent reasoning with rules and ontologies for the semantic web, 2014. URL: https://api.semanticscholar.org/CorpusID:9076559.