A logic-algebraic tool for reasoning with Knowledge-Based Systems

A logic-algebraic tool for reasoning with Knowledge-Based Systems1 Jos´e A. Alonso-Jim´enez1, Gonzalo A. Aranda-Corral2, Joaqu´ın Borrego-D´ıaz1, M. Magdalena Fern´andez-Lebr´on3, M. Jos´e Hidalgo-Doblado1 1Departamento de Ciencias de la Computaci´on e Inteligencia Artificial, E.T.S. Ingenier´ıa Inform´atica, Universidad de Sevilla, Avda. Reina Mercedes s.n. 41012-Sevilla, Spain 2Department of Information Technology, Universidad de Huelva Crta. Palos de La Frontera s/n. 21819 Palos de La Frontera. Spain 3Departamento de Matem´atica Aplicada I, E.T.S. Ingenier´ıa Inform´atica, Universidad de Sevilla, Avda. Reina Mercedes s.n. 41012-Sevilla, Spain Abstract A detailed exposition of foundations of a logic-algebraic model for reasoning with knowledge bases specified by propositional (Boolean) logic is presented. The model is conceived from the logical translation of usual derivatives on polynomials (on residue rings) which is used to design a new inference rule of algebro-geometric inspiration. Soundness and (refutational) completeness of the rule are proved. Some applications of the tools introduced in the paper are shown. Keywords: Polynomial Semantics, Symbolic Computing, Automated Deduction, Knowledge-Based Systems 1. Introduction Algebraic models for logic have been revealed as a useful tool for knowledge representation and mechanized reasoning. The relationship between certain algebraic structures and Computational Logic provides methods and tools for building, compiling and reasoning with Knowledge-Based Systems 1This work was partially supported by TIN2013-41086-P project (Spanish Ministry of Economy and Competitiveness), co-financed with FEDER funds. Preprint submitted to Elsevier (KBS) (see e.g. [1] for an introduction). This relationship also provides mathematical foundations for a number of Knowledge Representation and Reasoning (KRR) methods and algorithms, encompassing applications since the pioneer works for classical bivalued logic [2, 3] to extensions for multivalued logics [4, 5, 6, 7]. The framework has also been extended to other logics for Artificial Intelligence (AI) as the paraconsistent logic [8], and even towards other nonstandard reasoning tasks as the argument-based one (cf. [9]). One of the benefits of the interpretation of logic in polynomial rings is that enables the use of powerful algebraic tools as Gr¨obner Basis to compile KBS, exploiting this way the use of advanced Computer Algebra Systems in KRR. Roughly speaking, algebraic models for logic are mainly based on to specify, obtain and exploit solutions for the logical entailment problem and other related ones. Recall that the entailment problem in logic is stated as follows: given a Knowledge Base (KB) K, and a formula F, to decide whether Fis a logical consequence from K(denoted by K|=F), that is, whether every model of Kis also model of F. This paper is focused in to expound with detail an(other) algebraic model for KRR. Whilst aforementioned approaches do not need to design a new calculus (ideal membership translation -through Gr¨obner Basisof entailment question is sufficient), the approach presented here consists of to design an inference rule -called independence rulefrom an algebraic operation on polynomials2. This rule will allow address a number of other related problems. Although the independence rule is inspired in Algebra, the idea is intimately related with KRR strategies which are oriented to mitigate the complexity and size of the KB (which may be of large size), with the hope of reducing the computational cost of the deductive process when it is applied into specialized contexts or use cases. Two strategies of this type are interesting for the purposes of the paper and motivate this work. The first is to facilitate the design of divide-and-conquer strategies to deal with the entailment problem, a natural idea for managing KBs with hundreds of thousands of logical axioms with big size logical language (for example the strategy based on the reasoning with microtheories [11]). In this case the problem of ensuring the completeness of the designed strategy arises, being a critical issue the selection/synthesis of sound sub-KBs. In [12] 2The part of the paper devoted to this is an extended version of [10]. 2 authors propose a partition-based strategy in order to obtain subtheories. It is based on a syntax level analysis that provides individual partitions where to reason locally, and distributed reasoning needs of methods to propagate information among different partitions. The second strategy to consider is based on the ad-hoc reduction of KB for particular use cases (distilling the KB for using in context-based reasoning, for example). In [10] authors propose to reduce Kto K0, where K|=K0, and in K0only the language of the goal formula Fis used (thus it is expected that the size of K0to be smaller than the size of K). Then the entailment problem with respect to K0is considered. For this strategy to be successful -valid and completeKmust be a conservative extension of K0(or, equivalently, K0a conservative retraction of K[10]). A knowledge base K0in the language L0 is a conservative retraction of Kif Kis an extension of K0such that every L0-f´ormula entailed by Kis also entailed by K0. Then the use of conservative retraction allows to reduce the own KB we need to work, because it suffices to conservatively retracts the original KB to the specialized language of the formula-goal. A key question is how to compute such kind of sub-KBs. Whilst conservative extensions have been deeply investigated in several fields of Mathematical Logic and Computer Science (because they allow the formalization of several notions concerning refinements and modularity, see e.g. [13, 14, 15]), solutions focused on its dual notion, the conservative retraction, are obstructed by its logical complexity (see e.g. [16]). Beside the analysis of above strategy, as a secondary motivation of the approach, it is worth to mention the study of relevance in knowledge bases. To analyze, locate and remove redundancies in KB is a way to refine and improve the efficiency of KBS. These type of analysis are important in topics such as probabilistic reasoning, information filtering, etc. (see also [16] for a general overview). The basic mechanism to obtain conservative retractions consists of eliminating, step by step, the variables that we wish to eliminate from language. Such a mechanism is called variable forgetting. Since the first analysis in cognitive robotics [17], the problem of variable forgetting is a widely studied technique in IA. In particular the forgetting variable technique has been used to update or refine (logical, rule-based, CSP) programs. For example for resolution-based reasoning in specialized contexts (see e.g. [18]), in CSP and optimization [19], for simplification of rules [20] (included Answer Set Programming [21]). As it can be seen from these references, the interest in techniques for forgetting variables is not limited to classical (monotonous) 3 logics. It has also received attention in the field of non-monotonous reasoning (including the computational complexity of the problems). In the (epistemic) modal logics for (multi)agency this technique would be very useful to represent knowledge-based games [22, 23]. In addition, in the reasoning under inconsistency the use of variable forgetting allows to weaken the KB to obtain consistent subKBs (eliminating the variables involved in the inconsistency). This topic, discussed below, is studied as a tool for solving SAT. In this context, providing methods for variable forgetting is a step towards the availability of retraction algorithms for programming paradigms based on logics of different nature. Taking into account the aforementioned motivations, the aim of this paper is twofold. First, we intend to present a complete and detailed exposition of the foundations of the independence rule (That can be considered a tool for variable forgetting), whose basic ideas were published in [10], since no detailed exposition has been published until now. In fact, we generalize the cited paper by stating the results for any operator that induces a conservative retraction, leading as consequence that our case, the independence rule, is useful to compute the retractions. It is also illustrated how the rule is useful to design methods for solving some questions on KB. In particular the redundancy problem can be handled by the independence rule and Boolean derivatives (an essential tool to design this rule). The structure of the paper is as follows. Section 2 is devoted to summarize the basics on the algebraic interpretation of propositional logics. In Sect. 3 the notion of forgetting operator is introduced, and we show how conservative retractions can be computed by means of these kind of operators, as well as logical calculus induced by them are sound and (refutationally) complete. Section 4 presents a forgetting operator inspired on the projection of algebraic varieties. The logical translation of the operator is presented as a inference rule in Sect. 5. Boolean derivatives are used for characterizing logical relevance (in the case of sensitive variables) in algebraic terms (in section 6, Prop. 6.3). Some illustrative applications of the tools presented are described in Sect. 7. The paper finishes with a discussion on the results presented in the paper as well as some ideas about future work. 2. Background In this section fundamental relations between propositional logic and polynomials with coefficients in finite fields (in our case, the finite field with 4 Figure 1: The framework two elements, F2) are summarized. The main idea guiding the algebraic interpretation of logic is to identify a logical formula as a polynomial in such a way that the truth-value function induced by the formula could be understood as a polynomial function on F2. The diagram showed above (Fig. 1) depicts the relationship between both structures, whose elements will be detailed in the following subsections. The ideal I2:= hx1+x2 1, . . . , xn+x2 ni ⊆ F2[x] -on which we will talk about lateris used, and the map proj is the natural projection on the quotient ring. The remain elements of the diagram will be detailed bellow. We assume throughout the paper that the reader is familiar with propositional logic as well as with basic principles on polynomial algebra on positive characteristics. 2.1. Propositional logic and conservative retraction A propositional language is a finite set L={p1, . . . , pn}of propositional symbols (also called propositional variables). The set of formulas Form(L) is built up from in the usual way, using the standard connectives ¬,∧,∨,→ and >(>denotes the constant true, and ⊥is ¬>). Given two formulas F, G and p∈ L, we denote F{p/G}the formula obtained replacing every occurrence of pin Fby the formula G. An interpretation (or valuation) vis a function v:L→{0,1}. An interpretation vis a model of F∈Form(L) if it makes Ftrue in the usual classical truth functional way. Analogously, it is said that a vis a model of K(v|=K) if vis model of every formula in K. We denote by Mod(F) the set of models of F(resp. Mod(K) for the set of models of K). 5 A formula F(or Ka KB) is consistent if it exhibits at least one model. It is said that Kentails F(K|=F) if every model of Kis a model of F, that is, Mod(K)⊆Mod(F). Both notions can be naturally generalized to a KB, preserving the same notation. It is said that Kand K0are equivalent, K0≡K, if K|=K0and K0|=K. The same notation will also be used for the equivalence with (and between) formulas. It is said that Kis an extension of K0if L(K0)⊆ L(K) and ∀F∈Form(L(K0))[K0|=F=⇒K|=F] Kis a conservative extension of K0(or K0is a conservative retraction of K) if it is an extension such that every logic consequence of K expressed in the language L(K0) is also consequence of K0, ∀F∈Form(L(K0))[K|=F=⇒K0|=F] that is, Kextends K0but no new knowledge expressed by means of L(K0) is added by K. Given L0⊆ L(K), a conservative retraction on the language L0always exists. The canonical conservative retraction of Kto L0is defined as: [K, L0] = {F∈Form(L0) : K|=F} That is, [K, L0] is the set of L0-formulas which are entailed by K. In fact any conservative retraction on L0is equivalent to [K, L0]. The actual issue is to present a finite axiomatization of such formula set. 2.2. Propositional logic and the ring F2[x] The ring F2[x] is naturally chosen for working with algebraic interpretations of logic. To clarify the notation, an identification pi7→ xi(or p7→ xp) between Land the set of indeterminates is fixed. Notation on polynomials is standard. Given α= (α1, . . . , αn)∈Nn, let us define |α|:= max{α1, . . . , αn}. By xαwe denote the monomial xα1 1· · · xαn n. The degree of a(x)∈F2[x], is deg∞(a(x)) :=max{|α|:xαis a monomial of a}. If deg∞(a(x)) ≤1, the polynomial a(x) we shall denote a polynomial formula. It is defined degi(a(x)) as the degree w.r.t. xi. 6 2.3. Translation from formulas and vice versa The translation of Propositional Logics into Polynomial Algebra is based on the following translation (see Fig. 1, left diagram): The map P:Form(L)→F2[x] is defined by: •P(⊥) = 0, P(pi) = xi, P(¬F) = 1 + P(F) •P(F1∧F2) = P(F1)·P(F2) •P(F1∨F2) = P(F1) + P(F2) + P(F1)·P(F2) •P(F1→F2) = 1 + P(F1) + P(F1)·P(F2), and •P(F1↔F2) = 1 + P(F1) + P(F2) For the reciprocal translation (from poynomials to formulas) we use the map Θ : F2[x]→Form(L) defined by: •Θ(0) = ⊥,Θ(1) = >, Θ(xi) = pi, •Θ(a·b) = Θ(a)∧Θ(b), and Θ(a+b) = ¬(Θ(a)↔Θ(b)). It can be proved that Θ(P(F)) ≡Fand P(Θ(a)) = a. Sometimes, for the sake of readability, we will use the following property, that is a straightforward consequence of the previous assertions: Θ(1 + a+ab)≡Θ(a)→Θ(b) 2.4. Correspondence between valuations and points in Fn 2 The similar functional behavior of the formula Fand its polynomial translation P(F) is the basis of the relationship between logical semantics and polynomial functions. Let’s clarify what similar behavior means: •From valuations to points: Given a valuation v:L→{0,1}, the truth value of Fwith respect to vagrees with the value of P(F) on the point of ov∈Fndefined by the values provided by v: if (ov)i=v(pi) then v(F) = P(F)((ov)1, . . . (ov)n) •From points to valuations: Each o= (o1, . . . , on)∈Fn 2induces a valuation vodefined by: vo(pi) = 1 ⇐⇒ oi= 1 7 This way vo|=F⇐⇒ P(F)(ov) + 1 = 0 ⇐⇒ ov∈V(1 + P(F)) where V(.) is the well-known algebraic vanishing operator (see e.g. [24]: given a(x)∈F2[x], V(a(x)) = {o∈Fn 2:a(o) = 0} Summarizing we provide two maps among the set of valuations and points of Fn 2, which are bijections between models of the formula Fand points from the algebraic variety determined by 1 + P(F); Mod(F)→V(1 + P(F)) v7→ ov V(1 + P(F)) →Mod(F) o7→ vo For example, consider the formula F=p1→p2∧p3. The associated polynomial is P(F) = 1+ x1+x1x2x3. The valuation v={(p1,0),(p2,1),(p3,0)} is model of Fand induces the point ov= (0,1,0) ∈F3 2, which belongs to V(1 + P(F)) = V(x1+x1x2x3). 2.5. Polynomial projection Consider now the right-hand side diagram of Fig. 1. To simplify the relation between the semantics of propositional logic and geometry over finite fields we use the map Φ : F2[x]→F2[x] Φ(X α∈I xα) := X α∈I xsg(α) being sg(α) := (δ1, . . . , δn), where δiis 0 if αi= 0 and 1 otherwise. The map Φ selects the representative element of the equivalence class of the polynomial in F2[x]/I2that is a polynomial formula. So to associate a polynomial formula to a propositional formula Fit suffices to apply the composition π:= Φ ◦P, that we will call polynomial projection. For example, P(p1→p1∧p2) = 1 + x1+x2 1x2whereas π(p1→p1∧p2) = 1 + x1+x1x2 8 2.6. Propositional Logic and polynomial ideals We recall here the well-known correspondence between algebraic sets and polynomial ideals on the coefficient field F2, and propositional logic KBs. Given a subset X⊆(F2)n, we denote by I(X) the set (actually an algebraic ideal) of polynomials of F2[x] vanishing on X: I(X) = {a(x)∈F2[x] : a(u) = 0 for any u∈X} Symmetrically, given J⊆F2[x] it is possible to consider the previously mentioned algebraic set V(J), the “vanishing set”: V(J) = {u∈(F2)n:a(u) = 0 for any a(x)∈J} Nullstellensatz theorem for F2is stated as follows (see e.g. [8]): Theorem 2.1. (Nullstellensatz theorem with the coefficient field F2) •If A⊆Fn 2, then V(I(A)) = A, and •for every J∈Ideals(F2[x]),I(V(J)) = J+I2. From the Nullstellensatz theorem it follows that: F≡F0if and only if P(F) = P(F0) (mod I2) Therefore F≡F0if and only if π(F) = π(F0). The following theorem summarizes the main relationship between propositional logic and F2[x]: Theorem 2.2. (see e.g. [4]) Let K={F1, . . . , Fm}and Gbe a propositional formula. The following conditions are equivalent: 1. {F1, . . . , Fm} |=G. 2. 1 + P(G)∈ h1 + P(F1),...,1 + P(Fm)i+I2. 3. Vh1 + P(F1),...,1 + P(Fm)i ⊆ Vh1 + P(G)i Remark 2.3. If the use of Gr¨obner basis is considered, above conditions are equivalent to: 4.NF(1 + P(G),h1 + P(F1),...,1 + P(Fm)i+I2) = 0 where GB(I)denotes the Gr¨obner basis of ideal Iand NF(p,B)denotes a normal form of polinomial prespect to the Gr¨obner basis B. The complete description on Gr¨obner basis is not within the scope of this paper. A general reference for Gr¨obner Basis could be seen in [25]. Readers can find in [5] a quick tour on the use of Gr¨obner Basis in Propositional Logic. 9 due to the fact that both KBs are equivalent to [K, L \ {p, q}]. Therefore, for the sake of simplicity, we will write δQ[K] when syntactic presentation of this KB does not matter. A consequence of corollary 3.8 and theorem 3.7 is that entailment problem can be reduced to a similar problem but that it only uses variables of the goal formula. This property is called the location property: the entailment problem can be simplified by eliminating propositional variables that do not appear in the target formula. Corollary 3.9. (Location Property, [10]) The following conditions are equivalent: 1. K|=F 2. δL\var(F)[K]|=F Proof. It is trivial, because δL\var(F)[K]≡[K, var(F)]. 4. Boolean derivatives and independence rule on polynomials In order to define our forgetting operator we will make use of derivations on polynomials, by translating the usual derivation on F2[x] to an operator on propositional formulas. We review here some basic properties. Recall that a derivation on a ring Ris a map d:R→Rverifying d(a+b) = d(a) + d(b) and d(a·b) = d(a)·b+a·d(b) for any a, b ∈R The logical translation of derivations is builded as follows: Definition 4.1. [10] A map ∂:Form(L)→Form(L)is a Boolean derivative if there exists a derivation don F2[x]such that the following diagram is commutative: Form(L)∂ →Form(L) π↓#↑Θ F2[x]d →F2[x] That is, ∂= Θ ◦d◦π 16 In this paper we are particularly interested in the Boolean derivative, denoted by ∂ ∂p , induced by the derivation d=∂ ∂xp. The following result shows a semantic equivalent expression of this derivative. Proposition 4.2. ∂ ∂p F≡ ¬(F{p/¬p} ↔ F) Proof. It is straightforward to see that π(F{p/¬p})(x) = π(F)(x1, . . . , xp+ 1, . . . , xn) On the other hand it is easy to see that ∂ ∂xa(x) = a(x+ 1) + a(x) holds for polynomial formulas, hence ∂ ∂xp π(F) = π(F)(x1, . . . , xp+ 1, . . . , xn) + π(F)(x1, . . . , xp, . . . , xn) Therefore, by applying Θ we conclude that ∂ ∂pF= Θ( ∂ ∂xp π(F)) ≡ ¬(F{p/¬p} ↔ F) Notice that truth value of ∂ ∂p Fwith respect to a valuation does not depend of the truth value on the own p; hence, we can apply valuations on L\{p} to this formula. In fact, we can describe the structure of Fby isolating the role of pas follows: Lemma 4.3. [10] (p-normal form). Let F∈Form(L)and pbe a propositional variable. There exists F0∈Form(L\{p})such that F≡ ¬(F0↔p∧∂ ∂pF) Proof. Since π(F) is a polynomial formula, we can suppose that π(F) = a+xpbwith degxp(a) = degxp(b) = 0 Therefore F≡Θ(π(F)) ≡ ¬(θ(a)↔p∧Θ(b)) Then let F0= Θ(a), and, since b=∂ ∂xpπ(F), we have that Θ(b) = ∂ ∂p F. 17 Figure 4: Geometric interpretation of independence rule For example, let F=p∧q→r. Then π(F) = 1 + xpxq+xpxqxr= 1 + xp(xq+xqxr) Following the above proof, a= 1 and b=xq+xqxr(note that ∂ ∂xp(π(F)) = xq+xqxr). Therefore Θ(a) = >and Θ(b) = q∧ ¬r, so F≡ ¬(> ↔ p∧(q∧ ¬r)) The forgetting operator that we are going to define next, called independence rule, aims to represent the models of the conservative retraction as those that can be extended to models of F∧G(that is, the idea behind Lifting Lemma). Geometrically, if aand bare the polynomials π(F) and π(G) respectively, then the vanishing set V(1 + a, 1 + b) (which could correspond to the set of models both of Fand G) is projected by ∂p(see Fig. 4). The algebraic expression of the projection is described as a rule. Definition 4.4. The independence rule (or ∂-rule) on polynomial formulas is defined as follows: given a1, a2∈F2[x]and xan indeterminate a1, a2 ∂x(a1, a2) where ∂x(a1, a2) = 1 + Φ (1 + a1·a2)(1 + a1·∂ ∂x a2+a2·∂ ∂x a1+∂ ∂x a1·∂ ∂x a2) 18 If ai=bi+xp·ci,with degxp(bi) = degxp(ci) = 0 (i= 1,2), the rule we can rewritten as: ∂xp(a1, a2) = Φ [1 + (1 + b1·b2)[1 + (b1+c1)(b2+c2)]] For example, to compute a=∂x2(1 + x2x3x5+x3x5,1 + x1x2x3x4x5+x1x2x3x5) we take b1= 1 + x3x5, c1=x3x5and b2= 1, c2= (1 + x4)x1x3x5 so the result is a= 1 + x1x3x4x5+x1x3x5. Note that independence rule is symmetric. 5. Independence rule and non-clausal theorem proving The independence rule for formulas is defined as ∂p(F, G) := Θ(∂xp(π(F), π(G))) Following with above example, ∂p2(p3∧p5→p2, p1∧p2∧p3∧p5→p4) = = Θ(∂x2(1 + x2x3x5+x3x5,1 + x1x2x3x4x5+x1x2x3x5)) = = Θ(1 + x1x3x4x5+x1x3x5) = ¬(p1∧p3∧p4∧p5↔p1∧p3∧p5)≡ ≡p1∧p3∧p5→p4 It is worthy to point out some interesting features of the rule ∂p: if ∂p(F, G) is a tautology, then ∂p(F, G) = >, and if ∂p(F, G) is inconsistent then ∂p(F, G) = ⊥. Both features are consequence of the translation to polynomials: polynomial formulas corresponds of tautologies and inconsistencies are algebraically simplified to 1 and 0 in F2[x]/I2, respectively. In fact, we will usually work with the polynomial projections to exploit these features. Proposition 5.1. ∂pis sound 19 Proof. We have to prove F1∧F2|=∂p(F1, F2). Suppose that π(F1) = b1+xp·c1, π(F2) = b2+xp·c2 According to Thm. 2.2.(3), it is enough to prove that V(1 + π(F1)·π(F2)) ⊆V(1 + ∂xp(π(F1), π(F2))) Let u∈V(1 + π(F1)·π(F2)) ⊆Fn 2, that is, (b1+xpc1)(b2+xpc2)|x=u= 1 (†) (the notation used here is as usual: F(x)|x=uis F(u)). Let us distinguish two cases: •If the p-coordinate of uis 0, then by (†) it follows that b1|x=u=b2|x=u= 1 Therefore (1 + b1b2)|x=u= 0. •The p-coordinate of uis 1. In this case (b1+c1)(b2+c2)|x=u= 1 By examining the definition of ∂pwe conclude in both cases that ∂xp(π(F1), π(F2))|x=u= 1 so we have that u∈V(1 + ∂xp(π(F1), π(F2))). Theorem 5.2. ∂pis a forgetting operator Proof. The goal is to prove that [{F1, F2},L\{p}]≡∂p(F1, F2) Let us suppose that F1, F2∈Form(L) such that π(Fi) = bi+xpcii= 1,2 with bi, cipolynomial formulas without variable xp. Recall that in this case the expression of the rule is ∂xp(π(F1), π(F2)) = Φ ((1 + b1·b2) [1 + (b1+c1)(b2+c2)]) 20 Since the soundness of ∂phas been proved by the previous proposition, by Corollary 3.3 it is sufficient to show that any valuation von L\{p}model of ∂p(F1, F2) can be extended to ˆv|={F1, F2}. Let v|=∂p(F1, F2). Let us consider the point from Fn 2asociated to v,ov. It follows that ov∈V(π(∂p(F1, F2)) + 1) = V(∂xp(π(F1), π(F2)) + 1) = =V((1 + b1·b2)[1 + (b1+c1)(b2+c2)]) so ((1 + b1·b2)[1 + (b1+c1)(b2+c2)]) |x=ov= 0 In order to build the required extension ˆv, let us distinguish two cases: •If (1 + b1·b2)|x=ov= 0 then ˆv=v∪ {(xp,0)} |=F1∧F2. •If [1 + (b1+c1)(b2+c2)]|x=ov= 0 then ˆv=v∪ {(xp,1)} |=F1∧F2 With some abuse of notation, we use the same symbol, `∂, to denote similar notions that defined in Def. 3.6 but on polynomial formulas and rules ∂xp. In that way we can describe `∂-proofs on polynomials. For example, a ∂-refutation for the set π[{p→q, q ∨r→s, ¬(p→s)}] is 1. 1 + x1+x1x2[[π(p→q)]] 2. 1 + (x2+x3+x2x3)(1 + x4) [[π(q∨r→s)]] 3. x1(1 + x4) [[π(¬(p→s)]] 4. 1 + x1+x3+x1x4+x3x4+x1x3+x1x3x4[[∂x2to(1),(2)]] 5. 0 [[∂x1to (3),(4)]] Corollary 5.3. [10] Kis inconsistent if and only if K`∂⊥. Proof. It is consequence of theorems 3.7 and 5.2 The result, in algebraic terms, is as follows: 21 Corollary 5.4. Let F∈Form(L)and let Kbe a knowledge basis. The following conditions are equivalent: 1. K|=F 2. JK`∂0 Proof. (1) =⇒(2): Let us suppose K|=F. Then K+{¬F}is inconsistent. Since ∂pis refutationally complete, K+{¬F} `∂⊥. Thus {1 + π(G) : G∈K}∪{π(F)} `∂0 (2) =⇒(1): If a ∂-refutation is founded on polynomials, then by above theorem K∪ {¬F}is inconsistent. Remark 5.5. To compute conservative retractions we use an implementation (in Haskell language) of ∂pand ∂xp. In order to simplify the presentation, we only show the computation on polynomials (that is, the application of ∂xp), and we use the own propositional variables as polynomial variables (that is, we identify pand xp) to facilitate the readibility. The software used in the examples and experiments can be downloaded from https: // github. com/ DanielRodCha/ SAT-Pol Example 5.6. Let G=s→rand Kbe the KB K=       t∧p↔s t∧r→s t∧q→s p∧q∧s∧t→r To decide whether K|=G-by applying location lemmawe have to compute ∂L\{r,s}[K]≡∂p[∂q[∂t[K]]] * [pqrst+pqst+1,pt+s+1,qst+qt+1,rst+rt+1] (projection) * [pqrs+pqs+ps+s+1, ps+s+1, 1] (forgetting t) * [ps+s+1, 1] (forgetting q) * [1] (forgetting p) 22 Therefore: [K, L\{r, s}]≡ {>} 6|=G Consider now the formula F=p∧q∧t→s. In order to decide whether K|=F, by location lemma we have to compute [K, L(F)] ≡∂r[K] * [pqrst+pqst+1,pt+s+1,qst+qt+1,rst+rt+1] (projection) * [pqst+pqt+pt+qst+qt+s+1,pt+s+1,qst+qt+1,1] (forgetting r) To see that ∂r[K]|=Fit is sufficient to show that ∂r[K]∪ {¬F}is inconsistent. The computation is made in the projection set, by saturating the polynomial set: * [pt+s+1,qst+qt+1, pqst+pqt] (the retraction and ¬F) * [0] (applying sat∂) An approach to specify contexts in AI for reasoning is to determine which set of variables Q⊆Kprovides information and which variables are irrelevant for represent the specific context. In fact, in some approaches for formalizing context-based reasoning contexts are determined by this variable set. When Kdoes not provide any specific information about the context in which it is to be used, it is natural to conclude [K, Q] should only contain tautologies, that is, ∂L\Q[K] = {>}. In the previous example Kdoes not provide relevant information about the context determined by {r, s}, because [K, L\{r, s}] = {>}. 6. Characterization sensitive implications In addition to its use in the design and study of the independence rule, other use of Boolean derivatives is the detection of variables that are irrelevant in a formula (or, in terms of [26], to study when a formula is independent of a variable), and more generally, when a variable is irrelevant in a formula relativized to a KB (that is, in the models of the own KB). We will say that a variable pis irrelevant in a formula F(or Fis independent of p) if Fis equivalent to a formula in which pdoes not occur. This concept can be generalized to a set of variables in the natural way, and it can be proved that a Fformula is independent of a set of variables Xif and only if Fis independent from each variable of X(see [26]). In this paper also remarks the following result: 23 Proposition 6.1. The following conditions are equivalent: 1. Fis independent from x 2. F{x/>} ≡ F{x/⊥} 3. F{x/>} ≡ F 4. F{x/⊥} ≡ F To which we could add: 5. |=¬∂ ∂p(F) In this section we are interested in studying the notion of independence relativized to a KB. Note that it may happen that a variable may be relevant in a formula but not in the KB models we are working with. To distinguish the relativized notion from the original we will use the word sensitive. Definition 6.2. A formula Fis called sensitive in pwith respect to a knowledge basis Kif K6|=F{p/¬p} ↔ F. We say that Fis sensitive w.r.t. K(or simply sensitive, if Kis fixed) if Fis sensitive in all its variables. The following result habilitates the use of Gr¨obner basis for determining sensitiveness (by means of ideal membership test in condition (4)) or that of our interest, by means of ∂p-rules (condition (3)). It is straightforward to check that: Proposition 6.3. Let p∈var(F). The following conditions are equivalent: 1. Fis sensitive in pwith respect to a knowledge basis K 2. K∪ { ∂ ∂p(F)}is consistent 3. sat∂[K∪ { ∂ ∂p(F)}] = {>} 4. ∂xpπ(F)/∈JK+I2 Proof. (1) =⇒(2): Since K6|=F{p/¬p} ↔ F, there exists v|=K where v|=¬(F{p/¬p} ↔ F), that is, v|=K∪ { ∂ ∂p(F)} (2) =⇒(3) by completeness of `∂ (3) =⇒(4): Let v|=K∪ { ∂ ∂p(F)}(it is consistent by (3). Then π(∂ ∂p(F))(ov) = 1. Moreover π(G)(ov) = 1 for any G∈Khence ov∈JK. Therefore the polynomial ∂ ∂pπ(F) does not belong to JK 24 (4) =⇒(1): Suppose ∂ ∂xpπ(F)/∈Jk+I2so there exists o∈V(Jk) such that ∂ ∂xpπ(F)(o)6= 0. Then vo|=∂ ∂p(F) and vo|=K. Therefore K∪ { ∂ ∂p(F)} is consistent, so Fis sensitive in pw.r.t. K. From the definition itself it follows that Boolean derivatives can be used to tackle the problem of sensitive arguments in implications: Fis not sensitive in pw.r.t. Kiff K|=¬∂ ∂p F. In this case, there exists Gwith var(G) =var(F)\ {p}such that K|=F↔G(e.g. F{p/⊥}). Example 6.4. Lets us consider the following consistent KB as a rule-based system K=                                R1 : p1→p9 R2 : p1→p10 R3 : ¬p2→p9 R4 : ¬p2→p10 R5 : (p1∧p7)→p11 R6 : p3→p7 R7 : p3→p10 R8 : p4→p11 R9 : p5→p8 R10 : p6→p9 Let us consider as a set of potential facts (potential inputs of the system) F={p1, . . . , p6,¬p1,...,¬p6} We will say that a rule R∈Kis sensitive in pw.r.t. to Kand a subset of potential facts Cif Ris sensitive in pw.r.t. K∪ C. Let us compute some examples: •R1is sensitive in p1w.r.t. Kand the potential fact set {¬p2}. ∂ ∂p1 (R1) = θ(∂ ∂x1 (1 + x1(1 + x9)) = ¬p9 and K∪ {¬p2} 6|=¬p9 This condition can be checked (by using condition (3) of above proposition) showing that [K∪ {¬p2},{p9}]≡∂L\{p9}[K∪ {¬p2}] = {p9} |=¬p9 25 8.2. Refining the process In order to make the implementation of the realistic algorithms, we will use the following result that significantly reduces the number of applications of the variable forgetting rules in practice. Besides, using the fact that it’s symmetrical, we can even further reduce the number of applications of the operators: Proposition 8.5. In above conditions δp[K]≡ {F:pdoes not occur in F} ∪ δp[{F∈K:poccurs in F}] Proof. Let us denote by Athe first set of formulas and by Bthe second one. We just have to prove that A∪B|=δp[K]. Let δp(F, G) be a formula of δp[K]. By symmetry, it is enough to consider only three cases: •p /∈var(F)∪var(G). Then A|=F∧G≡δp(F, G) •p∈var(G)\var(F). Then A∪B|=F∧δp(>, G)≡δp(F, G) •p∈var(F)∩var(G). Then δp(F, G)∈B 8.3. Experimental results In this section, as an illustration, we will execute variable forgetting on a set of knowledge bases to show the efficiency of the rule proposed in this paper with respect to the canonical rule in the processing of forgetting operations (fundamentally, we will focus on the cost in space, the number of symbols used in the representation). Each experiment has been performed by randomly choosing some variables present in the knowledge base and order on them (common for both operators) and we will progressively apply the corresponding operators3. Below we describe the datasets and the results obtained. The examples are taken from the SAT Competition 2018 website4. In Fig. 7 their initial size (both in propositional logic and polynomial transformed) 3Although it is irrelevant to calculate the size of the knowledge bases, to estimate the time we have used a MacBook Air with a 1.6 GHz Intel Core i5 processor and 8 GB 1600 MHz DDR3 memory. The operating system is macOS High Sierra 10.13.5 4http://sat2018.forsyte.tuwien.ac.at 32 Name Size Size seconds Space (bytes) seconds Space (bytes) form. pol. Can. rule Can. Indep. Indep. mp1-bsat180-648 14715 18176 6.86 1,417,335,160 3.94 1,407,227,832 unsat250 24746 31800 74.60 26,453,571,424 0.92 864,549,664 mp1-squ any s09x07 c27 bail UNS 36619 60318 410.87 81,535,687,624 5.24 1,706,513,448 g2-modgen-n200-m90860q08c40-13698 236112 319913 31.55 16,500,421,928 6.58 5,153,583,936 mp1-klieber2017s-1000-023-eq 351346 416531 out of time – 518.07 426,862,970,928 mp1-tri ali s11 c35 bail UNS 37606 43493 4.34 1,510,720,256 0.48 498,118,016 mp1-Nb5T06 211656 252250 75.89 38,378,129,872 1.03 1,858,302,896 Figure 7: SAT instances used in the experiments: size (both formula and polynomial representation) and total cost using both rules is shown. The total time used in each dataset experiment (i.e. in the application of all the corresponding operators chosen for that experiment) for both the proposed and the canonical operator is also shown. In the following tables the results of the progressive implementation of the operators are shown. mp1-bsat180-648 2 4 6 8 10 1 2 3 ·105 Canonical Indep. rule Size of KB Size of KB Step (Indep. (canonical) rule) 1 15428 19757 2 16900 20876 3 25131 21866 4 26839 23516 5 34908 24612 6 36735 29269 7 54530 33490 8 55231 34985 9 57073 47857 10 169330 59215 11 384996 60313 33 unsat250 2 4 6 8 10 2 4 6 8 ·105 Canonical Indep. rule Size of KB Size of KB Step (Indep. (canonical) rule) 1 26280 34091 2 28906 35443 3 34141 35891 4 68952 37731 5 191069 39242 6 193949 40393 7 200293 54677 8 214468 56846 9 231861 61119 10 407926 62330 11 939192 64986 mp1-squ any s09x07 c27 bail UNS 2 4 6 8 10 2 4 6 8 ·105 Canonical Indep. rule Size of KB Size of KB Step (Indep. (canonical) rule) 1 37028 62498 2 37557 64058 3 38496 63921 4 53437 66035 5 411028 65907 6 589455 67631 7 731546 67512 8 825714 68884 9 890920 68774 10 995522 69832 g2-modgen-n200-m90860q08c40-13698 2 4 6 8 10 1 2 3 ·106 Canonical Indep. rule Size of KB Size of KB Step (Indep. (canonical) rule) 1 237141 321926 2 242392 326062 3 290876 327171 4 319155 332485 5 3339545 334528 6 3340602 341128 7 3346440 344213 8 3362678 348381 9 3367621 373298 10 3390750 537880 34 mp1-klieber2017s-1000-023-eq 23456 2 4 6 ·107 Canonical Indep. rule Size of KB Size of KB Step (Indep. (canonical) rule) 1 351346 1615542 2 1176815 28418531 3 2233525 28418518 4 7599271 28418513 5 74792215 28419039 6 out of time 28419304 mp1-tri ali s11 c35 bail UNS 234567 0.5 1 1.5 2 ·105 Canonical Indep. rule Size of KB Size of KB Step (Indep. (canonical) rule) 1 37877 44127 2 38312 44943 3 38884 44771 4 50809 44634 5 54837 48200 6 213958 48072 7 237610 51134 mp1-Nb5T06 2 4 6 8 10 12 14 16 0.5 1 1.5 2 ·107 Canonical Indep. rule Size of KB Size of KB Step (Indep. (canonical) rule) 1 212003 252400 2 213563 252570 3 222107 252724 4 222446 252862 5 224030 253000 6 232858 253482 7 233189 253620 8 234797 254102 9 243909 254240 10 294441 254378 11 3975580 254516 12 3975911 254998 13 3977425 255136 14 3985776 255278 15 4033048 255760 16 7353991 255898 17 22919499 256036 35 As we have observed in the experiments, despite the fact that initially the transformation to polynomials uses slightly more space, the growth in the size of the knowledge base representation when progressively applied by the operators improves considerably the resources needed with respect to the canonical operator. Note, as we have already noted, that we have compared our operator (not restricted to a sub-language of the propositional logic) with the non-specialized operator. 9. Conclusions and future work As we have already mentioned in the introduction, the algebraic interpretation of propositional logic represents a valuable bridge for applying algebraic techniques in KRR. In this paper we have proposed a new algebraic model to solve problems on KRR whose knowledge is represented by propositional logic. We are not concerned here about the practical computational cost of the use of independence rule, the aim of a next paper. We focused on its theoretical foundations and potential applications in KRR instead. The main technique introduced in the paper is the use of a new rule inspired in the projection of algebraic varieties and polynomial derivatives. Also, it is justified that with Boolean derivatives is possible to determine specific cases of conditional independence, the formula-variable independence relativized to a KB. The tools have been used to solve questions related with distilling KB to obtain relatively simpler KBs to solve context-based questions. Throughout the paper we have remarked some works related to the tools used here. These works are driven to exploit the computation and use of Gr¨obner Basis, whilst in this paper a new method is proposed (specific for F2). With regard to the practical complexity of the proposed method, the application of the independence rule is reduced to the the algebraic simplification of polynomials. Its calculation appears at two levels: first in the multiplication of Boolean polynomials (or in finite fields in general), since the rule of independence is reduced to products, and second in the transformation of formulas into polynomials for a complete knowledge base. With respect to the first question, the product of Boolean polynomials is a long-studied problem, for which refined algorithms exist (see e.g. [27]). The computational complexity of the application of the rule is irrelevant (it consists mainly of four polynomial products) compared to the second issue, 36 the translation of formulas into polynomials. Such kind of transformation has been widely used to compile and run (using Gr¨obner databases) rule-based programs, for example. The problems where the polynomial interpretation of the formulas (rules, for example) of a KB is used are problems where the formulas have very limited complexity. In this type of program, the number of variables that appear in a rule is very small compared to the total number (see e.g. [28, 29, 30]). Therefore the computation of conservative retraction is feasible with our approach. Moreover, in the context of algebraic interpretation of logic reasoning, the results shown in this article allow us to replace the use of ”black box” implementations (those that use a computer algebra system to compile and reason) with another also algebraic but ”white box” type, which can be verified/certified. The complexity of algebraic simplifications can be high when both the number of variables is large and the number of variables that occur in each knowledge base formula is relatively high (with respect to the size of the total set of variables). However it is not common (nor advisable) in programming paradigms such as logical programming (answer set or rule-based programming), DL ontologies, etc. With respect to the use of independence rule as SAT solver, although the rule is (refutationaly) complete, its intended use in this article is to calculate conservative retractions, and we have not presented a SAT algorithm other than the intuitive one (rule application saturation). In the GitHub repository https://github.com/DanielRodCha/SAT-Pol, variants are being developed to solve more efficiently SAT problems. With regard to the complexity of the problem of the variable forgetting in the case of propositional logic, it has been studied in considerable depth due to its relationship with the SAT problem (and, in general, with problems with Boolean functions) both for the foundations on the complete logic and for various fragments of this logic (see e.g. [26, 31]). As we have shown in the section devoted to experiments, computational cost of polynomials computations are irrelevant in practice, bearing in mind that our method is nos specialized for fragments of propositional logic, since it works on the full propositional logic. That section focuses on comparing the rule with the general rule of forgetting variables, since it does not seem appropriate to compare our proposal with other approaches specialized in fragments of propositional logic. As future work we will intend to work in two complementary research lines. On the one hand we intend to carry out the extension to many-valued logics and their applications [4, 5, 7] as well as to tackle the knowledge forgetting problem in modal logics [22]. If the underlying logic is many-valued, 37 the algebraic varieties of the polynomial translations of the propositions do not behave intuitively (see [1]). Therefore, we need to use an appropiate version of the the Nullstellensatz Theorem. Also, for this research line, a careful generalization of the concept of Boolean derivatives, with nice logical meaning, has to be carried out [32]. On the other hand, it is possible to use our model - in a similar way to the applications presented in the paperfor implementing expert systems based on the knowledge of different experts as in [9], for diagnosis (see [33]) or -in the behalf of authorsmore promising field of inconsistency management [34]. 10. Acknowledgements This work was partially supported by TIN2013-41086-P project (Spanish Ministry of Economy and Competitiveness), co-financed with FEDER funds. We also acknowledge the reviewers and editors for their valuable comments and suggestions, which have substantially improved the content of this article. 11. References References [1] E. Roanes-Lozano, L. M. Laita, A. Hernando, E. Roanes-Mac´ıas, An algebraic approach to rule based expert systems, Revista de la Real Academia de Ciencias Exactas, F´ısicas y Naturales. Serie A. Matem´aticas 104 (1) (2010) 19–40. [2] D. Kapur, P. Narendran, An equational approach to theorem proving in first-order predicate calculus, SIGSOFT Softw. Eng. Notes 10 (4) (1985) 63–66. [3] J. Hsiang, Refutational theorem proving using term-rewriting systems, Artif. Intell. 25 (3) (1985) 255 – 300. [4] J. Chazarain, A. Riscos, J. Alonso, E. Briales, Multi-valued logic and gr¨obner bases with applications to modal logic, J. Symb. Comput. 11 (3) (1991) 181 – 194. [5] L. M. Laita, E. Roanes-Lozano, L. de Ledesma, J. A. Alonso, A computer algebra approach to verification and deduction in many-valued knowledge systems, Soft Comput. 3 (1) (1999) 7–19. 38 [6] E. Roanes-Lozano, A. Hernando, L. M. Laita, E. Roanes-Mac´ıas, A gr¨obner bases-based approach to backward reasoning in rule based expert systems, Ann Math Artif Intel 56 (3) (2009) 297–311. [7] A. Hernando, E. Roanes-Lozano, L. M. Laita, A polynomial model for logics with a prime power number of truth values, J. Autom. Reasoning 46 (2) (2011) 205–221. [8] J. C. Agudelo-Agudelo, C. A. Agudelo-Gonz´alez, O. E. Garc´ıa-Quintero, On polynomial semantics for propositional logics, Journal of Applied Non-Classical Logics 26 (2) (2016) 103–125. [9] A. Hernando, E. Roanes-Lozano, An algebraic model for implementing expert systems based on the knowledge of different experts, Math. Comput. Simulat. 107 (2015) 92 – 107. [10] G. A. Aranda-Corral, J. Borrego-D´ıaz, M. M. Fern´andez-Lebr´on, Conservative retractions of propositional logic theories by means of boolean derivatives., in: Calculemus/MKM Lect. Notes Comput. Sci., Vol. 5625, Springer, 2009, pp. 45–58. [11] P. Blair, R. V. Guha, W. Pratt, Microtheories: An ontological engineer’s guide, Tech. rep., CyC Corp. (1992). [12] E. Amir, S. McIlraith, Partition-based logical reasoning for first-order and propositional theories, Artif. Intell. 162 (1-2) (2005) 49–88. [13] C. Lutz, F. Wolter, Conservative extensions in the lightweight description logic EL, in: CADE-21 Lect. Notes Comput. Sci. Vol. 4603, 2007, pp. 84–99. [14] M. J. Hidalgo-Doblado, J. A. Alonso-Jim´enez, J. Borrego-D´ıaz, F. Mart´ın-Mateos, J. Ruiz-Reina, Formally verified tableau-based reasoners for a description logic, J. Autom. Reasoning 52 (3) (2014) 331– 360. [15] F. Mart´ın-Mateos, J. Alonso, M. Hidalgo, J. Ruiz-Reina, Formal verification of a generic framework to synthetize sat-provers, J. Autom. Reasoning 32 (4) (2004) 287–313. 39 [16] J. Lang, P. Liberatore, P. Marquis, Conditional independence in propositional logic, Artif. Intell. 141 (1) (2002) 79 – 121. [17] F. Lin, R. Reiter, Forget it!, in: In Proceedings of the AAAI Fall Symposium on Relevance, 1994, pp. 154–159. [18] W. W. Bledsoe, L. M. Hines, Variable elimination and chaining in a resolution-based prover for inequalities, in: CADE Lect. Notes Comp. Sci. Vol. 87, 1980, pp. 70–87. [19] J. Larrosa, E. Morancho, D. Niso, On the practical use of variable elimination in constraint optimization problems: ’still-life’ as a case study, J. Artif. Intell. Res. 23 (2005) 421–440. [20] Y. Moinard, Forgetting literals with varying propositional symbols, J. Log. Comput. 17 (5) (2007) 955–982. [21] T. Eiter, K. Wang, Semantic forgetting in answer set programming, Artif. Intell. 172 (14) (2008) 1644 – 1672. [22] Y. Zhang, Y. Zhou, Knowledge forgetting: Properties and applications, Artif. Intell. 173 (16) (2009) 1525 – 1537. [23] K. Su, A. Sattar, G. Lv, Y. Zhang, Variable forgetting in reasoning about knowledge, J. Artif. Intell. Res. 35 (2009) 677–716. [24] D. A. Cox, J. Little, D. O’Shea, Ideals, Varieties, and Algorithms: An Introduction to Computational Algebraic Geometry and Commutative Algebra, 3/e (Undergraduate Texts in Mathematics), Springer-Verlag, Berlin, Heidelberg, 2007. [25] F. Winkler, Polynomial algorithms in computer algebra, Texts and monographs in symbolic computation, Springer, Wien, New York, 1996. [26] J. Lang, P. Liberatore, P. Marquis, Propositional independence - formula-variable independence and forgetting, J. Artif. Intell. Res. 18 (2003) 391–443. [27] R. P. Brent, P. Gaudry, E. Thom´e, P. Zimmermann, Faster multiplication in gf(2)[x], in: ANTS 2008 Lect. Notes Comput. Sci. Vol. 5011, 2008, pp. 153–166. 40 [28] C. Rodr´ıguez-Solano, L. M. Laita, E. Roanes-Lozano, L. L´opez-Corral, L. Laita, A computational system for diagnosis of depressive situations, Expert Syst. Appl. 31 (1) (2006) 47–55. [29] C. Roncero-Clemente, E. Roanes-Lozano, A multi-criteria computer package for power transformer fault detection and diagnosis, Appl. Math. Comput. 319 (2018) 153–164. [30] E. Roanes-Lozano, J. L. G. Garc´ıa, G. A. Venegas, A prototype of a RBES for personalized menus generation, Applied Mathematics and Computation 315 (2017) 615–624. [31] J. Marques-Silva, M. Janota, C. Menc´ıa, Minimal sets on propositional formulae. problems and reductions, Artif. Intell. 252 (2017) 22 – 50. [32] M. Fern´andez-Lebr´on, L. Narv´aez-Macarro, Hasse-schmidt derivations and coefficient fields in positive characteristics, J. Algebra 265 (1) (2003) 200 – 210. [33] J. Piury, L. M. Laita, E. Roanes-Lozano, A. Hernando, F.-J. PiuryAlonso, J. M. G´omez-Arg¨uelles, L. Laita, A gr¨obner bases-based rule based expert system for fibromyalgia diagnosis, Revista de la Real Academia de Ciencias Exactas, Fisicas y Naturales. Serie A. Matematicas 106 (2) (2012) 443–456. [34] J. Lang, P. Marquis, Reasoning under inconsistency: A forgetting-based approach, Artif. Intell. 174 (12) (2010) 799 – 823. 41