Paper deep dive

Hybrid MKNF with Classical Negation in the Rule Component

Arun Raveendran Nair Sheela, Christophe Rey, Florence De Grancey

Year: 2026Venue: arXiv preprintArea: cs.LOType: PreprintEmbeddings: 79

Intelligence

Status: succeeded | Model: Gemma-4-26B-A4B | Prompt: intel-v1 | Confidence: 90%

Last extracted: 7/24/2026, 2:50:26 AM

Summary

The paper introduces hMKNF¬, an extension of Hybrid MKNF knowledge bases that supports classical negation in the rule component. It addresses limitations in representing explicit negative knowledge in safety-critical applications by formally defining the syntax, semantics, and a three-valued well-founded model computation procedure for this extended formalism.

Entities (9)

hMKNF¬ · formalism · 98%Hybrid MKNF · formalism · 98%Classical Negation · concept · 95%Well-founded Semantics · concept · 92%Description Logics · formalism · 90%Logic Programming · formalism · 90%MKNF · logic · 90%Stable Partition · concept · 85%Well-founded Partition · concept · 85%

Relation Signals (6)

hMKNF¬ → extends → Hybrid MKNF

confidence 95% · We introduce hMKNF¬, an extension of hybrid MKNF under the well-founded semantics

hMKNF¬ → supports → Classical Negation

confidence 95% · supports classical negation in the rule component

Hybrid MKNF → integrates → Description Logics

confidence 90% · integrate Description Logics with Logic Programming

Hybrid MKNF → integrates → Logic Programming

confidence 90% · integrate Description Logics with Logic Programming

hMKNF¬ → uses → Well-founded Semantics

confidence 90% · extension of hybrid MKNF under the well-founded semantics

Well-founded Partition → isuniqueminimal → Stable Partition

confidence 85% · the well-founded partition is the unique minimal stable partition

Cypher Suggestions (0)

No Cypher suggestions yet.

Abstract

Abstract:Hybrid MKNF knowledge bases under the well-founded semantics integrate Description Logics with Logic Programming. However, they do not support classical negation in the rule component, limiting their ability to represent explicit negative knowledge. This limitation is particularly significant in safety-critical applications, where reasoning often requires explicit negative information rather than interpreting the absence of information as evidence of absence. To address this issue, we introduce an extension of Hybrid MKNF that supports classical negation in the rule component. We formally define the syntax and semantics of the extended language and present a general procedure for computing its well-founded model.

PDF

Open source PDF →Open local PDF →

Trouble viewing inline? Open PDF directly →

Full Text

77,323 characters extracted from source content.

Expand or collapse full text

W. Faber, L. Giordano, R. Rocha, V. Santos Costa (Eds.): 42nd International Conference on Logic Programming (ICLP 2026) EPTCS 450, 2026, p. 374–402, doi:10.4204/EPTCS.450.28 ©A.R.N. Sheela, C. Rey & F. De Grancey This work is licensed under the Creative Commons Attribution License. Hybrid MKNF with Classical Negation in the Rule Component Arun Raveendran Nair Sheela Université Clermont Auvergne, LIMOS France Thales your.email@example.com Christophe Rey Université Clermont Auvergne, LIMOS, CNRS France christophe.rey@example.com Florence De Grancey Thales florence.degrancey@example.com Hybrid MKNF knowledge bases under the well-founded semantics integrate Description Logics with Logic Programming. However, they do not support classical negation in the rule component, limiting their ability to represent explicit negative knowledge. This limitation is particularly significant in safety-critical applications, where reasoning often requires explicit negative information rather than interpreting the absence of information as evidence of absence. To address this issue, we introduce an extension of Hybrid MKNF that supports classical negation in the rule component. We formally define the syntax and semantics of the extended language and present a general procedure for computing its well-founded model. 1 Introduction Knowledge representation and reasoning studies formal methods for representing domain knowl- edge and performing tasks such as query answering through inference. Within this area, the integration of two formalisms, Description Logics (DLs) and Logic Programming, to support both open-world and closed-world reasoning has been widely studied [2]. Among existing approaches, hybrid MKNF is particularly expressive, as it combines DL ontologies with logic programming rules under the semantics of Minimal Knowledge and Negation as Failure (MKNF), extending first-order logic with the modal operatorsKandnot[6]. A three-valued characterisation of hybrid MKNF, capturing the well-founded semantics, was introduced in [5], together with a bottom-up method for computing the well-founded model in polynomial time, assuming polynomial-time DL reasoning. Consider modelling a knowledge base using hybrid MKNF, where the DL component provides a static description of domain entities and relations, and the rule component captures dynamic aspects such as events, actions, and state changes. The approach of [5] does not support classical negation in the rule component, despite it being allowed by MKNF semantics. Instead, negative information is expressed only via default negation (not), allowing the conclusion ofnotAwhen Ais not derivable. Consequently, negated conclusions rely on the absence of knowledge rather than explicit evidence, which may lead the rule component to infer domain states that do not reflect the actual situation. We illustrate this limitation with a simple example concerning the operational status of an airport runway:A runway is open if it is associated with an airport and is not known to be closed or obstructed.This requirement can be formalized as a hybrid MKNF A.R.N. Sheela, C. Rey & F. De Grancey375 knowledge baseK= (O,P), where the ontologyOcontains the axiomOpnRwy⊑Rwy,and the rule componentPincludes the following rule: KOpnRwy(Y)←KAirport(A),KhasRwy(A,Y),notob(A,Y),notCldRwy(Y).(1) Inferring runway availability from the absence of obstacle information (notob(A,Y)) is unsafe, since missing or delayed data does not imply that no obstacle exists. Rule 1 formalizes an operational condition that may vary dynamically at runtime. Representing such dynamic operational conditions in DL is inappropriate, and the default assumptionnotCldRwy(Y)cannot be expressed using DL axioms alone. Moreover, introducing auxiliary confirmation predicates does not resolve the issue, as confirmations of presence and absence may coexist without yielding a contradiction. A more robust representation relies on classical negation: KOpnRwy(Y)←KAirport(A),KhasRwy(A,Y),K¬ob(A,Y),notCldRwy(Y).(2) The rule(2)can be read as:A runway is open if an airport has the runway, it is not known to be closed, and it is known to have no obstacles.The use of classical negation makes contradictions explicit at the semantic level. Additional applications of hybrid MKNF extended with classical negation are discussed in [10]. Classical negation can be incorporated indirectly in the rule component via a syntactic transformation for unary predicates, as proposed in [5]. In this transformation, for each unary predicateA, a fresh conceptBis introduced in the DL component together with the axiom B≡¬A, allowingBto represent the classical negation ofAin rules. This approach requires additional knowledge engineering effort and is restricted to unary predicates. A further limitation of the approach in [5] is that it correctly computes the well-founded model only forcoherent hybrid MKNFknowledge bases, a subclass of hybrid MKNF [7]. For non-coherent knowledge bases, the bottom-up computation of [5] produces a well-founded model that differs from the declarative semantics, as shown in [7]. To address this, [7] propose a general guess-and-check method for computing three-valued MKNF models. However, this approach is inherently nondeterministic and does not formally establish the treatment of classical negation in the rule component. In this work, we address this gap by extending hybrid MKNF knowledge bases to unrestricted usage of classical negation in the rule component. We formally establish the treatment of classical negation by adapting key intuitions from [5, 7, 4]. Our main contributions are as follows: (i) We introducehMKNF¬, an extension of hybrid MKNF under the well-founded semantics that supports classical negation in the rule component (Section 2). (i)We present a three-valued characterization ofhMKNF¬knowledge bases viastable partitions adapted from [7], where thewell-founded partitionis the unique minimal stable partition which yields thewell-founded model(Section 3). (i)We present an operational procedure for the computation of the well-founded partition of hMKNF¬knowledge bases (Section 4). 1.1 Three-valued semantics for MKNF The Logic of MKNF is an extension of first-order logic with two modal operators,Kandnot [6]. Intuitively, the operatorKrepresents explicitly known information, whilenotdenotes information that is not explicitly known in a knowledge base. Together, these two operators behave in a way that corresponds to the closed-world assumption. LetΣ = (Σ c ,Σ f ,Σ p )be a first-order signature, whereΣ c ,Σ f , andΣ p are the sets of constants, function symbols, and predicate symbols, respectively, withΣ p containing the equality predicate 376Hybrid MKNF with Classical Negation in the Rule Component ≈. A first-order atomP(t 1 ,...,t n )is an MKNF formula, wherePis a predicate symbol and t 1 ,...,t n are first-order terms. Ifφandφ ′ are MKNF formulae, then¬φ,∃x:φ,Kφ,notφ, and φ∧φ ′ are also MKNF formulae. Moreover, formulae constructed using the connectives∨,⊃, and≡, as well as the universal quantifier∀, are interpreted as in first-order logic. A MKNF formulaφis ground if it contains no variables. A first-order interpretationIover a signatureΣ with domain∆maps each constanta∈Σ c to an elementa I ∈∆, eachn-ary function symbol f∈Σ f to a functionf I : ∆ n →∆, and eachn-ary predicate symbolP∈Σ p to a relationP I ⊆∆ n . Furthermore, for everyα∈∆, there exists a designated constantn α ∈Σ, called a name, such thatn I α =α. In [5], a three-valued MKNF structure is defined as a tuple(I,M,N), whereIis a first-order interpretation andM=⟨M,M 1 ⟩andN=⟨N,N 1 ⟩are pairs of sets of first-order interpretations such thatM 1 ⊆MandN 1 ⊆N. The evaluation of an MKNF formulaφunder the truth values t,u,f, ordered byf<u<t, with respect to a three-valued MKNF structure, is defined in Fig. 1.1: (I,M,N) P(t 1 ,...,t n ) = ( tiff(t I 1 ,...,t I n )∈P I , fiff(t I 1 ,...,t I n )/∈P I . (3) ((I,M,N)(¬φ) =    tif(I,M,N)(φ) =f, uif(I,M,N)(φ) =u, fif(I,M,N)(φ) =t, (4) (I,M,N)(φ 1 ∧φ 2 ) = min(I,M,N)(φ 1 ),(I,M,N)(φ 2 ),(5) (I,M,N)(φ 1 ⊃φ 2 ) = tif((I,M,N)(φ 2 )≥(I,M,N)(φ 1 ), fotherwise, (6) (I,M,N)(∃x:φ) = max(I,M,N)(φ[n α /x])|α∈∆,(7) (I,M,N)(Kφ) =    tif(J,⟨M,M 1 ⟩,N)(φ) =tfor allJ ∈M, fif(J,⟨M,M 1 ⟩,N)(φ) =ffor someJ ∈M 1 , uotherwise, (8) (I,M,N)(notφ) =    tif(J,M,⟨N,N 1 ⟩)(φ) =ffor someJ ∈N 1 , fif(J,M,⟨N,N 1 ⟩)(φ) =tfor allJ ∈N, uotherwise. (9) Figure 1: Evaluation of MKNF formulae with respect to a MKNF structure A three-valued MKNF interpretation is a pair(M,N)consisting of two sets of interpretations MandNsuch that∅⊂N⊆M. It satisfies a closed MKNF formulaφ, written as(M,N)|=φ, if and only if(I,⟨M,N⟩,⟨M,N⟩)(φ) =t. IfM=N, then the interpretation pair is called total. An MKNF interpretation pair(M,N)is athree-valued MKNF modelfor a closed MKNF formula φif(i)Satisfaction:(M,N)satisfiesφ, and(i)Maximality:for every MKNF interpretation pair (M ′ ,N ′ )withM⊆M ′ andN⊆N ′ , where at least one inclusion is proper andM ′ =N ′ ifM=N, there existsI ′ ∈M ′ such that(I ′ ,⟨M ′ ,N ′ ⟩,⟨M,N⟩)(φ)̸=t.A closed MKNF formulaφis said to beMKNF-consistentif there exists a three-valued MKNF model(M,N)forφ, Otherwise,φis MKNF-inconsistent. Under MKNF semantics, a knowledge base may admit multiple three-valued MKNF models. When it exists, thewell-founded modelis the unique model that maximizes the set of undefined modal atoms among all three-valued models. Formally, let(M,N)denote the well-founded model. Then, for any other three-valued MKNF model(M 1 ,N 1 ), it holds that M 1 ⊆MandN⊆N 1 . A.R.N. Sheela, C. Rey & F. De Grancey377 1.2 Hybrid MKNF A hybrid MKNF knowledge base is a pairK= (O,P)consisting of a decidable DL knowledge base O, which must be translatable into function-free first-order logic with equality and guarantee decidability of satisfiability and instance checking, and a finite set P of MKNF rules of the form [8]: KH←KA 1 ,...,KA n ,notB 1 ,...,notB m .(10) whereH,A i , andB j are function-free first-order atoms. A ruleris called positive ifm= 0, and it is called a fact ifn=m= 0. An atom occurring inPis called a DL-atom if its predicate symbol occurs in the ontologyO; otherwise, it is called a non-DL atom. A rule is called ground if it contains no variables. Letπdenote the MKNF translation of a hybrid MKNF knowledge base. The translation π(O)maps the DL ontology into first-order formulae. For a ruler∈Pwith free variables ̃x, the translation is defined as: π(r) =∀ ̃x : (KA 1 ∧·∧KA m ∧notB 1 ∧·∧notB n ⊃KH)(11) π(P) = r∈P π(r)π(K) =Kπ(O)∧π(P)(12) A hybrid MKNF knowledge baseKis MKNF-consistent if its MKNF translationπ(K)admits a three-valued MKNF model(M,N); otherwise, it is MKNF-inconsistent. An MKNF rule is said to be DL-safe if every variable occurring in the rule also occurs in at least one non-DL atom in its body. A hybrid MKNF knowledge baseKis DL-safe if all its MKNF rules are DL-safe. Decidability ofKfollows from the decidability of the underlying DL, the restriction that all atoms occurring in MKNF rules are function-free first-order atoms, and DL-safety. The original MKNF semantics may yield counterintuitive results when combining DLs and logic programs due to arbitrary universes and varying interpretations of constants; this issue is addressed in [9] by adopting thestandard name assumption, where interpretations are Herbrand ones with a countably infinite number of additional constants. 2 Extension with Classical Negation We extend hybrid MKNF knowledge bases by permitting classical negation in the rule component. The resulting formalism, denotedhMKNF¬, preserves the same restrictions as hybrid MKNF knowledge bases, including DL-safety [9] to ensure decidability, while allowing both positive and classically negated modal atoms in the rule component. We use the shorthandh(r)←b + (r),b − (r) to denote a rule of the form (10). Definition 2.1.AhMKNF¬knowledge base is a pairK= (O,P), whereOis a DL ontology andPis a finite set of MKNF rules. Each ruler∈Pis of the form,h(r)←b + (r),b − (r). whereh(r) =KH,b + (r) =KA 1 ,...,KA n , andb − (r) =notB 1 ,...,notB m . Moreover, Kξ∈h(r)∪b + (r)andnotξ∈b − (r), whereξis either a first-order atomAor its classical negation¬A. Also, denoteK(b − (r)) =Ka|nota∈b − (r)andb(r) =b + (r)∪b − (r). As defined in(11)and(12), ahMKNF¬knowledge base is translated into the MKNF formula π(K) =K,π(O)∧π(P). The componentπ(P)may contain modal atomsKAandnotA, as well as their classically negated formsK¬Aandnot¬A. Since classical negation is part of the MKNF language, these atoms are interpreted under the standard MKNF semantics. Let 378Hybrid MKNF with Classical Negation in the Rule Component (I,M,N)be a three-valued MKNF structure andφa formula. According to the evaluation in Fig. 1.1, classically negated modal atoms are evaluated with respect to(I,M,N): (I,M,N)(K¬φ) =    tif(J,⟨M,M 1 ⟩,N)(φ) =ffor allJ ∈M, fif(J,⟨M,M 1 ⟩,N)(φ) =tfor someJ ∈M 1 , uotherwise, (13) (I,M,N)(not¬φ) =    tif(J,M,⟨N,N 1 ⟩)(φ) =tfor someJ ∈N 1 , fif(J,M,⟨N,N 1 ⟩)(φ) =ffor allJ ∈N, uotherwise, (14) With respect to⟨M,M 1 ⟩, a classically negated modal atomK¬φistrueifφisfalsein all interpretations ofM,falseifφistruein some interpretation ofM 1 , andundefinedotherwise. The evaluation ofnot-atoms is defined symmetrically to that ofK-atoms. As a consequence, MKNF semantics enforces acoherence principleby default: ifK¬Aholds in a model, thennotA also holds; similarly, ifKAholds in a model, thennot¬Aholds. 3 Three-valued Model for hMKNF¬ This section develops the formal basis for constructing three-valued MKNF models forhMKNF¬ knowledge bases, building on partial partitions from [5] and stable partitions from [7], which are shown to extend to hMKNF¬. Given ahMKNF¬knowledge baseK= (O,P), its ground instantiation isK G = (O,P G ), whereP G =rθ|r∈P, θmaps each variable occurring inrto a constant ofK G .KandK G have the same models [5,9], and we henceforth consider only groundhMKNF¬knowledge bases. Following the approach of [5], we construct a finite set of ground modal atoms from a ground hMKNF¬knowledge baseK G = (O,P G ), analogous to a Herbrand base. Definition 3.1.LetK G = (O,P G )be a groundhMKNF¬knowledge base. The set of all modal atoms ofK G , denoted byEKA(K G ), is defined asEKA(K G ) =Kξ|r∈P G ,Kξ∈h(r)∪b + (r)∪ K(b − (r)), ξisAor¬A. A partial partition ofEKA(K G )is a pair(T,F)withT,F⊆EKA(K G ) andT∩F=∅. The setUis given byU=EKA(K G )\(T∪F). The relationship between a partial partition(T,F)ofEKA(K G )and a three-valued MKNF interpretation is formalized in the definition below. Definition 3.2.LetK G = (O,P G )be a groundhMKNF¬knowledge base. The partial partition (T,F)ofEKA(K G )is induced by a three-valued interpretation(M,N)if, for every modal atom KL∈EKA(K G )whereLis eitherξor¬ξ, the following conditions hold:(i)KL∈Timplies∀I∈ M: (I,⟨M,N⟩,⟨M,N⟩)(KL) =t;(i)KL∈Fimplies∀I∈M: (I,⟨M,N⟩,⟨M,N⟩)(KL) =f(i) KL /∈T∪Fimplies∀I∈M: (I,⟨M,N⟩,⟨M,N⟩)(KL) =u. We now define the notion of objective knowledge, adapted from [5]. Definition 3.3.LetK G = (O,P G )be a groundhMKNF¬knowledge base, and letS⊆EKA(K G ). Theobjective knowledgeofSwith respect totK G isOB O,S =π(O)∪ξ|Kξ∈S∪¬ξ|K¬ξ∈ S. A three-valued MKNF interpretation(M,N)with respect to a partial partition(T,F)of EKA(K G )is defined as follows. The setMcontains the models ofπ(O)extended withT(Def. 3.3), whileNcontains the models extended withTandU(Prop. 3 in [5]). The intuition behind this A.R.N. Sheela, C. Rey & F. De Grancey379 construction is to obtain a finite representation of ahMKNF¬knowledge base that captures its semantics. Proposition 3.1.Let(M,N)be a three-valued MKNF model of a groundhMKNF¬knowledge baseK G , and let(T,F)be the partial partition induced by(M,N). ThenM=I|I|=OB O,T andN=I|I|=OB O,EKA(K G ) . Proof.Proof is provided in Prop. B.1. Definition 3.4.LetK G = (O,P G )be a groundhMKNF¬knowledge base. Let(T,F)be a partial partition ofEKA(K G ). The MKNF interpretation pair(M,N)induced by(T,F)is defined as follows:M=I|I|=OB O,T andN=I|I|=OB O,EKA(K G ) . 3.1 Stable Partition Following [7], a stable partition is a partial partition(T,F)that induces, via Def. 3.4, a three-valued MKNF interpretation(M,N)that is a model of ahMKNF¬knowledge base. By construction,(M,N)satisfies the DL component ofK G . Hence,(T,F)is stable iff (i)(M,N) satisfies the rule component ofK G , and (i)(M,N)ismaximal, that is, there is no(M ′ ,N ′ )with M⊂M ′ orN⊂N ′ , still satisfying the rule component; moreover, ifM=N, thenM ′ =N ′ . The rule component is evaluated with respect to(M,N)by assigning each modal atomAthe truth valueA[T,F], which denotes the value ofAunder the three-valued MKNF interpretation (M,N)induced by(T,F). This evaluation relies onMandNbeing sets of interpretations satisfyingOB O,T andOB O,EKA(K G ) , respectively. Lemma 3.1.LetK G = (O,P G )be a groundhMKNF¬knowledge base and(T,F)a partial partition ofEKA(K G ). For everyξsuch thatKξ∈EKA(K G ): Kξ[T,F] =    tOB O,T |=ξ, fOB O,EKA(K G ) ̸|=ξ, uotherwise. notξ[T,F] =    tOB O,EKA(K G ) ̸|=ξ, fOB O,T |=ξ, uotherwise. Intuitively, Lem. 3.1, based on Prop. 3.1, shows that for anyx∈T,Kξ[T,F] =x(resp. notξ[T,F] =x) holds if and only ifKξ(resp.notξ) evaluates toxwith respect to MKNF interpretation(M,N)induced by partial partition(T,F). Lemma 3.2.Let(T,F)be a partial partition ofEKA(K G )and let(M,N)be the MKNF interpretation induced by(T,F). LetT=f,u,twithf<u<t. Then, for every ruler∈ P G , ∀I∈M,(I,⟨M,N⟩,⟨M,N⟩)(π(r)) =t iff h(r)[T,F]≥b(r)[T,F] ,whereb(r)[T,F] = minℓ[T,F]|ℓ∈b + (r)∪b − (r). Lem. 3.1 and Lem. 3.2 establish how the rule component of ahMKNF¬is evaluated with respect to a partial partition, allowing us to define the stable partitions. Definition 3.5(Stable partition).LetK G = (O,P G )be a groundhMKNF¬knowledge base and(T,F)a partial partition ofEKA(K G ). We call(T,F)astable partitionif and only if:(i) OB O,EKA(K G ) is satisfiable; (i) (i.1)for everyKξ∈EKA(K G ),OB O,T | =ξimpliesKξ∈TandOB O,EKA(K G ) ̸|=ξimplies Kξ∈F;(i.2)∀I∈M: (I,⟨M,N⟩,⟨M,N⟩)(π(r)) =tfor allr∈P G andI∈M, where(M,N) is the MKNF interpretation induced by(T,F); 380Hybrid MKNF with Classical Negation in the Rule Component (i)for any(T ′ ,F ′ )withT ′ ⊆TandF⊆F ′ (at least one proper), either there existsKξ∈ EKA(K G ) ′ such thatOB O,T ′ |=ξor there existsKξ∈F ′ thatOB O,EKA(K G ) ′ |=ξ, or there existsr∈P G such that∀I∈M ′ ,(I,⟨M ′ ,N ′ ⟩,⟨M,N⟩)(π(r)) =f, where(M ′ ,N ′ )is induced by(T ′ ,F ′ ). Theorem 3.1.LetK G = (O,P G )be a groundhMKNF¬knowledge base. Let(T,F)be a partial partition ofEKA(K G ).(T,F)is stable if and only if the three-valued MKNF interpretation (M,N)induced by(T,F)is a three-valued MKNF model ofK G . Proof.Proof is provided in Thm. B.1. Having established the semantics of stable partitions in Def. 3.5, we now present a computation procedure, adapted from [7], for checking whether a partial partition is stable. This procedure is used during the computation of the well-founded model of ahMKNF¬knowledge base explained in Section 4. To simplify computation,K¬Aornot¬Ain the rule component are handled by treating ¬Aas positive atom. The objective knowledgeOB O,S is constructed by translatingKA∈Sas AandK¬A∈Sas¬A, with classical negation treated as in first-order logic (Def. 3.3). For any first-order atomA, its complement is denoted byA, whereA=¬Aand¬A=A. Definition 3.6.LetK G = (O,P G )be a groundhMKNF¬knowledge base and let(T,F)be a partial partition ofEKA(K G )andX,S⊆EKA(K G ). We define the following operators: T S K G (X) =h(r)|r∈P G , b + (r)⊆X,K(b − (r))⊆S ∪Kξ|Kξ∈EKA(K G ),OB O,X |=ξ,(15) TU S K G (X) =h(r)|r∈P G , b + (r)⊆X,K(b − (r))⊆SandOB O,X ̸|= h(r) ∪Kξ|Kξ∈EKA(K G ),OB O,X |=ξ,(16) The operatorsT S K G andTU S K G are monotonic ([5]). As they range over the finite lattice of partial partitions ofEKA(K G ), they reach a least fixpoint in finitely many iterations, starting from the empty set. We denoteΓ(S)as the least fixpoint ofT S K G ,Γ ′ (S)as the least fixpoint of TU S K G andFa(S)asEKA(K G )\Γ ′ (S). Proposition 3.2.LetK G = (O,P G )be a groundhMKNF¬knowledge base.(T,F)is a sta- ble partition ofEKA(K G )if and only if (i)T= Γ(F), (i)F=Fa(EKA(K G ) )and (i) OB O,Γ(EKA(K G ) ) is satisfiable. Proof.Proof is provided in Prop. B.2. Well-founded partition.AhMKNF¬knowledge base may admit multiple three-valued MKNF models, each inducing a stable partition (Definition 3.5). Definition 3.7(Well-founded partition).LetK G be a groundhMKNF¬knowledge base. A stable partition(T W ,F W )ofK G is called thewell-founded partitionofK G if, for every stable partition(T,F)ofK G , it holds thatT W ⊆TandF W ⊆F. Theorem 3.2(Well-founded Model).LetK G be a groundhMKNF¬knowledge base. If(T W ,F W ) is the well-founded partition ofK G , then the MKNF interpretation pair(M W ,N W )induced by (T W ,F W )is the well-founded model ofK G . A.R.N. Sheela, C. Rey & F. De Grancey381 4 Computation of Well-founded Partition The computation of the well-founded partition for ahMKNF¬knowledge base follows a three- phase strategy (Fig. 4). The first phase applies a well-founded operator adapted from [4] (Subsection 4.1), followed by a unit propagation phase (Subsection 4.2), and finally a guess- and-check approach (Subsection 4.3). This strategy prioritises deterministic computation by relying on the first two phases and resorting to guess-and-check only when necessary, since not allhMKNF¬knowledge bases yield a well-founded partition after each phase. Some illustrative examples are moved to A. Phase 1: Well-founded Operator Def. 4.2 ⟳ Phase 2: Unit Propagation Def. 4.4 ⟳ Phase 3: Guess and Check (Compute All Stable Partitions) ∀ Prop. 3.2 holds? Prop. 3.2 holds? Stable Partitions Def. 3.7 holds? Well-founded Partition No WFP Input:K G Start with(∅,∅) Output:(T ω ,F ω )Output:(T E ,F E ) yesyes no Input:(T ω ,F ω ) no Input:(T E ,F E ) yes yes no Figure 2: Workflow for well-founded partition computation of a hMKNF¬knowledge base. 4.1 Phase 1: Fixpoint Computation of Well-founded Operator If the well-founded partition exists, the well-founded operator used here computes it in most cases, with the remaining cases handled by subsequent phases. This operator, originally introduced by [4], is defined with respect to a partial partition(T,F). It combines (i) the operatorT F K G (T)from Def. 3.6, which computes the modal atoms derivable from thehMKNF¬knowledge base, and (i) the operatorF K G (defined below), also called the unfounded set operator, which computes the largest set of modal atoms that are not derivable from thehMKNF¬knowledge base with respect to(T,F). A modal atomKH∈EKA(K G )belongs to an unfounded set if it does not admit a valid derivation from the rule componentPtogether with the DL ontologyO. Formally,KHis not derivable with respect to(T,F)ifOB O,EKA(K G ) ̸|=H,and for every ruler∈P G with head KH, the body ofrevaluates to false under(T,F), that is,b(r)[T,F] =f. However, when OB O,EKA(K G ) is unsatisfiable, the principle of explosion applies, and every formula becomes derivable from the objective knowledge. Consequently, this characterization of non-derivability no longer applies, and the unfounded set operatorF K G cannot be defined in a straightforward manner. We therefore adopt the unfounded set construction for hybrid MKNF knowledge bases from [4] and adapt it tohMKNF¬. Let(T,F)be a partial partition ofEKA(K G ), and letKHbe a ground modal atom. For any set of rulesR⊆P G ,head(R)is defined asξ|Kξ=h(r)for somer∈R. Definition 4.1(Unfounded set).LetK G = (O,P G )be a groundhMKNF¬knowledge base, and let(T,F)be a partial partition ofEKA(K G ). A setUF⊆EKA(K G )is anunfounded setwith respect to(T,F)if, for everyKH∈UF, whereHis eitherAor¬A, at least one of the following holds: •OB O,T |=H 382Hybrid MKNF with Classical Negation in the Rule Component •for everyR⊆P G such that 1.head(R)∪OB O,T |=H, and for allR ′ ⊂R,head(R ′ )∪OB O,T ̸|=H, and 2. for eachKξ∈F, the sethead(R)∪OB O,T ∪ξis satisfiable; there exists a ruler∈Rof the formh(r)←b + (r),b − (r)such that at least one of the following holds:K(b − (r))∩T̸=∅,b + (r)∩F̸=∅, orb + (r)∩UF̸=∅. Thegreatest unfounded setofK G with respect to(T,F), denotedF K G (T,F), is the largest unfounded set satisfying the above condition. Computing unfounded sets requires considering all possible derivations of a modal atom obtained by combining the rule component with the DL ontology, and verifying that none of these derivations succeeds with respect to the current partial partition (see Ex. A.2 in the appendix). For ahMKNF¬knowledge base, this task is computationally expensive in the general case. Since our objective is to define a semantics forhMKNF¬, we do not address the computation of unfounded sets and rely on this notion solely for theoretical purposes. However, we can either adopt the unfounded set computation proposed in [4] or restrict the DL part to Datalog-rewritable DLs, in which case unfounded sets can be computed by evaluating the rewritten rules. Based on Def. 4.1 ofF K G (T,F)and Def. 3.6 ofT F K G (T), we define the well-founded operator as follows: Definition 4.2(Well-founded Operator).LetK G = (O,P G )be a groundhMKNF¬knowledge base, and let(T,F)be a partial partition ofEKA(K G ). The well-founded operatorW K G with respect to(T,F)is defined asW K G (T,F) = (T F K G (T), F K G (T,F)). With respect to non contradictory partial partitions (Def. 4.3),W K G is monotonic and then has a least fixpoint. We next define when a partial partition is contradictory. This notion of contradiction can be used to detect MKNF inconsistency of a hMKNF¬knowledge base. Definition 4.3.LetK G = (O,P G )be a groundhMKNF¬knowledge base and letT,F⊆EKA(K G ). (T,F)isnon-contradictoryif and only if(T,F)is a partial partition andOB O,T is satisfiable. Otherwise,(T,F)is said to becontradictory. Then the operatorW K G is monotonic [4] with respect to the following order defined on non- contradictory partial partitions: for(T 1 ,F 1 )and(T 2 ,F 2 ), we write(T 1 ,F 1 )⊆(T 2 ,F 2 )ifT 1 ⊆T 2 andF 1 ⊆F 2 . That is, whenever(T,F)⊆(T ′ ,F ′ )and both partitions are non-contradictory, it holds thatW K G (T,F)⊆W K G (T ′ ,F ′ ). Alg. 1 computes the least fixpoint ofW K G by iterative construction starting from the initial partition(∅,∅). SinceTandFrange over subsets of the finite setEKA(K G ), convergence is guaranteed after finitely many steps, yielding the fixpoint W K G ↑ω= (T ω ,F ω ). Alg 1 checks whether(T ω ,F ω )is a stable partition (Prop. 3.2), terminating if the condition is satisfied and otherwise proceeding to Phase 2. The following proposition relates the partial partition(T ω ,F ω )computed as the fixpoint of W K G to all stable partitions of a hMKNF¬knowledge base. Proposition 4.1.LetK G = (O,P G )be a groundhMKNF¬knowledge base and(T ω ,F ω )a fixpoint of the well-founded operatorW K G . For any modal atomKH∈EKA(K G ), withHof the formξor¬ξ, and for every stable partition(T,F)ofK G , the following holds:KH∈T ω implies KH∈T, andKH∈F ω impliesKH∈F. Proof.Proof is provided in Prop. B.3. A.R.N. Sheela, C. Rey & F. De Grancey383 Algorithm 1:Fixpoint Computation ofW K G :Out(K G )∈⊥,(T W ,F W ) 1i←0,(T 0 ,F 0 )←(∅,∅) 2repeat 3(T i+1 ,F i+1 )←W K G (T i ,F i )(Def. 4.2) 4if(T i+1 ,F i+1 )is contradictory (Def. 4.3)then 5return⊥// MKNF-inconsistent (Thm. 4.1) 6i←i+ 1 7until(T i ,F i ) = (T i−1 ,F i−1 ) 8(T ω ,F ω )←(T i ,F i ) 9if(T ω ,F ω )is a stable partition (Prop. 3.2)then 10return(T W ,F W )←(T ω ,F ω )// Otherwise, continue with Phase 2 4.2 Phase 2: Unit Propagation. Unit propagation is applied when Phase 1 fails to compute a stable partition. The following example illustrates a situation in which this phase becomes necessary. Example 4.1.Consider thehMKNF¬knowledge baseK 1 = (O 1 ,P 1 ), whereπ(O 1 ) =cand P 1 =r 1 :Ka←notb., r 2 :Kb←nota., r 3 :K¬c←Ka..The fixpoint ofW K 1 is(T ω 1 ,F ω 1 ) = (∅,K¬c). By Proposition 3.2,(T ω 1 ,F ω 1 )is not stable, sinceOB O,Γ(EKA(K G ) ω 1 ) is unsatisfiable (withΓ(EKA(K G ) ω 1 ) =Ka,Kb,K¬c).Reason.This partition is not a stable partition because of ruler 3 . With respect to(T ω 1 ,F ω 1 ), the headh(r 3 ) =K¬cis false, while its body b(r 3 ) =Kais undefined (Lemma 3.1); therefore, the rule is not satisfied (Lemma 3.2). As the head ofr 3 is false, satisfaction requires its body to be false as well. Applying unit propagation [4] enforcesKato be false, which in turn allows ruler 2 to deriveKbas true. Thus, from(∅,K¬c) we obtain the partial partition(Kb,Ka,K¬c)which is stable according to Prop. 3.2. More precisely, letr∈P G and let(T,F)be a partial partition ofEKA(K G )such that h(r)[(T,F)]evaluates tofalseandb(r)[(T,F)]evaluates toundefined. If there exists exactly one modal atomKL∈b + (r)∪K(b − (r))such thatKL /∈T∪F, then the truth value ofKLis forced in order to satisfy the rule. In particular,KLmust be assignedfalseifKL∈b + (r), and trueifKL∈K(b − (r)). This intuition is formalized in Definition 4.4 by introducing two unit propagation operators. Definition 4.4(Unit Propagation Operators).LetK G = (O,P G )be a groundhMKNF¬knowl- edge base, and let(T ω ,F ω )denote the fixpoint of the operatorW K G . LetKa∈EKA(K G ), wherea is either an atomAor its classical negation¬A. For any setsX,Y⊆EKA(K G ), we define two unit-propagation operators: UPT (T ω ,F ω ) K G (X,Y) =Ka|∃r∈P G such thatOB O,T ω ∪X |= h(r), b + (r)⊆T ω ∪X, K(b − (r))∩(T ω ∪X) =∅andK(b − (r))\(F ω ∪Y) =Ka, UPF (T ω ,F ω ) K G (X,Y) =Ka|∃r∈P G such thatOB O,T ω ∪X |= h(r),K(b − (r))⊆F ω ∪Y, b + (r)∩(F ω ∪Y) =∅andb + (r)\(T ω ∪X) =Ka . The atoms newly derived by unit propagation may, in turn, enable additional consequences stemming from both the DL ontology and the rule component. To capture this interaction, we introduce the extending operatorE K G . 384Hybrid MKNF with Classical Negation in the Rule Component Definition 4.5.LetK G = (O,P G )be a groundhMKNF¬knowledge base, and let(T ω ,F ω )be the fixpoint ofW K G . ForX,Y⊆EKA(K G ), we define E (T ω ,F ω ) K G (X,Y) = UPT (T ω ,F ω ) K G (X,Y)∪T Y K G (X), UPF (T ω ,F ω ) K G (X,Y)∪F K G (X,Y) . The operatorE (T ω ,F ω ) K G is monotonic with respect to set inclusion, analogously to the well- founded operator. Hence, iterative application from the empty partition(∅,∅)is guaranteed to converge to a least fixpointE (T ω ,F ω ) K G ↑ω= (T E ,F E )after finitely many steps. Alg. 2 iteratively computes this fixpoint and returns(T E ,F E )if it is stable, otherwise proceeding to Phase 3. Algorithm 2:Fixpoint Computation ofE K G :Out(K G )∈⊥,(T W ,F W ) 11j←0,(T ′ 0 ,F ′ 0 )←(∅,∅) 12repeat 13(T ′ j+1 ,F ′ j+1 )←E (T ω ,F ω ) K G (T ′ j ,F ′ j )(Def. 4.4) 14if(T ′ j+1 ,F ′ j+1 )is contradictory (Def. 4.3)then 15return⊥// MKNF-inconsistent (Thm. 4.1) 16j←j+ 1 17until(T ′ j ,F ′ j ) = (T ′ j−1 ,F ′ j−1 ) 18(T E ,F E )←(T ′ j ,F ′ j ) 19if(T E ,F E )is a stable partition (Prop. 3.2)then 20return(T W ,F W )←(T E ,F E )// Otherwise, continue with Phase 3 The Prop. 4.2 states that the partial partition(T E ,F E ), computed as the fixpoint ofE K G , is contained in all stable partitions of a hMKNF¬knowledge base. Proposition 4.2.LetK G = (O,P G )be a groundhMKNF¬knowledge base and(T E ,F E )a fixpoint ofE K G . For any modal atomKH∈EKA(K G ), withHof the formξor¬ξ, and for every stable partition(T,F)ofK G , the following holds:KH∈T E impliesKH∈T, andKH∈F E impliesKH∈F. Proof.Proof is provided in Prop. B.4. 4.3 Phase 3: Guess-and-Check Approach. In somehMKNF¬knowledge bases, Phases 1 and 2 are insufficient to compute the well-founded partition. In such cases, we employ a guess-and-check phase to ensure the completeness of the overall procedure. We illustrate this with a simple example. Example 4.2.Consider thehMKNF¬knowledge baseK 2 = (O 2 ,P 2 ), whereπ(O 2 ) =c andP 2 =r 1 :Ka←notb., r 2 :Kb←nota., r 3 :K¬c←Kd,Ka., r 4 :Kd←Ka,notd.. (T ω 2 ,F ω 2 ) = (∅,K¬c)and(T E 2 ,F E 2 ) = (∅,K¬c). The objective knowledgeOB O,Γ(EKA(K G ) E 2 ) is unsatisfiable (withΓ(EKA(K G ) E 2 ) =Ka,Kb,K¬c,Kd). Hence, neither(T ω 2 ,F ω 2 )nor (T E 2 ,F E 2 )is a stable partition. To compute the well-founded partition, we must therefore enumer- ate all stable partitions and select the minimal one according to Def. 3.7.K 2 admits two stable partitions extending(T E 2 ,F E 2 )and satisfying Prop. 3.2:(T 1 ,F 1 ) = (Kb,K¬c,Ka,Kd)and (T 2 ,F 2 ) = (Kb,K¬c,Ka). The well-founded partition ofK 2 is(T 2 ,F 2 ), according to Def. 3.7 (T 2 =T 1 andF 2 ⊆F 1 ). A.R.N. Sheela, C. Rey & F. De Grancey385 Prop. 4.1 and Prop. 4.2 guarantees that the partial partition(T E ,F E ), although not stable, is contained in every stable partition. Starting from this base partition (Ex. 4.2), we therefore adopt aguess-and-checkapproach that enumerates all partial partitions extending(T E ,F E )and identifies those that are stable according to Prop.3.2. This procedure is described in Alg. 3. Algorithm 3:Stable Partition Computation:Out(K)∈⊥,(T W ,F W ),NoWFM 22U←EKA(K G )\(T E ∪F E ),S←∅ 23foreachT u ⊆Udo 24foreachF u ⊆U u do 25T S ←T E ∪T u ,F S ←F E ∪F u 26if(T S ,F S )stable (Prop. 3.2)then 27S←S∪(T S ,F S ) 28ifS=∅then 29return⊥// MKNF-inconsistent 30if∃(T,F)∈Ssuch that Def 3.7 holdsthen 31return(T W ,F W )←(T,F) 32return"NoWFM" // no well-founded model 4.4 Well-founded Model Algorithms 1, 2, and 3 compute an outputOut(K)∈⊥,(T W ,F W ),NoWFMfor a groundhMKNF¬ knowledge baseK, where(T W ,F W )is stable partition,⊥denotes MKNF inconsistency and NoWFMdenotes the absence of a unique stable partition. Theorem 4.1.LetK G = (O,P G )be a groundhMKNF¬knowledge base, and letOut(K G )denote the output of Algorithms 1, 2, and 3. (1) IfOut(K G ) =⊥, thenK G is MKNF-inconsistent. (2) IfOut(K G ) = (T W ,F W ), then(T W ,F W )is the well-founded partition ofK G , and the induced three-valued MKNF interpretation(M W ,N W )is the well-founded MKNF model ofK G . (3) If Out(K G ) =NoWFM, thenK G has no well-founded model. Proof.Proof is provided in Thm. B.5. The data complexity of computing the well-founded partition of ahMKNF¬knowledge base depends on the phase in which the stable partition is obtained. If it is computed in Phases 1 or 2, the complexity depends on the data complexity of DL reasoning and unfounded set computation. If it is only obtained in Phase 3, all extensions of the partial partition(T,F)obtained after Phase 2 over the remaining atomsU=EKA(K G )\(T∪F)are enumerated, yielding at most3 |U| candidates; each candidate can be checked to be a stable partition in polynomial time relative to DL reasoning [7], resulting overall in exponential. Proposition 4.3.LetK G = (O,P G )be a DL-safehMKNF¬knowledge base. Assume data complexityC 1 for computing unfounded sets with respect to a partial partition(T,F), andC 2 for DL satisfiability and ground entailment. Let(T 1 W ,F 1 W )and(T 2 W ,F 2 W )be the partitions obtained after Phase 2 and Phase 3, respectively.(i)If(T 1 W ,F 1 W )coincides with the well-founded partition ofK G , then it can be computed with data complexityPTime C 1 ∪C 2 .(i)If(T 2 W ,F 2 W )coincides with the well-founded partition ofK G then it can be computed with data complexity isEXPTime P C 1 . 386Hybrid MKNF with Classical Negation in the Rule Component 5 Discussion and Related Works Table 5 summarizes the comparison betweenhMKNF¬, [5], and [7]. The approach of [5] applies only to coherent hybrid MKNF knowledge bases, where the well-founded partition is obtained by an alternating fixpoint construction (based on [11]). Another related work is [4], which introduces a well-founded operator that we adapt in this work. However, its primary goal is constraint propagation for the efficient computation of two-valued MKNF models. Moreover, it is shown in [4] that the resulting well-founded partition coincides with one obtained by [5]. AspecthMKNF¬[5][7] Knowledge basesAll Hybrid MKNF¬Coherent Hybrid MKNF All Hybrid MKNF Rule componentwith classical negationwithout classical negation without classical negation Well-founded partition Computation Fixpoint computation with unit propagation fallback to guess-and-check Fixpoint computation Guess-and-check ComplexityProp.4.3PTime C 2 Existence of a stable partition:NPTime PTime C 2 Table 1: Comparison with Related Approaches The main advantage of our approach is that it supports classical negation in the rule component while providing a general procedure for computing the well-founded model of arbitraryhMKNF¬ knowledge bases. A current limitation is that we do not present a method for unfounded set computation, although existing methods for hybrid MKNF can be adopted. Additionally, the proposed computation methodology may require a guess-and-check approach (phase 3), which is exponential in the worst case. This phase is nevertheless unavoidable to ensure correctness and completeness, as Phases 1 and 2 are insufficient to compute the well-founded partition for some hMKNF¬knowledge bases. AhMKNF¬reasoner can be implemented using either bottom-up or top-down approaches. Assuming unfounded set computation method exists, a bottom-up solver applies the fixpoint operators of Algorithms 1–3 directly. But this approach may be inefficient in applications with frequent knowledge base updates. In the top-down approach, one option is to translate the hMKNF¬knowledge base into a logic program with oracle predicates for DL calls, together with transformations for enforcing coherency principle and detect contradictions. A formal proof is then required to establish that the well-founded model of the resulting program corresponds to the well-founded partition of thehMKNF¬knowledge base. This would enable the use of SLG resolution extended with oracle calls, similar to [1]. However, this approach supports only Phases 1 and 2 of the computation; Phase 3 requires global reasoning and cannot be supported. Thus, the approach is complete only for knowledge bases whose well-founded partition is obtained in Phase 1 or Phase 2. Another possible strategy is to define an abstract solver in which the fixpoint operators are evaluated over a reified representation of the rule component, while interacting with the DL reasoner on demand. This allows the fixpoint to be computed through a recursive, top-down evaluation, similar to [3]. A.R.N. Sheela, C. Rey & F. De Grancey387 6 Conclusion and Future Work In this work, we introducedhMKNF¬, an extension of hybrid MKNF knowledge bases that supports classical negation in the rule component, together with a general methodology for computing its well-founded model. The proposed approach applies to arbitraryhMKNF¬ knowledge bases and is based on the computation of a well-founded partition through a three- phase process. Building on this foundation, we plan to develop a query answering system for hMKNF¬knowledge bases. References [1]José Júlio Alferes, Matthias Knorr & Terrance Swift (2013):Query-Driven Procedures for Hybrid MKNF Knowledge Bases.ACM Trans. Comput. Log.14(2), p. 16:1–16:43, doi:10.1145/2480759.2480768. [2] Wlodzimierz Drabent, Thomas Eiter, Giovambattista Ianni, Thomas Krennwallner, Thomas Lukasiewicz & Jan Maluszynski (2009):Hybrid Reasoning with Rules and Ontologies. In François Bry & Jan Maluszynski, editors:Semantic Techniques for the Web, The REWERSE Perspective, Lecture Notes in Computer Science5500, Springer, p. 1–49, doi:10.1007/978-3-642-04581-3_1. [3] Ana Sofia Gomes, José Júlio Alferes & Terrance Swift (2010):Implementing Query Answering for Hybrid MKNF Knowledge Bases. In Manuel Carro & Ricardo Peña, editors:Practical Aspects of Declarative Languages, 12th International Symposium, PADL 2010, Madrid, Spain, January 18-19, 2010. Proceedings,Lecture Notes in Computer Science5937, Springer, p. 25–39, doi:10.1007/978-3- 642-11503-5_4. [4]Jianmin Ji, Fangfang Liu & Jia-Huai You (2017):Well-founded Operators for Normal Hybrid MKNF Knowledge Bases.Theory and Practice of Logic Programming17(5–6), p. 889–905, doi:10.1017/S1471068417000291. [5]Matthias Knorr, José Júlio Alferes & Pascal Hitzler (2011):Local closed world reasoning with description logics under the well-founded semantics.Artif. Intell.175(9-10), p. 1528–1554, doi:10.1016/J.ARTINT.2011.01.007. [6]Vladimir Lifschitz (1991):Nonmonotonic Databases and Epistemic Queries. In John Mylopoulos & Raymond Reiter, editors:Proceedings of the 12th International Joint Conference on Artificial Intelligence. Sydney, Australia, August 24-30, 1991, Morgan Kaufmann, p. 381–386. [7]Fangfang Liu & Jia-Huai You (2017):Three-valued semantics for hybrid MKNF knowledge bases revisited.Artificial Intelligence252, p. 123–138, doi:10.1016/j.artint.2017.08.003. [8]Boris Motik & Riccardo Rosati (2007):A Faithful Integration of Description Logics with Logic Programming. In Manuela M. Veloso, editor:IJCAI 2007, Proceedings of the 20th International Joint Conference on Artificial Intelligence, Hyderabad, India, January 6-12, 2007, p. 477–482. [9]Boris Motik & Riccardo Rosati (2010):Reconciling description logics and rules.J. ACM57(5), p. 30:1–30:62, doi:10.1145/1754399.1754403. [10] Arun Raveendran Nair Sheela, Florence De Grancey, Christophe Rey & Victor Charpenay (2026): Hybrid MKNF for Aeronautics Applications: Usage and Heuristics. In:41st ICLP,Rende, Italy, 2025, Electronic Proceedings in Theoretical Computer Science439, p. 349–366, doi:10.4204/EPTCS.439.24. [11]Allen Van Gelder (1993):The alternating fixpoint of logic programs with negation.Journal of Computer and System Sciences47(1), p. 185–221, doi:10.1016/0022-0000(93)90024-Q. 388Hybrid MKNF with Classical Negation in the Rule Component A Examples Example A.1(Phase 1 Example).Consider ahMKNF¬knowledge baseK= (O,P), where π(O) =f∧(b⊃¬d)and P 1 =r 1 :K¬a←.r 2 :Ka←notb. r 3 :Kb←nota. r 4 :Kc←Ka. r 5 :Ke←K¬d,Kf. r 6 :Kg←notg.. Consider the three-valued MKNF interpretation ofπ(K)given by (M 1 ,N 1 ) = f,e,b,f,e,b,g,f,e,b,c,f,e,b,g,c,f,e,b,g,f,e,b,g,c . It holds that(M 1 ,N 1 )|=π(K 1 ), and there exists no(M ′ 1 ,N ′ 1 )such thatM 1 ⊂M ′ 1 andN 1 ⊂N ′ 1 with(M ′ 1 ,N ′ 1 )|=π(K 1 ). Therefore,(M 1 ,N 1 )is a three-valued MKNF model ofK 1 . With respect to(M 1 ,N 1 ),K¬a,nota,Kf,Ke,K¬d,Kbist,,KcisfandKgisu. Example A.2(Unfounded Set, Example A.1 continued).LetK= (O,P)and (T,F) = (K¬a,Kf,∅). SinceOB O,K¬a,Kf |=¬a,Kais unfounded with respect to(T,F). Moreover, the only rule supportingKcisR=Kc←Ka, for whichOB O,T ∪head(R)|=c, whiler∈Rwe haveKa∈b + (r)withKais unfounded. Hence,Kcis also unfounded. So F (K¬a,Kf,∅) K G =Ka,Kc. Example A.3(Example A.1 continued).Consider a hMKNF¬knowledge baseK= (O,P). EKA (K G ) =K¬a,Ka,Kb,Kd,Kf,Ke,K¬d,Kg. Computing the well-founded partition of Kas follows: W K ↑0 = (∅,∅), W K ↑1 = (K¬a,Kf,∅), W K ↑2 = (K¬a,Kf,Ka,Kc), W K ↑3 = (K¬a,Kf,Kb,Ka,Kc), W K ↑4 = (K¬a,Kf,Kb,K¬d,Ka,Kc), W K ↑5 = (K¬a,Kf,Kb,K¬d,Ke,Ka,Kc,Kd), W K ↑6 = (K¬a,Kf,Kb,K¬d,Ke,Ka,Kc,Kd). SinceW K ↑5 =W K ↑6, a fixpoint is reached. (T ω ,F ω ) = (K¬a,Kf,Kb,K¬d,Ka,Kc,Kd). The objective knowledgeOB O,Γ(EKA(K G ) ω ) is satisfiable (withΓ(EKA(K G ) ω ) =K¬a,Ka,Kb,Kc,Kg,Kf,Ke,K¬d). So(T ω ,F ω )is stable partition, and also the well-founded partition. The well-founded model(M W ,N W )where M W =I|I|=OB O,T ω andN W =I|I|=OB O,EKA(K G ) ω The well-founded model is (M W ,N W ) = f,e,b,f,e,b,g,f,e,b,c,f,e,b,g,c,f,e,b,g,f,e,b,g,c . Example A.4.Consider the hybrid MKNF knowledge baseK= (O,P),whereπ(O) =¬a∧band P=Ka←Kb. EKA(K G ) =Ka,Kb. We obtain (T 0 ,F 0 ) =W K ↑0 = (∅,∅), (T 1 ,F 1 ) =W K ↑1 = (K¬a,Kb,∅), (T 2 ,F 2 ) =W K ↑2 = (Ka,K¬a,Kb,Ka) A.R.N. Sheela, C. Rey & F. De Grancey389 SinceOB O,T 2 is unsatisfiable andT 2 ∩F 2 ̸=∅, soKis MKNF-inconsistent. Example A.5(Phase 2 Example).Consider thehMKNF¬knowledge baseK= (O,P), where π(O) =cand P=r 1 :Ka←notb, r 2 :Kb←nota, r 3 :K¬c←Ka. EKA(K G ) =Ka,Kb,K¬c. W K ↑0 = (∅,∅), W K ↑1 = (∅,K¬c) W K ↑2 = (∅,K¬c) SinceW K ↑2 =W K ↑1, a fixpoint is reached.(T ω ,F ω ) = (∅,K¬c).(T ω ,F ω )is not stable, sinceOB O,Γ(EKA(K G ) ω ) is unsatisfiable (withΓ(EKA(K G ) ω ) =Ka,Kb,K¬c). E (T ω ,F ω ) K ↑0 = (∅,∅), E (T ω ,F ω ) K ↑1 = (∅,Ka,K¬c) E (T ω ,F ω ) K ↑2 = (Kb,Ka,K¬c) E (T ω ,F ω ) K ↑3 = (Kb,Ka,K¬c) SinceE (T ω ,F ω ) K ↑3 =E (T ω ,F ω ) K ↑2, a fixpoint is reached.(T E ,F E ) = (Kb,Ka,K¬c)which is stable partition and also the well-founded partition. The well-founded model(M W ,N W )where M W =I|I|=OB O,T E andN W =I|I|=OB O,EKA(K G ) E . The well-founded model is (M W ,N W ) = c,b,c,b,a,c,b,c,b,a . Example A.6(Inconsistent MKNF Example).Consider ahMKNF¬knowledge baseK= (O,P),whereπ(O) =cand P=r 1 :Ka←nota.,r 1 :K¬c←nota. EKA(K G ) =Ka,K¬c. W K ↑0 = (∅,∅), W K ↑1 = (∅,K¬c) W K ↑2 = (∅,K¬c) SinceW K ↑2 =W K ↑1, a fixpoint is reached.(T ω ,F ω ) = (∅,K¬c).(T ω ,F ω )is not stable, sinceOB O,Γ(EKA(K G ) ω ) is unsatisfiable (withΓ(EKA(K G ) ω ) =Ka,K¬c). (T 0 ,F 0 ) =E (T ω ,F ω ) K ↑0 = (∅,∅), (T 1 ,F 1 ) =E (T ω ,F ω ) K ↑1 = (Ka,K¬c) (T 2 ,F 2 ) =E (T ω ,F ω ) K ↑2 = (Ka,K¬c,Ka) SinceOB O,T 2 is satisfiable butT 2 ∩F 2 ̸=∅, soK 2 is MKNF-inconsistent. 390Hybrid MKNF with Classical Negation in the Rule Component Example A.7.Consider the hMKNF¬knowledge baseK= (O,P), whereπ(O) =cand P=r 1 :Ka←notb, r 2 :Kb←nota, r 3 :K¬c←Kd,Ka, r 4 :Kd←Ka,notd. EKA(K G ) =Ka,Kb,K¬c,Kd. W K ↑0 = (∅,∅), W K ↑1 = (∅,K¬c) W K ↑2 = (∅,K¬c) SinceW K ↑2 =W K ↑1, a fixpoint is reached.(T ω ,F ω ) = (∅,K¬c).(T ω ,F ω )is not stable, since OB O,Γ(EKA(K G ) ω ) is unsatisfiable (withΓ(EKA(K G ) ω ) =Ka,Kb,Kd,K¬c). E (T ω ,F ω ) K ↑0 = (∅,∅), E (T ω ,F ω ) K ↑1 = (∅,K¬c) E (T ω ,F ω ) K ↑2 = (∅,K¬c) SinceE (T ω ,F ω ) K ↑3 =E (T ω ,F ω ) K ↑2, a fixpoint is reached.(T E ,F E ) = (∅,K¬c)is not a stable partition. We now compute all stable partitions using a guess-and-check approach. LetU=EKA(K G )\ (T E ∪F E ),so thatU=Ka,Kb,Kd.Since|U|= 3, there exist3 3 = 27partial partitions ex- tending(T E ,F E ), each of which must be checked for stability. Admits two stable partitions extending(T E ,F E )and satisfying Prop. 3.2:(T 1 ,F 1 ) = (Kb,K¬c,Ka,Kd)and(T 2 ,F 2 ) = (Kb,K¬c,Ka). The well-founded partition is(T 2 ,F 2 ), according to Def. 3.7(T 1 =T 2 and F 2 ⊆F 1 ). (T W ,F W ) =Kb,K¬c,Ka) The well-founded model is (M W ,N W ) = c,b,c,b,a,c,b,c,b,a . Example A.8.Consider the hMKNF¬knowledge baseK= (O,P),whereπ(O) =cand P=r 1 :Ka←notb.r 2 :Kb←nota.r 3 :K¬c←K¬d,Ka. r 4 :K¬d←noth.r 5 :Kh←not¬d.. EKA(K G ) =Ka,Kb,K¬d,K¬c,Kh. W K ↑0 = (∅,∅), W K ↑1 = (∅,K¬c) W K ↑2 = (∅,K¬c) SinceW K ↑2 =W K ↑1, a fixpoint is reached.(T ω ,F ω ) = (∅,K¬c).(T ω ,F ω )is not stable, sinceOB O,Γ(EKA(K G ) ω ) is unsatisfiable (withΓ(EKA(K G ) ω ) =Ka,Kb,Kd,K¬c). E (T ω ,F ω ) K ↑0 = (∅,∅), E (T ω ,F ω ) K ↑1 = (∅,K¬c) E (T ω ,F ω ) K ↑2 = (∅,K¬c) A.R.N. Sheela, C. Rey & F. De Grancey391 SinceE (T ω ,F ω ) K ↑3 =E (T ω ,F ω ) K ↑2, a fixpoint is reached.(T E ,F E ) = (∅,K¬c)is not a stable partition. We now compute all stable partitions using a guess-and-check approach. LetU=EKA(K G )\ (T E ∪F E ),so thatU=Ka,Kb,Kd,Kh. (T 1 ,F 1 ) = (Kb,K¬c,Ka) (T 2 ,F 2 ) = (Kh,K¬c,K¬d) Here there exist no stable partition satisfying Definition 3.7, so no well-founded partition. B Proofs Proposition B.1.Let(M,N)be a three-valued MKNF model of a groundhMKNF¬knowledge baseK G , and let(T,F)be the partial partition induced by(M,N). ThenM=I|I|=OB O,T andN=I|I|=OB O,EKA(K G ) . Proof. The proof of this proposition is analogous to the proof of the corresponding result in [5]. The only additional aspect to be addressed is that the partition(T,F)may contain modal atoms involving classical negation. We show that this extension does not affect the validity of the construction. Consider a groundhMKNF¬knowledge baseK G = (O,P G ). Let(M,N)be a three-valued MKNF model ofK G , and let(T,F)ofEKA(K G )be the partition induced by(M,N). Let(M ′ ,N ′ )be the three-valued interpretation pair computed using B.1. We need to prove thatM=M ′ andN=N ′ . First We prove thatM⊆M ′ . LetI∈M. We show thatI∈M ′ . From Proposition B.1, for everyI ′ ∈M ′ , it holds thatI ′ |=OB O,T . By definition,M ′ is the set of interpretations that satisfyOB O,T . Hence, it suffices to show thatI|=OB O,T . Since(M,N)is a three-valued model ofK G , every interpretationI∈MsatisfiesI|=π(O). Moreover,Tis the set of modal atoms induced by the three-valued model(M,N). Thus, for every modal atomKξ∈T, the following condition holds: ∀I∈M,(I,⟨M,N⟩,⟨M,N⟩)Kξ=t. LetK¬A∈T. By the semantics of modal atoms,K¬A=tholds if and only ifAis false in every interpretationI∈M. Hence, for allI∈M, we haveI|=¬A, and thereforeI̸|=A. Equivalently,∀I∈M, A /∈I.Consequently, ∀I∈M,(I,⟨M,N⟩,⟨M,N⟩)K¬A=t. Since this argument applies to every modal atom inT, it follows thatI|=OB O,T . Therefore, I∈M ′ , and we conclude thatM⊆M ′ . We prove thatN⊆N ′ . LetI∈N. We show thatI∈N ′ . By definition,I∈N ′ if and only ifI|=OB O,EKA(K G ) . LetU=EKA(K G )\(T∪F).Thus, it suffices to show that I|=π(O)∪ ξ|Kξ∈T ∪ ξ|Kξ∈U. SinceN⊆M, we haveI∈M. HenceI|=OB O,T , and thereforeI|=π(O)∪ ξ|Kξ∈ T. It remains to show thatI|=ξ|Kξ∈U. LetKξ∈Ube arbitrary. Since(M,N)is a three-valued model ofK G , we have that∀I∈M: (I,⟨M,N⟩,⟨M,N⟩)Kξ=uonly ifξ /∈ J 1 for someJ 1 ∈Mandξ∈J 2 for allJ 2 ∈N.In particular,ξ∈Jfor allJ∈N, and since 392Hybrid MKNF with Classical Negation in the Rule Component I∈N, it follows thatI|=ξ. AsKξ∈Uwas arbitrary, we conclude thatI|=ξ|Kξ∈U. Similarly, for classical negation, since(M,N)is a three-valued model ofK G , we have that ∀I∈M: (I,⟨M,N⟩,⟨M,N⟩)K¬ξ=uonly ifξ∈J 1 for someJ 1 ∈Mandξ /∈J 2 for allJ 2 ∈N. Therefore,I|=π(O)∪ ξ|Kξ∈T ∪ ξ|Kξ∈U.Consequently,I|=OB O,EKA(K G ) , and henceI∈N ′ . Thus,N⊆N ′ . Now to proveM ′ =MandN ′ =N. We know that(M,N)is a three-valued model ofK G , so∀I∈M: (I,⟨M,N⟩,⟨M,N⟩)K G =timplies∀I∈M: (I,⟨M,N⟩,⟨M,N⟩)Kπ(O)∧π(P G ) =t. Now, Proposition B.1, we have∀I∈M: (I,⟨M ′ ,N ′ ⟩,⟨M,N⟩)Kπ(O) =t. It remains to show that∀I∈M: (I,⟨M ′ ,N ′ ⟩,⟨M,N⟩)Kπ(P G ) =t. Recall thatT⊆EKA(K G )are the sets of true positive literals and classical negated literals, respectively, with respect toP G . 1. From Definition 3.2, for everyKξ∈Tand the three-valued MKNF model(M,N), we have ∀I∈M: (I,⟨M,N⟩,⟨M,N⟩)(Kξ) =t.Moreover, for everyI ′ ∈M ′ , sinceI ′ |=OB O,T and Kξ∈T, it follows that∀I ′ ∈M ′ : (I ′ ,⟨M ′ ,N ′ ⟩,⟨M,N⟩)(Kξ) =t. 2.Similarly, for everyK¬ξ∈Tand the three-valued MKNF model(M,N), we have∀I∈M: (I,⟨M,N⟩,⟨M,N⟩)(K¬ξ) =t.By the semantics ofKwith classical negation, this implies thatξis false in every interpretationI∈M. The same holds for the three-valued interpretation(M ′ ,N ′ ). Indeed, by Proposition B.1, letM ′ be the set of interpretationsI ′ such thatI ′ |=OB O,T . Then, for everyI ′ ∈M ′ , it holds thatI ′ |=¬ξ, and henceI ′ ̸|=ξ. Equivalently,∀I ′ ∈M ′ , ξ /∈I ′ .Consequently, ∀I ′ ∈M ′ : (I ′ ,⟨M ′ ,N ′ ⟩,⟨M,N⟩)(K¬ξ) =t. 3. LetKξ∈Fand consider the three-valued MKNF model(M,N). We have (I,⟨M,N⟩,⟨M,N⟩)(Kξ) =f.This means that there exists an interpretationJ∈Nsuch thatJ̸|=ξ. SinceN⊆N ′ , it follows that there exists an interpretationJ ′ ∈N ′ such thatJ ′ ̸|=ξ. Therefore,(I ′ ,⟨M ′ ,N ′ ⟩,⟨M,N⟩)(Kξ) =f,for everyI ′ ∈M ′ . 4.LetK¬ξ∈Fand consider the three-valued MKNF model(M,N). By the semantics ofK, we have (I,⟨M,N⟩,⟨M,N⟩)(K¬ξ) =f.This means that there exists an interpretationJ∈Nsuch thatJ|=ξ. SinceN⊆N ′ , it follows that there exists an interpretationJ ′ ∈N ′ such thatJ ′ |=ξ. Therefore,(I ′ ,⟨M ′ ,N ′ ⟩,⟨M,N⟩)(K¬ξ) =f,for everyI ′ ∈M ′ . 5. For everyKξ∈U, and the three-valued MKNF model(M,N), we have ∀I∈M : (I,⟨M,N⟩,⟨M,N⟩)Kξ=u, this holds if and only if there exists an interpretation I 1 ∈Msuch thatI 1 ̸|=ξ, and for all interpretationsJ∈N, it holds thatJ|=ξ. SinceM⊆M ′ , there exists an interpretationI ′ 1 ∈M ′ such thatI ′ 1 ̸|=ξ. Moreover, by definition ofN ′ , every interpretationJ ′ ∈N ′ satisfiesπ(O)∪T∪U. In particular, for every J ′ ∈N ′ , we haveJ ′ |=ξ. Therefore, there exists an interpretation inM ′ in whichξis false, andξis true in all interpretations inN ′ . Hence,(I ′ ,⟨M ′ ,N ′ ⟩,⟨M,N⟩)(Kξ) =u,for every I ′ ∈M ′ . 6. For everyK¬ξ∈U,and the three-valued MKNF model(M,N), we have ∀I∈M: (I,⟨M ′ ,N ′ ⟩,⟨M,N⟩)Kξ=u. This happen when someI∈Mwhereξ∈Iand all J∈Nwhereξ /∈I. SinceM⊆M ′ so there exist at-least one interpretationI ′ ∈M ′ where A.R.N. Sheela, C. Rey & F. De Grancey393 ξ∈I ′ . Moreover, by definition ofN ′ , every interpretationJ ′ ∈N ′ satisfiesπ(O)∪T∪U. In particular, for everyJ ′ ∈N ′ , we haveJ ′ notmodelsξ ifK¬ξ∈UTherefore, there exists an interpretation inM ′ in whichξis true, andξis false in all interpretations inN ′ . Hence,(I ′ ,⟨M ′ ,N ′ ⟩,⟨M ′ ,N ′ ⟩)(K¬ξ) =u,for everyI ′ ∈M ′ . Hence, we conclude∀I ′ ∈M ′ : (I,⟨M ′ ,N ′ ⟩,⟨M,N⟩)(Kπ(O)∧π(P G )) =t,which implies that the evaluations under(M,N)and(M ′ ,N ′ )coincide for every ground atom of thehMKNF¬ knowledge base. Consequently, both pairs(M,N)and(M ′ ,N ′ )represent the same model. Lemma B.1.Let(T,F)be a partial partition ofEKA(K G ), and let(M,N)be the MKNF interpretation induced by(T,F). For everyξsuch thatKξ∈EKA(K G ), Kξ[T,F] =      tOB O,T |=ξ, fOB O,EKA(K G ) ̸|=ξ, uotherwise. notξ[T,F] =      tOB O,EKA(K G ) ̸|=ξ, fOB O,T |=ξ, uotherwise. Proof.Let(T,F)be a partial partition ofEKA(K G )and let(M,N)be the MKNF interpretation induced by(T,F), withM=I|I|=OB O,T andN=J|J|=OB O,EKA(K G ) . (i)∀I∈M,(I,(M,N),(M,N))(Kξ) =tholds precisely when∀I∈M, I|=ξ. SinceM= I|I|=OB O,T , this means that for allI∈M,I|=OB O,T andI|=ξ. This is equivalent to OB O,T |=ξ. (i)∀I∈M,(I,(M,N),(M,N))(Kξ) =fholds exactly when∃J∈N, J̸|=ξ. SinceN=J| J|=OB O,EKA(K G ) , this condition is equivalent toOB O,EKA(K G ) ̸|=ξ. (i)∀I∈M,(I,(M,N),(M,N))(Kξ) =uholds exactly when∀J∈N, J|=ξand∃I∈M, I̸|=ξ. SinceN=J|J|=OB O,EKA(K G ) , the first condition is equivalent toOB O,EKA(K G ) |=ξ. Since M=I|I|=OB O,T , the second condition is equivalent toOB O,T ̸|=ξ. Since the sameKξ satisfiesKξ∈EKA(K G ) ξ /∈T, both conditions hold. (iv)∀I∈M,(I,(M,N),(M,N))(notξ) =tholds precisely when∃J∈N, J̸|=ξ. this condition is equivalent toOB O,EKA(K G ) ̸|=ξ. (v)∀I∈M,(I,(M,N),(M,N))(notξ) =fholds exactly when∀I∈M, I|=ξ. SinceM= I|I|=OB O,T , this means that for allI∈M,I|=OB O,T andI|=ξ. This is equivalent to OB O,T |=ξ. (vi)∀I∈M,(I,(M,N),(M,N))(notξ) =uholds exactly when∀J∈N, J|=ξand∃I∈M, I̸|= ξ. SinceN=J|J|=OB O,EKA(K G ) , the first condition is equivalent toOB O,EKA(K G ) |=ξ. SinceM=I|I|=OB O,T , the second condition is equivalent toOB O,T ̸|=ξ. Since the same KξsatisfiesKξ∈EKA(K G ) ξ /∈T, both conditions hold. This completes the proof. Lemma B.2.Let(T,F)be a partial partition ofEKA(K G )and let(M,N)be the MKNF inter- pretation induced by(T,F). Then, for every ruler∈P G , ∀I∈M,(I,⟨M,N⟩,⟨M,N⟩)(π(r)) = t iff h(r)[T,F]≥b(r)[T,F] ,whereb(r)[T,F] = minℓ[T,F]|ℓ∈b + (r)∪b − (r). Proof.Fixr∈P G . By definition,π(r)is the formula π(r) = b + (r)∧b − (r) ⊃h(r). 394Hybrid MKNF with Classical Negation in the Rule Component Let(T,F)be the partial partition ofEKA(K G )and let(M,N)be the MKNF interpretation induced by(T,F). Consider the MKNF structure(I,M,N)withM=⟨M,N⟩andN=⟨M,N⟩. Writeb + (r)∧b − (r)asℓ 1 ∧·∧ℓ k , whereℓ 1 ,...,ℓ k =b + (r)∪b − (r). By Equation (5) in Fig. 1.1, (I,M,N)(ℓ 1 ∧·∧ℓ k ) = min(I,M,N)(ℓ i )|1≤i≤k. By Lemma B.1, for every literalℓ, (I,M,N)(ℓ) =ℓ[T,F]. Therefore, (I,M,N)(b + (r)∧b − (r)) = minℓ[T,F]|ℓ∈b + (r)∪b − (r)=b(r)[T,F]. Now apply Equation (6) to the implicationπ(r). Takingφ 1 :=b + (r)∧b − (r)andφ 2 :=h(r), Equation (6) yields (I,M,N)(π(r)) =tiff(I,M,N)(h(r))≥(I,M,N)(b + (r)∧b − (r)). Sinceh(r)is a modal atom, Lemma B.1 gives (I,M,N)(h(r)) =h(r)[T,F]. Combining the above equalities, we obtain (I,M,N)(π(r)) =tiffh(r)[T,F]≥b(r)[T,F], as required. Theorem B.1.LetK G = (O,P G )be a groundhMKNF¬knowledge base. Let(T,F)be a partial partition ofEKA(K G ).(T,F)is stable if and only if the three-valued MKNF interpretation (M,N)induced by(T,F)is a three-valued MKNF model ofK G . Proof.To prove the theorem, it suffices to establish the following three conditions: 1.Three-valued interpretation. We show that(M,N)is a three-valued interpretation, that is, ∅⊆N⊆M. 2. Satisfaction condition. We show that(M,N)satisfies the knowledge baseK G , namely, K G |= (M,N),which is equivalent to∀I∈M: (I,⟨M,N⟩,⟨M,N⟩) π(K G ) =t. 3.Maximality criterion. We show that there exist no interpretations(M ′ ,N ′ )such thatM⊆M ′ andN⊆N ′ with at least one inclusion being proper, and(I,⟨M,N⟩,⟨M,N⟩) π(K G ) ̸=t. Three-valued interpretation: Inclusion∅⊆N⊆M.From Definition 3.5,OB O,EKA(K G ) is satisfiable (condition (i)). Therefore, there exists an interpretationJsuch thatJ|=OB O,EKA(K G ) , which implies thatN̸=∅, and hence∅⊆N. We now show thatN⊆M. LetJ∈N. By definition ofN,J|=OB O,EKA(K G ) . SinceT⊆EKA(K G ) , every model ofOB O,EKA(K G ) is also a model ofOB O,T . Thus,J|=OB O,T , and thereforeJ∈M. The converse inclusion does not hold in general. Indeed, there may exist an interpretationI∈Msuch thatI|=OB O,T butI̸|=OB O,EKA(K G ) , sinceOB O,EKA(K G ) may contain axioms not present inOB O,T . Consequently,M⊈Nin general. A.R.N. Sheela, C. Rey & F. De Grancey395 Satisfaction condition:(M,N)|=K G .By definition, we haveπ(K G ) =Kπ(O)∧π(P G ).Thus, to show that(M,N)|=K G , it suffices to prove that(M,N)|=Kπ(O)and(M,N)|=π(P G ). By Proposition 3.1,π(O)is satisfied by every interpretationI∈M. Hence,(M,N)|=Kπ(O). It remains to show that(M,N)|=π(P G ). From Definition 3.5, condition (i), for every rule π(r)∈π(P G )and every interpretationI∈M, we have∀I∈M: (I,⟨M,N⟩,⟨M,N⟩)(π(r)) =t. Therefore,∀I∈M: (I,⟨M,N⟩,⟨M,N⟩)(π(P G )) =t.Consequently,(M,N)|=Oand(M,N)|=P G which implies(M,N)|=K G . Maximality criterion.We show that there exists no pair(M ′ ,N ′ )such thatM⊆M ′ and N⊆N ′ , with at least one inclusion being proper, and(M ′ ,N ′ )|=K G . Assume towards a contradiction that there exists a three-valued MKNF interpretation(M ′ ,N ′ )such thatM⊆M ′ andN⊆N ′ , with at least one inclusion being proper, and(M ′ ,N ′ )is three-valihed MKNF model that is,(M ′ ,N ′ )|=K G . Let(T ′ ,F ′ )be the partial partition induced by(M ′ ,N ′ ). By Proposition 3.1,OB O,T ′ ⊆OB O,T andOB O,EKA(K G ) ′ ⊆OB O,EKA(K G ) , sinceM⊆M ′ and N⊆N ′ , and monotonicity ofOB O,· ,T ′ ⊆TandF⊆F ′ , with at least one inclusion being proper. Moreover, since(M ′ ,N ′ )|=K G , the condition of Definition 3.5(i) holds for(T ′ ,F ′ ), contradicting Definition 3.5(i). Hence, no such(M ′ ,N ′ )exists, and(M,N)is maximal. Therefore,(M,N)is a three-valued MKNF model ofK G = (O,P G ). Conversely, let(M,N)be a three-valued MKNF model ofK G , and let(T,F)be the partial partition induced by(M,N). We show that(T,F)is a stable partition according to Definition 3.5. Condition (i).Since(M,N)is a three-valued MKNF model, Proposition B.1 guarantees that OB O,EKA(K G ) is satisfiable. Hence, Condition (i) holds. Condition (i).Condition (i) consists of two parts. Condition (i.1).LetKξ∈EKA(K G ). IfOB O,T |=ξ, then by Proposition B.1, every interpretationI∈Msatisfiesξ. Hence,Kξ∈T. IfOB O,EKA(K G ) ̸|=ξ, then there exists an interpretation compatible withEKA(K G ) falsifiesξ. this impliesKξ∈F. Therefore, Condition (i.1) is satisfied. Condition (i.2).For every ruler∈P G and every interpretationI∈M, we have∀I∈ M : (I,⟨M,N⟩,⟨M,N⟩)(π(r)) =t,since(M,N)is a three-valued MKNF model, so(M,N)|=K G hence∀I∈M: (I,⟨M,N⟩,⟨M,N⟩)(π(P G )) =t,. Thus, Condition (i.2) holds. Condition (i).Since(M,N)is a three-valued MKNF model, there exists no three-valued MKNF interpretation(M ′ ,N ′ )such thatM⊆M ′ andN⊆N ′ ,for whichK G |= (M ′ ,N ′ ). M⊆M ′ andN⊆N ′ ,atleast on of the inclusion being proper Let(T ′ ,F ′ )be a partial partition induced by(M ′ ,N ′ )such thatT ′ ⊆TandF⊆F ′ , with at least one of these inclusions being proper. Consequently, at least one of the following holds: •there existsKξ∈EKA(K G ) ′ such thatOB O,T ′ |=ξ; or •there existsKξ∈EKA(K G ) ′ such thatOB O,EKA(K G ) ′ ̸|=ξ; or •there exists a ruler∈P G such that for allI∈M ′ ,(I,⟨M ′ ,N ′ ⟩,⟨M,N⟩)(π(r)) =f. 396Hybrid MKNF with Classical Negation in the Rule Component Hence, Condition (i) is satisfied. All conditions of Definition 3.5 are satisfied. Therefore, the induced partition(T,F)by a three-valued MKNF model(M,N)is a stable partition. Proposition B.2.LetK G = (O,P G )be a groundhMKNF¬knowledge base.(T,F)is a sta- ble partition ofEKA(K G )if and only if (i)T= Γ(F), (i)F=Fa(EKA(K G ) )and (i) OB O,Γ(EKA(K G ) ) is satisfiable. Proof.LetK G = (O,P G )be a ground hybrid MKNF knowledge base, and let(T,F)be a partial partition ofEKA(K G ). By Proposition 3.1, the partition(T,F)induces a three-valued MKNF interpretation(M,N). To show that(M,N)is a three-valued MKNF model ofK G , it suffices to establish that(T,F)is a stable partition. According to Definition 3.5, this requires showing three conditions. Here we prove that if a partial partition(T,F)satisfiesT= Γ(F),F=Fa(EKA(K G ) ), andOB O,Γ(EKA(K G ) ) is satisfiable, then it satisfies all the conditions of a stable partition. (i)T= Γ(F), whereΓ(F)is the least fixpoint ofT F K G , and T F K G (X) =h(r)|r∈P G , b + (r)⊆X,K(b − (r))⊆F ∪Kξ|Kξ∈EKA(K G ),OB O,X |=ξ,(17) Γ(F) =lfp(T F K G ). Fix an arbitrary ruler∈P G and write π(r) =b + (r)∧b − (r)⊃h(r). Let(X n ) n≥0 be the sequence defined by X 0 =∅andX n+1 =T F K G (X n ) (n≥0). SinceT F K G is monotone andEKA(K G )is finite, the sequence stabilizes at somek, that is, X k =X k+1 , and hence Γ(F) =lfp(T F K G ) = [ n≥0 X n . In particular,X 1 =T F K G (X 0 )contains exactly: (i) all headsh(r)of rulesr∈P G whose positive body is empty, that is,b + (r) =∅, and whose negative modal conditions satisfyK(b − (r))⊆F; and (i) all modal atomsKξ∈EKA(K G )such thatOB O,∅ |=ξ. More generally, for everyn≥0, X n+1 contains the heads of all rulesrsuch thatb + (r)⊆X n andK(b − (r))⊆F, together with all Kξentailed byOB O,X n . Γ(F)containsh(r)for all rulesr∈P G such thatb(r)[T,F]is true.b + (r)⊆X,andK(b − (r))⊆ F.Kξ|Kξ∈EKA(K G ),OB O,X |=ξwill ensure that for everyKξ∈EKA(K G ),OB O,T |=ξ impliesKξ∈T. Thus,T= Γ(F)shows that all derivable modal atoms with respect toFare in T. TU EKA(K G ) K G (X) =h(r)|r∈P G , b + (r)⊆X,K(b − (r))⊆(EKA(K G ) )andOB O,X ̸|= h(r) ∪Kξ|Kξ∈EKA(K G ),OB O,X |=ξ,(18) Let(Y n ) n≥0 be the sequence defined by Y 0 =∅andY n+1 =TU EKA(K G ) K G (Y n ) (n≥0). A.R.N. Sheela, C. Rey & F. De Grancey397 SinceEKA(K G )is finite, the sequence stabilizes at somek, that is,Y k =Y k+1 , and we denote Γ ′ (EKA(K G ) ) =lfp TU EKA(K G ) K G = [ n≥0 Y n . In particular,Y 1 =TU EKA(K G ) K G (Y 0 )contains exactly: (i) all headsh(r)of rulesr∈P G such thatb + (r) =∅,K(b − (r))⊆(EKA(K G ) ), andOB O,∅ ̸|=h(r); and (i) all modal atoms Kξ∈EKA(K G )such thatOB O,∅ |=ξ. More generally, for everyn≥0,Y n+1 contains the heads of all rulesrsuch thatb + (r)⊆Y n , K(b − (r))⊆(EKA(K G ) ), andOB O,Y n ̸|=h(r), together with all modal atomsKξentailed by OB O,Y n . LetΓ ′ (S)be the least fixpoint ofTU S K G , which containsh(r)for all rulesr∈P G such that b(r)[T,F]is true or possibly true (undefined). Modal atoms that cannot be derived in this way are considered false and belong toFa(EKA(K G ) ), defined asEKA(K G )\Γ ′ (EKA(K G ) ). This also satisfyOB O,EKA(K G ) ̸|=ξimpliesKξ∈F; The only potential violation arises when there exists a ruler∈P G such thatb(r)[T,F] =u andh(r)[T,F] =t; soh(r)[T,F] =fhence r will not satisfied withrespect to(T,F)however, this case is excluded by the satisfiability ofOB O,Γ(EKA(K G ) ) .Γ(EKA(K G ) ). Moreover, the satisfiability ofOB O,EKA(K G ) ensures that the partition(T,F)induces a three-valued MKNF model(M,N)according to Proposition 3.1. Hence, conditions i.1 and i.2 of Definition 3.5 are satisfied. We must show that for every partial partition(T ′ ,F ′ )such thatT ′ ⊆TandF⊆F ′ ,with at least one inclusion being proper, there exists a ruler∈P G such that the MKNF interpretation(M ′ ,N ′ )induced by(T ′ ,F ′ ) satisfies (I,(M ′ ,N ′ ),(M,N))(π(r)) =f. The maximality proof follows fromT= Γ(F)andF=Fa(EKA(K G ) ), since the least fixpoint construction implies that there is no smaller set that still satisfies the required conditions. Theorem B.2(Well-founded Model).LetK G be a groundhMKNF¬knowledge base. If(T W ,F W ) is the well-founded partition ofK G , then the MKNF interpretation pair(M W ,N W )induced by (T W ,F W )is the well-founded model ofK G . Proof.Let(T W ,F W )be the well-founded partition ofK G , and let(T,F)be any stable partition ofK G . By Definition 3.7, we haveT W ⊆TandF W ⊆F. SinceT W ⊆T, every interpretation that satisfiesOB O,T also satisfiesOB O,T W . Thus, I|I|=OB O,T ⊆I|I|=OB O,T W . this impliesM⊆M W (From Proposition B.1). Similarly, fromF W ⊆Fit follows thatEKA(K G ) ⊆EKA(K G ) W . Hence, I|I|=OB O,EKA(K G ) W ⊆I|I|=OB O,EKA(K G ) , which impliesN W ⊆N. Therefore, for every three-valued MKNF model(M,N)induced by a stable partition ofK G , we haveM⊆M W andN W ⊆N. That is,(M W ,N W )is minimal with respect to the information ordering defined by(M W ,N W )⪯ k (M,N)iffM⊆M W andN W ⊆N, such that for all three-valuhed MKNF model(M,N)as introduced in [5]. Consequently,(M W ,N W ) is the well-founded MKNF model ofK G . 398Hybrid MKNF with Classical Negation in the Rule Component Proposition B.3.LetK G = (O,P G )be a groundhMKNF¬knowledge base and(T ω ,F ω )a fixpoint of the well-founded operatorW K G . For any modal atomKH∈EKA(K G ), withHof the formξor¬ξ, and for every stable partition(T,F)ofK G , the following holds:KH∈T ω implies KH∈T, andKH∈F ω impliesKH∈F. Proof. LetW K G ↑0 = (∅,∅)andW K G ↑(i+ 1) =W K G (W K G ↑i)for alli≥0, and writeW K G ↑ i= (T i ,F i ). Let an arbitrary stable partition ofK G and denote it by(T,F). We prove by induction oni≥0the following property(I i ): For every ground modal atom KH∈EKA(K G ), ifKH∈T i thenKH∈T, and ifKH∈F i thenKH∈F. Base case (i= 0).SinceW K G ↑0 = (∅,∅),(I 0 )holds trivially. Induction step.Assume that(I i )holds forW K G ↑i= (T i ,F i ). We show that(I i+1 )holds for W K G ↑(i+ 1) = (T i+1 ,F i+1 ) =W K G (T i ,F i ). Induction hypothesis(IH1).For every ground modal atomKH∈EKA(K G ), ifKH∈T i then KH∈T, and ifKH∈F i thenKH∈F. By Definition 4.2, (T i+1 ,F i+1 ) =W K G (T i ,F i ) = T F i K G (T i ),F K G (T i ,F i ) . We first prove the first part of(I i+1 ), namely that for every ground modal atomKH∈ EKA(K G ), ifKH∈T i+1 thenKH∈T. Thus, it suffices to show thatKH∈T F i K G (T i )implies KH∈T. By Definition 3.6, T F i K G (T i ) =h(r)|r∈P G , b + (r)⊆T i ,K(b − (r))⊆F i ∪ Kξ|Kξ∈EKA(K G ),OB O,T i |=ξ. This definition consists of two parts. We denote the rule part as T F i P G (T i ) =h(r)|r∈P G , b + (r)⊆T i ,K(b − (r))⊆F i , and the ontology part as T F i O (T i ) =Kξ|Kξ∈EKA(K G ),OB O,T i |=ξ. We consider the two cases separately. Rule case.LetKH∈T F i P G (T i ). Then there exists a ruler∈P G of the form h(r)←b + (r),b − (r), where b + (r) =KA 1 ,...,KA n andb − (r) =notB 1 ,...,notB m . By definition,KH∈T F i P G (T i )if and only ifh(r) =KHand KA 1 ,...,KA n ⊆T i andKB 1 ,...,KB m ⊆F i . A.R.N. Sheela, C. Rey & F. De Grancey399 By the induction hypothesis IH1,KA k ∈Tfor allk(1≤k≤n) andKB l ∈Ffor alll (1≤l≤m) . Hence, the body ofris satisfied with respect to(T,F), and thereforeKH∈T. The caseK¬His analogous. Ontology case.LetKH∈T F i O (T i ). By definition, OB O,T i |=H, or respectivelyOB O,T i |=¬Hin the case ofK¬H. By the induction hypothesis IH1, every modal atom occurring inT i is included inTand OB O,T i |=H. Hence follow thatKH∈T. SinceT i is included in all stable partition and OB O,T i |=Hstates thatKHis also included inTThe caseK¬His analogous.(B) Atoms in F i+1 .Recall thatF i+1 =F (T i ,F i ) K G is the union of all unfounded sets with respect to(T i ,F i ). Let KH∈F i+1 (respectively,K¬H∈F i+1 ). We show thatKH(respectively,K¬H) belongs toF. From IH1, every modal atom inT i is included inT, and every modal atom inF i is included inF. Case 1 (Coherency principle).Assume thatOB O,T i | =H, whereA=¬Aand¬A=A. Moreover, by IH1, everyKH∈T i also belongs toT. Hence, ifOB O,T i |=H, thenKH∈F i+1 . Consequently, KH(respectively,K¬H) belongs toF. Case 2KH(respectively,K¬H) belongs to some unfounded setUFwith respect to(T i ,F i ). for every a set of rulesR⊆P G such thathead(R)∪OB O,T |=H, and for allR ′ ⊂R,head(R ′ )∪ OB O,T i ̸| =H, and for eachKξ∈F i , the sethead(R)∪OB O,T i ∪ξis satisfiable; there exists a ruler∈Rof the formh(r)←b + (r),b − (r)such that at least one of the following holds: Moreover, for every such setRthere exists a ruler∈Rfor which at least one of the following conditions holds: 1.body + (r)∩F i ̸=∅; 2.body − (r)∩T i ̸=∅; 3.body + (r)∩UF̸=∅. We show that in each case there exist ar∈Rwhereb(r)is not satisfied with respect to the stable partition(T,F), contradicting the assumed support. If (1) holds, takeKA∈body + (r)∩F i . By IH1,KA∈F, and hence the positive body ofris not satisfied with respect to(T,F). If (2) holds, takeKB∈body − (r)∩T i . By IH1,KB∈T, and therefore the negative body literal ofris violated with respect to(T,F). If (3) holds, takeKA∈body + (r)∩UF. SinceUF⊆F i+1 andF i+1 ⊆F, it follows that KA∈F. Hence, the positive body ofris not satisfied with respect to(T,F). In all cases, the assumed setRis required to entailKHfrom the objective knowledgeOB O,T i ∪head(R) (respectively,K¬H). Moreover, for each such assumed setR, there exists at least one ruler∈R whose body is false with respect to(T i ,F i ). By the induction hypothesis IH1,(T i ,F i )is included in every stable partition(T,F). SinceKHis declared false with respect to(T i ,F i ), it follows thatKH(respectively,K¬H) belongs toF. Proposition B.4.LetK G = (O,P G )be a groundhMKNF¬knowledge base and(T E ,F E )a fixpoint ofE K G . For any modal atomKH∈EKA(K G ), withHof the formξor¬ξ, and for every stable partition(T,F)ofK G , the following holds:KH∈T E impliesKH∈T, andKH∈F E impliesKH∈F. 400Hybrid MKNF with Classical Negation in the Rule Component Proof.LetE (T ω ,F ω ) K G ↑0 = (∅,∅)andE (T ω ,F ω ) K G ↑(i+ 1) =E (T ω ,F ω ) K G (E (T ω ,F ω ) K G ↑i)for alli≥0, and writeE (T ω ,F ω ) K G ↑i= (T i ,F i ). Fix an arbitrary stable partition ofK G = (O,P G )and denote it by(T,F). We prove by induction oni≥0the following property(I i ): for every ground modal atom KH∈EKA(K G ), ifKH∈T i thenKH∈T, and ifKH∈F i thenKH∈F. Base case (i= 0).SinceE (T ω ,F ω ) K G ↑0 = (∅,∅), property(I 0 )holds trivially. Induction step.Assume that(I i )holds forE (T ω ,F ω ) K G ↑i= (T i ,F i ). We show that(I i+1 )holds for (T i+1 ,F i+1 ) =E (T ω ,F ω ) K G (T i ,F i ). Induction hypothesis (IH).For everyKH∈EKA(K G ), ifKH∈T i thenKH∈T, and ifKH∈F i thenKH∈F. By Definition 4.5, (T i+1 ,F i+1 ) = UPT (T ω ,F ω ) K G (T i ,F i )∪T F i K G (T i ), UPF (T ω ,F ω ) K G (T i ,F i )∪F K G (T i ,F i ) . We consider atoms added toT i+1 andF i+1 separately. (A) Atoms inT i+1 .LetKH∈T i+1 . Then eitherKH∈T F i K G (T i )orKH∈UPT (T ω ,F ω ) K G (T i ,F i ). Ontology and rule case.IfKH∈T F i K G (T i ), then the argument is identical to the corresponding case for the well-founded operator in Proposition 4.1. Unit-propagation case.LetKH∈UPT (T ω ,F ω ) K G (T i ,F i ). By Definition 4.4, there exists a ruler∈P G such that: •OB O,T ω ∪T i |=h(r), •b + (r)⊆T ω ∪T i , •K(b − (r))∩(T ω ∪T i ) =∅, •K(b − (r))\(F ω ∪F i ) =KH. By IH, all modal atoms inT i (resp.F i ) are contained inT(resp.F). In-order to satisfy the body ofris satisfied with respect to(T,F)KHmust be true sinceKH∈b − (r)it follows that KH∈T. (B) Atoms inF i+1 .LetKH∈F i+1 . Then eitherKH∈F K G (T i ,F i )orKH∈UPF (T ω ,F ω ) K G (T i ,F i ). Ontology and unfoundedness case.IfKH∈F K G (T i ,F i ), then the argument follows from Proposi- tion 4.1. Unit-propagation case.IfKH∈UPF (T ω ,F ω ) K G (T i ,F i ), then by Definition 4.4 there exists a rule r∈P G such that: •OB O,T ω ∪T i |=h(r), •K(b − (r))⊆F ω ∪F i , •b + (r)∩(F ω ∪F i ) =∅, •b + (r)\(F ω ∪F i ) =KH. A.R.N. Sheela, C. Rey & F. De Grancey401 By IH, all modal atoms inT i (resp.F i ) are contained inT(resp.F). In-order to satisfy the body ofris satisfied with respect to(T,F)KHmust be false sinceKH∈b + (r)it follows that KH∈F.Conclusion.In all cases, atoms added toT i+1 (resp.F i+1 ) belong toT(resp.F). Thus, (I i+1 )holds. By induction, the claim holds for alli≥0, and in particular for the least fixpoint(T E ,F E ) = E (T ω ,F ω ) K G ↑ω. Proposition B.5.LetK G = (O,P G )be a groundhMKNF¬knowledge base, and letOut(K G ) denote the output of Algorithms 1, 2, and 3. (1) IfOut(K G ) =⊥, thenK G is MKNF-inconsistent. (2) IfOut(K G ) = (T W ,F W ), then(T W ,F W )is the well-founded partition ofK G , and the induced three-valued MKNF interpretation(M W ,N W )is the well-founded MKNF model ofK G . (3) If Out(K G ) =NoWFM, thenK G has no well-founded model. Proof.Result (1). Let(T i ,F i )be a partial partition produced at some iteration ofW K G or E (T ω ,F ω ) K G . By Propositions 4.1 and 4.2,(T i ,F i )is contained in every stable partition ofK G . If T i ∩F i ̸=∅, then some modal atom is both true and false, which is impossible in any three-valued MKNF model; hence,K G is MKNF-inconsistent. IfOB O,T i is unsatisfiable, then no MKNF interpretation pair induced via(T i ,F i )(Proposition 3.1), and consequently no three-valued MKNF model ofK G exists. Therefore, ifOut(K G ) =⊥, thenK G is MKNF-inconsistent. Result (1). Let(T,F)be an arbitrary stable partition ofK G . By Proposition 4.1, Proposi- tion 4.2, and Algorithm 3, for every modal atomKH∈EKA(K G ), ifKH∈T W thenKH∈T, and ifKH∈F W thenKH∈F. HenceT W ⊆TandF W ⊆F. Since(T W ,F W )is itself a stable partition from Proposition 3.2, it follows by Definition 3.7 that(T W ,F W )is the well-founded partition and its induced three-valued MKNF interpretation(M W ,N W )is the well-founded model from Theorem 3.2. Proposition B.6.LetK G = (O,P G )be a DL-safehMKNF¬knowledge base. Assume data complexityC 1 for computing unfounded sets with respect to a partial partition(T,F), andC 2 for DL satisfiability and ground entailment. Let(T 1 W ,F 1 W )and(T 2 W ,F 2 W )be the partitions obtained after Phase 2 and Phase 3, respectively.(i)If(T 1 W ,F 1 W )coincides with the well-founded partition ofK G , then it can be computed with data complexityPTime C 1 ∪C 2 .(i)If(T 2 W ,F 2 W )coincides with the well-founded partition ofK G then it can be computed with data complexity isEXPTime P C 1 . Proof.(i)If(T 1 W ,F 1 W )coincides with the well-founded partition ofK G , then it can be computed with data complexityPTime C 1 ∪C 2 . Suppose(T 1 W ,F 1 W ) =W K G ↑ω. Here, W K G (T,F) = T F K G (T), F K G (T,F) . The computation ofF K G (T,F)(unfounded sets) has data complexityC 1 . The computation of T F K G (T)depends on the data complexityC 2 for DL satisfiability and ground entailment. The operatorW K G is applied over the finite setEKA(K G ), henceW K G ↑ω reaches a fixpoint in at most2|EKA(K G )|iterations. Therefore,(T 1 W ,F 1 W ) =W K G ↑ωcan be computed by iteratingW K G a polynomial number of times, where each iteration depends on computations inC 1 andC 2 . Suppose(T 1 W ,F 1 W ) =E K G ↑ω, where E (T ω ,F ω ) K G (X,Y) = UPT (T ω ,F ω ) K G (X,Y)∪T Y K G (X), UPF (T ω ,F ω ) K G (X,Y)∪F K G (X,Y) . 402Hybrid MKNF with Classical Negation in the Rule Component The computations ofT F K G (T)andF K G (T,F)are as above, as are the computations of UPT (T ω ,F ω ) K G (X,Y)andUPF (T ω ,F ω ) K G (X,Y). In the worst case,E (T ω ,F ω ) K G (X,Y)↑ωreaches a fixpoint in at most|EKA(K G )|iterations. (i)If(T 2 W ,F 2 W )coincides with the well-founded partition ofK G then it can be computed with data complexity isEXPTime P C 1 . Let(T,F)be the partial partition obtained after Phase 2, and let U=EKA(K G )\(T∪F) be the set of atoms whose truth value is still undetermined. Any completion of(T,F)into a total partition overEKA(K G )assigns to each atom inUone of the three statuses: true, false, or undefined. Hence, the number of completions is bounded by3 |U| . Phase 3 enumerates all such completions, producing at most3 |U| candidates(T ′ ,F ′ )extending (T,F). For each candidate(T ′ ,F ′ ), the algorithm checks whether(T ′ ,F ′ )is a stable partition ofK G . This check can be carried out in polynomial time in the data, with oracle access to unfounded set computation of data complexityC 1 [7]. Therefore, the per-candidate verification runs inP C 1 . Consequently, the overall computation time is bounded by 3 |U| with oracle access toC 1 , and thus belongs toEXPTime P C 1 in data complexity. Finally, once the set of stable partitions has been computed (in the worst case containing up to3 |U| candidates), selecting(T 2 W ,F 2 W )from this set requires comparing candidates and thus takes at most exponential time in|U|. Therefore, the selection step does not increase the overall data-complexity bound, and(T 2 W ,F 2 W )can be computed with data complexityEXPTime P C 1 .

Instant research discovery