Encoding formulas with partially constrained weights in a possibilistic-like many-sorted propositional logic

1 Introduction

Information is often pervaded with uncertainty, and logics of different types have been developed for handling uncertain pieces of knowledge, some based on probability theory, others based on non-additive formalisms such as possibility theory. The lack of total certainty of a piece of information is then assessed by means of an evaluation that estimates the degree of certainty of the piece of information under the form of a precise value, or at least of a bound that constrains its value. For instance, a possibilistic logic expression of the form a0 ✁ ✄ ✆ ✞ encodes the constraint ✠ a0 ✁ ✞ ☞ ✆ , where ✁ is a proposition, ✆ ✎ a0 ✒ ✄ ✕ ✗ , and ✠ is a necessity measure [Dubois et al., 1994], with the intended meaning that p is certain at level at least ✆ .

In this paper, only partial information is supposed to be available about the relative ordering between the weights of the formulas in the base. More precisely, propositional formulas are associated with symbolic weights, and a set of

Henri Prade

IRIT (CNRS-UPS) 118, Route de Narbonne 31062 Toulouse Cedex 04, France. prade@irit.fr

constraints on these weights is speci�ed to express the relative importance of these weights. These weights may be compound symbolic expressions (e.g., as the result of formal computations) involving maximum and minimum operations.

For handling these symbolic weights, we propose an approach that uses a logical encoding of the weights. Indeed, one may think of expressing that a piece of information ✁ is not totally certain, by stating that ✁ is true under some (unspeci�ed) condition, namely �things are not abnormal�. Thus, the uncertain statement ✁ can be written ✁ ✙ ✛ , which can be read � ✁ is true or it is abnormal (A)�. Then note that if one simultaneously asserts ✁ ✙ ✛ and ✤ ✁ ✙ ✛ ✧ , i.e. it is somewhat certain that ✁ is true and it is also somewhat certain that ✁ is false, ✛ ✙ ✛ ✧ can be derived from the two pieces of information, which expresses that in a way or another we are in an abnormal situation. In this paper, since ✁ ✙ ✛ will be used as an encoding of the possibilistic formula a0 ✁ ✄ ✆ ✞ , ✛ may be a propositional formula if ✆ is a symbolic expression. For instance, the case of multiple abnormality situations for ✁ will be encoded by ✁ ✙ ✛ ✮ ✙ ✰ ✰ ✰ ✙ ✛ ✶ .

This suggests a way of dealing with propositional formulas with partially constrained weights in a purely logical setting. In possibilistic logic, formulas with a weight strictly greater than the inconsistency level of the knowledge base are immune to inconsistency and can be safely used in deductive reasoning. In the proposed approach, the weights attached to the inferred formulas are handled as symbolic expressions, as well as the inconsistency level of the base. A procedure is described which enables us to determine when the available information is enough for knowing if a symbolic weight is greater than another or not.

The paper proposes a uni�ed and general framework to represent and handle partially-constrained weighted formulas, using propositional logic. Its main contributions are:

• ✸ to encode available pieces of information ✹ using a propositional knowledge base ✺ ✻ . Each symbolic weight ✆ is represented by a propositional expression ✛ . Each compound expression is associated with a propositional formula, obtained by replacing maximum by a conjunction, and minimum by a disjunction. An uncertain formula a0 ✁ ✄ ✆ ✞ will be represented by a propositional logical formula ✁ ✙ ✛ , where ✁ and ✛ are built using two different sets of variables: ✾ and ✿ . Intuitively, ✁ ✙ ✛ means that ✁ is uncertain, and its uncertainty degree is
• encoded by a logical formula ✛ .
• ✸ to encode constraints ❀ on symbolic weights with another propositional knowledge base ✺ ❁ . The inequality ✆ ☞ ❃ will be represented using material implication. The fact that ✆ is at least as large as ❃ , will be encoded by a propositional formula ✛ ❅ ❇ (i.e., ✤ ✛ ✙ ❇ ). Maximum and minimum operations are also encoded here using respectively conjunctions and disjunctions.
• ✸ to de�ne an inference relation in order to draw plausible conclusions from ✺ ✻ and ✺ ❁ . This inference is sound and complete with respect to a semantics based on preferential models. It extends the possibilistic logic (where the constraints on symbolic weights induce a total preordering).
• ✸ to characterize this inference process by �forgetting� variables of ✾ , and by �forgetting� negative literals from ✿ . The inference process basically comes down to infer from ✺ ✻ and ✺ ❁ the strongest positive formula (that does not contain negation symbol), denoted ❉ ❊ ● ■ a0 ✺ ✻ ✄ ✺ ❁ ✞ , that only contains variables from ✿ . Intuitively, ❉ ❊ ● ■ a0 ✺ ✻ ✄ ✺ ❁ ✞ represents the logical counterpart of the inconsistency degree of the knowledge base.
• ✸ to use recent results on compilations (e.g., [Darwiche, 2004]) to compute plausible inferences. More precisely, the knowledge base ✺ ✻ ▼ ✺ ❁ is �rst compiled intoDNF. These formats allow then to have a linear computation of ❉ ❊ ● ■ a0 ✺ ✻ ✄ ✺ ❁ ✞ .

After a brief survey of possibilistic logic in Section 2, Section 3 states the problem of reasoning from possibilistic formulas with partially constrained uncertainty weights. Section 4 provides its purely logical counterpart as a two-sorted logic and de�nes a sound and complete inference process from the two knowledge bases encoding respectively the pieces of uncertain information, and the constraints on the uncertainty levels. The handling of symbolic weights in the inference process is then characterized in section 5 in terms of forgetting variables, and in terms of DNF (or d-DNNF compilation) of the knowledge bases. This section also brie�y considers the case of totally ordered information corresponding to standard possibilistic knowledge bases.

2 Brief background on possibilistic logic

We start with a brief refresher on possibilistic logic (for more details see [Dubois et al., 1994]). A possibilistic logic formula is a pair made of a classical logic formula and a weight ✆ expressing certainty. The weight ✆ ✎ a0 ✒ ✄ ✕ ✗ of a formula ✁ is interpreted as the lower bound of a necessity measure ✠ , i.e., the possibilistic logic expression a0 ✁ ✄ ✆ ✞ is understood as ✠ a0 ✁ ✞ ☞ ✆ . Since ✠ a0 ✁ ❚ ❯ ✞ ❲ ❳ ❊ ● a0 ✠ a0 ✁ ✞ ✄ ✠ a0 ❯ ✞ ✞ it is always possible to put a possibilistic formula a0 ✁ ✄ ✆ ✞ under the form of a conjunction of clauses a0 ✁ ❪ ✄ ✆ ✞ if ✁ ❫ ❚ ❪ ✁ ❪ . The basic inference rule in possibilistic logic put in clausal form is the resolution rule: a0 ✤ ✁ ✙ ❯ ✄ ✆ ✞ ❝ a0 ✁ ✙ ❡ ✄ ❃ ✞ ✐ a0 ❯ ✙ ❡ ✄ ❳ ❊ ● a0 ✆ ✄ ❃ ✞ ✞ . Classical resolution is retrieved when all the weights are equal to 1. Let ✹ ❲ ❧ a0 ✁ ❪ ✄ ✆ ❪ ✞ ♣ ❊ ❲ ✕ ✄ ● a115 be a knowledge base. The level of inconsistency of ✹ is de�ned as:

a116 ● ■ a0 ✹ ✞ ❲ ❳ ✆ ✈ ❧ ✆ ♣ ✹ ✇ ✐ ① ✞ a115 (by convention ❳ ✆ ✈ ② ❲ ✒ ). where ✹ ✇ ❲ ❧ ✁ ❪ ♣ a0 ✁ ❪ ✄ ✆ ❪ ✞ ✎ ✹ ✄ and ✆ ❪ ☞ ✆ a115 .

It can be shown that a116 ● ■ a0 ✹ ✞ ❲ ✒ iff ✹ ⑦ ❲ ❧ ✁ ❪ ♣ a0 ✁ ❪ ✄ ✆ ❪ ✞ ✎ ✹ a115 is consistent in the usual sense.

Refutation can be easily extended to possibilistic logic. Proving a0 ✁ ✄ ✆ ✞ from ✹ amounts to adding a0 ✤ ✁ ✄ ✕ ✞ , put in clausal form, to ✹ , and using the above rules repeatedly until getting ✹ ▼ ❧ a0 ✤ ✁ ✄ ✕ ✞ a115 ✐ a0 ① ✄ ✆ ✞ . Clearly, we are interested here in getting the empty clause ① with the greatest possible weight, i.e., a116 ● ■ a0 ✹ ▼ ❧ a0 ✤ ✁ ✄ ✕ ✞ a115 ✞ ☞ ✆ . Indeed, the conclusion a0 ✁ ✄ ✆ ✞ is valid only if ✆ ❷ a116 ● ■ a0 ✹ ✞ .

Semantic aspects of possibilistic logic, including soundness and completeness results with respect to the above syntactic inference, are presented in [Dubois et al., 1994]. Semantically, a possibilistic knowledge base ✹ ❲ ❧ a0 ✁ ❪ ✄ ✆ ❪ ✞ ♣ ❊ ❲ ✕ ✄ ● a115 is understood as a complete pre-ordering on the set of interpretations: ❹ ❷ ✻ ❹ ✧ iff ❳ ✆ ✈ ❧ ✆ ❪ ♣ a0 ✁ ❪ ✄ ✆ ❪ ✞ ✎ ✹ and ❹ ✧ ❼ ❾ ❲ ✁ ❪ a115 ❷ ❳ ✆ ✈ ❧ ✆ ➁ ♣ a0 ✁ ➁ ✄ ✆ ➁ ✞ ✎ ✹ and ❹ ❼ ❾ ❲ ✁ ➁ a115 . Thus ❹ is all the less plausible as it falsi�es formulas of higher degrees.

3 Possibilistic logic with symbolic weights

3.1 Representing beliefs

Let ✾ be a set of propositional variables. Let ❉ ➂ be a propositional language built from ✾ using the propositional connectors ❚ ✄ ✙ ✄ ✤ . Let ➃ be a set of symbolic weights or variables. Each symbol in ➃ takes its value in the interval ➄ ✒ ✄ ✕ ✗ .

In the following, ordinary propositions are denoted by lower case letters ✁ ✄ ❯ ✄ ❡ ✄ ✰ ✰ ✰ ✄ symbolic weights are denoted by lower case letters from the beginning of the alphabet ✆ ✄ ❃ ✄ ■ ✰ ✰ ✰ .

Let ✹ ❲ ❧ a0 ✁ ❪ ✄ ✆ ❪ ✞ ♣ ❊ ❲ ✕ ✄ ✰ ✰ ✰ ✄ ● a115 be a knowledge base with symbolic weights, where a0 ✁ ❪ ✄ ✆ ❪ ✞ expresses that ✁ ❪ is a believed with a symbolic weight ✆ ❪ . ✆ ❪ can be a compound expression, namely a max/min expression. More precisely, max/min expressions are obtained only using the two following rules: i) ✆ ✎ ➃ is a max/min expression, ii) if ✆ and ❃ are max/min expressions, then ❳ ✆ ✈ a0 ✆ ✄ ❃ ✞ and ❳ ❊ ● a0 ✆ ✄ ❃ ✞ are also max/min expressions.

Example 1 Let ✁ and ❡ be two propositional symbols. Let ✆ ✄ ❃ ✄ ■ ✄ ➆ ✄ ➇ be �ve symbolic weights. In the following, we will use the following base:

✹ ❲ ❧ a0 ✁ ✄ ❳ ✆ ✈ a0 ✆ ✄ ❃ ✞ ✞ ✄ a0 ✤ ✁ ✙ ❡ ✄ ❳ ❊ ● a0 ■ ✄ ➆ ✞ ✞ ✄ a0 ✤ ❡ ✄ ➇ ✞ ✞ a115 , to illustrate the main concepts of the paper. ✹ re�ects that ✁ is asserted by two sources having reliability ✆ and ❃ respectively, while for ✤ ✁ ✙ ❡ it is unsure if the information should be considered as having reliability equal to ■ or to ➆ .

3.2 Representing constraints

Constraints bearing on symbolic weights are described by a set of inequalities. A simple form of constraints is: ✆ ❪ ☞ ❃ ❪ , where ✆ ❪ and ❃ ❪ are elements of ➃ . These constraints ✆ ❪ ☞ ❃ ❪ restrict the possible values that ✆ ❪ and ❃ ❪ can take in ➄ ✒ ✄ ✕ ✗ .

More generally, the set of constraints are inequalities between max/min expressions of the form:

✆

Note that any set of constraints ❀ can be equivalently rewritten into a canonical form:

This follows from the facts that i) ✆ ☞ ❳ ✆ ✈ a0 ❃ ✄ ■ ✞ is equivalent to ✆ ☞ ❃ and ✆ ☞ ■ , ii) ❳ ❊ ● a0 ❃ ✄ ■ ✞ ☞ ✆ is equivalent to ❃ ☞ ✆ and ■ ☞ ✆ , and iii) max and min are distributive.

In the following, we assume that constraints in ❀ are in this canonical form.

Given a set of constraints ❀ , we are interested in checking whether a given equality ✆ ☞ ❃ ( ✆ and ❃ are max/min expressions) follows from this set of constraints.

De�nition 1 Let a and b be two max/min expressions.

• ✸ An assignment a116 is a function that assigns to each symbolic weight a degree belonging to a0 ✒ ✄ ✕ ✗ .
• ✸ An assignment a116 is a solution of ❀ if it satis�es each constraint of ❀ .
• ✸ ✆ ☞ ❃ follows from ❀ if each solution of ❀ is also a solution of ✆ ☞ ❃ .

The derivation of strict inequality can be de�ned recursively as follows. Let ✆ and ❃ be two elements of ➃ , then ✆ ❷ ❃ follows from C iff ✆ ☞ ❃ follows from ❀ and ❃ ☞ ✆ does not follow from ❀ (i.e., there is no proof for ❃ ☞ ✆ ). Now, let ✆ ✮ , ..., ✆ ✶ , ❃ ✮ , ..., ❃ ➋ be symbolic weights in ➃ . Then ❳ ✆ ✈ a0 ✆ ✮ ✄ ✰ ✰ ✰ ✄ ✆ ✶ ✞ ❷ ❳ ❊ ● a0 ❃ ✮ ✄ ✰ ✰ ✰ ✄ ❃ ➋ ✞ is derived from ❀ if there exist ✆ ❪ and ❃ ➁ such that ✆ ❪ ❷ ❃ ➁ . Lastly, the derivation from ❀ of strict inequality between two general max/min expressions can be de�ned using the fact that this derivation is equivalent to a derivation of a set strict inequalities of the canonical form ❳ ✆ ✈ a0 ✆ ✮ ✄ ✰ ✰ ✰ ✄ ✆ ✶ ✞ ❷ ❳ ❊ ● a0 ❃ ✮ ✄ ✰ ✰ ✰ ✄ ❃ ➋ ✞ , with ✆ ❪ 's and ❃ ❪ 's as symbolic weights.

Example 2 With the base of the above example, we will also consider the following set of constraints :

Note that since ➇ ☞ ✆ does not belong to the re�exive and transitive closure of ❀ , we may consider using a closed world assumption that the inequality is strict. The same holds for other inequalities.

3.3 Plausible inference and semantics

Given a knowledge base with symbolic weights, a116 ● ■ a0 ✹ ✞ is now a max/min expression of symbolic weights and the plausible inference of ✁ amounts to establish from ❀ that a116 ● ■ a0 ✹ ▼ ❧ a0 ✤ ✁ ✄ ✕ ✞ a115 ✞ ❷ a116 ● ■ a0 ✹ ✞ .

Here the weight ✕ continues to be the top certainty level, i.e., ➔ ✆ ✎ ➃ ✄ ✕ ☞ ✆ .

Our semantics is based on preferential models. We use the principle of best-out ordering de�ned in [Benferhat et al., 1993], to derive from ✹ a partial pre-order on the set of interpetations, denoted by ❷ ✻ , in agreement with possibilistic logic. Let ❹ , and ❹ ✧ be two interpretations. Then:

❹ ❷ ✻ ❹ ✧ iff for each a0 ✁ ➁ ✄ ❃ ➁ ✞ such that ❹ ❼ ❾ ❲ ✁ ➁ , there exists a0 ❯ ❪ ✄ ✆ ❪ ✞ such that ❹ ✧ ❼ ❾ ❲ ❯ ❪ and ✆ ❪ ❷ ❃ ➁ follows from ❀ .

Then, a conclusion ❯ is said to be a plausible consequence of a0 ✹ ✄ ❀ ✞ if ❯ is true in all preferredmodels (w.r.t. ❷ ✻ ).

An important result is the complete and soundness result, namely :

Proposition 1 a116 ● ■ a0 ✹ ▼ ❧ a0 ✤ ✁ ✄ ✕ ✞ a115 ✞ ❷ a116 ● ■ a0 ✹ ✞ follows from ❀ iff ✁ is true in all preferred models w.r.t ❷ ✻ .

Example 3 Let us consider the above example, where :

✹ ❲ ❧ a0 ✁ ✄ ❳ ✆ ✈ a0 ✆ ✄ ❃ ✞ ✞ ✄ a0 ✤ ✁ ✙ ❡ ✄ ❳ ❊ ● a0 ■ ✄ ➆ ✞ ✞ ✄ a0 ✤ ❡ ✄ ➇ ✞ ✞ a115 , and ❀ ❲ ❧ ✆ ☞ ➇ ✄ ■ ☞ ✆ ✄ ➆ ☞ ➇ a115 ✰

Given ✹ and ❀ we are interested to check if ❡ follows from ✹ and ❀ . Let us compute a116 ● ■ a0 ✹ ✞ . By de�nition, we have:

Let us simplify this expression, with the help of the constraints in ❀ , we have:

a116 ● ■ a0 ✹ ✞ ❲ ❳ ❊ ● a0 ❳ ✆ ✈ a0 ✆ ✄ ❃ ✞ ✄ ❳ ❊ ● a0 ■ ✄ ➆ ✞ ✄ ➇ ✞

❲ ❳ ✆ ✈ a0 ➇ ✄ ❳ ❊ ● a0 ❃ ✄ ➇ ✞ ✞ , hence:

We now need to compute a116 ● ■ a0 ✹ ▼ a0 ✤ ❡ ✄ ✕ ✞ ✞ , we get:

a116 ● ■ a0 ✹ ▼ a0 ✤ ❡ ✄ ✕ ✞ ✞ ❲ ❳ ✆ ✈ a0 a116 ● ■ a0 ✹ ✞ ✄ ❳ ❊ ● a0 ❳ ✆ ✈ a0 ✆ ✄ ❃ ✞ ✄ ❳ ❊ ● a0 ■ ✄ ➆ ✞ ✞ ✞

❲ ❳ ✆ ✈ a0 ➇ ✄ ❳ ✆ ✈ a0 ❳ ❊ ● a0 ✆ ✄ ■ ✄ ➆ ✞ ✄ ❳ ❊ ● a0 ❃ ✄ ■ ✄ ➆ ✞ ✞ ✞

❲ ❳ ✆ ✈ a0 ➇ ✄ ❳ ❊ ● a0 ✆ ✄ ➆ ✞ ✄ ❳ ❊ ● a0 ❃ ✄ ■ ✄ ➆ ✞ ✞

❲ ❳ ✆ ✈ a0 ❳ ❊ ● a0 ✆ ✄ ➆ ✞ ✄ ❳ ❊ ● a0 ❃ ✄ ■ ✄ ➆ ✞ ✞ ✰

It can be checked from ❀ that a116 ● ■ a0 ✹ ▼ ❧ a0 ✤ ❡ ✄ ✕ ✞ a115 ✞ ❷ a116 ● ■ a0 ✹ ✞ , since for instance ❳ ❊ ● a0 ✆ ✄ ➆ ✞ ❷ ➇ .

4 Propositional logic encoding of partially-constrained weighted formulas

In standard possibilistic logic (recalled in Section 2), the weights ✆ ❪ 's are assumed to be known. In this section, these weights are only partially known. Propositions are then associated with symbolic weights or variables. These symbolic weights are related by a set of constraints. The following subsections describe in detail the representation of uncertain beliefs and constraints, in a propositional logic setting.

4.1 Encoding constraints

This subsection presents the encoding of constraints on the set of symbolic weights using propositional logic. In the following we associate to each symbolic weight ✆ of the knowledge base a propositional symbol denoted by the corresponding capital letter ✛ . We denote by ✿ the set of propositional symbols associated with ➃ (with ✿ ➣ ✾ ❲ ② ). Let ❉ ↔ be the propositional language built from ✿ using the propositional connectors ❚ ✄ ✙ ✄ ✤ .

One possible way to check if ✆ ☞ ❃ follows from ❀ is to use propositional logic, and encode ❀ as a set of clauses.

Given ❀ , its encoding in propositional logic is immediate. Namely, a constraint ✆ ☞ ❃ is translated into ✤ ✛ ✙ ❇ in the agreement with the fact that ✆ and ❃ are lower bounds (of a necessity measure) and thus ✆ refers to the set of numbers ➄ ✒ ✄ ✕ ✗ and ➄ ✆ ✄ ✕ ✗ ↕ ➄ ❃ ✄ ✕ ✗ holds iff ✆ ☞ ❃ . The translationof ✆ ☞ ❃ into ✤ ✛ ✙ ❇ can be read as as �if the situation is at least very abnormal ( ✛ ), it is at least abnormal ( ❇ )� (indeed, the greater ✆ , the more certain ✁ in a0 ✁ ✄ ✆ ✞ , and the more exceptional a situation where ✁ is false).

To refer to the maximum (max), we use the conjunction operator ( ❚ ), namelymax(a,b) will be encoded by ✛ ❚ ❇ . Indeed, the tautology ✤ a0 ✛ ❚ ❇ ✞ ✙ ✛ re�ects ❳ ✆ ✈ a0 ✆ ✄ ❃ ✞ ☞ ✆ . To refer to the minimum (min), we use the disjunctive operator ( ✙ ), namely min(a,b) will be encoded using ✛ ✙ ❇ . A clause ✤ ✛ ✮ ✙ ✰ ✰ ✰ ✙ ✤ ✛ ➋ ✙ ❇ ✮ ✙ ✰ ✰ ✰ ✙ ❇ ✶ will hence encodes a constraint ❳ ✆ ✈ a0 ✆ ✮ ✄ ✰ ✰ ✰ ✄ ✆ ➋ ✞ ☞ ❳ ❊ ● a0 ❃ ✮ ✄ ✰ ✰ ✰ ✄ ❃ ✶ ✞ . More formally,

De�nition 2 Let ❀ be a set of constraints. The propositional logic base associated with ❀ , denoted by ✺ ❁ , is de�ned by : ✺ ❁ ❲ ❧ ✤ ✛ ✮ ✙ ✰ ✰ ✰ ✙ ✤ ✛ ➋ ✙ ❇ ✮ ✙ ✰ ✰ ✰ ✙ ❇ ✶ ♣ ❳ ✆ ✈ a0 ✆ ✮ ✄ ✰ ✰ ✰ ✄ ✆ ➋ ✞ ☞ ❳ ❊ ● a0 ❃ ✮ ✄ ✰ ✰ ✰ ✄ ❃ ✶ ✞ ✎ ❀ a115 .

Example 4 A total order ❀ ❲ ❧ ✆ ✮ ☞ ✆ ➙ ✄ ✆ ➙ ☞ ✆ ➛ ✄ ✰ ✰ ✰ ✄ ✆ ✶ ➜ ✮ ☞ ✆ ✶ a115 is encoded by : ✺ ❁ ❲ ❧ ✤ ✛ ❪ ✙ ✛ ❪ ➝ ✮ ♣ ❊ ❲ ✕ ✄ ✰ ✰ ✄ ● ➞ ✕ a115 .

The following proposition shows that inequalities induced from ❀ can be obtained using our propositional encoding:

Proposition 2 Let ✆ , and ❃ be two symbolic weights. Then : ✆ ☞ ❃ follows from ❀ iff ✺ ❁ ❾ ❲ ✤ ✛ ✙ ❇ .

This proposition can be easily generalized for any inequality of the form ✆ ☞ ❃ where ✆ and ❃ are max/min expressions, using remarks of Section 3.2. Namely any derivation of inequalities between max/min expressions, can be rede�ned in terms of derivations between symbolic weights. For instance, it can be checked that ✆ ❷ ❃ follows from ❀ iff ✺ ❁ ❾ ❲ ✤ ✛ ✙ ❇ holds but ✺ ❁ ❾ ❲ ✤ ❇ ✙ ✛ does not hold.

We call S-positive formulas the formulas built from ✿ by only using the conjunction and disjunction operator. For instance, ✛ ✙ ❇ is an S-positive formula, while ✤ ✛ ✙ ❇ is not an S-positive formula.

4.2 Encoding uncertain information

As suggested in the introduction, the idea is to manipulate symbolic weights as formulas. Thus, a possibilistic formula a0 ✁ ✄ ✆ ✞ is associated with the classical clause ✁ ✙ ✛ where ✛ means something as �the situation is abnormal�. Interestingly enough, this view agrees with the qualitative representation of uncertainty in terms of lower bounds of a necessity measure used in possibilistic logic. The following de�nition gives the propositional logic encoding of possibilistic knowledge base:

De�nition 3 Let ✹ ❲ ❧ a0 ✁ ❪ ✄ ✆ ❪ ✞ a115 be a possibilistic knowledge base. Let ✛ ❪ be a S-positive formula associated with ✆ ❪ (by replacing in ✆ ❪ the minimum with the disjunction, and the maximum by the conjunction). Then the propositional base associated with ✹ , denoted by ✺ ✻ , is de�ned by : ✺ ✻ ❲ ❧ ✁ ❪ ✙ ✛ ❪ ♣ a0 ✁ ❪ ✄ ✆ ❪ ✞ ✎ ✹ and ✛ ❪ is the S-positive formula associated with ✆ ❪ a115

4.3 Characterizing plausible inferences

Until now, we have shown how to encode in propositional logic uncertain beliefs ✹ and the constraints ❀ on weights associated with these beliefs. This section de�nes the notion of plausible conclusions that can be drawn from a0 ✹ ✄ ❀ ✞ . The set ✺ ❁ is used at two stages: �rst it is used for simplifying the expression of the inconsistency degree, and then it is used to check, in the refutation, if the inconsistency degree of the augmented base increases.

De�nition 4 An S-prime formula of ✺ ✻ ▼ ✺ ❁ is an Spositive formula, denoted by ❉ ❊ ● ■ a0 ✺ ✻ ✞ , such that i) ✺ ✻ ▼ ✺ ❁ ❾ ❲ ❉ ❊ ● ■ a0 ✺ ✻ ✞ , and ii) there is no ➡ (not equivalent to ❉ ❊ ● ■ a0 ✺ ✻ ✞ ) such that ✺ ✻ ▼ ✺ ❁ ❾ ❲ ➡ and ➡ ❾ ❲ ❉ ❊ ● ■ a0 ✺ ✻ ✞ .

Up to logical equivalence, ❉ ❊ ● ■ a0 ✺ ✻ ✞ is unique.

This de�nition allows to have a sound and complete inference relation with respect to the semantics given above. Indeed, the following proposition shows that ❉ ❊ ● ■ a0 ✺ ✻ ✞ is the logical counterpart of a116 ● ■ a0 ✹ ✞ .

Proposition 3 Let ✺ ✻ and ✺ ❁ . Let ➢ a0 ✹ ✞ be a propositional formula obtained from a116 ● ■ a0 ✹ ✞ by replacing maximum by a conjunction, minimum by a disjunction, and the symbolic weights by their associated literals. Then ➢ a0 ✹ ✞ is logically equivalent to ❉ ❊ ● ■ a0 ✺ ✻ ✞ given in De�nition 4.

5 Computing plausible inference using DNF formats

We propose a characterisation of plausible inference using the idea of forgetting variables (see for instance [Lang et al., 2003; Darwiche and Marquis, 2004] for more details). Forgetting a variable ✁ from ✺ comes down to remove any reference of ✁ in ✺ .

De�nition 5 Let ✁ be a propositional symbol of ✾ . Then : ➤ ➥ ❡ ➦ ➇ ➧ ✾ ✆ ❡ ❊ ✆ ❃ ➨ ➇ a0 ✺ ✄ ✁ ✞ ❲ ✺ ➩ ➫ ➭ ✙ ✺ ➩ ➫ ➯

✺ ➩ ➫ ➭ (resp. ✺ ➩ ➫ ➯ ) is the knowledge base obtained from ✺ by replacing ✁ by false (resp. true). To forget a set of variables, we forget variable by variable, namely if ✛ denotes a set of variables, then: ➤ ➥ ❡ ➦ ➇ ➧ ✾ ✆ ❡ ❊ ✆ ❃ ➨ ➇ a0 ✺ ✄ ✛ ✞ ❲ ➤ ➥ ❡ ➦ ➇ ➧ ✾ ✆ ❡ ❊ ✆ ❃ ➨ ➇ a0 ➤ ➥ ❡ ➦ ➇ ➧ ✾ ✆ ❡ ❊ ✆ ❃ ➨ ➇ a0 ✺ ✄ ✁ ✞ ✄ ✛ ➞ ❧ ✁ a115 ✞ .

It is also possible to only forget literals (atoms or negated atoms):

De�nition 6 Let ➨ be a literal. Then : ➤ ➥ ❡ ➦ ➇ ➧ ❉ ❊ ➧ ➇ ❡ ✆ ➨ a0 ✺ ✄ ➨ ✞ ❲ ✺ ➲ ➫ ➯ ✙ a0 ✤ ➨ ❚ ✺ ✞

Some properties of ForgetVariable ([Darwiche and Marquis, 2004], [Lang et al., 2003]), viewing a base as a conjunct of its formulas:

1. ➤ ➥ ❡ ➦ ➇ ➧ ✾ ✆ ❡ ❊ ✆ ❃ ➨ ➇ a0 ➳ ✙ ➡ ✄ ✛ ✞ ❲ ➤ ➥ ❡ ➦ ➇ ➧ ➵ ✆ ❡ ❊ ✆ ❃ ➨ ➇ a0 ➳ ✄ ✛ ✞ ✙ ➤ ➥ ➦ ➇ ➧ ➵ ✆ ❡ ❊ ✆ ❃ ➨ ➇ a0 ➡ ✄ ✛ ✞ ✰
2. if ➡ does not contain any varaible of A, then ➤ ➥ ❡ ➦ ➇ ➧ ✾ ✆ ❡ ❊ ✆ ❃ ➨ ➇ a0 ➳ ❚ ➡ ✄ ✛ ✞ ❲ ➡ ❚ ➤ ➥ ❡ ➦ ➇ ➧ ✾ ✆ ❡ ❊ ✆ ❃ ➨ ➇ a0 ➳ ✄ ✛ ✞
3. if ➳ is a consistent conjunction of literals, then ➤ ➥ ❡ ➦ ➇ ➧ ✾ ✆ ❡ ❊ ✆ ❃ ➨ ➇ a0 ➳ ✄ ✛ ✞ consists in removing the variables in ✛ from ➳ .

ForgetLiteral satis�es (1) and (2) which is enough for the purpose of the paper. The following shows that getting ❉ ❊ ● ■ a0 ✺ ✻ ✞ is equivalent to �rst forget all formulas of the language, and then all negative literals of ✿

Proposition 4 Let NegS be the set of negative literals in ✺ ✻ ▼ ✺ ❁ . Let ➤ ❲ ➤ ➥ ❡ ➦ ➇ ➧ ✾ ✆ ❡ ❊ ✆ ❃ ➨ ➇ a0 ✺ ✻ ✄ ✾ ✞ . Then ❉ ❊ ● ■ a0 ✺ ✻ ✞ is equivalent to ➤ ➥ ❡ ➦ ➇ ➧ ❉ ❊ ➧ ➇ ❡ ✆ ➨ a0 ✺ ❁ ❚ ➤ ✄ ✠ ➇ ➦ ✿ ✞ ✰

This result is very important since it provides an ef�cient way to draw plausible conclusion from ✹ and ❀ . Indeed, forgetting a variable (resp. literal) can be achieved in a polynomial time if knowledge bases are in some formats like DNF or d-DNNF [Darwiche and Marquis, 2004]. The procedure for checking if a proposition ✁ can be derived from ✹ and ❀ can be described as follows:

• Step 1: transform ✹ and ❀ into ✺ ✻ and ✺ ❁
• Step 2: Put ✺ ✻ into a DNF (or d-DNNF) form
• Step 3.1: Forget Variables of ✾ from ✺ ✻
• Step 3.2: Forget Negated atoms of ✿ from ✺ ❁ ▼ ✺ ✻ . This gives ❉ ❊ ● ■ a0 ✺ ✻ ✞ .
• Step 4: Put ✺ ✻ ▼ ❧ ✤ ✁ a115 into a DNF (or d-DNNF) form
• Step 5.1: Forget Variables of ✾ from ✺ ✻ ▼ ❧ ✤ ✁ a115
• Step5.2: ForgetNegated atoms of ✿ from ✺ ❁ ▼ ✺ ✻ ▼ ❧ ✤ ✁ a115 . This gives ❉ ❊ ● ■ a0 ✺ ✻ ➻ ➼ ➽ ➩ ➾ ✞ .
• Step 6: Use proposition 2 and results of Section 4.1 to check if p is a plausible consequence of ✹ and ❀ or not.

Forgetting a variable in a DNF amounts to forget it in each term, and forgetting it in a term amounts just to suppress the term. This clearly shows that this is polyomial in time. A similar procedure applies as well to d-DNNF format. This format known as Deterministic, Decomposable Negation Normal Form has been proposed recently [Darwiche, 2004] is a compact format, and has allowed the computation of generally intractable logical queries in time polynomial in the form size. An algorithm has been presented in [Darwiche, 2004] for compiling Conjunctive Normal Forms into d-DNNF directly. Our approach can clearly take advantage of this format as well.

Let us illustrate the above procedure with the following example:

Example 5 Let us consider again Example 3, where we have: ✹ ❲ ❧ a0 ✁ ✄ ❳ ✆ ✈ a0 ✆ ✄ ❃ ✞ ✞ ✄ a0 ✤ ✁ ✙ ❡ ✄ ❳ ❊ ● a0 ■ ✄ ➆ ✞ ✞ ✄ a0 ✤ ❡ ✄ ➇ ✞ ✞ a115 , and ❀ ❲ ❧ ✆ ☞ ➇ ✄ ■ ☞ ✆ ✄ ➆ ☞ ➇ a115 ✰ Let ✛ ✄ ❇ ✄ ❀ ✄ ➘ ✄ ➴ be the propositional symbols associated with symbolic weights ✆ ✄ ❃ ✄ ■ ✄ ➆ ✄ ➇ .

Step 1 : Encoding ✹ and ❀

The encoding of ❀ in propositional logic gives :

✺ ❁ ❲ ❧ ✤ ✛ ✙ ➴ ✄ ✤ ❀ ✙ ✛ ✄ ✤ ➘ ✙ ➴ a115

✺ ✻ ❲ ❧ ✁ ✙ a0 ✛ ❚ ❇ ✞ ✄ ✤ ✁ ✙ ❡ ✙ ❀ ✙ ➘ ✄ ✤ ❡ ✙ ➴ a115 .

The encoding of ✹ gives :

Step 2 : Putting ✺ ✻ into a DNF form

We �rst put ✺ ✻ in a DNF form, which gives :

a0 ✁ ❚ ❀ ❚ ✤ ❡ ✞ ✙ a0 ✁ ❚ ➘ ❚ ✤ ❡ ✞ ✙ a0 ✛ ❚ ❇ ❚ ✤ ✁ ❚ ✤ ❡ ✞ ✙ a0 ✛ ❚ ❇ ❚ ❀ ❚ ✤ ❡ ✞ ✙ a0 ✛ ❚ ❇ ❚ ➘ ❚ ✤ ❡ ✞ ✙ a0 ✁ ❚ ❡ ❚ ➴ ✞ ✙ a0 ✁ ❚ ❀ ❚ ➴ ✞ ✙ a0 ✁ ❚ ➘ ❚ ➴ ✞ ✙ a0 ✛ ❚ ❇ ❚ ✤ ✁ ❚ ➴ ✞ ✙ a0 ✛ ❚ ❇ ❚ ❡ ❚ ➴ ✞ ✙ a0 ✛ ❚ ❇ ❚ ❀ ❚ ➴ ✞ ✙ a0 ✛ ❚ ❇ ❚ ➘ ❚ ➴ ✞

Now we forget the two variables p and r of V. By using properties (1)-(3); and after simpli�cation, we get:

Step 3.1: Forgetting Variables of V

➤ ➥ ❡ ➦ ➇ ➧ ✾ ✆ ❡ ❊ ✆ ❃ ➨ ➇ a0 ✺ ✻ ✄ ✾ ✞ ❫ ❀ ✙ ➘ ✙ ➴ ✙ a0 ✛ ❚ ❇ ✞ Note that this is exactly the logical counterpart of a116 ● ■ a0 ✹ ✞ given by (1) in Example 3 (after remplacing, ✙ by minimum operation, ❚ by maximum operation).

Step 3.2: Forgetting Negated atoms of ✿

Now, let us forget literals from ✺ ❁ ❚ ➤ ➥ ❡ ➦ ➇ ➧ ✾ ✆ ❡ ❊ ✆ ❃ ➨ ➇ a0 ✺ ✻ ✄ ✾ ✞ . We get:

Again this is exactly the logical counterpart of the expression (2) given in Example 3.

We are now interested to check if ❡ is a plausible consequence of ✹ and ❀ .

The DNF form associated with ✹ ▼ ❧ ✤ ❡ a115 is:

Step 4 : Putting in DNF form ✹ ▼ ❧ ✤ ❡ a115

a0 ✁ ❚ ❀ ❚ ✤ ❡ ✞ ✙ a0 ✁ ❚ ➘ ❚ ✤ ❡ ✞ ✙ a0 ✛ ❚ ❇ ❚ ✤ ✁ ❚ ✤ ❡ ✞ ✙ a0 ✛ ❚ ❇ ❚ ❀ ❚ ✤ ❡ ✞ ✙ a0 ✛ ❚ ❇ ❚ ➘ ❚ ✤ ❡ ✞ ✙ a0 ✁ ❚ ❀ ❚ ➴ ❚ ✤ ❡ ✞ ✙ a0 ✁ ❚ ➘ ❚ ➴ ❚ ✤ ❡ ✞ ✙ a0 ✛ ❚ ❇ ❚ ✤ ✁ ❚ ➴ ❚ ✤ ❡ ✞ ✙ a0 ✛ ❚ ❇ ❚ ❀ ❚ ➴ ❚ ✤ ❡ ✞ ✙ a0 ✛ ❚ ❇ ❚ ➘ ❚ ➴ ❚ ✤ ❡ ✞

Step 5.1. : Forgetting variables of V in ✹ ▼ ❧ ✤ ❡ a115

➤ ➥ ❡ ➦ ➇ ➧ ✾ ✆ ❡ ❊ ✆ ❃ ➨ ➇ a0 ✹ ▼ ❧ ✤ ❡ a115 ✄ ✾ ✞ ❲ a0 ❀ ❚ ✤ ✛ ✞ ✙ a0 ➘ ❚ ✤ ✛ ✞ ✙ a0 ❀ ❚ ➴ ✞ ✙ a0 ➘ ❚ ➴ ✞ ✙ a0 ✛ ❚ ❇ ❚ ➴ ✞

Forgetting negative literals of ✿ gives :

Step 5.2 : Forgetting Negative atoms

❉ ❊ ● ■ a0 ✺ ✻ ▼ ❧ ✤ ❡ a115 ✞ ❲ a0 ✛ ❚ ❇ ❚ ➴ ✞ ✙ a0 ❀ ❚ ➴ ❚ ✛ ✞ ✙ a0 ➘ ❚ ➴ ✞

Using results of Section 4.1, it can be checked that ❡ is a plausible consequence of ✹ and ❀ , as we have already seen in Example 3 that .

Step 6: Checking plausible inference

We �nish this section by brie�y discussing the case where weights associated with constraints are totally ordered. Let ✹ ❲ ❧ a0 ✁ ❪ ✄ ✆ ❪ ✞ ♣ ❊ ❲ ✕ ✄ ✰ ✰ ✰ ✄ ● a115 . We assume without loss of generality that ✆ ✮ ☞ ✆ ➙ ☞ ✰ ✰ ✰ ☞ ✆ ✶ . The knowledge bases ✺ ✻ and ✺ ❁ are :

✺ ✻ ❲ ❧ ✁ ❪ ✙ ✛ ❪ ♣ a0 ✁ ❪ ✄ ✆ ❪ ✞ ✎ ✹ a115 , and

✺ ❁ ❲ ❧ ✤ ✛ ❪ ✙ ✛ ❪ ➝ ✮ ♣ ❊ ❲ ✕ ✄ ✰ ✰ ✰ ✄ ● ➞ ✕ a115 .

Let ➘ be the result of putting ✺ ✻ ▼ ✺ ❁ into a DNF form, and ❉ ❊ ● ■ a0 ✺ ✻ ✄ ✺ ❁ ✞ be the result of forgetting variables of ✾ and negative atoms from ➃ . Then for totally orderedweights, it is possible to compute a compiled base (as in standard possibilistic logic), denoted by ❀ ➥ ● ➈ a0 ✺ ✻ ▼ ✺ ❁ ✞ , as follows:

• ✸ If the inconsistency degree of ✹ is ✆ ➁ (namely a116 ● ■ a0 ✹ ✞ ❲ ✆ ➁ ), then ❀ ➥ ● ➈ a0 ✺ ✻ ▼ ✺ ❁ ✞ is logically equivalent to ➤ ➥ ❡ ➦ ➇ ➧ ✾ ✆ ❡ ❊ ✆ ❃ ➨ ➇ a0 ✤ ✛ ✮ ❚ ✰ ✰ ✰ ❚ ✤ ✛ ➁ ➜ ✮ ❚ ➘ ✄ ➃ ✞
• ✸ If ✹ is consistent, then ❉ ❊ ● ■ a0 ✺ ✻ ✄ ✺ ❁ ✞ ❀ ➥ ● ➈ a0 ✺ ✻ ▼ ✺ ❁ ✞ is logically equivalent to ➤ ➥ ❡ ➦ ➇ ➧ ✾ ✆ ❡ ❊ ✆ ❃ ➨ ➇ a0 ✤ ✛ ✮ ❚ ✰ ✰ ✰ ❚ ✤ ✛ ✶ ❚ ➘ ✄ ➃ ✞ .

Note that ❀ ➥ ● ➈ a0 ✺ ✻ ▼ ✺ ❁ ✞ is under DNF form, and we have: ✁ is a possibilistic consequence of ✹ iff ❀ ➥ ● ➈ a0 ✺ ✻ ▼ ✺ ❁ ✞ ✐ ✁ ✰

Example 6 Let ✹ ❲ ❧ a0 ✁ ✄ ✒ ✰ ➱ ✞ ✄ a0 ❯ ✄ ✒ ✰ ✃ ✞ ✄ a0 ✤ ✁ ✙ ✤ ❯ ✄ ✒ ✰ ❐ ✞ ✄

a0 ✤ ✁ ✄ ✒ ✰ ❒ ✞ a115 . Let ✛ ✄ ❇ ✄ ❀ ✄ ➴ be propositional symbols associated respectively with the weights of the knowledge base (namely ✒ ✰ ➱ ✄ ✒ ✰ ✃ ✄ ✒ ✰ ❐ ✄ ✒ ✰ ❒ ). The two propositional bases are: ✺ ✻ ❲ ❧ ✛ ✙ ✁ ✄ ❇ ✙ ❯ ✄ ❀ ✙ ✤ ✁ ✙ ✤ ❯ ✄ ➴ ✙ ✤ ✁ a115 , and ✺ ❁ ❲ ❧ ✤ ✛ ✙ ❇ ✄ ✤ ❇ ✙ ❀ ✄ ✤ ❀ ✙ ➴ a115 ✰

The DNF associated with ✺ ✻ ▼ ✺ ❁ is:

D= a0 ✁ ❚ ❯ ❚ ❀ ❚ ➴ ❚ ✤ ✛ ✞ ✙ a0 ✁ ❚ ❇ ❚ ❀ ❚ ➴ ✞ ✙ a0 ✛ ❚ ❇ ❚ ❀ ❚ ➴ ✞ Let us forget variables of ✾ , and negative atoms from ➃ , we get :

❀ ❚ ➴ ✙ ❇ ❚ ❀ ❚ ➴ ✙ ✛ ❚ ❇ ❚ ❀ ❚ ➴

which is equivalent to : ❀ ❚ ➴ Now let us add ✤ ✛ ❚ ✤ ❇ to ➘ we get:

Now forgetting variables of S gives : ❀ ➥ ● ➈ a0 ✺ ✻ ▼ ✺ ❁ ✞ ❲ ✁ ❚ ❯ , from which it can be checked that ➡ is a possibilistic consequence of ✹ iff ✁ ❚ ❯ ✐ ➡ ✰

D = ✁ ❚ ❯ ❚ ❀ ❚ ➴ ❚ ✤ ✛ ❚ ✤ ❇

6 Related works

Using abnormality predicates in a logical setting is explicitly underlying several non-monotonic formalisms such as circumscription [McCarthy, 1980]. The idea is then to minimize abnormality and circumscribe it to a minimal number of individuals. The use of abnormality propositional literals is different here. Namely, no minimization process takes place (we are not dealing with exception-tolerant reasoning), and the symbolic weight attached to a formula ✁ can itself be a compound formula re�ecting the complex conditions under which it holds that ✁ is true. What is proposed is more in the spirit of multiple source information, where the con�dence of the information depends on the source, or on the topic, for instance.

Our representation framework for qualitative uncertainty does not require the knowledge of a complete pre-ordering of the different certainty levels attached to formulas. The uncertainty pervading a proposition may be either viewed as a precise notion, or as imprecisely stated by means of constraints that are opened to revision if new information becomes available. In both kinds of framework, one may only have a partial knowledge of the uncertainty. In the �rst case, uncertainty is handled under the form of absolute statements such as ➦ a0 ✁ ✞ ❲ ✆ (where ➦ is an uncertaintymeasure and ✁ is a proposition), or under the formof relative statements such as ✁ ❷ ❯ (where ❷ is a partial ordering encoding a plausibility relation expressinghere that the plausibility of ✁ is strictly greater than the one of ❯ , as discussed in [Halpern, 1997]. Then, adding the piece of information that ✁ entails ❯ leads to inconsistency since if ✁ entails ❯ classically, it is expected that the plausibility of ❯ is at least equal to the one of ✁ . However, note that in possibilistic logic ✠ a0 ✁ ✞ ☞ ✆ and ✠ a0 ❯ ✞ ☞ ❃ together with the inequality ✆ ☞ ❃ is a weaker statement that ✠ a0 ✁ ✞ ☞ ✠ a0 ❯ ✞ . Benferhat et al. [Benferhat et al., 2004] propose a semantic approach for reasoning with partially ordered information in a possibilistic logic setting. The logical handling of formulas with unknown certainty weights together with the constraints relating these weights presented here turns to be much simpler and computationally more tractable.

7 Conclusion

The problem of reasoning with pieces of information having different con�dence levels is raised by the handling of multiple source information. In case of partial information on the relative values of these levels, the problem becomes more dif�cult. An elegant method is proposed here for solving it, by rewriting the uncertain pieces of information in a two-sorted logic, and encoding the available information on the relative values of the certainty levels in a logical way. Putting the two bases in DNF format and using forgetting variables techniques enable us to compute the symbolic counterpart of the inconsistency level of a knowledge base in a linear way, and then to draw plausible inferences. Moreover, the representation technique that is used also provides a way for compiling a standard possibilistic knowledge base, a result analogous to the one obtained by Darwiche and Marquis [Darwiche and Marquis, 2004] for another type of weighted logic, the penalty logic, using d-DNNF format. This paper also brie�y discusses the case of totally ordered weights, from which the number of extra variables (used to encode weights) and the number of extra binary clauses (used to encode the total ordering) necessary for the inference process is equal to the number of different weights used in base. The full development of a compilation of standard possibilistic knowledge bases in propositional logic is left for further research. Besides, another potential expected bene�t of the approach, is a contribution to the solution of the drowning problem in possibilistic logic. Indeed, it can be checked that the symbolic inconsistency level of ✺ ❲ ❧ ✁ ✙ ✛ ✄ ✤ ✁ ✙ ❇ ✄ ❯ ✙ ❀ a115 , is a116 ● ■ a0 ✺ ✞ ❲ ✛ ✙ ❇ , where C does not appear, which should provide a way for �nding out the �free� formulas in K that are not involved in any inconsistency con�ict.

Acknowledgments: The authors would like to thank Pierre Marquis for his useful discussions.