Ph Besnard
email: besnard@irit.fr

É Grégoire
email: gregoire@cril.univ-artois.fr

S Ramon
email: ramon@cril.univ-artois.fr

Overriding subsuming rules

This paper is concerned with intelligent agents that are able to perform nonmonotonic reasoning, not only with, but also about general rules with exceptions. More precisely, the focus is on enriching a knowledge base Ŵ with a general rule that is subsumed by other rules already there. Such a problem is important because evolving knowledge needs not follow logic as it is well-known from e.g., the belief revision paradigm. However, belief revision is mainly concerned with the case that the extra information logically conflicts with Ŵ. Otherwise, the extra knowledge is simply doomed to extend Ŵ with no change altogether. The problem here is different and may require a change in Ŵ even though no inconsistency arises. The idea is that when a rule is to be added, it might need to override any rule that subsumes it: preemption must take place. A formalism dedicated to reasoning with and about rules with exceptions is introduced. An approach to dealing with preemption over such rules is then developed. Interestingly, it leads us to introduce several implicants concepts for rules that are possibly defeasible.

Introduction

Assume a knowledge base Ŵ contains the rule If the switch is on then the light is on. When If the switch is on and the lamp bulb is ok then the light is on needs to be introduced inside Ŵ, it seems natural to require this new rule to preempt the older rule: it is no longer enough to know that the switch is on to be able to conclude that the light is on, it must additionally be the case that Ŵ yields the information that the lamp bulb is ok. First, let us observe that a monotonic logic cannot capture such dynamics of reasoning by simply adding the new rule. According to monotonicity, any conclusion drawn from a given set of premises can still be inferred whatever additional premises happen to supplement this set. In such a logic, the statement the light is on (concluded from the former rule and the statement the switch is on) is still concluded even though the second rule is added, and, worse yet, regardless of any information stating that the lamp bulb is broken. Also, the usual approaches to belief revision following the seminal work in [1] fail to address this issue directly because they make the new information to be set-theoretically unioned with Ŵ in case no inconsistency arises. In the paper, it is shown how solving the problem can be done through specific contraction steps followed by an expansion one, as those operations are called in the belief revision research area. Let us stress that moving to a nonmonotonic formalism where exceptions to rules depend on consistency checks like adding If the switch is on and if it can be consistently assumed that the lamp bulb is ok, then the light is on does not change the problem.

Technically, the problem can be described as follows: Given a set Ŵ of formulas and a rule R, what changes should Ŵ undergo so as to infer R but not to infer any R ′ subsuming R? In symbols, where Ŵ . stands for Ŵ after these changes have taken place,

Ŵ . |∼ R and Ŵ . |∼ R ′
Clearly, the problem first requires several matters to be settled. First, the syntax for rules (in which R, R ′ , . . . are expressed) is to be defined. Second, an inference relation (denoted |∼) allowing rules to be handled needs to be settled. Third, a concept of implicant for rules expressing what does R ′ subsuming R mean needs to be proposed, before an approach to solve the above preemption issue can be defined.

Accordingly, the paper is organized as follows. First, we analyze situations where a new belief requires the subsuming ones to be expelled (but no means is provided to automatically identify such cases -it is not the aim of this paper). In the following Section, a general formalism for representing rules with exceptions is introduced with the aim of encompassing various logic-based approaches allowing such rules, including default reasoning. Section 4 introduces useful inference tools to reason about such rules, while Section 5 connects the tools with default logic. In Section 6, a useful X-derivation concept is proposed, allowing both plain formulas and rules to be inferred under the possible assumption of additional formulas or other rules with exceptions. Sections 7 and 8 investigate concepts of implicant for rules with exceptions. The approach to the preemption issue is then developed in Section 9, based on the X-derivation and the latter implicant concepts. Finally, some avenues for future research are provided in the conclusion.

Throughout the paper, the following notations are used: ¬, ∨, ∧ and ⊃ denote the classical negation, disjunction, conjunction and material implication connectives, respectively. When is a set of formulas, Cn( ) denotes the deductive closure of under a given logic, of whichdenotes the consequence relationship,⊥ denotes absurdity, and ⊤ denotes any tautology.

About new beliefs that require subsuming beliefs to be expelled

The focus in this paper is on rational agents that are equipped with sound and complete logical inference mechanisms about beliefs. As modeled in the so-called AGM framework [1] that gave rise to the belief revision research area, the natural situation where a rational agent is handling a new belief that is not conflicting with its previous ones, requires the belief to be merely added to its set of beliefs.

As illustrated in the introduction, such a very simple schema is not universal and does not cover all possible situations. In some circumstances, a new belief requires some former ones to be expelled even though inconsistency does not threaten.

In this paper, the focus is on new non-conflicting beliefs that are intended to prevail over preexisting ones. Prevailing means here that the new belief must be adopted and other beliefs that logically subsume it must be expelled. In the lamp example, If the switch is on then the light is on subsumes (i.e., has for strict consequence) If the switch is on and the lamp is ok then the light is on and must be expelled so that the new rule prevails. Thus, this study only concerns situations where a new piece of information is given and when this new one must prevail over a pre-existing set of premises.

We believe that this occurs frequently in real-life. A typical situation is when we refine our knowledge and beliefs so that we need to adopt a more precise rule and block less precise pre-existing ones, as in the lamp example. From a logical point of view, a more precise information can be a strict deductive consequence of a more general one. Hence, the need to get rid of the more general ones.

Let us stress that when we want a new rule if A and B then C to prevail, this does not entail that not B is a counter-example for deriving C from A. Actually, C can perhaps also be obtained from A is true and B is false. For example, assume we refine a medical diagnosis system. We might want to assert the rule If symptom1 and has-been-in-Africa then disease1 and want it to prevail. So we need to reject If symptom1 then disease1 and adopt the new (more precise) rule. This does not require not has-been-in-Africa to be a counter-example from deriving disease1 from symptom1. Disease1 could perhaps also be derived when we have symptom1 and has-been-in-Amazonia, according to another rule.

Even more importantly, the need for a new piece of information to prevail over the preexisting subsuming premises is actually neither restricted to the (intuitive) concept of "more precise" rules or "more precise" information. Actually, it need not even be restricted to rules (and thus counter-examples to rules), nor to their syntax, but exists for any kind of formulas. For example, assume that the pre-existing beliefs contain John is in his office or John is at home. The need to block subsumption also occurs when we want the new, in some sense more accurate, piece of information John is in his office or John is at home or John is in his club to prevail. Interestingly, the language that we are going to develop to model rules also allows to represent formulas that do not appear as rules from an epistemological point of view. The treatment allowing new beliefs to prevail applies to them, too. Some words of caution are needed here since we are using full and complete logical mechanisms. In standard logic, any literal (namely, any possibly negated elementary fact) entails any rule having the literal as a consequent: Light is on entails any possible rule having light is on as the consequent. Accordingly, when we enforce a rule that must prevail, we might need to get rid of elementary beliefs. In the paper, we always assume that every belief in a set Ŵ of premises can be expelled when a new belief needs to prevail. On the one hand, applying the technique might thus require to leave outside Ŵ formulas that must not be expelled in such a process. On the other hand, in many problems involving the analysis of interacting rules, such an analysis must be conducted without case-specific concrete data. For example, in rule-based expert systems, the rule-base contains generic rules whereas the working memory contains data related to a specific case and temporary conclusions. In such a specific context, our technique to make rules prevail must consider the rule-base only.

Interestingly, the approach that we present in this paper can appear as a combination of (forms of) multiple contraction and expansion operators, which have been studied in the standard Boolean logic setting for belief revision (see [START_REF] Fuhrmann | A survey of multiple contractions[END_REF] for a survey on multiple contraction operators). In this respect, this paper is, for one of its facets, a generalization of some first results about blocking subsumption in the standard Boolean case that were presented in [START_REF] Besnard | Enforcing logically weaker knowledge in classical logic[END_REF] and for which rationality postulates are proposed in [START_REF] Besnard | Preemption operators[END_REF]. In this paper, the preemption issue is investigated within the setting of a family of non-monotonic logics allowing forms of default assumptions. The handling of complex reasonings involving rules with exceptions leads us to elaborate reasoning paradigms that are not captured by existing (generalized) AGM-like frameworks.

PEC rules

These last three decades, many research efforts in the Artificial Intelligence community have been devoted to the logicbased formalization of various forms of reasoning, especially defeasible ones, giving rise to large families of nonmonotonic logics. Noticeably, some of the most popular tools to handle forms of defeasible reasoning remain rules with exceptions, e.g., in the form of defaults [START_REF] Reiter | A logic for default reasoning[END_REF]. They permit an inference system to jump to default conclusions and to withdraw them when new information shows that these conclusions now lead to inconsistency. Usually, such a default rule is based on logical formulas, that is, expressions of a formal language upon which an inference system (no matter how poor or rich) models some kind of reasoning. The goal of this paper is not to introduce a new nonmonotonic logic in this respect. Instead, we settle on a generic framework that allows the various types of knowledge involved in rules with exceptions to be represented in a single uniform way. Instantiating the framework to a given traditional nonmonotonic logic might require additional constraints on the representation and inference formalisms.

Let us first concentrate on rules with exceptions under consistency tests. Our leading example is then expressed as If the switch is on and if it can be consistently assumed that the lamp bulb is ok, then the light is on and consists of three parts: its premises, its exceptions, and its conclusions. Accordingly, we thus aim at representing rules with exceptions in a uniform way within a unified setting that is, among other things, meant to be general enough as to encompass e.g. default logic while allowing us to instantiate it to other logical formalisms. It should also allow the representation of both monotonic knowledge and rules involving consistency checks.

Given a logical language, a PEC rule (for Premises-Exceptions-Conclusions) is a triple consisting of three sets of formulas. First, the premises, which are the necessary conditions for this rule to apply. Then, the exceptions, which call for consistency tests. Finally, the conclusions, which list the claims that can be made whenever the rule applies.

Definition 1 (PEC-rule).

A PEC rule is a triple R = (P, E, C) where P = {ρ 1 , . . . , ρ k } and C = {ς 1 , . . . , ς n } are consistent sets of formulas and E = {ǫ 1 , . . . , ǫ m } is a set of non-tautological formulas.

In the definition, we impose no constraint on the language: there may, or may not, be connectives such as negation, conjunction, disjunction and the like. There may even be no connective at all. However, an underlying inference relation must be available. Of course, this means that the logical formalism used must have a form of tautology (please note the subtlety here: this does not mean that the logical formalism used must have tautologies). In the rest of the paper, we assume however the availability of the connectives of standard Boolean logic.

A PEC rule can be interpreted in different ways, depending on how its set of premises and its set of conclusions are captured logically (presumably, conjunctively or disjunctively). In the sequel, without loss of generality, we consider only unary PEC rules, that is, PEC rules whose sets of premises and sets of conclusions are singletons (the involved formulas having been assembled through the concerned conjunctive or disjunctive paradigm). Abusing the notation in order to improve readability, we often omit curly brackets for these singletons.

Definition 2 (Unary PEC rule).

A PEC rule R = (P, E, C) is unary iff P and C are singleton sets.

Example 1. The PEC rule (switch_on, {¬lamp_bulb_ok}, light_on) is an encoding of the rule with exception "If the switch is on and, consistently assuming that the lamp bulb is ok, then the light is on".

Example 2. The PEC rule ({switch_on, lamp_bulb_ok}, ∅, light_on) is an encoding of a similar rule where the impossibility to derive e.g. "lamp_bulb_ok" can block the inference of "light_on". In this respect, "¬lamp_bulb_ok" would be an exception to the rule, which is however not to be included in the set of exceptions of the PEC rule, since it is not a consistency-based exception.

Example 3. The PEC rule (⊤, ∅, light_on) is an encoding of the fact "the light is on". Example 4. The PEC rules (switch_on, ∅, light_on), (switch_on ⊃ light_on, ∅, ∅) and (∅, ∅, switch_on ⊃ light_on) are various encodings of the exception-free rule "If the switch is on then the light is on".

As can be seen in the previous examples, exceptions to a rule that are supposed to be derived in the monotonic fragment of the logic (vs. consistency checks) are not included in the set of exceptions in the PEC rule, which is devoted to exceptions based on consistency checks. Indeed, we shall adopt a semantical view of formulas of the monotonic fragment of the logic and e.g. allow for a clausal representation. Accordingly, the premise and conclusion status can be interchanged through modus tollens and no information is given to interpret a literal as playing the specific role of an exception to a rule in a clausal representation. Thus, the word "exception" will be reserved in this paper to "exception based on consistency check". The various possible encodings of knowledge between premises and conclusions is similar to e.g. the well-known difference in default logic between defaults with prerequisites and the corresponding prerequisite-free defaults [cf 4]. Also, -is assumed to admit ⊤ to represent effectively some formula.

Reasoning with and about PEC rules

Let us define a concept of a derivation for the very general language of PEC rules. Interestingly, it will not only allow us to handle both monotonic and defeasible rules in the same setting, but it will also allow us to derive both of them.

A word of warning: in the following, ⊢ does not represent an inference relation. ⊢ α (resp. ⊢ α) means that α has (resp. has not) the status "inferred" within the derivation. Also, "not inferred within the derivation" does not mean "whose negated form cannot be inferred using the inferred formulas occurring in the derivation" (which is a weaker notion, clearly uninteresting). A word of terminology: ⊢ α and ⊢ α are said to be signed formulas. Most naturally, ⊢ γ (resp. ⊢ γ ) is said to be positive (resp. negative). Definition 3 (Derivation). Let Ŵ be a set of PEC rules and ℵ = (ρ, {ǫ 1 , . . . , ǫ n }, ς ) one PEC rule. A derivation of ℵ from Ŵ is a tree T whose nodes are standard signed Boolean formulas s.t.:

1. for all leaves of the form ⊢ α, 4. every node ⊢ α that is not a leaf has as parents,

• either (⊤, ∅, α) ∈ Ŵ, • or (α 1 , ∅, α 2 ) ∈ Ŵ and α = α 1 ⊃ α 2 , • or α = ρ, 2. for all leaves of the form ⊢ β, β / ∈ Cn({γ s.t. (⊤, ∅, γ ) ∈ Ŵ} ∪ {γ 1 ⊃ γ 2 s.t. (γ 1 , ∅, γ 2 ) ∈ Ŵ} ∪ {α s.t. ⊢ α is a node of T}), 3. if ⊢ β is a node then it is a leaf,
• either a tuple (⊢ α 1 , . . . , ⊢ α k ). In this case, α ∈ Cn({α 1 , . . . , α k }).

• or a tuple (⊢ α 1 , ⊢ β 1 , . . . , ⊢ β m ) where m ≥ 1. In this case, (α

1 , {β 1 , . . . , β m }, α) ∈ Ŵ. 5. ρ ∈ {α s.t. ⊢ α is a leaf of T} ∪ {⊤}, {ǫ 1 , . . . , ǫ n } = {β s.t. ⊢ β is a node of T}, ⊢ ς is the root of T.
We note Ŵ|∼ {ǫ 1 ,...,ǫ n } ℵ and, when {ǫ 1 , . . . , ǫ n } is empty, Ŵ|∼ℵ.

Let us provide some intuitions and examples. First, consider the simple case of standard Boolean logic: items 2 and 3 are ineffective because there are no negative nodes, while items 4 and 5 get simpler for the same reason. Items 1 & 2 require a positive node to correspond either with a standard Boolean formula encoded inside a PEC rule of Ŵ, or with the premise ρ of the PEC rule ℵ derived by the tree. This latter alternative translates the idea that a derivation allows a rule to be derived through a construction that can assume that the premise of the rule is established. Item 4 gets simpler: only standard deduction can take place in the tree. Indeed, the tree is then reduced to a standard derivation tree from Boolean logic. Item 5 defines the three components of the ℵ rule derived by the tree.

Example 5. Let Ŵ = {(a, ∅, b), (⊤, ∅, a), (b, ∅, c)}. The tree from Fig. 1 is a derivation of (⊤, ∅, c) from Ŵ (please note that the first part of item 5 is satisfied by ρ ∈ {⊤}). Note that this tree is also a derivation of (a, ∅, c), of (a ⊃ b, ∅, c) and

(b ⊃ c, ∅, c) from Ŵ. Example 6. Let Ŵ = {(a, ∅, b), (b, ∅, c)}.
The tree of Fig. 1 is a derivation of (a, ∅, c) from Ŵ (please note that a plays the role of an additional hypothesis). The tree of Fig. 1 is also a derivation of (a, ∅, c) from Ŵ ∪ {(⊤, ∅, a)}.

Example 7. Let Ŵ = {(⊤, ∅, a), (b, ∅, c)}. The tree from Fig. 1 is a derivation of (a ⊃ b, ∅, c) from Ŵ. Note that ρ plays the role of an additional hypothesis. This tree is also a derivation of (a ⊃ b, ∅, c) from Ŵ ∪ {(⊤, ∅, ¬a)}, although the ⊢ a node in the tree is inconsistent with the ¬a fact encoded through (⊤, ∅, ¬a). When some PEC rules in Ŵ have a non-empty set of exceptions, derivation trees may capture reasoning under some proviso(s) (meaning that there are possible exceptions). Item 2 guarantees reasoning to be consistent in the sense that exception-free information from Ŵ (that may, or may not, occur as positive nodes) does not yield exceptions whose absence is required for the reasoning developed to be acceptable (cf Example 10 with Cn being classical logic and Example 11 with Cn being an arbitrary logic). This needs not prevent trivialization (in which case only derivations with no negative node may exist). Item 3 indicates that consistency statements occur as hypotheses, they are not inferred. Item 4 makes sure that each node, if not a leaf, is inferred from exception-free information and/or consistency hypotheses. Only inference steps from Cn and rules (with exceptions) in Ŵ may apply. Lastly, item 5 specifies what components the PEC rule derived consists of:

• Its conclusion is the root of the derivation tree.

• Its exceptions exhaust all consistency hypotheses occurring in the derivation tree (cf Example 9).

• Its premise, if not ⊤, either amounts to some exception-free statement represented by a rule from Ŵ, or it is an extra formula that plays the role of an additional hypothesis in the reasoning (cf Example 9). Example 9. Let Ŵ = {(a ∧ b, {d, e}, f ), (f , ∅, c)}.The tree from Fig. 3 is a derivation of (a ∧ b, {d, e}, c) from Ŵ (please note that ρ is a ∧ b that plays the role of an additional hypothesis and that {d, e} exhausts all negative nodes of the derivation tree). The tree from Fig. 3 is not a derivation of (a∧b, {d, e, g}, c) from Ŵ (item 5 in the definition of a derivation fails because g is listed as an exception of the derived PEC rule but ⊢ g is not a node of the derivation tree). The tree from Fig. 3 is not a derivation of (b, {d, e}, c) from Ŵ (here, item 5 is failed for a different reason: the purported ρ is b but ⊢ b is not a leaf of the derivation tree).

Example 10. Let Ŵ = {(a ∧ b, {d, e}, f ), (f , ∅, c), (⊤, ∅, ¬f )}. If Cn is taken to be classical logic, the tree of Fig. 3 is not a derivation of (a ∧ b, {d, e}, c) from Ŵ. The reason is that item 2 fails as follows. First, ⊢ f is a node of the derivation tree hence f ∈ {α | ⊢ α is a node of T}. Second, (⊤, ∅, ¬f

) belongs to Ŵ hence ⊤ ⊃ ¬f ∈ {γ 1 ⊃ γ 2 | (⊤, ∅, γ 1 ⊃ γ 2 ) ∈ Ŵ}.
Third, item 2 then becomes β ∈ Cn({f , . . . , ⊤ ⊃ ¬f }) that must be checked for β being d and e. However, as Cn is classical logic, Cn({f , . . . , ⊤ ⊃ ¬f }) contains all formulas of the language, among them are d and e.

Example 11. Let Ŵ = {(a∧b, {d, e}, f ), (f , ∅, d), (d, {¬c}, c)}. The tree from Fig. 4 is not a derivation of (a∧b, {d, e, ¬c}, c) from Ŵ because item 2 is violated. First, ⊢ d is a node of the derivation tree hence d ∈ {α | ⊢ α is a node of T}. As ⊢ d is a leaf, β ∈ Cn({d, . . .}) must be checked for β being d and failure is obvious.

A versatile approach

Again, it must be clear that the present work is not the definition of a new nonmonotonic logic and its proof theory. Instead, it is the definition of a framework expressive enough to capture an approach to the problem of overriding subsuming rules, and general enough to be instantiated by a number of logical formalisms. Importantly, the concept of a derivation is only a tool towards this aim which can be tailored to the proof theory of various logics.

For instance, and importantly, the above concept of a derivation does not match inference in Reiter's default logic. First, derivations have been defined independently of any extension concept and a derivation tree does not require all rules whose premises are satisfied to be applied and occur in the tree. In particular, it happens that derivations exist although there is no extension (cf Example 12). ¬a , yet there exists a derivation of the PEC rule (⊤, {¬d, ¬e}, c) from Ŵ ′ , as can be seen from the tree of Fig. 5.

Similarly, Example 13 shows that it may happen that a formula is in no extension although there exists a derivation for it.

Example 13. Let Ŵ = ( , ) be a default theory with = ⊤:a b , a:¬b c and = {a}. Let us represent Ŵ by the set of PEC rules Ŵ ′ = {(⊤, {¬a}, b), (a, {b}, c), (⊤, ∅, a)}. Ŵ has a single extension, i.e., E = Cn({a, b}). Although the formula c is not in E, there exists a derivation of the PEC rule (⊤, {b}, c) from Ŵ ′ as shown by the tree of Fig. 6.

Still, the concept of a derivation is powerful enough to capture credulous reasoning as modeled by default logic, as the straightforward following property establishes it. Property 1. Let Ŵ = ( , ) be a default theory and Ŵ . a set of PEC rules translating Ŵ. For every formula f belonging to an extension E of Ŵ, there exists a derivation (⊤, {ǫ 1 , . . . , ǫ n }, f ) from Ŵ . where {¬ǫ 1 , . . . , ¬ǫ n } is a subset of the justifications of the generating defaults of Ŵ with respect to E. Importantly, derivations are not meant to be optimal proofs: there is no endeavor as to avoid detours or to impose shortcuts. Lastly, a concept of consistency can be introduced into the PEC framework.

Definition 4 (Consistency

). Ŵ is consistent iff Ŵ |∼(⊤, ∅, ⊥).
As usual, a notion of consistency opens up a choice of negations. Whatever such a choice of a negation ∼ for PEC rules, it is likely to be such that both Ŵ |∼ R and Ŵ |∼ ∼R while Ŵ |∼ R & ∼R (where & stands for some conjunction of PEC rules, again whatever choice is made there) is possible. In purpose, we have thus left out any notion of inferential closure and similarly any subgrouping of consequences, e.g. in forms of extensions à la default logic.

X-derivation

We are now to extend the concept of a derivation by taking into account an additional hypothesis, which, in full generality, can be a PEC rule (with or without exceptions). This concept will be useful in our approach to preempting rules since we will have to consider what could be inferred provided that a given PEC rule that must not be subsumed is introduced inside Ŵ. This full-fledged account is called an X-derivation, the details of which are explained and more generally discussed after the formal definition below.

Definition 5 (X-derivation). Let Ŵ be a set of PEC rules and X a PEC rule. An X-derivation of ℵ = (ρ, {ǫ 1 , . . . , ǫ n }, ς ) from Ŵ is a tree T whose nodes are signed standard Boolean formulas s.t.:

1. for every leaf of the form ⊢ α,

• either (⊤, ∅, α) ∈ Ŵ ∪ {X}, • or (α 1 , ∅, α 2 ) ∈ Ŵ ∪ {X} and α = α 1 ⊃ α 2 , • or α = ρ, 2. for every leaf of the form ⊢ β, β / ∈ Cn({γ s.t. (⊤, ∅, γ ) ∈ Ŵ ∪ {X}} ∪ {γ 1 ⊃ γ 2 s.t. (γ 1 , ∅, γ 2 ) ∈ Ŵ ∪ {X}} ∪{α s.t. ⊢ α is a node of T}), 3. if ⊢ β is a node
then it is a leaf, 4. every node ⊢ α that is not a leaf has as parents,

• either a tuple (⊢ α 1 , . . . , ⊢ α k ). Actually, the PEC rule X can be regarded as supplementing the set of PEC rules Ŵ. Accordingly, if X = (⊤, ∅, ⊤), then an X-derivation of ℵ from Ŵ happens to be a derivation of ℵ from Ŵ (cf Example 14). The role of each of the three components of the derived rule ℵ is detailed by item 5. Importantly, item 1 expresses that if a positive leaf (tautologies aside) is not some exception-free information encoded as a PEC rule from Ŵ then it is the premise of ℵ. Similarly to Definition 3, conditional reasoning can be conducted using exception-free information as an extra hypothesis, turning it into a positive leaf. However, the conditional piece can now be the X rule itself (more exactly, an equivalent form) when X represents a formula of classical logic for instance (cf Example 16). When X is a PEC rule (̺, {ξ 1 , . . . , ξ h }, ν) that does have exceptions, if its premise ̺ stands as a positive leaf (i.e., ⊢ ̺) not issued from a rule in Ŵ (i.e., there exists no (κ, ∅, ζ ) in Ŵ such that κ ⊃ ζ be ̺), then ̺ turns out to be the premise of ℵ (cf Example 18).

When X is used in the derivation and that the premise ̺ of X is not a leaf, then ̺ comes from a subproof in the tree (cf Example 19). In all cases, when X is used in the derivation, its premise occurs (as an hypothesis or an intermediate conclusion) higher in the tree. Therefore, not only is X introduced as an extra hypothesis, but when it is mentioned in the tree, if its premise ̺ does not come from a subproof then ⊢ ̺ occurs as a leaf (and is regarded as established); hence ̺ enters the set of premises of ℵ (where ℵ is the PEC rule which is the conclusion of the derivation).

More generally, an X-derivation encompasses conditional reasoning in various forms because it involves consistency hypotheses, it can include an extra rule X, and assumes the premise of ℵ (the PEC rule to be inferred).

Example 14. Let us return to Example 9, i.e., Ŵ = {(a ∧ b, {d, e}, f ), (f , ∅, c)}. The tree of Fig. 7, reproduced from Example 9, is both a derivation and a (⊤, ∅, ⊤)-derivation of (a ∧ b, {d, e}, c) from Ŵ.

Example 15. Again, Ŵ = {(a ∧ b, {d, e}, f ), (f , ∅, c)} as in Example 9. The tree of Fig. 7 is a (⊤, ∅, a ∧ b)-derivation of (a ∧ b, {d, e}, c) from Ŵ, although in a rather vacuous way because the extra hypothesis X = (⊤, ∅, a ∧ b) is left unused. The tree of Fig. 7 is not a (⊤, ∅, a ∧ b)-derivation of (⊤, {d, e}, c) from Ŵ. The reason is that item 1 in the definition of an X-derivation is not satisfied because a ∧ b is not of the form α 1 ⊃ α 2 while ρ = ⊤. In contrast, the tree in the next example is a (⊤, ∅, a ∧ b)-derivation of (⊤, {d, e}, c) from Ŵ.

Example 16. Let us still consider Ŵ = {(a ∧ b, {d, e}, f ), (f , ∅, c)}. The tree of Fig. 8 is a (⊤, ∅, a ∧ b)-derivation of (⊤, {d, e}, c) from Ŵ (informally meaning that assuming a ∧ b allows us to conclude c, unless d or e be the case).

Example 17. Once more, Ŵ = {(a∧b, {d, e}, f ), (f , ∅, c)}. The tree of Fig. 7 is a (a∧b, {d, e}, f )-derivation of (a∧b, {d, e}, c) from Ŵ although in a rather vacuous way because X = (a∧b, {d, e}, f ) is in Ŵ. Indeed, the tree of Fig. 7 is also a (a∧b, {d, e}, f )derivation of (a ∧ b, {d, e}, c) from Ŵ ′ where Ŵ ′ is taken to be Ŵ \ {(a ∧ b, {d, e}, f )}.

Example 18. Let Ŵ = {(f , {e}, c)}. The tree of Fig. 9 is a (a ∧ b, {d}, f )-derivation of (a ∧ b, {d, e}, c) from Ŵ. Please observe that the premise of X, namely a ∧ b, is not issued from Ŵ hence is also the premise of ℵ (here, X is (a ∧ b, {d}, f ) and ℵ is (a ∧ b, {d, e}, c)).

Example 19. Let Ŵ = {(a ∧ b, {d, e}, f )}. The tree of Fig. 10 is a (f , {g}, c)-derivation of (a ∧ b, {d, e, g}, c) from Ŵ.

PEC-implicants

PEC-implicants are intended to extend and adapt the usual concept of implicants modulo a set of formulas to the PEC formalism and with respect to the X-derivation mechanism. This concept will allow us to capture the idea of having one rule entailing another rule, as part of our problem dealing with subsuming rules. However, we believe that the PEC-implicants concepts can have various other applications, as they generalize the standard-logic concept of implicants to a more expressive generic nonmonotonic framework. Let us provide the definition before we explain the intuitions and motivations justifying it.

Definition 6 (PEC-implicant). Let Ŵ be a set of unary PEC rules and R = (ρ, {ǫ 1 , . . . , ǫ m }, ς ) be a unary PEC rule. A unary PEC rule R ′ is a PEC-implicant of R modulo Ŵ iff there exists an R ′ -derivation D of (ρ, E * , ς ) from Ŵ s.t.

1. ∀e ′ ∈ E * , ∃e ∈ {ǫ 1 , . . . , ǫ m } s.t. e ∈ Cn({e ′ }), 2. ∀e ′′ ∈ {ǫ 1 , . . . , ǫ m } \ E * , e ′′ ∈ Cn{α | ⊢ α is a node of D}.
Definition 7 (Strict PEC-implicant). Let Ŵ be a set of unary PEC rules. Let R and R ′ be two unary PEC rules.

R ′ is a strict PEC-implicant of R modulo Ŵ iff R ′ is a PEC-implicant of R and R is not a PEC-implicant of R ′ .
To simplify matters, Cn stands for classical logic in all of the following examples.

First, let us note that in the monotonic fragment of the PEC formalism, i.e. when all rules exhibit empty sets of exceptions, neither item 1 nor item 2 does apply. Consequently, Definition 6 reduces to R ′ is an implicant of R modulo Ŵ iff there exists an R ′ -derivation of R from Ŵ (noted Ŵ|∼ R ′ R). Moreover, the derivation tree is a standard deduction one, possibly making use of R ′ and where the premise ρ of R can play the role of an additional hypothesis.

Example 20. Let Ŵ = {(g ∧ h, ∅, c), (⊤, ∅, h)} be a set of PEC rules. Let R = (a ∧ b, ∅, c) and R ′ = (a, ∅, g) be two PEC rules. R ′ is a PEC-implicant of R modulo Ŵ.
Indeed, the tree of Fig. 11 is an R ′ -derivation of R from Ŵ. As a leaf of the tree, the premises of R (namely a ∧ b) are thus assumed to be satisfied when the derivation is performed.

Example 21. Let Ŵ = {(g ∧ h, ∅, c), (⊤, ∅, h)} a set of PEC rules. Let R = (a ∧ b, ∅, c) and R ′ = (⊤, ∅, g) be two PEC rules.
The leftmost tree of Fig. 12 does not make R ′ to be a PEC-implicant of R modulo Ŵ. Indeed, this tree is not an R ′ -derivation of R from Ŵ since the premise of R (i.e., a ∧ b) does not belong to the set of positive nodes of the tree. This violates the first part of item 7 in Definition 5. Note that R ′ is a (strict) PEC-implicant of (⊤, ∅, c) through the aforementioned tree. Now, R ′ is a PEC-implicant of R modulo Ŵ through the rightmost tree of Fig. 12. Indeed, this tree is an R ′ -derivation of R from Ŵ.

Note that, in this tree, we assume that the premise of R is satisfied, although it does not play a significant role here.

Example 22. Let Ŵ = {(a, ∅, c)} be a set of PEC rules. Let R = (a ∧ b, ∅, c) and R ′ = (⊤, ∅, x) be two PEC rules. R ′ is a PEC-implicant of R modulo Ŵ. Indeed, the tree from Fig. 13 is an R ′ -derivation of R from Ŵ.Note that this tree is also a derivation of R from Ŵ. Let us now consider the general case. When PEC rules with non empty sets of exceptions are considered, items 1 and 2 of Definition 6 apply. Intuitively, it is necessary to take into account the possible links between the exceptions of R and the exceptions of R ′ . These links must be such that if R ′ does not apply due to one of its exceptions then R must not apply. On the contrary, if R does not apply due to one of its exceptions, it might be the case that R ′ applies. Thus, on the one hand, all exceptions of R ′ must be as strong as at least one exception of R (see ¬d, Example 23, ¬d ∧ ¬f , Examples 24 and 25).

On the other hand, the exceptions occurring in the derivation tree used to show the implication and that are not implied by an exception of R ′ must also be as strong as at least one exception of R (see ¬e ∧ ¬h, Example 25). Thus, it is necessary to consider the possible links between the exceptions of R and the nodes in the derivation tree showing the implication. Our intuition leads us to require that the proof of the implication (through the derivation tree) does not entail an exception of R (see ¬e, Example 26 et e, Example 27).

Thus, showing that R ′ is a PEC-implicant of R = (ρ, {ǫ 1 , . . . , ǫ m }, ς ) modulo Ŵ, amounts to showing that there exists an R ′ -derivation of (ρ, E * , ς ) where E * consists of the negative nodes of the tree (belonging or not to the set of exceptions of R ′ ), it must be the case that each element of E * implies an exception of R (item 1) and it must be the case that no exception of R that is not in E * is a logical consequence of the positive nodes in the tree. Note that if there exists a derivation of R from Ŵ (according to Definition 3) then for some PEC rules R ′ , R ′ is a PEC-implicant of R modulo Ŵ, without R ′ playing any role in the derivation (see Example 29).

Example 23. Let Ŵ be an empty set of PEC rules. Let R = (a ∧ b, {¬d, ¬e}, c) and R ′ = (a, {¬d}, c) be two PEC rules. R ′ is a PEC-implicant of R modulo Ŵ through the tree of Fig. 14. Indeed, this tree is an R ′ -derivation of (a ∧ b, {¬d}, c) from Ŵ. In accordance with item 1, ¬d (exception of R ′ ) belongs to the set of exceptions of R and in accordance with item 2, ¬e cannot be deduced from {a, a ∧ b, c}.

Example 24. Let Ŵ be an empty set of PEC rules. Let R = (a, {¬d, ¬e}, c) and R ′ = (a, {¬d ∧ ¬f }, c) be two PEC rules. R ′ is a PEC-implicant of R modulo Ŵ, as shown by the tree of Fig. 15. Indeed, this tree is an R ′ -derivation of (a, {¬d ∧ ¬f }, c) from Ŵ. In accordance with item 1, ¬d ∧ ¬f (exception of R ′ ) implies ¬d (an exception of R) and in accordance with item 2, neither ¬d nor ¬e (the members of {ǫ 1 , . . . , ǫ m }) are implied by {a, c} (the formulas attached to the positive nodes of the tree).

Example 25. Let Ŵ = {(a, {¬e ∧ ¬h}, g)} be a set of PEC rules. Let R = (a, {¬d, ¬e}, c) and R ′ = (g, {¬d ∧ ¬f }, c) be two PEC rules. R ′ is a PEC-implicant of R modulo Ŵ, as illustrated by the tree of Fig. 16. Indeed, this tree is an R ′ -derivation of (a, {¬d ∧ ¬f , ¬e ∧ ¬h}, c) from Ŵ. In accordance with item 1, ¬d ∧ ¬f (which is in E * and is an exception of R ′ ) implies ¬d (an exception of R) and ¬e ∧ ¬h (which is E * and is an exception of the only PEC rule of Ŵ) implies ¬e (an exception of R). In accordance with item 2, neither ¬d nor ¬e (the members of {ǫ 1 , . . . , ǫ m }) are implied by {a, c, g} (formulas corresponding to the positive nodes of the tree).

Example 26. Let Ŵ = {(a, ∅, ¬e), (¬e, ∅, f )} be a set of PEC rules. Let R = (a ∧ b, {¬d, ¬e}, c) and R ′ = (f , {¬d}, c) be two PEC rules. R ′ is not a PEC-implicant of R modulo Ŵ through the tree of Fig. 17. Indeed, although this tree is an R ′ -derivation of (a ∧ b, {¬d}, c) from Ŵ, the item 2 from Definition 6 is not respected: ⊢ ¬e is a node of the tree although ¬e is an exception of R. Example 27. Let Ŵ = {(a, {e}, f )} be a set of PEC rules. Let R = (a ∧ b, {¬d, ¬e}, c) and R ′ = (f , {¬d}, c) be two PEC rules. R ′ is not a PEC-implicant of R modulo Ŵ through the tree of Fig. 18. Although the latter one is an R ′ -derivation of (a ∧ b, {¬d, e}, c) from Ŵ, item 1 from Definition 6 is violated: e is a formula of E * from which no formula from {¬d, ¬e} can be inferred.

Example 28. Let Ŵ be an empty set of PEC rules. Let R = (a, {¬b}, b) and R ′ = (⊤, ∅, a ⊃ b) be two PEC rules. R ′ is a PEC-implicant of R modulo Ŵ through the tree from Fig. 19. Indeed, this tree is an R ′ -derivation of (a, ∅, b) from Ŵ. Item 1 is satisfied since E * is empty. Moreover, in accordance with item 2, ¬b cannot be deduced from {a, b, a ⊃ b} (i.e., the formulas attached to the positive nodes of the tree).

Example 29. Let Ŵ = {(a, {d, e}, c)} be a set of PEC rules. Let R = (a ∧ b, {d, e}, c) and R ′ = (x, {z}, y) be two PEC rules. R ′ is a PEC-implicant of R modulo Ŵ. Indeed, the tree from Fig. 20 is an R ′ -derivation of R from Ŵ. Let us stress that here R ′ does not play any role in the derivation: This tree is also a derivation of R from Ŵ.

Fairly weak requirements about Cn are enough to show that being a PEC-implicant defines a pre-order. Of special interest then is the case that two PEC rules are PEC-implicants of each other: They surely are equivalent in a strong sense closely related to Cn-equivalence of exceptions. It is straightforward to obtain such a result, as follows.

Property 2. Given two unary PEC rules

R = (ρ, {ǫ 1 , . . . , ǫ m }, ς ) and R ′ = (ρ ′ , {ǫ ′ 1 , . . . , ǫ ′ n }, ς ′ ), if R is a PEC-implicant of R ′ modulo Ŵ
, and R ′ is a PEC-implicant of R modulo Ŵ where Ŵ = ∅ then:

1. ρ -ρ ′ and ρ ′ -ρ, 2. ∀ǫ i ∈ {ǫ 1 , . . . , ǫ m }, ∃ǫ j , ǫ ′ k where ǫ j ∈ {ǫ 1 , . . . , ǫ m } and ǫ ′ k ∈ {ǫ ′ 1 , . . . , ǫ ′ n }, s.t. ǫ j -ǫ i and ǫ j -ǫ ′ k and ǫ ′ k -ǫ j .

The idea underlying the previous result is to extend to PEC rules the idea that when two objects are symmetrically related with each other through a given relation, then they must be equivalent in some sense (other than the trivial equivalence obtained from the binary relation under consideration). In particular, item 2 means that exceptions in R and R ′ are the same, up to logical equivalence (by subsumption, there can be more exceptions in R or in R ′ , though).

Essential implicants and prime implicants

From now on, we write implicant as a shorthand for PEC-implicant. We have seen that some implicants only play a superfluous role in the X-derivation used to show the implication. According to our goal to insert a PEC rule while ensuring that rules subsuming it are rejected, we should not discard those implicants. To this end, we define a concept of essential implicant that does not select them.

We assume that an operator \ is available in the PEC framework. Intuitively, \ is a syntactical contraction operator between a set of PEC rules and a PEC rule: Ŵ \ R contracts Ŵ from R (and from any equivalent PEC rule to R, in accordance with the equivalence concept introduced at the end of the previous Section). Definition 8 (Essential implicant). Let Ŵ be a set of PEC rules, R and R ′ be PEC rules. R ′ is an essential implicant of R modulo Ŵ iff there exists Ŵ ′ ⊆ Ŵ \ {R} s.t. :

(a, ∅, c) from Ŵ ′ , as the rightmost tree of Fig. 21 shows. On the other hand, there cannot exist any derivation of R ′ or of any of its implicants, modulo Ŵ ′ \ {R ′′ } since Ŵ ′ \ {R ′′ } is empty. Consider now the essential implicants of R ′′ modulo Ŵ. Note that Ŵ ′ = Ŵ \ {R ′′ } = Ŵ = ∅. It is easy to see that, at the same time, R ′ and R are not essential implicants of R ′′ modulo Ŵ ′ . Thus, R ′′ is both a strict essential implicant of R and of R ′ modulo Ŵ. Consequently, R ′′ is not a prime implicant of R modulo Ŵ. Also, note that although R ′ is a strict essential implicant of R modulo Ŵ, R ′ is not necessarily a prime implicant of R modulo Ŵ. Indeed, other strict essential implicants of R modulo Ŵ can exist, of which R ′ is a strict essential implicant modulo Ŵ (e.g., the PEC rule R ′′′ = (a ∧ b, {¬d ∧ ¬f }, c) is a strict essential implicant of R modulo Ŵ and R ′ is a strict essential implicant of R ′′′ modulo Ŵ).

Example 31. Let Ŵ = {(a, {¬d, ¬e}, c)} be a set of PEC rules and R = (a ∧ b, {¬d, ¬e}, c) a PEC rule. First, let us consider the essential implicants of R modulo Ŵ. Note that here Ŵ \ {R} = Ŵ. Thus, there can only exist two different Ŵ ′ , namely:

• Ŵ ′ 1 = Ŵ, • Ŵ ′ 2 = ∅.
The PEC rule R ′ = (x, {¬z}, y) is not an essential implicant of R modulo Ŵ. First, consider Ŵ ′

1 . On the one hand, R ′ is an implicant of R modulo Ŵ ′ 1 . Indeed, as shown in the tree of Fig. 22, there exists an R ′ -derivation of R modulo Ŵ ′ 1 . But on the other hand, as the same tree shows it, there exists a derivation of R modulo Ŵ ′ 1 \ {R ′ } (note that Ŵ ′ 1 \ {R ′ } = Ŵ). Now, consider Ŵ ′ 2 . Clearly, there does not exist any R ′ -derivation of R modulo Ŵ ′ 2 . Thus, R ′ is not an implicant of R modulo Ŵ ′

Fig. 1 .

 1 Fig. 1. Tree from Examples 5-7.

Fig. 2 .

 2 Fig. 2. Tree from Example 8.

Fig. 3 .

 3 Fig. 3. Tree from Examples 9 and 10.

Fig. 4 .

 4 Fig. 4. Tree from Example 11.Example 8. Let Ŵ = {(⊤, ∅, a)}. The tree from Fig.2is a derivation of (¬a, ∅, c) from Ŵ. Note that ρ plays the role of an additional hypothesis.

Fig. 5 .

 5 Fig. 5. Tree from Example 12.

Fig. 6 .

 6 Fig. 6. Tree from Example 13. Example 12. Let Ŵ = ( , ) be a default theory with = { ⊤:a ¬a , b:d,e c } and = {b}. Let us represent Ŵ by the PEC rules Ŵ ′ = {(⊤, {¬a}, ¬a), (b, {¬d, ¬e}, c), (⊤, ∅, b)}. Ŵ has no extension because contains the default ⊤:a

Fig. 7 .

 7 Fig. 7. Tree from Examples 14, 15 and 17.

Fig. 8 .

 8 Fig. 8. Tree from Example 16.

Fig. 9 .

 9 Fig. 9. Tree from Example 18.

Fig. 10 .Fig. 11 .

 1011 Fig. 10. Tree from Example 19.

Fig. 12 .

 12 Fig. 12. Trees from Example 21.

Fig. 13 .

 13 Fig. 13. Tree from Example 22.

Fig. 14 .

 14 Fig. 14. Tree from Example 23.

Fig. 15 .

 15 Fig. 15. Tree from Example 24.

Fig. 16 .

 16 Fig. 16. Tree from Example 25.

Fig. 17 .

 17 Fig. 17. Tree from Example 26.

Fig. 18 .

 18 Fig. 18. Tree from Example 27.

Fig. 19 .

 19 Fig. 19. Tree from Example 28.

Fig. 20 .

 20 Fig. 20. Tree from Example 29.

Fig. 21 .

 21 Fig. 21. Trees from Example 30.

Fig. 22 .

 22 Fig. 22. Tree from Example 31.

Fig. 23 .

 23 Fig. 23. Trees from Example 32.

  In this case, α ∈ Cn({α 1 , . . . , α . ρ ∈ {α s.t. ⊢ α is a leaf of T} ∪ {⊤}, {ǫ 1 , . . . , ǫ n } = {β s.t. ⊢ β is a node of T} and ⊢ ς is the root of T.

	We note Ŵ|∼

k }) • or a tuple (⊢ α 1 , ⊢ β 1 , . . . , ⊢ β m ) where m ≥ 1. In this case, (α 1 , {β 1 , . . . , β m }, α) ∈ Ŵ ∪ {X}. 5{ǫ 1 ,...,ǫ n } X

ℵ and Ŵ|∼ X ℵ when {ǫ 1 , . . . , ǫ n } is empty.

Acknowledgements

Part of this work has been supported by the Région Nord/Pas-de-Calais and the EC through a FEDER grant. The authors thank the anonymous reviewers for their valuable comments and suggestions.

Accordingly, R ′ is not a strict essential implicant of R modulo Ŵ and it thus not a prime implicant. On the contrary, the PEC rule R ′′ = (a, {¬d, ¬e}, c) is an essential implicant of R modulo Ŵ. On the one hand, R ′′ is an implicant of R modulo Ŵ ′ 1 .

Indeed, the tree from Fig. 22 is an R ′′ -derivation of R modulo Ŵ ′ 1 . On the other hand, there does not exist any derivation of R or of one of its implicants modulo Ŵ ′ 1 \ {R ′′ }. Indeed in this case Ŵ ′ 1 \ {R ′′ } = ∅. Consider now the essential implicants R ′′ modulo Ŵ. Note that in this case Ŵ \ {R ′′ } = ∅. Thus, there exists only one Ŵ ′ and it is empty. It is easy to see that R is not an essential implicant of R ′′ modulo Ŵ. R ′′ is thus a strict essential implicant of R modulo Ŵ. Thus, amongst {R ′ , R ′′ }, only R ′′ and its equivalent forms can be candidates for being prime implicants of R modulo Ŵ.

Example 32. Let Ŵ = {(a, {¬d ∧ ¬f }, c ∧ x)} be a set of PEC rules and R = (a ∧ b, {¬d, ¬e}, c) one PEC rule. First, consider the essential implicants of R modulo Ŵ. Note that here Ŵ \ {R} = Ŵ. Thus, only two different Ŵ ′ exist, namely:

Indeed, as the leftmost tree of Fig. 23 shows, there exists an R ′ -derivation of (a

On the other hand, as the rightmost tree of Fig. 23 shows, there exists a derivation of (a ∧ b, {¬d ∧ ¬f }, c),

Consequently, R ′ is not a strict essential implicant of R modulo Ŵ hence is not a prime implicant. On the contrary, the PEC rule

Indeed, the rightmost tree of Fig.

23 is an R ′′ -derivation of (a ∧ b, {¬d ∧ ¬f }, c) modulo Ŵ ′ 1 . On the other hand, there does not exist any derivation of R or of any of its implicants modulo Ŵ ′ 1 \ {R ′′ }. Indeed, in this case, Ŵ ′ 1 \ {R ′′ } = ∅. Now, consider the essential implicants of R ′′ modulo Ŵ. Note that here Ŵ \ {R ′′ } = ∅. Thus, there exists only one Ŵ ′ and it is empty. It is easy to see that R is not an essential implicant of R ′′ modulo Ŵ. R ′′ is thus a strict essential implicant of R modulo Ŵ. Thus, amongst {R ′ , R ′′ }, only R ′′ and its equivalent forms can be candidates for being prime implicants of R modulo Ŵ.

Example 33. Let Ŵ = {(a, {¬d ∧ ¬f }, c), (a ∨ h, ∅, c)} be a set of PEC rules and R = (a ∧ b, {¬d, ¬e}, c) a PEC rule. First, consider the essential implicants of R modulo Ŵ. Note that here Ŵ \ {R} = Ŵ. Thus, there exists four different Ŵ ′ , namely:

. Indeed, as the leftmost tree of Fig. 24 shows it, there exists an R ′ -derivation of (a

. On the other hand, there does not exist any derivation of R or of one of its implicants modulo Ŵ ′

. Indeed, as the middle tree of Fig. 24 shows it, there exists an

. On the other hand, there does not exist any derivation of R or of one of its implicants

Thus, there exists only two different Ŵ ′ , namely:

Indeed, as the rightmost tree of Fig. 24 shows, there exists an R ′′ -derivation of (a, ∅, c) modulo Ŵ ′ 1 . On the other hand, there does not exist any derivation of R ′ or of one of its implicants modulo Ŵ ′ 1 \ {R ′′ } since Ŵ ′ 1 \ {R ′′ } = ∅. Now consider the essential implicants of R ′′ modulo Ŵ. Note that here Ŵ \ {R ′′ } = {(a, {¬d ∧ ¬f }, c)}. Thus, there exist only two different Ŵ ′ , namely:

Again, it is easy to see that R is not an essential implicant of R ′′ modulo Ŵ. R ′′ is thus a strict essential implicant of R modulo Ŵ. However, R ′ is not an essential implicant of R ′′ modulo Ŵ. To show it, it is useful to consider the subsets Ŵ ′ of Ŵ \ {R ′′ } :

•

Thus, R ′′ is a strict essential implicant of R ′ modulo Ŵ. Consequently, R ′′ cannot be a prime implicant of R modulo Ŵ

Overriding subsuming rules

We are now ready to introduce our approach to override subsuming rules. To override the subsuming rules of a PEC rule R and make R to preempt, it is presumably not sufficient to "withdraw" all prime implicants of R and insert R. Indeed, as shown in the next example, there may remain in the resulting Ŵ some information of a change, e.g. so that whenever R is derivable, one of its strict PEC-implicants is also derivable.

Assume that we want to augment Ŵ with R in such a way that R is not subsumed. Clearly, there is no prime implicant of R in Ŵ. However, introducing R in Ŵ will allow a ∨ b to be deduced, which is a strict implicant of a ∨ b ∨ c.

Accordingly, the process will thus be a little more elaborate. The intuition behind the approach is best explained in the Boolean framework: assume that a formula g is to be introduced inside Ŵ so that g is not subsumed. In the case g is consistent with Ŵ, it is necessary to retract g ⊃ f for every prime implicant f of g. Intuitively, when g is then inserted inside Ŵ, no way to infer f remains available. Such an idea has been explored for the Boolean framework in [START_REF] Besnard | Enforcing logically weaker knowledge in classical logic[END_REF].

Let us extend this idea to the full PEC-framework and X-derivation mechanism. In the sequel, we assume an operator \ to be available in the PEC framework with the following features. Intuitively, \ is a kind of contraction operator which applies to a set of PEC rules and to a pair of PEC rules: Ŵ \ (R, R ′ ) is intended to contract Ŵ of R ′ in the presence of R. Formally, it is expected to enjoy the following properties.

where R, R ′ , R ′′ are PEC rules and Ŵ is a set of PEC rules that does not need to be consistent. The last property is not natural for a pure contraction operator. However, it proves convenient in allowing us to state the following natural definition.

Definition 11. Let R ′ be a prime PEC-implicant of R modulo Ŵ.

Let R ′ be a prime implicant of R modulo Ŵ.

Proof. First let us show that Ŵ ⊕ R ′ R|∼ ǫ R. According to Definition 11, R ∈ Ŵ ⊕ R ′ R. Thus, we can build a tree whose root is ⊢ ς and whose parents are ⊢ ρ and ⊢ ǫ 1 , . . . , ⊢ ǫ n . This tree clearly obeys all conditions of Definition 3: only item 2 requires more analysis. We need to prove that ǫ i ∈ Cn({γ

Let us address the consistency issue of Ŵ ⊕ R ′ R. We have shown that

were to exist, then it would contain positive nodes only (item 5 of Definition 3), which, due to item 4 of the aforementioned definition, would

, which we just have proved to be impossible. Thus, there does not exist any derivation of (⊤, ∅, ⊥) from Ŵ \ (R, R ′ ). Accordingly, there does not exist any derivation of (⊤, ∅, ⊥) from Ŵ \ (R, R ′ ) ∪ {R} because such a derivation would have ⊢ ⊥ as its a root, which would violate item 2 from Definition 3 for all ǫ i of R (there exists at least one since n ≥ 1).

Let us finish the proof by showing that

In accordance with Definition 5, there does not exist any R-derivation of R ′ from Ŵ \ (R, R ′ ). Thus, there does not exist any derivation of

The next step consists in iterating the above process on all primes implicants of R. Assuming that the \ operator is extended so that it applies to all the elements of its second argument, which is now a set of PEC rules; we only need one more definition.

Let Y be the set of prime implicants of R modulo Ŵ.

It is easy to show that this definition enjoys the properties attached to the ⊕ R ′ operator (see Theorem 1). Accordingly, the set of PEC rules delivered by Ŵ ⊕ Y R is consistent; it allows R to be deduced, while, at the same time, it prevents R to be subsumed. Theorem 2. Let Ŵ be a set of PEC rules. Let R = (ρ, {ǫ 1 , . . . , ǫ n }, ς ) be a PEC rule s.t. n ≥ 1 and s.t. ǫ i ∈ Cn({ρ , ς }) for i = 1..n. Let Y be the set of prime implicants of R modulo Ŵ.

Conclusions and future work

The contribution of this paper is at least twofold. First, a unified framework has been presented that allows both monotonic knowledge and defeasible rules to be represented and reasoned about in a uniform way. Derivation tools have been defined allowing to reason and infer both kinds of knowledge indifferently. The next step will be to address algorithmic aspects of X-derivations and associated inference, within the propositional setting. Also, the X-derivation concept implements the possibility to state defeasible rules as extra assumptions, which are coming in addition to the defeasible character of rules with exceptions. We believe that this two-level form of hypothetical reasoning could be further explored and refined. Also, a whole family of forms of implicants could be devised for defeasible rules, depending on the actual form of reasoning that is modeled and on the intended actual epistemological roles of the involved exceptions, premises and conclusion. Second, this framework has been exploited to solve a specific problem in knowledge representation and reasoning that has not received much attention so far. Namely, how could new information override the relevant subsuming information which is currently available? We claim that such an issue should not be taken for granted. Indeed, in real life we do often get new knowledge that is logically weaker but that appears more informative than the previously recorded one, and should therefore be preferred.