# The Possibilistic Horn Non-Clausal Knowledge Bases

Gonzalo E. Imaz
Artificial Intelligence Research Institute (IIIA) - CSIC, Barcelona, Spain
email<EMAIL_ADDRESS>

###### Abstract

Posibilistic logic is the most extended approach to handle uncertain and
partially inconsistent information. Regarding normal forms, advances in
possibilistic reasoning are mostly focused on clausal form. Yet, the encoding
of real-world problems usually results in a non-clausal (NC) formula and NC-
to-clausal translators produce severe drawbacks that heavily limit the
practical performance of clausal reasoning. Thus, by computing formulas in its
original NC form, we propose several contributions showing that notable
advances are also possible in possibilistic non-clausal reasoning.

Firstly, we define the class of Possibilistic Horn Non-Clausal Knowledge
Bases, or $\mathcal{\overline{H}}_{\Sigma}$, which subsumes the classes:
possibilistic Horn and propositional Horn-NC.
$\mathcal{\overline{H}}_{\Sigma}$ is shown to be a kind of NC analogous of the
standard Horn class.

Secondly, we define Possibilistic Non-Clausal Unit-Resolution, or
$\mathcal{UR}_{\Sigma}$, and prove that $\mathcal{UR}_{\Sigma}$ correctly
computes the inconsistency degree of $\mathcal{\overline{H}}_{\Sigma}$
members. $\mathcal{UR}_{\Sigma}$ had not been proposed before and is
formulated in a clausal-like manner, which eases its understanding, formal
proofs and future extension towards non-clausal resolution.

Thirdly, we prove that computing the inconsistency degree of
$\mathcal{\overline{H}}_{\Sigma}$ members takes polynomial time. Although
there already exist tractable classes in possibilistic logic, all of them are
clausal, and thus, $\mathcal{\overline{H}}_{\Sigma}$ turns out to be the first
characterized polynomial non-clausal class within possibilistic reasoning.

We discuss that our approach serves as a starting point to developing
uncertain non-clausal reasoning on the basis of both methodologies: DPLL and
resolution.

Keywords: Possibilistic Logic; Horn; Non-Clausal; Inconsistency; Tractability;
Resolution; DPLL; Satisfiability Testing; Logic Programming.

##  1 Introduction

Possibilistic logic is the most popular approach to represent and reason with
uncertain and partially inconsistent knowledge. Regarding normal forms, the
encoding of real-world problems does usually not result in a clausal formula
and although a possibility non-clausal formula is theoretically equivalent to
some possibilistic clausal formula [26, 22], approaches needing clausal form
transformations are practically infeasible or have experimentally shown to be
highly inefficient as discussed below.

Two kinds of clausal form transformation are known: (1) one is based on the
repetitive application of the distributive laws to the input non-clausal
formula until a logically equivalent clausal formula is obtained; and (2) the
other transformation, Tsetin-transformation [59], is based on recursively
substituting sub-formulas in the input non-clausal formula by fresh literals
until obtaining an equi-satisfiable, but not equivalent, clausal formula.

The first transformation blows up exponentially the formula size, and since
real-world problems have a large number of variables and connectives, the huge
dimension of the resulting clausal formulas prevents even highly-efficient
state-of-the-art solvers from attaining solutions in a reasonable time.

The second kind of transformation also involves a number of drawbacks. The
Tseitin-transformation usually produces an increase of formula size and number
of variables, and also a loss of information about the formula’s original
structure. Besides in most cases, the normal form is not unique. Deciding how
to perform the transformation enormously influences the solving process and it
is usually impossible to predict which strategy is going to be the best, as
this depends on the concrete solver used and on the kind of problem which
should be solved. Further, Tseitin-transformation keeps the satisfiability
test but losses the logical equivalence, which rules out its usage in many
real-world problems.

We abandon the assumption that the input formula should be transformed to
clausal form and directly process it in its original structure. Since real-
world problems rarely occur in clausal form, we allow an arbitrary nesting of
conjunctions and disjunctions and only limit the scope of the negation
connective. The non-clausal form considered here is popularly called negation
normal form (NNF), and can be obtained deterministically and causing only a
negligible increase of the formula size.

Developing methods for NC reasoning is an actual concern in the principlal
fields of classical logic, namely satisfiability solving [54, 43], logic
programming [17, 14], theorem proving [31, 53] and quantified boolean formulas
[30, 13], and in many other fields (see [40] and the references thereof). And
within non-classical logics, NC formulas with different functionalities have
been studied in a profusion of languages: signed many-valued logic [47, 8,
58], Łukasiewicz logic [42], Levesque’s three-valued logic [15], Belnap’s
four-valued logic [15], M3 logic [1], fuzzy logic [35], fuzzy description
logic [34], intuitionistic logic [55], modal logic [55], lattice-valued logic
[60] and regular many-valued logic [39]. We highlight the proposal in [49, 50]
as is the only existing approach, to our knowledge, to deal with possibilistic
non-clausal formulas, concretely within the answer set programming field.

On the other side, the Horn clausal formulas are pivotal elements of our
proposed possibilistic reasoning approach towards combining non-clausal
expressiveness with high efficiency. Horn formulas are recognized as central
for deductive databases, declarative programming, and more generally, for
rule-based systems. In fact, Horn formulas have received a great deal of
attention since 1943 [45, 38] and, at present, there is a broad span of areas
within artificial intelligence relying on them, and their scope covers a
fairly large spectrum of realms spread across many logics and a variety of
reasoning settings.

Regarding possibilistic Horn formulas, computing their inconsistency degree is
a tracta-ble problem [41] and even almost-lineal [3]. Related to this standard
Horn class but going beyond clausal form, we present a novel possibilistic
class, denoted $\mathcal{\overline{H}}_{\Sigma}$, that is in NC form and that
we call Horn Non-Clausal (Horn-NC). We show that
$\mathcal{\overline{H}}_{\Sigma}$ is a sort of non-clausal analogous of the
possibilistic Horn class. Besides the latter,
$\mathcal{\overline{H}}_{\Sigma}$ also subsumes the class of propositional
Horn-NC formulas recently presented [40].

From a computational view, we prove that computing the inconsistency degree of
$\mathcal{\overline{H}}_{\Sigma}$ members is a tractable problem. This result
signifies that polynomiallity in our context is preserved when upgrading both
from clausal to non-clausal form and from propositional to possibilistic
logic. Polynomiallity is preserved when upgrading from clausal to non-clausal
form because both classes possibilistic Horn [41] and possibilistic Horn-NC
are tractable. Similarly, polynomiallity is preserved when upgrading from
propositional to possibilistic logic because both classes propositional Horn-
NC [40] and possibilistic Horn-NC are tractable.

In summary, our contributions are: introducing the hybrid class of
Possibilistic Horn Non-Clausal Knowledge Bases, or
$\mathcal{\overline{H}}_{\Sigma}$, and then, proving that computing their
inconsistency degree is a polynomial problem. Our contributions are outlined
next.

Firstly, the syntactical Horn-NC restriction is determined by lifting the Horn
clausal restriction “a formula is Horn if all its clauses have any number of
negative literals and at most one positive literal”, to the non-clausal level
in the following manner: “a propositional NC formula is Horn-NC if all its
disjunctions have any number of negative disjuncts and at most one non-
negative disjunct”. By extending such definition to possibilistic logic, we
establish straightforwardly that: a possibilistic NC knowledge base is Horn-NC
only if all its propositional formulas are Horn-NC. Accordingly,
$\mathcal{\overline{H}}_{\Sigma}$ is defined as the class of Possibilistic
Horn-NC Knowledge Bases. Note that $\mathcal{\overline{H}}_{\Sigma}$ naturally
subsumes the standard possibilistic Horn clausal class.

The set relations that the new class $\mathcal{\overline{H}}_{\Sigma}$ bears
to the standard possibilistic classes Horn ($\mathcal{H}_{\Sigma}$), Non-
Clausal ($\mathcal{NC}_{\Sigma}$) and Clausal ($\mathcal{C}_{\Sigma}$) are
depicted in Fig. 1. Specifically, we show the next relationships of
$\mathcal{\overline{H}}_{\Sigma}$ with $\mathcal{H}_{\Sigma}$ and
$\mathcal{NC}_{\Sigma}$: (1) $\mathcal{\overline{H}}_{\Sigma}$ and
$\mathcal{{H}}_{\Sigma}$ are related in that $\mathcal{\overline{H}}_{\Sigma}$
subsumes syntactically $\mathcal{{H}}_{\Sigma}$ but both classes are
semantically equivalent; and (2) $\mathcal{\overline{H}}_{\Sigma}$ and
$\mathcal{NC}_{\Sigma}$ are related in that $\mathcal{\overline{H}}_{\Sigma}$
contains all NC bases whose clausal form is Horn. Thus, in view of (1) and (2)
relations, $\mathcal{\overline{H}}_{\Sigma}$ is a sort of NC analogous of
$\mathcal{{H}}_{\Sigma}$.

$\
\mathcal{NC}_{\Sigma}$$\mathcal{C}_{\Sigma}$$\mathcal{\overline{H}}_{\Sigma}$$\mathcal{{H}}_{\Sigma}$

Fig. 1. The Horn, clausal, Horn-NC and NC classes.

Secondly, we establish the inferential calculus Posibilistic Non-Clausal Unit-
Resolution, or $\mathcal{UR}_{\Sigma}$, and then prove that
$\mathcal{UR}_{\Sigma}$ correctly computes the inconsistency degree of the
bases in the class $\mathcal{\overline{H}}_{\Sigma}$. NC unit-resolution for
propositional logic has been recently presented [40] and
$\mathcal{UR}_{\Sigma}$ is its generalization to possibilistic logic.
$\mathcal{UR}_{\Sigma}$ is formulated in a clausal-like fashion, which
contrasts with the functional-like fashion of the existing (full) non-clausal
resolution [46]. We argue that our clausal-like formulation eases the
understanding of $\mathcal{UR}_{\Sigma}$, the building of the required formal
proofs and the future generalization of $\mathcal{UR}_{\Sigma}$ to determine
Non-Clausal Resolution for possibilistic and for other uncertainty logics.

Thirdly, we prove that computing the consistency degree of
$\mathcal{\overline{H}}_{\Sigma}$ members has polynomial complexity. There
indeed exist polynomial classes in possibilistic logic but all of them are
clausal [41], and so, the tractable non-clausal fragment was empty. We think
that this is just a first tractable result in possibilistic reasoning and that
the approach presented here will serve to widen the tractable possibilistic
non-clausal fragment.

Below we give an specific possibilistic non-clausal base $\Sigma$, whose
suffix notation will be detailed in Section 2 and wherein $P,Q,\ldots$ and
$\neg{P},\neg{Q},\ldots$ are positive and negative literals, respectively, and
$\phi_{1}$, $\phi_{2}$ and $\phi_{3}$ are non-clausal propositional formulas.
We will

$\varphi=\\{\wedge\ \,P\ \,(\vee\ \ \neg Q\ \ \\{\wedge\ \ (\vee\ \ \neg P\ \
\neg Q\ \ R\,)\ \ (\vee\ \ \phi_{1}\ \ \\{\wedge\ \ \phi_{2}\ \ \neg
P\,\\}\,)\ \,Q\,\\}\,)\ \ {\phi_{3}}\ \\}$ $\Sigma=\\{\,\langle\varphi:{\bf
0.8}\rangle\quad\langle P:{\bf 0.8}\rangle\quad\langle\neg Q:{\bf
0.6}\rangle\quad\langle R:{\bf
0.6}\rangle\quad\langle\phi_{1}:{\bf.3}\rangle\quad\langle\phi_{3}:{\bf
1}\rangle\,\\}$

show that $\Sigma$ is Horn-NC when $\phi_{3}$ is Horn-NC and at least one of
$\phi_{1}$ or $\phi_{2}$ is negative.

Recapitulating, the list of properties of $\mathcal{\overline{H}}_{\Sigma}$ is
given below, where the last two properties have been shown in [40] for
propositional logic but are inherited by $\mathcal{\overline{H}}_{\Sigma}$:

  * •

Computing the inconsistency degree of $\mathcal{\overline{H}}_{\Sigma}$ is
tractable.

  * •

$\mathcal{\overline{H}}_{\Sigma}$ subsumes syntactically the possibilitic Horn
class.

  * •

$\mathcal{\overline{H}}_{\Sigma}$ is equivalent semantically to the
possibilitic Horn class.

  * •

$\mathcal{\overline{H}}_{\Sigma}$ contains all possibilitic NC bases whose
clausal form is Horn.

  * •

$\mathcal{\overline{H}}_{\Sigma}$ is linearly recognizable [40].

  * •

$\mathcal{\overline{H}}_{\Sigma}$ is strictly succincter111Succinctness was
defined in [33]. than the possibilistic Horn class [40].

The presented approach serves as starting point to develop approximate non-
clausal reasoning based on (1) DPLL and (2) resolution: (1)
$\mathcal{UR}_{\Sigma}$ paves the way to define DPLL in NC since its NC Unit-
Propagation is based on NC Unit-Resolution, i.e. $\mathcal{UR}_{\Sigma}$; and
(2) the existing NC resolution [46] presents some deficiencies derived from
its functional-like formalization, such as not precisely defining the
potential resolvents. Our clausal-like formalization of
$\mathcal{UR}_{\Sigma}$ skips such deficiencies and signifies a step forward
towards defining NC resolution for at least those uncertainty logics for which
clausal resolution is already defined, e.g. possibilistic logic [23, 24].

This paper is organized as follows. Section 2 and 3 present background on
propositional non-clausal formulas and on possibilistic logic, respectively.
Section 4 defines the class $\mathcal{\overline{H}}_{\Sigma}$. Section 5
introduces the calculus $\mathcal{UR}_{\Sigma}$. Section 6 provides examples
illustrating how $\mathcal{UR}_{\Sigma}$ computes
$\mathcal{\overline{H}}_{\Sigma}$ members. Section 7 provides the formal
proofs of the correctness of $\mathcal{UR}_{\Sigma}$ and of the tractability
of $\mathcal{\overline{H}}_{\Sigma}$. Section 8 focuses on related and future
work. Last section summarizes the main contributions.

##  2 Propositional Non-Clausal Logic

This section presents some terminologies used in this paper and background on
non-clausal (NC) propositional logic (see [9] for a complete background). We
present first the needed syntactical concepts and then the semantical ones. We
begin by introducing the language.

######  Definition 2.1.

The NC language is formed by the sets: constants $\\{{\bf\bot,\top}\\}$,
propositions $\mathcal{P}=$ {P, Q, R, …}, connectives {$\neg,\vee,\wedge\\}$
and auxiliary symbols (, ), { and }.

Next we describe the required elements relative to clausal formulas.

######  Definition 2.2.

$X$ (resp. $\neg{X}$) with $X\in\mathcal{P}$ is a positive (resp. negative)
literal. $\mathcal{L}$ is the set of literals. Constants and literals are
atoms. $(\vee\ \ell_{1}\ \ell_{2}\ \ldots\ \ell_{k})$, the $\ell_{i}$ being
literals, is a clause. A clause with at most one positive literal is Horn.
$\\{\wedge\ C_{1}\ C_{2}\ \ldots\ C_{n}\\}$, the $C_{i}$ being clauses, is a
clausal formula. $\mathcal{C}$ and $\mathcal{H}$ are the set of clausal and
Horn formulas, respectively.

Note. We firstly justify our chosen notation of non-clausal formulas before
defining them. Thus, for the sake of readability of non-clausal formulas, we
will employ:

  1. 1.

The prefix notation as it requires only one $\vee/\wedge$-connective per
formula, while infix notation requires $k-1$, $k$ being the arity of the
involved $\vee/\wedge$-connective.

  2. 2.

Two formula delimiters (see Definition 2.3), $(\vee\,\ldots\,)$ for
disjunctions and $\\{\wedge\,\ldots\,\\}$ for conjunctions, to better
distinguish them inside non-clausal formulas.

So our next definition is that of non-clausal formulas222Also called ”negation
normal form formulas” in the literature., whose differential feature is that
the connective $\neg$ can occur only in front of propositions, i.e. at atomic
level.

######  Definition 2.3.

The non-clausal formulas over a set of propositional variables $\mathcal{P}$
is the smallest set $\mathcal{NC}$ such that the following conditions hold:

  * •

$\\{\bot,\top\\}\cup\mathcal{L}\,\subset\,\mathcal{NC}$.

  * •

If $\forall i\in\\{1,\ldots k\\}$, $\varphi_{i}\in\mathcal{NC}$ then
$\\{\wedge\ \varphi_{1}\ldots\varphi_{i}\ldots\varphi_{k}\\}\in\mathcal{NC}$.

  * •

If $\forall i\in\\{1,\ldots k\\}$, $\varphi_{i}\in\mathcal{NC}$ then $\,(\vee\
\varphi_{1}\ldots\varphi_{i}\ldots\varphi_{k})\in\mathcal{NC}$.

– $\\{\wedge\,\varphi_{1}\ldots\varphi_{i}\ldots\varphi_{k}\\}$ and any
$\varphi_{i}$ are called conjunction and conjunct, respectively.

– $(\vee\,\varphi_{1}\ldots\varphi_{i}\ldots\varphi_{k})$ and any
$\varphi_{i}$ are called disjunction and disjunct, respectively.

– $[\odot\,\varphi_{1}\ldots\varphi_{i}\ldots\varphi_{k}]$ stands for both
$(\vee\,\varphi_{1}\ldots\varphi_{i}\ldots\varphi_{k})\mbox{\ and \
}\\{\wedge\,\varphi_{1}\ldots\varphi_{i}\ldots\varphi_{k}\\}.$

######  Example 2.4.

$\varphi_{1}$ to $\varphi_{3}$ below are NC formulas, while $\varphi_{4}$ is
not. We will show that $\varphi_{2}$ is Horn-NC while $\varphi_{1}$ is not
Horn-NC, and as $\varphi_{3}$ includes $\varphi_{1}$, then $\varphi_{3}$ is
not Horn-NC either. On the other side, the example in the Introduction is
Horn-NC under certain conditions.

  * •

$\ \varphi_{1}=\\{\wedge\ \ (\vee\ \ \neg{P}\ \ Q\ \ \bot\,)\ \ (\vee\ \ Q\ \
\\{\wedge\ \neg{R}\ \ S\ \ \top\,\\}\,)\,\\}$

  * •

$\ \,\varphi_{2}=(\vee\ \ \\{\wedge\ \ \neg{P}\ \ \top\\}\ \ \\{\wedge\ \
(\vee\ \ \neg{P}\ \ R\,)\ \ \\{\wedge\ \ Q\ \ (\vee\ \ P\ \
\neg{S}\,)\,\\}\,\\}\ \ \\{\wedge\ \ \bot\ \ Q\\}\,)$

  * •

$\ \varphi_{3}=(\vee\ \ \varphi_{1}\ \ \\{\wedge\ \ Q\ \ (\vee\ \ \varphi_{1}\
\ \neg{Q}\ \ \varphi_{2})\,\\}\ \ \\{\wedge\ \ \varphi_{2}\ \ \top\ \
\varphi_{1}\,\\}\,)$

  * •

$\varphi_{4}=\neg(\vee\ \varphi_{1}\ \varphi_{2})$ ∎

######  Definition 2.5.

Sub-formulas are recursively defined as follows. The unique sub-formula of an
atom is the atom itself, and the sub-formulas of a formula
$\varphi=\langle\odot\ \varphi_{1}\ldots\varphi_{i}\ldots\varphi_{k}\rangle$
are $\varphi$ itself plus the sub-formulas of the $\varphi_{i}$’s.

######  Example 2.6.

The sub-formulas of a clausal formula are the formula itself plus its clauses,
literals and constants.

######  Definition 2.7.

NC formulas are modeled by trees if: (i) the nodes are: each atom is a leaf
and each occurrence of a $\wedge/\vee$-connective is an internal node; and
(ii) the arcs are: each sub-formula $[\odot\
\varphi_{1}\ldots\varphi_{i}\ldots\,\varphi_{k}]$ is a $k$-ary hyper-arc
linking the node of $\odot$ with, for every $i$, the node of $\varphi_{i}$ if
$\varphi_{i}$ is an atom and with the node of its connective otherwise.

######  Example 2.8.

The tree of $\\{\wedge\ \,\neg R\ \,(\vee\ \,\\{\wedge\ \,\neg P\ \,Q\\}\
\,\bot\ \,(\vee\ \,\neg P\ \,\neg R)\,)\,\\}$ is given in Fig. 2.

pt$\wedge$pt$\neg{R}$pt$\vee$pt$\wedge$pt$\neg{P}$pt$Q$pt$\bot$pt$\vee$pt$\neg{P}$pt$\neg{R}$

Fig. 2. Tree of Example 2.8.

∎

Remark. Directed acyclic graphs (DAGs) generalize trees and allow for
important savings in space and time. Our approach also applies when NC
formulas are represented and implemented by DAGs. Nevertheless, for
simplicity, we will use formulas representable by trees in the illustrative
examples throughout this article.

$-$ In the remaining of this section, we present semantical notions.

$-$ In the next definition (first line), the empty disjunction $(\vee)$ is
considered equivalent to a $\bot$-constant and the empty conjunction
$\\{\wedge\\}$ to a $\top$-constant.

######  Definition 2.9.

An interpretation $\omega$ maps the formulas $\mathcal{NC}$ into the truth-
value set $\\{0,1\\}$ and is extended from propositional variables
$\mathcal{P}$ to formulas $\mathcal{NC}$ via the rules below, where
$X\in\mathcal{P}$ and $\varphi_{i}\in\mathcal{NC}$, $1\leq i\leq k$. We will
denote $\Omega$ the universe of interpretations.

  * •

$\omega(\bot)=\omega(\,(\vee)\,)=0$ and
$\omega(\top)=\omega(\,\\{\wedge\\}\,)=1$.

  * •

$\omega(X)+\omega(\neg X)=1$.

  * •

$\omega(\,(\vee\
\varphi_{1}\ldots\varphi_{i}\ldots\varphi_{k})\,)\,=\mathrm{max}\\{\omega(\varphi_{i}):1\leq
i\leq k\\}$.

  * •

$\omega(\,\\{\wedge\
\varphi_{1}\ldots\varphi_{i}\ldots\varphi_{k}\\}\,)=\mathrm{min}\\{\omega(\varphi_{i}):1\leq
i\leq k\\}$.

######  Definition 2.10.

$\varphi$ and $\varphi^{\prime}$ being formulas, some well-known semantical
notions follow. An interpretation $\omega$ is a model of $\varphi$ if
$\omega(\varphi)=1.$ If $\varphi$ has a model then it is consistent and
otherwise inconsistent. $\varphi$ and $\varphi^{\prime}$ are (logically)
equivalent, denoted $\varphi\equiv\varphi^{\prime}$, if $\forall\omega$,
$\omega(\varphi)=\omega(\varphi^{\prime})$. $\varphi^{\prime}$ is logical
consequence of $\varphi$, denoted $\varphi\models\varphi^{\prime}$, if
$\forall\omega$, $\omega(\varphi)\leq\omega(\varphi^{\prime})$.

Next, some well-known rules allowing to simplify formulas are supplied.

######  Definition 2.11.

Constant-free, equivalent formulas are straightforwardly obtained by
recursively applying to sub-formulas the simplifying rules below:

$\bullet$ Replace $(\vee\ \top\ \varphi\,)$ with $\top$.

$\bullet$ Replace $\\{\wedge\ \bot\ \varphi\,\\}$ with $\bot$.

$\bullet$ Replace $\\{\wedge\ \top\ \varphi\,\\}$ with $\varphi$.

$\bullet$ Replace $(\vee\ \bot\ \varphi\,)$ with $\varphi$.

######  Example 2.12.

The constant-free, equivalent NC formula of $\varphi_{2}$ in Example 2.4 is:

$\varphi=(\vee\ \ \neg P\ \ \\{\wedge\ \ (\vee\ \ \neg P\ \ R)\ \ \\{\wedge\ \
Q\ \ (\vee\ \ P\ \ \neg S)\,\\}\,\\})$

Remark. For simplicity and since free-constant, equivalent formulas are easily
obtained, hereafter we will consider only free-constant formulas.

##  3 Necessity-Valued Possibilistic Logic

Let us have a brief refresher on necessity-valued possibilistic logic (the
reader may consult [22, 25, 26] for more details).

###  3.1 Semantics

At the semantic level, possibilistic logic is defined in terms of a
possibilistic distribution $\pi$ on the universe $\Omega$ of interpretations,
i.e. an $\Omega\rightarrow[0,1]$ mapping which intuitively encodes for each
$\omega\in\Omega$ to what extent it is plausible that $\omega$ is the actual
world. $\pi(\omega)=0$ means that $\omega$ is impossible, $\pi(\omega)=1$
means that nothing prevents $\omega$ from being true, whereas
$0<\pi(\omega)<1$ means that $\omega$ is only somewhat possible to be the real
world. Possibility degrees are interpreted qualitatively: when
$\pi(\omega)>\pi(\omega^{\prime})$, $\omega$ is considered more plausible than
$\omega^{\prime}$. A possibilistic distribution $\pi$ is _normalized_ if
$\exists\omega\in\Omega,\pi(\omega)=1$, i.e. at least one interpretation is
entirely plausible.

A possibility distribution $\pi$ induces two uncertainty functions from the
formulas $\mathcal{NC}$ to $[0,1]$, called possibility and necessity functions
and noted $\Pi$ and $N$, respectively, which allow us to rank formulas. $\Pi$
is defined by Dubois _et al._ (1994) [22] as:

$\Pi(\varphi)=\mathrm{max}\\{\pi(\omega)\ |\
\omega\in\Omega,\omega\models\varphi\\},$

and evaluates the extent to which $\varphi$ is consistent with the beliefs
expressed by $\pi$. The dual _necessity measure_ $N$ is defined by:

$N(\varphi)=1-\Pi(\neg\varphi)=\mathrm{inf}\\{1-\pi(\omega)\ |\
\omega\in\Omega,\omega\nvDash\varphi\\},$

and evaluates the extent to which $\varphi$ is entailed by the available
beliefs [22]. So the lower the possibility of an interpretation that makes
$\varphi$ False, the higher the necessity degree of $\varphi$. $N(\varphi)=1$
means $\varphi$ is a totally certain piece of knowledge, whereas
$N(\varphi)=0$ expresses the complete lack of knowledge of priority about
$\varphi$. Note that always $N(\top)=1$ for any possibility distribution,
while $\Pi(\top)=1$ (and, related, $N(\bot)$=0) only holds when the
possibility distribution is normalized, i.e. only normalized distributions can
express consistent beliefs [22].

A major property of $N$ is Min-Decomposability:
$\forall\varphi,\psi,N(\varphi\wedge\psi)=\mathrm{min}(N(\varphi),N(\psi))$.
However, for disjunctions only
$N(\varphi\vee\psi)\geq\mathrm{max}(N(\varphi),N(\psi))$ holds. Further, one
has $N(\varphi)\leq N(\psi)$ if $\varphi\models\psi$, and hence,
$N(\varphi)=N(\psi)$ if $\varphi\equiv\psi$.

###  3.2 Syntactics

A possibilistic formula is a pair
$\langle\varphi:\alpha\rangle\in\mathcal{NC}\times(0,1]$, where $\varphi$ is a
propositional NC formula, $\alpha\in(0,1]$ expresses the certainty that
$\varphi$ is the case, and it is interpreted as the semantic constraint
$N(p)\geq\alpha$. So formulas of the form $\langle\varphi:0\rangle$ are
excluded. A possibilistic base $\Sigma$ is a collection of possibilistic
formulas
$\Sigma=\\{\langle\varphi_{i}:\alpha_{i}\rangle\,|\,i=1,\ldots,k\,\\}$ and
corresponds to a set of constraints on possibility distributions. The
classical knowledge base associated with $\Sigma$ is denoted as $\Sigma^{*}$,
i.e. $\Sigma^{*}=\\{\varphi|\langle\varphi:\alpha\rangle\in\Sigma\\}$.
$\Sigma$ is consistent if and only if $\Sigma^{*}$ is consistent. It is
noticeable that, due to Min-Decomposability, a possibilistic logic base can be
easily put in clausal form.333Nevertheless, as said previously, this
translation can blow up exponentially the size of formulas and so can
dramatically reduce the overall efficiency of the clausal reasoner.

Typically, there can be many possibility distributions that satisfy the set of
constraints $N(\varphi)\geq\alpha$ but we are usually only interested in the
_least specific possibility distribution_ , i.e. the possibility distribution
that makes minimal commitments, namely, the greatest possibility distribution
w.r.t. the following ordering: $\pi$ is a least specific possibility
distribution compatible with $\Sigma$ if for any $\pi^{\prime}$,
$\pi^{\prime}\neq\pi$, compatible with $\Sigma$, one has
$\forall\omega\in\Omega,\pi(\omega)\geq\pi^{\prime}(\omega)$. Such a least
specific possibility distribution always exists and is unique [22].

Thus, for a given $\langle\varphi:\alpha\rangle$, possibilistic distributions
should consider that an $\omega$ that makes $\varphi$ True is possible at the
maximal level, say 1, while an $\omega$ that makes $\varphi$ False is possible
at most at level $1-\alpha$. Thus the semantic counterpart of a base $\Sigma$,
or the least specific distribution $\pi_{\Sigma}$ is defined by,
$\forall\omega,\omega\in\Omega$:

$\pi_{\Sigma}(\omega)=\left\\{\begin{array}[]{l l}1&\ \mbox{if}\ \
\forall\langle\varphi_{i},\alpha_{i}\rangle\in\Sigma,\omega\models\varphi_{i}\\\
\mathrm{min}\\{1-\alpha_{i}\,|\,\omega\nvDash\varphi_{i},\,\langle\varphi_{i},\alpha_{i}\rangle\in\Sigma\\}&\
\mbox{otherwise}\\\ \end{array}\right.$

######  Proposition 3.1.

Let $\Sigma$ be a possibilistic base. For any possibility distribution $\pi$
on $\Omega$, $\pi$ satisfies $\Sigma$ if and only if $\pi\leq\pi_{\Sigma}$.

Proposition 3.1 says that $\pi_{\Sigma}$ is the least specific possibility
distribution satisfying $\Sigma$ and it has been shown in reference [22].

###  3.3 Syntactic Deduction

This subsection introduces some few notions about deduction in possibilistic
logic and starts by the well-known possibilistic inference rules to be handled
in this article:

######  Definition 3.2.

We define below three rules, where
$\ell\in\mathcal{L};\varphi,\psi\in\mathcal{NC}$ and $\alpha,\beta\in(0,1]$.
The first is possibilistic resolution [23, 24]; the second rule is Min-
Decomposability; and the third rule, Max-Necessity, follows from the semantic
constraint meaning of $\langle\varphi:\alpha\rangle$.

  * •

$\mbox{\text@underline{Resol}}:\quad\ \langle\,(\vee\ \,\ell\
\,\varphi):\alpha\rangle,\langle\,(\vee\ \,\neg\ell\ \,\psi):\beta\,\rangle\
\vdash\ \langle\ (\vee\ \,\varphi\ \psi):\mbox{\bf min}\\{\alpha,\beta\\}\
\rangle$.

  * •

$\mbox{\text@underline{MinD}}:\quad\,\langle\varphi:\alpha\rangle,\
\langle\psi:\beta\rangle\ \vdash\ \langle\ \\{\wedge\,\varphi\
\psi\\}:\mbox{\bf min}\\{\alpha,\beta\\}\ \rangle$.

  * •

$\mbox{\text@underline{MaxN}}:\quad\langle\varphi:\alpha\rangle,\
\langle\varphi:\beta\rangle\ \vdash\ \langle\ \varphi:\mbox{\em\bf
max}\\{\alpha,\beta\\}\ \rangle$.

Before formulating the soundness and completeness theorem in possibilistic
logic, we need to introduce the next concept of $\alpha$-cut; we call the
$\alpha$-cut (resp. strict $\alpha$-cut) of $\Sigma$, denoted
$\Sigma_{\geq\alpha}$ (resp. $\Sigma_{>\alpha}$), the set of classical
formulas in $\Sigma$ having a necessity degree at least equal to $\alpha$
(resp. strictly greater than $\alpha$), namely
$\Sigma_{\geq\alpha}=\\{\varphi\,|\,\langle\varphi:\beta\rangle\in\Sigma,\beta\geq\alpha\\}$
(resp.
$\Sigma_{>\alpha}=\\{\varphi\,|\,\langle\varphi:\beta\rangle\in\Sigma,\beta>\alpha\\}$).

######  Theorem 3.3.

The following soundness and completeness theorem holds:

$\Sigma\models_{\pi}\langle\varphi:\alpha\rangle\ \Leftrightarrow\
\Sigma\vdash_{\mathrm{Res}}\langle\varphi:\alpha\rangle\quad\Longleftrightarrow\quad\Sigma_{\geq\alpha}\models\varphi\
\Leftrightarrow\ \Sigma_{\geq\alpha}\vdash\varphi$

where $\models_{\pi}$ means any $\omega$ compatible with $\Sigma$ is also
compatible with $\langle\varphi:\alpha\rangle$, or formally,
$\forall\omega,\pi_{\Sigma}(\omega)\leq\pi_{\\{\langle
p:\alpha\rangle\\}}(\omega)$. $\vdash_{\mathrm{Res}}$ relies on the repeated
use of possibilistic resolution.

The last half of the above expression reduces to the soundness and
completeness theorem of propositional logic applied to each level cut of
$\Sigma$, which is an ordinary propositional base.

###  3.4 Partial Inconsistency

The inconsistency degree of a base $\Sigma$ in terms of its $\alpha$-cut can
be equivalently defined as the largest weight $\alpha$ such that the
$\alpha$-cut of $\Sigma$ is inconsistent:

$\mathrm{Inc}(\Sigma)=\mathrm{max}\\{\alpha\,|\,\Sigma_{\geq\alpha}\,\mathrm{is\
inconsistent}\\}.$

$\mathrm{Inc}(\Sigma)=0$ entails $\Sigma^{*}$ is consistent. In [22], the
inconsistency degree of $\Sigma$ is defined by the least possibility
distribution $\pi_{\Sigma}$, concretely
$\mathrm{Inc}(\Sigma)=1-\mathrm{sup}_{\omega\in\Omega}\pi_{\Sigma}(\omega).$

To check whether $\varphi$ follows from $\Sigma$, one should add
$\langle\neg\varphi:1\rangle$ to $\Sigma$ and then check whether
$\Sigma\cup\\{\langle\neg\varphi:1\rangle\\}\vdash\langle\bot:\alpha\rangle$.
Equivalently the maximum $\alpha$ s.t.
$\Sigma\models\langle\varphi:\alpha\rangle$ is given by the inconsistency
degree of $\Sigma\cup\\{\langle\neg\varphi:1\rangle\\}$, i.e.
$\Sigma\models\langle\varphi:\alpha\rangle$ iff
$\alpha=\mathrm{Inc}(\Sigma\cup\\{\langle\neg\varphi,1\rangle\\}).$

######  Proposition 3.4.

The next statements are proven in [22]:

$\Sigma\models\langle\varphi:\alpha\rangle\ \ \mbox{\em iff}\ \
\Sigma\cup\\{\langle\neg\varphi:1\rangle\\}\vdash\langle\bot:\alpha\rangle\ \
\mbox{\em iff}\ \
\alpha=\mathrm{Inc}(\Sigma\cup\\{\langle\neg\varphi:1\rangle\\})\ \ \mbox{\em
iff}\ \ \Sigma_{\geq\alpha}\vdash\varphi.$

This result shows that any deduction problem in possibilistic logic can be
viewed as computing an inconsistency degree.

###  3.5 Clausal and Non-Clausal Bases

According to previous definitions, to each class of propositional formulas
corresponds a class of possibilistic bases. Below, we define the possibilistic
classes handled here and after recall the complexity of computing the
inconsistency degree of their members.

######  Definition 3.5.

A possibilistic base
$\Sigma=\\{\langle\varphi_{i}:\alpha_{i}\rangle\,|\,i=1,\ldots,k\,\\}$ is
called Horn, clausal or NC if all its formulas $\varphi_{i},1\leq i\leq 1$,
are Horn, clausal or NC, respectively. $\mathcal{H}_{\Sigma}$,
$\mathcal{C}_{\Sigma}$ and $\mathcal{NC}_{\Sigma}$ denote, respectively, the
classes of possibilistic Horn, clausal and NC bases.

In this article we define in Definition 4.19 a novel possibilistic class, i.e.
the possibilistic Horn-NC class. Next we just define acronyms associated to
the problems of computing the inconsistency degree of the four mentioned
possibilistic classes.

######  Definition 3.6.

Horn-INC, CL-INC, Horn-NC-INC and NC-INC denote respectively the problems of
computing the inconsistency degree of Horn, clausal, Horn-NC and NC bases.

Complexities. Regarding the complexities of the previous problems, we have:

  1. $\bullet$

Clausal Pbs.: CL-INC is Co-NP-complete [41] and Horn-INC is polynomial [41].

  2. $\bullet$

NC-INC is Co-NP-complete. This claim stems from: (i) Theorem 3.3 applies to
both clausal and NC bases; and (ii) checking whether an interpretation is a
model of an NC propositional formula is polynomial as for clausal formulas.

  3. $\bullet$

Horn-NC-INC has polynomial complexity as proven in Section 7.

##  4 The Possibilistic Horn-NC Class: $\mathcal{\overline{H}}_{\Sigma}$

This section defines the class $\mathcal{\overline{H}}_{\Sigma}$ of
Possibilistic Horn Non-Clausal (Horn-NC) bases and states its properties and
relationships with other possibilistic classes. The proofs were given in [40]
but are provided in an Appendix for the sake of the paper being self
contained.

$\mathcal{\overline{H}}_{\Sigma}$ subsumes the next two classes:

  * •

possibilistic Horn, or $\mathcal{{H}}_{\Sigma}$; and

  * •

propositional Horn-NC, or $\mathcal{\overline{H}}$ (recently presented [40]).

We first define the latter, i.e. the class $\mathcal{\overline{H}}$ of
propositional Horn-NC formulas, which is the propositional component of the
new possibilistic class $\mathcal{\overline{H}}_{\Sigma}$ to be introduced.

###  4.1 Simple Definition of $\mathcal{\overline{H}}$

Below, we define $\mathcal{\overline{H}}$ in a simple way, and in the next
subsection, will give its detailed definition by taking a closer look to this
simple definition. We start by defining the negative formulas, which
generalize the negative literals in the clausal framework.

######  Definition 4.1.

A non-clausal formula is negative if it has uniquely negative literals. We
will denote $\mathcal{N}^{-}$ the set of negative formulas.

######  Example 4.2.

Trivially negative literals are basic negative formulas. Another example of
negative NC formula is $(\vee\ \ \\{\wedge\ \,\neg P\ \,\neg R\,\\}\ \
\\{\wedge\ \,\neg S\ \,(\vee\ \,\neg P\ \,\neg
Q\,)\,\\}\,)\in\mathcal{N}^{-}$. ∎

Next we upgrade the Horn pattern “a Horn clause has (any number of negative
literals and) at most one positive literal” to the NC context in the next
straightforward way:

######  Definition 4.3.

An NC formula is Horn-NC if all its disjunctions have any number of negative
disjuncts and at most one non-negative disjunct. We denote
$\mathcal{\overline{H}}$ the class of Horn-NC formulas.

Clearly the class $\mathcal{\overline{H}}$ subsumes the Horn class
$\mathcal{H}$. From Definition 4.3 it follows trivially that all sub-formulas
of any Horn-NC are Horn-NC too. Yet, the converse does not hold: there are
non-Horn-NC formulas whose all sub-formulas are Horn-NC.

######  Example 4.4.

One can see that $\varphi_{1}$ below has only one non-negative disjunct and so
$\varphi_{1}$ is Horn-NC, while $\varphi_{2}$ is not Horn-NC as it has two
non-negative disjuncts.

  * •

$\varphi_{1}=(\vee\ \ \\{\wedge\ \ \neg Q\ \ \neg S\\}\ \ \\{\wedge\ \ R\ \
P\,\\}\,).$

  * •

$\varphi_{2}=(\vee\ \ \\{\wedge\ \ \neg Q\ \ S\\}\ \ \\{\wedge\ \ R\ \ \neg
P\,\\}\,)$. ∎

######  Example 4.5.

We now consider both $\varphi$ in Example 2.12 (copied below) and
$\varphi^{\prime}$ below too, which results from $\varphi$ by just switching
its literal $\neg P$ for $P$:

  * •

$\varphi=(\vee\ \ \neg P\ \ \\{\wedge\ \ (\vee\ \ \neg P\ \ R)\ \ \\{\wedge\ \
Q\ \ (\vee\ \ P\ \ \neg S)\,\\}\,\\})$

  * •

$\varphi^{\prime}=(\vee\ \ \ P\ \ \,\\{\wedge\ \ (\vee\ \ \neg P\ \ R)\ \
\\{\wedge\ \ Q\ \ (\vee\ \ P\ \ \neg S)\,\\}\,\\})$

All disjunctions of $\varphi$, i.e. $(\vee\ \,\neg P\ \,R)$, $(\vee\ P\ \neg
S)$ and $\varphi$ itself (By Definition 2.5, $\varphi$ is a sub-formula of
$\varphi$), have exactly one non-negative disjunct; so $\varphi$ is Horn-NC.
Yet, $\varphi^{\prime}=(\vee\ P\ \phi)$, $\phi$ being non-negative, has two
non-negative disjuncts; thus $\varphi^{\prime}$ is not Horn-NC. ∎

###  4.2 Detailed Definition of $\mathcal{\overline{H}}$

Before giving a fine-grained definition of $\mathcal{\overline{H}}$, we
individually and inductively specify:

$\bullet$ Horn-NC conjunctions, in Lemma 4.6, and

$\bullet$ Horn-NC disjunctions, in Lemma 4.8,

and subsequently, we compactly specify $\mathcal{\overline{H}}$ by merging
both specifications.

Just as conjunctions of Horn clausal formulas are Horn too, likewise
conjunctions of Horn-NC formulas are Horn-NC too, which is straightforwardly
formalized next.

######  Lemma 4.6.

Conjunctions of Horn-NC formulas are Horn-NC as well, formally:

$\\{\wedge\
\varphi_{1}\,\ldots\,\varphi_{i}\ldots\,\varphi_{k}\\}\in\mathcal{\overline{H}}\mbox{\em\
\ iff \ \ for }1\leq i\leq k,\ \varphi_{i}\in\mathcal{\overline{H}}.$

  * Proof.

It is obvious that if all sub-formulas $\varphi_{i}$ individually verify
Definition 4.3 so does a conjunction thereof, and vice versa. $\blacksquare$

######  Example 4.7.

If $H$ is Horn, $\phi_{1}$ is $\varphi_{1}$ from Example 4.4 and $\phi_{2}$ is
$\varphi$ from Example 4.5, i.e. $\phi_{1}$ and $\phi_{2}$ are Horn-NC, then
for instance $\varphi_{1}=\\{\wedge\ H\ \phi_{1}\ \phi_{2}\\}$ is Horn-NC. ∎

In order to give now a detailed definition of $\mathcal{\overline{H}}$, we
verify that Definition 4.3 can be equivalently reformulated in the next
inductive manner: “an NC is Horn-NC if all its disjunctive sub-formulas have
any number of negative disjuncts and one disjunct is Horn-NC”. This leads to
the next formalization and statement.

######  Lemma 4.8.

A NC disjunction $\varphi=(\vee\
\varphi_{1}\ldots\varphi_{i}\ldots\varphi_{k})$ with $k\geq 1$ disjuncts
pertains to $\mathcal{\overline{H}}$ iff $\varphi$ has $k-1$ negative
disjuncts and one Horn-NC disjunct, formally

$\varphi=(\vee\
\varphi_{1}\ldots\varphi_{i}\ldots\varphi_{k})\in\mathcal{\overline{H}}\mbox{\em\
\ iff}\quad\exists i\ \mbox{\em s.t.}\ \varphi_{i}\in\mathcal{\overline{H}}\ \
\mbox{\em and}\ \ \forall j\neq i,\varphi_{j}\in\mathcal{N}^{-}.$

  * Proof.

See Appendix. $\blacksquare$

The next claims follow trivially from Lemma 4.8:

$\bullet$ Horn clauses are non-recursive Horn-NC disjunctions.

$\bullet$ NC disjunctions with all negative disjuncts are Horn-NC.

$\bullet$ NC disjunctions with $k\geq 2$ non-negative disjuncts are not Horn-
NC.

Next, we first reexamine, bearing Lemma 4.8 in mind, the formulas from Example
4.4, included in Example 4.9, and then those from Example 4.5, included in
Example 4.10.

######  Example 4.9.

Below we analyze $\varphi_{1}$ and $\varphi_{2}$ from Example 4.4.

  * •

$\varphi_{1}=(\vee\ \ \\{\wedge\ \ \neg Q\ \ \neg S\\}\ \ \\{\wedge\ \ R\ \
P\,\\}\,).$

– Clearly $\\{\wedge\ \ \neg Q\ \ \neg S\\}\in\mathcal{N}^{-}$.

– By Lemma 4.6, $\\{\wedge\ \ R\ \ P\,\\}\in\mathcal{\overline{H}}$.

– By Lemma 4.8, $\varphi_{1}\in\mathcal{\overline{H}}$.

  * •

$\varphi_{2}=(\vee\ \ \\{\wedge\ \ \neg Q\ \ S\\}\ \ \\{\wedge\ \ R\ \ \neg
P\,\\}\,)$.

– Obviously $\\{\wedge\ \ \neg Q\ \ S\\}\notin\mathcal{N}^{-}$ and $\\{\wedge\
\ R\ \ \neg P\,\\}\notin\mathcal{N}^{-}$.

– According to Lemma 4.8, $\varphi_{2}\notin\mathcal{\overline{H}}$. ∎

######  Example 4.10.

Consider again $\varphi$ and $\varphi^{\prime}$ from Example 4.5 and recall
that $\varphi^{\prime}$ results from $\varphi$ by just switching its literal
$\neg P$ for $P$. Below we check one-by-one whether or not the sub-formulas of
both $\varphi$ and $\varphi^{\prime}$ are in $\mathcal{\overline{H}}$.

  * •

By Lemma 4.8, $(\vee\ \ \neg P\ \ R)\in\mathcal{\overline{H}}$.

  * •

By Lemma 4.8, $(\vee\ \ P\ \ \neg S)\in\mathcal{\overline{H}}$.

  * •

By Lemma 4.6, $\\{\wedge\ \ Q\ \ (\vee\ \ P\ \ \neg
S)\,\\}\in\mathcal{\overline{H}}$.

  * •

By Lemma 4.6, $\phi=\\{\wedge\ \ (\vee\ \ \neg P\ \ R)\ \ \\{\wedge\ \ Q\ \
(\vee\ \ P\ \ \neg S)\,\\}\,\\}\in\mathcal{\overline{H}}$.

  * •

Using previous formula $\phi$, we have $\varphi=(\vee\ \neg P\ \,\phi\,)$.

– Since $\neg P\in\mathcal{N}^{-}$ and $\phi\in\mathcal{\overline{H}}$, by
Lemma 4.8, $\varphi\in\mathcal{\overline{H}}$.

  * •

The second formula in Example 4.5 is $\varphi^{\prime}=(\vee\ P\ \phi\,)$.

– Since $P,\,\phi\notin\mathcal{N}^{-}$, by Lemma 4.8,
$\varphi^{\prime}\notin\mathcal{\overline{H}}$. ∎

By using Lemmas 4.6 and 4.8, the class $\mathcal{\overline{H}}$ is
syntactically, compactly and inductively defined as follows.

######  Definition 4.11.

We define the set $\mathcal{\widehat{H}}$ over the set of propositional
variables $\mathcal{P}$ as the smallest set such that the conditions below
hold, where $k\geq 1$ and $\mathcal{L}$ is the set of literals.

  * (1)

$\mathcal{L}\subset\mathcal{\widehat{H}}.$

  * (2)

If $\forall i,\,\varphi_{i}\in\mathcal{\widehat{H}}\ \ \mbox{then}\ \
\\{\wedge\
\varphi_{1}\,\ldots\,\varphi_{i}\ldots\varphi_{k}\\}\in\mathcal{\widehat{H}}.$

  * (3)

If $\varphi_{i}\in\mathcal{\widehat{H}}$ and $\forall j\neq i$,
$\varphi_{j}\in\mathcal{N}^{-}\ \ \mbox{then}\ \ (\vee\
\varphi_{1}\ldots\varphi_{i}\ldots\,\varphi_{k})\in\mathcal{\widehat{H}}.$

######  Theorem 4.12.

We have that $\mathcal{\widehat{H}}=\mathcal{\overline{H}}$.

  * Proof.

See Appendix. $\blacksquare$

Theorem 4.12 below states that $\mathcal{\widehat{H}}$ and
$\mathcal{\overline{H}}$ indeed coincide, namely Definition 4.11 is the
recursive and compact definition of the class $\mathcal{\overline{H}}$ of
Horn-NC formulas. Besides, inspired by Definition 4.11, in [40] a linear
algorithm is designed that recognizes whether a given NC $\varphi$ is Horn-NC
and, such property is inherited by the possibilistic Horn-NC formulas.

######  Example 4.13.

Viewed from Definition 4.11, we analyze $\varphi$ and $\varphi^{\prime}$ from
Example 4.10:

  * •

By (3), $(\vee\ \ \neg P\ \ R)\in\mathcal{\overline{H}}$.

  * •

By (3), $(\vee\ \ P\ \ \neg S)\in\mathcal{\overline{H}}$.

  * •

By (2), $\\{\wedge\ \ Q\ \ (\vee\ P\ \ \neg S)\,\\}\in\mathcal{\overline{H}}$.

  * •

By (2), $\phi=\\{\wedge\ \ (\vee\ \ \neg P\ \ R)\ \ \\{\wedge\ \ Q\ \ (\vee\ \
P\ \ \neg S)\,\\}\,\\}\in\mathcal{\overline{H}}$.

  * •

By (3), $\varphi=(\vee\ \ \neg P\ \ \phi\,)\in\mathcal{\overline{H}}$

  * •

By (3), $\varphi^{\prime}=(\vee\ \ P\ \ \phi\,)\notin\mathcal{\overline{H}}$.
∎

######  Example 4.14.

If we assume that $\varphi_{1}$, $\varphi_{2}$ and $\varphi_{3}$ are negative
and $\varphi_{4}$ and $\varphi_{5}$ are Horn-NC, then according to Definition
4.11, four examples of Horn-NC formulas follow.

  * •

By (3), $\varphi_{6}=(\vee\ \ \varphi_{1}\ \
\varphi_{4})\in\mathcal{\overline{H}}$.

  * •

By (2), $\varphi_{7}=\\{\wedge\ \ \varphi_{1}\ \ \varphi_{5}\ \
\varphi_{6}\\}\in\mathcal{\overline{H}}$.

  * •

By (3), $\varphi_{8}=(\vee\ \ \varphi_{1}\ \ \varphi_{2}\ \
\varphi_{7})\in\mathcal{\overline{H}}$.

  * •

By (2), $\varphi_{9}=\\{\wedge\ \ \varphi_{6}\ \ \varphi_{7}\ \
\varphi_{8}\\}\in\mathcal{\overline{H}}$. ∎

Next, we analyze a more complete example, concretely $\varphi$ from the
Introduction.

######  Example 4.15.

Let us take $\varphi$ below, wherein $\phi_{1},\phi_{2}$ and $\phi_{3}$ are NC
formulas:

$\varphi=\\{\wedge\ \,P\ \,(\vee\ \ \neg Q\ \ \\{\wedge\ \ (\vee\ \ \neg P\ \
\neg Q\ \ R\,)\ \ (\vee\ \ \phi_{1}\ \ \\{\wedge\ \ \phi_{2}\ \ \neg
P\,\\}\,)\ \,Q\,\\}\,)\ \ {\phi_{3}}\ \\}.$

The disjunctions of $\varphi$ and the proper $\varphi$ can be rewritten as
follows:

  * •

$\psi_{1}=(\vee\ \ \neg P\ \ \neg Q\ \ R\,)$.

  * •

$\psi_{2}=(\vee\ \ \phi_{1}\ \ \\{\wedge\ \ \phi_{2}\ \ \neg P\\}\,)$.

  * •

$\psi_{3}=(\vee\ \ \neg Q\ \ \\{\wedge\ \ \psi_{1}\ \ \psi_{2}\ \,Q\,\\}\,).$

  * •

$\varphi=\\{\wedge\ \ P\ \ \psi_{3}\ \ \phi_{3}\,\\}.$

We analyze one-by-one such disjunctions and finally the proper $\varphi$:

  * •

$\psi_{1}$: Trivially, $\psi_{1}$ is Horn, so
$\psi_{1}\in\mathcal{\overline{H}}$.

  * •

$\psi_{2}$: $\psi_{2}\in\mathcal{\overline{H}}$ if
$\phi_{1},\phi_{2}\in\mathcal{\overline{H}}$ and if at least one of $\phi_{1}$
or $\phi_{2}$ is negative.

  * •

$\psi_{3}$: $\psi_{3}\in\mathcal{\overline{H}}$ if
$\psi_{2}\in\mathcal{\overline{H}}$ (as $\psi_{1}\in\mathcal{\overline{H}}$).

  * •

$\varphi$: $\varphi\in\mathcal{\overline{H}}$ if
$\psi_{2},\phi_{3}\in\mathcal{\overline{H}}$ (as
$\psi_{3}\in\mathcal{\overline{H}}$ if $\psi_{2}\in\mathcal{\overline{H}}$).

Summarizing the conditions on $\varphi$ and on $\psi_{2}$, we have that:

$\bullet$ $\varphi$ is Horn-NC if $\phi_{3}$, $\phi_{1}$ and $\phi_{2}$ are
Horn-NC and if at least one of $\phi_{1}$ or $\phi_{2}$ is negative.

If we consider that $\varphi$ implicitly verifies Definition 4.3 (all sub-
formulas of a Horn-NC are Horn-NC), then we conclude that $\varphi$ is Horn-NC
if at least one of $\phi_{1}$ or $\phi_{2}$ is negative. ∎

###  4.3 Properties of the Class $\mathcal{\overline{H}}$

An important feature of Horn-formulas is the following:

######  Theorem 4.16.

Applying $\vee/\wedge$-distributivity to a Horn-NC $\varphi$ results in a Horn
formula.

  * Proof.

See Appendix. $\blacksquare$

We already saw that syntactically $\mathcal{\overline{H}}$ subsumes
$\mathcal{{H}}$, but besides, $\mathcal{\overline{H}}$ is semantically related
to $\mathcal{{H}}$ as Theorem 4.17 claims.

######  Theorem 4.17.

$\mathcal{\overline{H}}$ and $\mathcal{{H}}$ are semantically equivalent: each
formula in a class is logically equivalent to some formula in the other class.

  * Proof.

By Theorem 4.16, for every $\varphi\in\mathcal{\overline{H}}$ there exists
$H\in\mathcal{H}$ such that $\varphi\equiv H$. The converse follows from the
fact that $\mathcal{H}\subset\mathcal{\overline{H}}$. $\blacksquare$

The next theorem make it explicit how the classes Horn-NC and NC are related.

######  Theorem 4.18.

$\mathcal{\overline{H}}$ contains the next NC fragment: if applying
$\wedge/\vee$ distributivity to an NC formula $\varphi$ results in a Horn
formula, then $\varphi$ is in $\mathcal{\overline{H}}$.

  * Proof.

See Appendix. $\blacksquare$

The syntactical and semantical properties exhibited by
$\mathcal{\overline{H}}$ affirmed by the last three theorems suggest that
$\mathcal{\overline{H}}$ is a kind of NC analogous of the standard Horn class
$\mathcal{{H}}$.

###  4.4 The Definition of $\mathcal{\overline{H}}_{\Sigma}$

Finally, from $\mathcal{\overline{H}}$, we straightforwardly define the class
$\mathcal{\overline{H}}_{\Sigma}$ of possibilistic Horn-NC bases.

######  Definition 4.19.

A possibilistic Horn-NC formula is a pair $\langle\varphi:\alpha\rangle$,
where $\varphi\in\mathcal{\overline{H}}$ and $\alpha\in(0\ 1]$. A
possibilistic Horn-NC base $\Sigma$ is a set of possibilistic Horn-NC
formulas. $\mathcal{\overline{H}}_{\Sigma}$ denotes the class of possibilistic
Horn-NC bases.

######  Example 4.20.

We take the next Horn-NCs: $\varphi$ from Example 4.5 and $\varphi_{9}$ from
Example 4.14. By $\varphi^{\prime}$ we denote $\varphi$ from Example 4.15
considering that the specified conditions warranting that $\varphi$ is Horn-NC
are met. An example of a possibilistic Horn-NC base is:

$\\{\,\langle P\,:\,{\bf.8}\rangle,\ \langle\varphi\,:\,{\bf.8}\rangle,\
\langle\varphi_{9}\,,\,{\bf.5}\rangle,\
\langle\varphi^{\prime}\,,\,{\bf.9}\rangle,\ \langle\neg
Q\,,\,{\bf.1}\rangle\,\\}.$

######  Corollary 4.21.

$\mathcal{\overline{H}}_{\Sigma}$ and $\mathcal{{H}}_{\Sigma}$ are
semantically equivalent: each formula in a class is equivalent to some formula
in the other class.

  * Proof.

It follows from the definitions of $\mathcal{\overline{H}}_{\Sigma}$ and
$\mathcal{{H}}_{\Sigma}$ and Theorem 4.17. $\blacksquare$

######  Corollary 4.22.

$\mathcal{\overline{H}}_{\Sigma}$ is the next $\mathcal{NC}_{\Sigma}$
fragment: if $\langle\varphi:\alpha\rangle\in\mathcal{NC}_{\Sigma}$ and
applying $\wedge/\vee$ distributivity to $\varphi$ results in a Horn formula,
then $\langle\varphi:\alpha\rangle\in\mathcal{\overline{H}}_{\Sigma}$.

###### Proof.

It follows from the definitions of $\mathcal{\overline{H}}_{\Sigma}$ and
$\mathcal{NC}_{\Sigma}$ and Theorem 4.18. ∎

Remark. Since $\mathcal{\overline{H}}$ is the NC analogous of $\mathcal{{H}}$
so is $\mathcal{\overline{H}}_{\Sigma}$ of $\mathcal{{H}}_{\Sigma}$.

##  5 Possibilistic NC Unit-Resolution $\mathcal{UR}_{\Sigma}$

Possibilistic clausal resolution was defined in the 1980s [23, 24] but
possibilistic non-clausal resolution has not been proposed yet. This section
is a step forward towards its definition as we define Possibilistic Non-
Clausal Unit-Resolution, denoted $\mathcal{UR}_{\Sigma}$, which is an
extension of the calculus presented in [40] for propositional logic. The main
inference rule of $\mathcal{UR}_{\Sigma}$ is called URΣ, and while the other
rules in $\mathcal{UR}_{\Sigma}$ are simple, URΣ is somewhat involved and so
is presented progressively as follows:

$\bullet$ for quasi-clausal Horn-NC bases in Subsection 5.1; and

$\bullet$ for nested Horn-NC bases in Subsection 5.2.

Afterwards, Subsection 5.3 describes $\mathcal{UR}_{\Sigma}$, which besides
URΣ, comprises: (a) the propositional rule URP, which is URΣ adapted to
propositional logic, (b) the propositional simplification rules, and (c) the
possibilistic rules MinD and MaxN. Subsection 5.4 gives the algorithm to
obtain $\mbox{Inc}(\Sigma)$ which combines $\mathcal{UR}_{\Sigma}$ with
$\alpha$-cuts of the input $\Sigma$. To end this section, Subsection 5.5 gives
two further inferences rules, not needed for warranting the completeness of
$\mathcal{UR}_{\Sigma}$. We recall that $\bot$ and $(\vee)$ are equivalent
(see Definition 2.9).

###  5.1  Quasi-Clausal NC Unit-Resolution

We start our presentation with propositional formulas and then switch to
possibilistic bases. Assume propositional formulas with the quasi-clausal
pattern below in which
${{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\ell}}$
and
${{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\neg{\ell}}}$
are any literal and its negated one, and the $\varphi$’s and the $\phi$’s are
formulas:

$\\{{{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\wedge}}\
\varphi_{1}\,\ldots\,\varphi_{l-1}\
{{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\ell}}\
\varphi_{l+1}\,\ldots\,\varphi_{i-1}\
({{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\vee}}\
\,\phi_{1}\,\ldots\,\phi_{j-1}\
{{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\neg{\ell}}}\
\phi_{j+1}\,\ldots\,\phi_{k})\ \varphi_{i+1}\,\ldots\,\varphi_{n}\\}$

We say that these formulas are quasi-clausal because if the $\varphi$’s and
$\phi$’s were clauses and literals, respectively, then such formulas would be
clausal. It is not hard to see that a quasi-clausal formula is equivalent to a
formula of the kind:

$\\{{{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\wedge}}\
\varphi_{1}\,\ldots\,\varphi_{l-1}\
{{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\ell}}\
\varphi_{l+1}\,\ldots\,\varphi_{i-1}\
({{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\vee}}\
\phi_{1}\,\ldots\,\phi_{j}\,\phi_{j+1}\,\ldots\,\phi_{k})\
\varphi_{i+1}\,\ldots\,\varphi_{n}\\}$

and thus, one can derive the next simple inference rule for propositional
formulas:

$\frac{{{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\ell}}\
{{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\wedge}}\
({{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\vee}}\ \
\phi_{1}\,\ldots\,\phi_{j}\
{{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\neg{\ell}}}\
\phi_{j+1}\,\ldots\,\phi_{k})}{({{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\vee}}\
\ \phi_{1}\,\ldots\,\phi_{j}\ \phi_{j+1}\,\ldots\,\phi_{k})}$ (1)

Notice that for clausal formulas, Rule (1) coincides with clausal unit-
resolution.

Now let us switch to possibilistic bases. The setting in which NC unit-
resolution is applicable is when $\Sigma$ has two Horn-NC formulas such that
one is a unit clause
$\langle{{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\ell}}:\alpha\rangle$
and the other has the pattern: $\langle\,\\{\wedge\
\varphi_{1}\,\ldots\,\varphi_{i}\
({{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\vee}}\
\,\phi_{1}\,\ldots\,\phi_{j-1}\
{{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\neg{\ell}}}\
\phi_{j+1}\,\ldots\,\phi_{k})\
\varphi_{i+1}\,\ldots\,\varphi_{n}\\}:\beta\,\rangle$. Namely, as $\Sigma$ is
an implicit conjunction of its formulas, then $\Sigma$ contains a conjunction:

$\langle{{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\ell}}:\alpha\rangle\wedge\langle\,\\{\wedge\
\varphi_{1}\,\ldots\,\varphi_{i-1}\
({{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\vee}}\
\,\phi_{1}\,\ldots\,\phi_{j-1}\
{{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\neg{\ell}}}\
\phi_{j+1}\,\ldots\,\phi_{k})\
\varphi_{i+1}\,\ldots\,\varphi_{n}\\}:\beta\,\rangle$ (2)

In this setting and by using Min-Decomposability, i.e.
$N(\varphi\wedge\psi)=\mathrm{min}(N(\varphi),N(\psi))$ (Definition 3.2), one
can easily derive the next possibilistic inference:

$\frac{\langle{{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\ell}}\,:\,\alpha\rangle\
{{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\wedge}}\
\langle\,({{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\vee}}\
\ \phi_{1}\,\ldots\,\phi_{j}\
{{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\neg{\ell}}}\
\phi_{j+1}\,\ldots\,\phi_{k})\,:\,\beta\rangle}{\langle\,({{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\vee}}\
\ \phi_{1}\,\ldots\,\phi_{j}\ \phi_{j+1}\,\ldots\,\phi_{k})\,:\,\mathrm{\bf
min}\\{\alpha,\beta\\}\,\rangle}$ (3)

The soundness of (3) follows immediately from the property Min-
Decomposability. If
$\mathcal{D}({{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\neg{\ell}}})$
stands for $(\vee\ \phi_{1}\,\ldots\,\phi_{j}\,\phi_{j+1}\,\ldots\,\phi_{n})$,
then the previous rule can be concisely rewritten as:

$\frac{\langle{{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\ell}}\,:\,\alpha\rangle\
\,{{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\wedge}}\
\,\langle\,({{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\vee}}\
\,{{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\neg{\ell}}}\
\,\mathcal{D}({{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\neg{\ell}}})\,)\,:\beta\rangle}{\langle\mathcal{D}({{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\neg{\ell}}})\,:\,\mathrm{\bf
min}\\{\alpha,\beta\\}\,\rangle}{{\mbox{\,}}}$ (4)

Notice that the previous rule amounts to substituting the formula referred to
by the right conjunct in the numerator with the formula in the denominator,
and in practice, to just eliminate
${{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\neg{\ell}}}$
and update the necessity weight. Let us illustrate these notions.

######  Example 5.1.

Let $\Sigma$ be a base including $\varphi_{1}$ and $\varphi_{2}$ below, where
$\phi$ is a formula:

  * •

$\varphi_{1}=\langle{{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}P}}:{\bf.8}\rangle$

  * •

$\varphi_{2}=\langle\,\\{{{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\wedge}}\
\phi\ (\vee\ \ \neg{R}\ \
{{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\neg{P}}}\
\ S\,)\ \ (\vee\ \ S\ \ \\{\wedge\ \ \neg{Q}\ \ \neg{P}\,\\}\,)\ \
R\,\\}\,:\,{\bf.6}\rangle.$

Taking
${{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}P}}$ in
$\varphi_{1}$ and the left-most
${{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\neg{P}}}$
in $\varphi_{2}$, we have
$\mathcal{D}({{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\neg{P}}})=(\vee\
\neg{R}\ S)$, and by applying

$\Sigma\leftarrow\Sigma\,\cup\,\langle\,\\{{{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}\wedge}}\
\,\phi\ \,(\vee\ \ \neg{R}\ \ S\,)\ \ (\vee\ \ S\ \ \\{\wedge\ \ \neg{Q}\ \
\neg{P}\,\\}\,)\ \ R\,\\}\,:\,{\bf.6}\,\rangle.$

Rule (4) to $\varphi_{2}$, the above formula is deduced and added to the base
$\Sigma$. ∎

We now extend our analysis from formulas with pattern
$\langle\,({{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\vee}}\
\,{{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\neg{\ell}}}\
\,\mathcal{D}({{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\neg{\ell}}})\,):\beta\rangle$
to formulas with pattern
$\langle\,({{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\vee}}\
\
\mathcal{C}({{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\neg{\ell}}})\
\
\mathcal{D}({{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\neg{\ell}}})\,):\beta\,\rangle$
wherein
$\mathcal{C}({{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\neg{\ell}}})$
is the maximal sub-formula that becomes false when
${{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\neg{\ell}}}$
is false, namely,
$\mathcal{C}({{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\neg{\ell}}})$
is: $(i)$ the maximal sub-formula, and $(ii)$ equivalent to a conjunction of
the kind
${{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\neg{\ell}}}\,\wedge\,\psi$.
In other words,
$\mathcal{C}({{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\neg{\ell}}})$
is the maximal sub-formula ”conjunctively linked” to
${{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\neg{\ell}}}$.

For instance If the input base $\Sigma$ contains
$\langle{{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}{\ell}}}:\alpha\rangle$
and another formula of the kind:

$\langle\ (\vee\ \varphi_{1}\quad\\{\wedge\ \phi_{1}\ \\{\wedge\
{{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\neg{\ell}}}\
(\vee\ \ \phi_{2}\ \neg{P}\,)\\}\ \phi_{3}\\}\quad\varphi_{2}):\beta\ \rangle$

then
$\mathcal{C}({{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\neg\mathcal{\ell}}})=\\{\wedge\
\phi_{1}\ \\{\wedge\
{{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\neg{\ell}}}\
(\vee\ \ \phi_{2}\ \neg{P}\,)\\}\ \phi_{3}\,\\}$ because:

$(ii)$
$\mathcal{C}({{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\neg\mathcal{\ell}}})$
is equivalent to
${{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\neg{\ell}}}\wedge\psi={{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\neg{\ell}}}\wedge\\{\wedge\
\phi_{1}\ (\vee\ \phi_{2}\ \neg{P}\,)\ \phi_{3}\\}$; and

$(i)$ no sub-formula
$\mathcal{C}^{\prime}({{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\neg\mathcal{\ell}}})$
bigger than
$\mathcal{C}({{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\neg\mathcal{\ell}}})$
verifies
$\mathcal{C}^{\prime}({{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\neg\mathcal{\ell}}})\equiv{{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\neg{\ell}}}\wedge\psi^{\prime}$.

Clearly, if
${{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\neg{\ell}}}$
becomes false so does
$\mathcal{C}({{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\neg\mathcal{\ell}}})=\\{\wedge\
\phi_{1}\ \\{\wedge\
{{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\neg{\ell}}}\
(\vee\ \ \phi_{2}\ \neg{P}\,)\\}\ \phi_{3}\,\\}$.

Remark.
$\mathcal{C}({{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\neg{\ell}}})$
contains
${{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\neg{\ell}}}$
but
$\mathcal{D}({{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\neg{\ell}}})$
excludes it.

######  Example 5.2.

The formula given below is an extension of $\varphi_{2}$ from Example 5.1, in
which, by clarity, its previous sub-formula $(\vee\ S\ \\{\wedge\ \neg{Q}\
\neg{P}\,\\}\,)$ is denoted $\phi_{1}$ and the previous literal
${{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\neg{P}}}$
is now extended to the formula $\\{\wedge\
{{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\neg{P}}}\
(\vee\ S\ \neg{R})\,\\}$ including
${{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\neg{P}}}$:

$\varphi=\langle\,\\{{{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\wedge}}\
\phi\ (\vee\ \neg{R}\ \\{\wedge\
{{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\neg{P}}}\
(\vee\ S\ \neg{R})\,\\}\ \ S\,)\ \ \phi_{1}\ \ R\,\\}\,:\,{\bf.6}\,\rangle$

Taking the left-most
${{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\neg{P}}}$
($\phi_{1}$ has also another literal ${\neg{P}}$), $\varphi$ has a sub-formula
with pattern
$({{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\vee}}\
\mathcal{C}({{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\neg{P}}})\
\mathcal{D}({{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\neg{P}}})\,)$,
in which
$\mathcal{C}({{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\neg{P}}})=\\{\wedge\
{{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\neg{P}}}\
\ (\vee\ S\ \neg{R})\,\\}$ and
$\mathcal{D}({{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\neg{P}}})=(\vee\
\,\neg{R}\ S).$ ∎

Regarding the inference rule, we have that when $\Sigma$ has both a unitary
clause
$\langle{{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\ell}}\,:\,\alpha\rangle$
and another formula $\langle\varphi:\beta\rangle$ such that $\varphi$ has the
pattern
$({{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\vee}}\
\,\mathcal{C}({{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\neg{\ell}}})\
\,\mathcal{D}({{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\neg{\ell}}})\,)$,
then the possibilistic NC unit-resolution rule is easily obtained by extending
Rule (4) as follows:

$\frac{\langle{{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\ell}}\,:\,\alpha\rangle\
\,{{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\wedge}}\
\,\langle\,({{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\vee}}\
\,\mathcal{C}({{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\neg{\ell}}})\
\,\mathcal{D}({{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\neg{\ell}}})\,)\,:\beta\,\rangle}{\langle\,\mathcal{D}({{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\neg{\ell}}}\,)\,:\,\mathrm{\bf
min}(\alpha,\beta)\,\rangle}{{\mbox{\,}}}$ (5)

The soundness of (5) follows from
${{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\ell}}\wedge\mathcal{C}({{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\neg{\ell}}})\equiv\bot$
and its proof is given in Section 7. Fig. 3 depicts Rule (5) where the left
and right trees represent, respectively, the numerator and denominator of (5).

$\wedge$$\langle{{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\ell}}:\alpha\rangle\
\
$$\langle{{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\vee}}:\beta\rangle$$\mathcal{C}({{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\neg{\ell}}})$$\mathcal{D}({{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\neg{\ell}}})$

$\wedge$$\langle{{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\ell}}:\alpha\rangle\
\ $$\ \
\langle{{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\vee}}:\mathrm{\bf
min}(\alpha,\beta)\rangle$$\mathcal{D}({{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\neg{\ell}}})$

Fig. 3. Depicting Rule (5).

######  Example 5.3.

Rule (5) with
$\varphi_{1}=\langle{{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}P}}:{\bf.3}\rangle$
and with $\varphi$ from Example 5.2 derives:

$\Sigma\leftarrow\Sigma\,\cup\,\langle\,\\{{{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}\wedge}}\
\,\phi\ \,(\vee\ \,\neg{R}\ S\,)\ \ \phi_{1}\ \ R\,\\}\,:\,{\bf.3}\,\rangle.$

###  5.2 Nested NC Unit-Resolution

Coming back to the almost-clausal formulas expressed in (2) and extending its
literal
${{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\neg{\ell}}}$
to
$\mathcal{C}({{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\neg{\ell}}})$,
we now rewrite them compactly as indicated below, where $\Pi$ and
$\Pi^{\prime}$ denote a concatenation of formulas, namely
$\Pi=\varphi_{1}\ldots\varphi_{i-1}$ and
$\Pi^{\prime}=\varphi_{i+1}\ldots\varphi_{n}$:

$\langle{{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\ell}}\,:\,\alpha\rangle\wedge\langle\
\\{{{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\wedge}}\
\,\Pi\
\,({{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\vee}}\
\mathcal{C}({{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\neg{\ell}}})\
\mathcal{D}({{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\neg{\ell}}})\,)\
\,\Pi^{\prime}\\}:\beta\ \rangle$

We now analyze the nested Horn-NC bases $\Sigma$ to which NC unit-resolution
can be indeed applied. That is, $\Sigma$ must have a unit-clause
$\langle{{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\ell}}\,:\,\alpha\rangle$
and a possibilistic nested Horn-NC formula, denoted $\langle\Pi:\beta\rangle$,
with a syntactical pattern of the next kind444The notation $[\odot\
\varphi_{1}\ldots\varphi_{k}]$ was introduced in Definition 2.3, bottom.:

$\langle\ [\odot_{1}\ \,\Pi_{1}\ \ldots\ \ [\odot_{k}\ \ \Pi_{k}\
\,({{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\vee}}\
\mathcal{C}({{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\neg{\ell}}})\
\mathcal{D}({{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\neg{\ell}}})\,)\
\,\Pi^{\prime}_{k}\,]\ \ \ldots\ \,\Pi^{\prime}_{1}\,]:\beta\ \rangle$

where all the $\Pi_{j}$’s and $\Pi_{j}^{\prime}$’s are concatenations of
formulas, e.g. for the nesting level $j,1\leq j\leq k$, we have
$\Pi_{j}=\varphi_{j_{1}}\ldots\varphi_{j_{i-1}}$ and
$\Pi^{\prime}_{j}=\varphi_{j_{i+1}}\ldots\varphi_{j_{n_{j}}}$. Since the
presence of formulas in the base $\Sigma$ means that they are conjunctively
linked, then one has:

$\langle{{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\ell}}\,:\,\alpha\rangle\wedge\
\langle\ [\odot_{1}\ \,\Pi_{1}\ \ldots\ \ [\odot_{k}\ \ \Pi_{k}\
\,({{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\vee}}\
\mathcal{C}({{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\neg{\ell}}})\
\mathcal{D}({{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\neg{\ell}}})\,)\
\,\Pi^{\prime}_{k}\,]\ \ \ldots\ \,\Pi^{\prime}_{1}\,]:\beta\ \rangle$ (6)

By following the same principle that led us to Rule (5) and taking into
account that
$N(\varphi_{1}\wedge\varphi_{2})=\mbox{min}\\{N(\varphi_{1}),N(\varphi_{1})\\}$,
one obtains the nested NC unit-resolution rule:

$\frac{\langle{{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\ell}}\,:\,\alpha\rangle\wedge\
\langle\,[\odot_{1}\
\Pi_{1}\ldots[\odot_{k}{{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\
}\ \Pi_{k}\ \
({{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\vee}}\ \
\mathcal{C}({{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\neg{\ell}}})\
\
\mathcal{D}({{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\neg{\ell}}})\,)\
\ \Pi^{\prime}_{k}\,]}\ldots\,\Pi^{\prime}_{1}]:\beta\ \rangle}{\langle\
[\odot_{1}\
\Pi_{1}\ldots[\odot_{k}{{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\
}\ \Pi_{k}\ \
\mathcal{D}({{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\neg{\ell}}})\
\ \Pi^{\prime}_{k}\,]}\ldots\,\Pi^{\prime}_{1}]:\mbox{\bf
min}\\{\alpha,\beta\\}\ \rangle}{\ \mbox{}}$ (7)

Recapitulating, Rule (7) indicates that if the Horn-NC $\Sigma$ has two
formulas such that one is a unit clause
$\langle{{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\ell}}\,:\,\alpha\rangle$
and the other $\langle\Pi:\beta\rangle$ has the pattern of the right conjunct
in the numerator, then $\Pi$ can be replaced with the formula in the
denominator. In practice, applying (7) amounts to just removing
$\mathcal{C}({{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\neg{\ell}}})$
from $\Pi$ and updating the necessity weight.

We now denote $\Pi$ the right conjunct in the numerator of (7) and by
$\Pi\succ({{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\vee}}\
\mathcal{C}({{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\neg{\ell}}})\
\mathcal{D}({{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\neg{\ell}}})\,)$
denote that
$({{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\vee}}\
\mathcal{C}({{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\neg{\ell}}})\
\mathcal{D}({{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\neg{\ell}}})\,)$
is a sub-formula of $\Pi$. Rule (7) above can be compacted, giving rise to a
more concise formulation of URΣ:

$\displaystyle\frac{\langle{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\ell}:\alpha\rangle\
{{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\wedge}}\
\langle\
\Pi\succ({{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\vee}}\
\
\mathcal{C}({{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\neg\ell}})\
\
\mathcal{D}({{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\neg\ell}})\,):\beta\
\rangle}{\langle\
\Pi\succ\mathcal{D}({{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\neg\ell}}):\mathrm{\bf
min}\\{\alpha,\beta\\}\ \rangle}{\mbox{\,{\em UR${}_{\Sigma}$}}}$

The soundness of the rule URΣ follows from
${{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\ell}}\wedge\mathcal{C}({{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\neg{\ell}}})\equiv\bot$
and is proven in Section 7. Two simple examples illustrating how URΣ works are
Examples 6.1 and 6.2. Two more complete examples are Examples 6.5 and 6.6 but
they employ other inferences and mechanisms relative to
$\mathcal{UR}_{\Sigma}$ given in the remaining of this section.

Remark. It is not difficult to check that, for clausal formulas, URΣ coincides
with the standard possibilistic clausal unit-resolution [22, 26]. This
clausal-like formulation of NC unit-resolution contrasts with the functional-
like one of classical NC resolution handled until now in the literature and
presented in [46] (see also [5]). We believe that our version, as previously
said, is more suitable to understand, implement and formally analyze.

###  5.3 The Calculus $\mathcal{UR}_{\Sigma}$

Besides URΣ, the calculus $\mathcal{UR}_{\Sigma}$ also includes the rules: (a)
propositional NC unit-resolution, or URP, which is URΣ but applied inside
propositional formulas, (b) the rules to simplify propositional formulas, and
(c) the possibilistic rules Min-Decomposability (MinD) and Max-Necessity
(MaxN) mentioned in Definition 3.2.

####  5.3.1 Propositional NC Unit-Resolution

A major difference between computing the inconsistency degree of clausal and
non-clausal bases is that the unity members of the former, i.e. clauses, are
always consistent, while a non-clausal formula can itself be inconsistent.
That is, the input $\Sigma$ can contain a formula $\langle\Pi:\alpha\rangle$
where $\Pi$ is inconsistent, and if so, $\langle\Pi:\alpha\rangle$ is
equivalent to $\langle\bot:\alpha\rangle$, which brings to:

######  Proposition 5.4.

If $\langle\Pi:\alpha\rangle\in\Sigma$ and $\Pi$ is inconsistent then
$\mathrm{Inc}(\Sigma)\geq\alpha$.

  * Proof.

By definition
$\mathrm{Inc}(\Sigma)=\mathrm{max}\\{\beta\,|\,\Sigma_{\geq\beta}\mbox{ is
inconsistent}\\}$. Trivially if $\Pi$ is inconsistent then
$\bot\in\Sigma_{\geq\alpha}$, and thus, $\Sigma_{\geq\alpha}$ is inconsistent.
So $\mathrm{Inc}(\Sigma)\geq\alpha$. $\blacksquare$

Hence, first of all, the propositional formula $\Pi$ of each
$\langle\Pi:\alpha\rangle\in\Sigma$ must be checked for consistency. If $\Pi$
is inconsistent, then, by definition, $\mathrm{Inc}(\Sigma)$ is the maximum of
$\alpha$ and the inconsistency degree of the strict $\alpha$-cut of $\Sigma$.
Thus, one can remove from $\Sigma$ all formulas $\langle\Pi:\beta\rangle$ such
that $\beta\leq\alpha$ and search whether $\mathrm{Inc}(\Sigma_{>\alpha})>0$.

The inference rule URP testing the consistency of a propositional $\Pi$, where
$\langle\Pi:\alpha\rangle\in\Sigma$, is easily derived from URΣ by considering
that the conjunction of a unit clause
${{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}{\ell}}}$
and of a formula $\Pi$ containing
$\mathcal{C}({{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\neg{\ell}}})$
happens inside $\Pi$. Thus URP is as follows:

$\displaystyle\frac{\langle\
{{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\ell}}\
{{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\wedge}}\
\Pi\succ({{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\vee}}\
\
\mathcal{C}({{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\neg{\ell}}})\
\
\mathcal{D}({{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\neg{\ell}}})\,):\alpha\
\rangle}{\langle\
\Pi\succ\mathcal{D}({{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\neg{\ell}}}):\alpha\rangle}{\mbox{\em
UR${}_{P}$}}$ (8)

A complete example through which we show how URP proceeds testing the
consistency of propositional NC formulas is Example 6.3 in the next section,
and Example 6.4 illustrates the effects of applying Proposition 5.4.

####  5.3.2 Simplification Formulas Rules

Each application of the previous URΣ and URP demands the subsequent
application of trivial logical simplifications of propositional formulas. For
instance, $(\vee\ \varphi\ (\vee\ P\ (\vee\ \neg R\ \phi)))$ and $(\vee\ P\
\\{\wedge\ (\vee)\ \varphi\\})$ can be obviously substituted by $(\vee\
\varphi\ P\ \neg R\ \phi)$ and $P$, respectively. Next we formalize such kind
of simplification rules. Being $\Pi$ the propositional formula of a
possibilistic formula $\langle\Pi:\alpha\rangle$ in a base $\Sigma$, the first
two rules below simplify formulas by (upwards) propagating $(\vee)$ from sub-
formulas to formulas:

$\frac{\langle\
\Pi\succ\,({{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}\vee}}\
\
\phi_{1}\ldots\phi_{i-1}\,(\vee)\,\phi_{i+1}\ldots\phi_{k}\,):\alpha\rangle}{\langle\
\Pi\succ({{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}\vee}}\
\ \phi_{1}\ldots\phi_{i-1}\,\phi_{i+1}\ldots\phi_{k}\,):\alpha\
\rangle}{{\bf\bot}\vee}$

$\frac{\langle\
\Pi\succ\\{{{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}\wedge}}\
\
\varphi_{1}\ldots\varphi_{i-1}\,(\vee)\,\varphi_{i+1}\ldots\varphi_{k}\,\\}:\alpha\rangle}{\langle\
\Pi\succ\,(\vee):\alpha\ \rangle}{{\bf\bot}\wedge}$

The next two rules remove redundant connectives. The first one removes a
connective $\odot$ if it is applied to a single formula, i.e. $[\odot\
\phi_{1}]$, and the second one removes a connective if it is inside another
equal connective, i.e. applies to sub-formulas with the pattern
$[{{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}\odot_{1}}}\
\ \varphi_{1}\ldots\varphi_{i-1}\,[\odot_{2}\
\phi_{1}\ldots\phi_{n}\,]\,\varphi_{i+1}\ldots\varphi_{k}\,],\odot_{1}=\odot_{2}$.
So the formal rules are:

$\frac{\langle\
\Pi\succ[{{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}\odot_{1}}}\
\ \varphi_{1}\ldots\varphi_{i-1}\,[\,\odot_{2}\
\phi_{1}\,]\,\varphi_{i+1}\ldots\varphi_{k}\,]:\alpha\rangle}{\langle\
\Pi\succ[{{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}\odot_{1}}}\
\
\varphi_{1}\ldots\varphi_{i-1}\,\phi_{1}\,\varphi_{i+1}\ldots\varphi_{k}\,]:\alpha\rangle}{\,\odot\phi}$

$\frac{\langle\
\Pi\succ[{{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}\odot_{1}}}\
\ \varphi_{1}\ldots\varphi_{i-1}\,[\odot_{2}\
\phi_{1}\ldots\phi_{n}\,]\,\varphi_{i+1}\ldots\varphi_{k}\,]:\alpha\
\rangle,\odot_{1}=\odot_{2}}{\langle\
\Pi\succ[{{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}\odot_{1}}}\
\
\varphi_{1}\ldots\varphi_{i-1}\,\phi_{1}\ldots\phi_{n}\,\varphi_{i+1}\ldots\varphi_{k}\,]:\alpha\
\rangle}{\,\odot\odot}$

####  5.3.3 Possibilistic Rules

We recall the possibilistic rules in Definition 3.2. We pay attention to the
case in which a conjunction $\langle\,\\{\wedge\ \
\varphi_{1}\ldots\varphi_{i}\ldots\varphi_{k}\\}:\alpha\rangle$ is deduced. It
is clear that, in this case, we can deduce that the necessity weight of each
individual conjunct $\varphi$ is $\alpha$:

$\frac{\langle\,\\{\wedge\ \
\varphi_{1}\ldots\varphi_{i}\ldots\varphi_{k}\\}:\alpha\rangle}{\\{\langle\varphi_{1}:\alpha\rangle,\ldots,\langle\varphi_{i}:\alpha\rangle,\ldots,\langle\varphi_{k}:\alpha\rangle\\}}{\mbox{\em\
\text@underline{MinD}}}$

The last needed rule to be included in $\mathcal{UR}_{\Sigma}$ is MaxN:

$\langle\varphi:\alpha\rangle,\langle\varphi:\beta\rangle\vdash\langle\varphi:\mbox{max}\\{\alpha,\beta\\}\rangle\quad\mbox{\em\text@underline{MaxN}}$

####  5.3.4 The Calculus $\mathcal{UR}_{\Sigma}$

The calculus $\mathcal{UR}_{\Sigma}$ is composed of all the above inference
rules:

######  Definition 5.5.

We define $\mathcal{UR}_{\Sigma}$ as the calculus formed by URΣ, URP, the
rules MinD and MaxN, and the simplification rules, namely

$\mathcal{UR}_{\Sigma}=\\{\mbox{UR}_{\Sigma},\mbox{UR}_{P},\mbox{MinD},\mbox{MaxN},{\bf\bot}\vee,{\bf\bot}\wedge,\odot\,\phi,\odot\odot\,\\}.$

Examples 6.1 and 6.2 are simple examples of how $\mathcal{UR}_{\Sigma}$
proceeds. Example 6.5, and its continuation Example 6.6, are quite complete
examples. Example 6.5 illustrates how $\mathcal{UR}_{\Sigma}$ searches for
just one empty clause $\langle\bot:\alpha\rangle$ and Example 6.6 determines
$\mbox{Inc}(\Sigma)$.

Remark. Having established possibilistic NC unit-resolution, the procedure NC
unit-propagation for possibilistic NC formulas can be designed, and on top of
it, the possibilistic NC DPLL scheme can be defined.

###  5.4 Finding $\mbox{Inc}(\Sigma)$

The calculus $\mathcal{UR}_{\Sigma}$ determines just one sub-set of
contradictory formulas along with its inconsistency degree. Yet, a given
$\Sigma$ can typically contain many contradictory subsets, each of them
induces the deduction of one empty clause $\langle\bot:\alpha\rangle$. By
definition of
$\mbox{Inc}(\Sigma)=\mbox{max}\\{\alpha:\Sigma_{\geq\alpha}\mbox{is
inconsistent}\\}$ and by Proposition 3.4, we have that:

$\mbox{Inc}(\Sigma)=\mbox{max}\\{\alpha:\Sigma_{\geq\alpha}\mbox{is
inconsistent}\\}=\mbox{max}\\{\alpha\,|\,\Sigma\vdash\langle\bot:\alpha\rangle\\}.$
(9)

Our simple strategy to find $\mbox{Inc}(\Sigma)$ is as follows. Firstly, using
$\mathcal{UR}_{\Sigma}$, we determine one inconsistent subset
$\Sigma_{1}\subseteq\Sigma$ and its $\mbox{Inc}(\Sigma_{1})=\alpha$, which
according to (9), amounts to deducing $\langle\bot:\alpha\rangle$. In the
future, we are only interested in knowing whether $\mbox{Inc}(\Sigma)>\alpha$
and so, for that, we require only the strict $\alpha$-cut of $\Sigma$, i.e.
$\Sigma_{>\alpha}$. Again using $\mathcal{UR}_{\Sigma}$, we attempt to deduce
$\langle\bot:\beta\rangle$ and, if it is obtained, continue with
$\Sigma_{>\beta}$. These operations are recursively performed until getting a
consistent base, i.e. the empty clause is no longer deduced. Then the
$\alpha$-cut of the last inconsistent base is the sought $\mbox{Inc}(\Sigma)$.
This process is algorithmically described below. Find should be called with
Inc = 0.

Find($\Sigma$, Inc)

  1. (1)

Apply $\mathcal{UR}_{\Sigma}$ to $\Sigma$ and if $\langle\bot:\alpha\rangle$
is derived then go to (2) else Return Inc.

  2. (2)

We search whether there exists $\beta>\alpha$ such that $\Sigma_{>\beta}$ is
inconsistent. Thus, we update $\Sigma\leftarrow\\{\langle\varphi:\beta\rangle\
|\ \langle\varphi:\beta\rangle\in\Sigma,\ \beta>\alpha\\}$ and ${\bf
Inc}\leftarrow\alpha$; and call Find($\Sigma$, Inc).

The value Inc returned by Find is $\mbox{Inc}(\Sigma)$, which is proven in
Section 7. If Inc = 0 then the input $\Sigma$ is consistent. In Example 6.6,
we illustrate the algorithmic strategy of Find.

###  5.5 Further Inferences Rules

This last subsection presents two further inferences rules no required to
ensure completeness but, since they allow shorter proofs, their appropriate
management can yield significant speed-ups. These two rules are: Propositional
NC Local Unit-Resolution and Possibilistic NC Hyper Unit-Resolution.

####  5.5.1 Propositional NC Local-Unit-Resolution

$\mbox{UR}_{P}$ could also apply to propositional sub-formulas and can be used
in the general framework of non-Horn-NC bases. The $\mbox{UR}_{P}$ local
application means that applying $\mbox{UR}_{P}$ to sub-formulas $\varphi$ of
any formula $\Pi$, where $\langle\Pi:\alpha\rangle\in\Sigma$, such that
$\varphi$ has the $\mbox{UR}_{P}$ numerator pattern, should be authorized.
Namely, applying $\mbox{UR}_{P}$ to sub-formulas with pattern
$\varphi={{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\ell}}\
{{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\wedge}}\
\Pi\cdot({{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\vee}}\
\mathcal{C}({{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\neg\ell}})\
\mathcal{D}({{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\neg\ell}})\,)$
should be permitted and so, $\varphi$ could be substituted with
${{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\ell}}\
{{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\wedge}}\
\Pi\cdot\mathcal{D}({{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\neg\ell}})$.
Hence, the formal specification of the Propositional NC Local-Unit-Resolution
rule, LUR, for any non-Horn-NC $\varphi$ is:

$\displaystyle\frac{\langle\
\Pi\succ(\,{{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\ell}}\
\ {{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\wedge}}\
\
\varphi\succ({{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\vee}}\
\
\mathcal{C}({{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\neg\ell}})\
\
\mathcal{D}({{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\neg\ell}})\,)\
\ ):\alpha\ \rangle}{\langle\
\Pi\succ(\,{{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\ell}}\
{{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\wedge}}\
\varphi\succ\mathcal{D}({{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\neg\ell}})\,):\alpha\
\rangle}{{\mbox{\em\ \text@underline{LUR}}}}$

This inference rule should be read: if $\langle\Pi:\alpha\rangle\in\Sigma$ and
$\Pi$ has a conjunctive sub-formula with a literal
${\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\ell}$
conjunctively linked to a sub-formula $\varphi$ having pattern
$({{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\vee}}\ \
\mathcal{C}({{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\neg\ell}})\
\
\mathcal{D}({{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\neg\ell}})\,)$,
then its component
$\mathcal{C}({{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\neg\ell}})$
can be eliminated.

An example illustrating the functioning of the previous rule is Example 6.7.

Remark. The introduction of this new rule LUR applicable to certain sub-
formulas habilitates new sequences of inferences, and so, shorter proofs are
now available.

######  Proposition 5.6.

Let $\langle\Pi,\alpha\rangle\in\Sigma$. If applying LUR to $\Pi$ results in
$\Pi^{\prime}$, then $\Pi$ and $\Pi^{\prime}$ are logically equivalent.

  * Proof.

The soundness of LUR follows from that of URP proved in Lemma 7.3.
$\blacksquare$

Remark. The obtaining of the simplification rules for their local application
to sub-formulas is similarly obtained.

####  5.5.2 Possibilistic NC Hyper-Unit-Resolution

The given definition of possibilistic NC unit-resolution, or URΣ, can be
extended in order to obtain Possibilistic NC Hyper-Unit-Resolution (HUR). Then
assume that the possibilistic base has a unit-clause
$\langle{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\ell}:\alpha\rangle$
and two sub-formulas
$({{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\vee}}\ \
\mathcal{C}({{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\neg\ell^{1}}})\
\
\mathcal{D}({{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\neg\ell^{1}}})\,)$
and
$({{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\vee}}\ \
\mathcal{C}({{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\neg\ell^{2}}})\
\
\mathcal{D}({{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\neg\ell^{2}}})\,)$,
where $\neg\ell^{i}$ denotes a specific occurrence of $\neg\ell$. The
simultaneous application of NC unit-resolution with two sub-formulas is
formally expressed as follows:

$\frac{\langle{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\ell}:\alpha\rangle\
{{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\wedge}}\
\langle\Pi^{1}\succ\,({{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\vee}}\
\
\mathcal{C}({{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\neg\ell^{1}}})\
\
\mathcal{D}({{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\neg\ell^{1}}})\,):\beta^{1}\rangle\
{{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\wedge}}\
\langle\Pi^{2}\succ\,({{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\vee}}\
\
\mathcal{C}({{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\neg\ell^{2}}})\
\
\mathcal{D}({{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\neg\ell^{2}}})\,):\beta^{2}\rangle}{\langle\Pi^{1}\succ\mathcal{D}({{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\neg\ell^{1}}}):\mathrm{\bf
min}\\{\alpha,\beta^{1}\\}\,\rangle\,\wedge\,\langle\Pi^{2}\succ\mathcal{D}({{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\neg\ell^{2}}}):\mathrm{\bf
min}\\{\alpha,\beta^{2}\\}\,\rangle}{\mbox{\em}}$

If the sub-formula
$\langle\Pi^{i}\succ({{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}\vee}}\
\mathcal{C}({{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}\neg\ell^{i}}})\
\mathcal{D}({{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}\neg\ell^{i}}})):\beta^{i}\rangle$
is denoted
$\langle\Pi,\mathcal{CD}({{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}\neg\ell}}),\beta\rangle^{i}$,
then HUR for $k$ sub-formulas is formally expressed below, where, for $i,1\leq
i\leq k$, $\beta^{\prime i}=min\\{\alpha,\beta^{i}\\}$.

$\displaystyle\frac{\langle{{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\ell}}:\alpha\rangle\
{{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\wedge}}\
\langle\Pi,\mathcal{CD}({{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\neg\ell}}),\beta\rangle^{1}{{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\wedge}}\ldots{{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\wedge}}\
\langle\Pi,\mathcal{CD}({{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\neg\ell}}),\beta\rangle^{i}\
{{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\wedge}}\,\ldots{{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\wedge}}\
\langle\Pi,\mathcal{CD}({{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\neg\ell}}),\beta\rangle^{k}}{\langle\Pi,\mathcal{D}({{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\ell}}),\beta^{\prime}\rangle^{1}\
{{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\wedge}}\
\ldots\
{{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\wedge}}\
\langle\Pi,\mathcal{D}({{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\ell}}),\beta^{\prime}\rangle^{i}\
{{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\wedge}}\
\ldots\
{{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\wedge}}\
\langle\Pi,\mathcal{D}({{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\neg\ell}}),\beta^{\prime}\rangle^{k}}{\mbox{\em\
\text@underline{HUR}}}$

Since
${{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}\neg\ell^{i}}},1\leq
i\leq k$, are literal occurrences that are pairwise different, so are the sub-
formulas $\mathcal{CD}^{i}$ (and so $\mathcal{D}^{i}$) in the numerator and
denominator of HUR. However, the formulas $\Pi^{i}$ are not necessarily
different; see Example 6.8 for this concrete question and in general for
checking the working of the rule HUR.

Remark. An NC hyper unit-resolution rule, more general than HUR, can be
devised to include simultaneously several unit-clauses so that for each unit-
clause $\langle\ell:\alpha\rangle$ several sub-formulas
$\langle\Pi^{i}\succ({{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}\vee}}\
\mathcal{C}({{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}\neg\ell^{i}}})\
\mathcal{D}({{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}\neg\ell^{i}}})):\beta^{i}\rangle$
can be considered. In other words, one can consider simultaneously $k\geq 2$
unit clauses and so simultaneously apply $k\geq 2$ HUR rules.

##  6 Illustrative Examples

This section gives examples illustrating the notions presented in the previous
sections. Concretely, we provide the next examples:

– Example 6.1: a simple inconsistent possibilistic Horn-NC base.

– Example 6.2: a simple consistent possibilistic Horn-NC base.

– Example 6.3: a complete propositional Horn-NC formula.

– Example 6.4: an input base with an inconsistent propositional formula.

– Example 6.5: a complete possibilistic Horn-NC base.

– Example 6.6: an example showing the strategy of Find.

– Example 6.7: an example of NC Local Unit-Resolution.

– Example 6.8: an example of NC Hyper Unit-Resolution.

Among such examples, we highlight Examples 6.5 and 6.6, which contain a rather
complete Horn-NC base, whose inconsistency degree is obtained in two phases.
The first one is provided in Example 6.5, and the second in Example 6.6. All
inference rules of $\mathcal{UR}_{\Sigma}$ are needed as well as their
combination with the strict $\alpha$-cuts of the input $\Sigma$.

######  Example 6.1.

Let us assume that $\Sigma$ is the next possibilistic Horn-NC base:

$\Sigma=\\{\,\langle P:{\bf.8}\rangle,\ \,\langle\,\Pi_{1}=(\vee\ \ \\{\wedge\
\ \neg P\ \ \neg Q\\}\ \ Q):{\bf.6}\rangle,\ \,\langle\,(\vee\ \neg P\ \neg
Q):{\bf.7}\rangle\\}$

  * •

URΣ with $\langle P:{\bf.8}\rangle$ and $\Pi_{1}$ gives rise to the next
matchings:

– $\ \Pi=\Pi_{1}$

– $\
({{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\vee}}\ \
\mathcal{C}({{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\neg
P}})\
\mathcal{D}({{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\neg
P}})\,)=\Pi_{1}$

– $\
\mathcal{C}({{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\neg
P}})=\\{\wedge\ \ \neg P\ \ \neg Q\\}$

– $\
\mathcal{D}({{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\neg
P}})=Q$

  * •

Hence, URΣ adds: $\Sigma\leftarrow\Sigma\ \cup\ \langle\,(\vee\
\,Q):{\bf.6}\rangle$

  * •

Applying simplifications to the last formula: $\Sigma\leftarrow\Sigma\ \cup\
\langle Q:{\bf.6}\rangle$

  * •

URΣ with $\langle Q:{\bf.6}\rangle$ and with the last formula in the initial
$\Sigma$ gives:

– $\ \Pi=(\vee\ \neg P\ \neg Q)$

– $\
({{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\vee}}\ \
\mathcal{C}({{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\neg
Q}})\
\mathcal{D}({{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\neg
Q}})\,)=\Pi$

– $\
\mathcal{C}({{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\neg
Q}})={{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\neg
Q}}$

– $\
\mathcal{D}({{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\neg
Q}})=\neg P$

  * •

Hence, URΣ adds: $\Sigma\leftarrow\Sigma\ \cup\ \langle\,(\vee\ \neg
P):{\bf.6}\rangle$

  * •

Resolving $\langle P:{\bf.8}\rangle$ in the input $\Sigma$ with the last
formula: $\Sigma\leftarrow\Sigma\ \cup\langle\bot:{\bf.6}\rangle$

  * •

Therefore $\mathcal{UR}_{\Sigma}$ obtains $\mbox{Inc}(\Sigma)={\bf.6}$ ∎

######  Example 6.2.

Let us assume that $\Sigma$ is the next possibilistic Horn-NC base:

$\Sigma=\\{\,\langle Q:{\bf.8}\rangle,\ \,\langle\,\Pi_{1}=(\vee\ \ \neg Q\ \
\\{\wedge\ \ R\ \ (\vee\ \
{{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\neg Q}}\ \
\\{\wedge\ \ S\ \ \neg P\\}\,)\,\\}\,):{\bf.6}\rangle,\ \,\langle\,(\vee\ \neg
P\ \neg Q):{\bf.7}\rangle\\}$

  * •

URΣ with $\langle Q:{\bf.8}\rangle$ and with the rightest
${{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\neg Q}}$
in $\Pi_{1}$ gives the next matchings:

– $\ \Pi=\Pi_{1}$

– $\
({{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\vee}}\ \
\mathcal{C}({{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\neg
Q}})\
\mathcal{D}({{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\neg
Q}})\,)=(\vee\ \
{{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\neg Q}}\ \
\\{\wedge\ \ S\ \ \neg P\\}\,)$

– $\
\mathcal{C}({{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\neg
Q}})={{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\neg
Q}}$

– $\
\mathcal{D}({{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\neg
Q}})=\\{\wedge\ \ S\ \ \neg P\\}$

  * •

Hence, URΣ adds: $\Sigma\leftarrow\Sigma\ \cup\ \langle\,(\vee\ \ \neg Q\ \
\\{\wedge\ \ R\ \ (\vee\ \ \\{\wedge\ \ S\ \ \neg
P\\}\,)\,\\}\,):{\bf.6}\rangle$

  * •

After simplifications: $\Sigma\leftarrow\Sigma\ \cup\ \langle\,(\vee\ \
{{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\neg Q}}\ \
\\{\wedge\ \ R\ \ S\ \ \neg P\,\\}\,):{\bf.6}\rangle$

  * •

Using again $\langle Q:{\bf.8}\rangle$ and the last formula:

– $\ \Pi=(\vee\ \
{{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\neg Q}}\ \
\\{\wedge\ \ R\ \ S\ \ \neg P\,\\}\,)$

– $\
({{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\vee}}\ \
\mathcal{C}({{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\neg
Q}})\
\mathcal{D}({{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\neg
Q}})\,)=\Pi$

– $\
\mathcal{C}({{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\neg
Q}})={{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\neg
Q}}$

– $\
\mathcal{D}({{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\neg
Q}})=\\{\wedge\ \ R\ \ S\ \ \neg P\,\\}$

  * •

Hence, URΣ adds: $\Sigma\leftarrow\Sigma\ \cup\ \langle\,(\vee\ \ \\{\wedge\ \
R\ \ S\ \ \neg P\,\\}\,):{\bf.6}\rangle$

  * •

After simplifications: $\Sigma\leftarrow\Sigma\ \cup\ \langle\,\\{\wedge\ \ R\
\ S\ \ \neg P\,\\}\ :{\bf.6}\rangle$

  * •

Applying the rule MinD: $\Sigma\leftarrow\Sigma\ \cup\\{\langle
R:{\bf.6}\rangle,\langle S:{\bf.6}\rangle,\langle\neg P:{\bf.6}\rangle\\}$.

  * •

Using the first and last formulas in the initial $\Sigma$:
$\Sigma\leftarrow\Sigma\ \cup\ \langle\,(\vee\ \neg P):{\bf.7}\rangle$

  * •

Applying MaxN with $\langle\neg P:{\bf.6}\rangle$ and $\langle\,(\vee\ \neg
P):{\bf.7}\rangle$ the former is eliminated.

  * •

No more resolvents apply.

  * •

The propositional component of $\Sigma$ is consistent, so
$\mbox{Inc}(\Sigma)=0$. ∎

Next, we give a rather elaborated propositional formula and show how the
propositional NC unit-resolution, or URP, together with the simplification
rules, detect its inconsistency.

######  Example 6.3.

Let us assume that the input $\Sigma$ has a possibilistic Horn-NC
$\langle\varphi:\alpha\rangle$ given below, where $\phi_{1}$ and $\phi_{2}$
are assumed to be Horn-NC formulas.

$\langle\ \varphi=\\{\wedge\ \ (\vee\ \ R\ \phi_{1})\ \ (\vee\ \ \neg{P}\ \
\\{\wedge\ \ (\vee\ \ \neg{P}\ \ \neg{R}\,)\quad(\vee\ \ \phi_{2}\ \
\\{\wedge\ \ \neg{Q}\ \
{{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\neg{P}}}\,\\}\,)\
\ R\,\\}\,)\
{{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}P}}\,\\}:\alpha\
\rangle$

The tree associated with $\varphi$ is depicted in Fig. 4, left.

$\wedge:\alpha$$\vee$
$\phi_{1}$
$\vee$$\neg{P}$
$\wedge$$\vee$$\neg{P}$
$\neg{R}$
$\vee$$\phi_{2}$
$\wedge$$\neg{Q}$
$\neg{P}$

$\wedge:\alpha$$\vee$
$\phi_{1}$
$\vee$$\neg{P}$
$\wedge$$\vee$$\neg{P}$
$\neg{R}$
$\vee$$\phi_{2}$

Fig. 4. Formulas $\varphi$ (left) and $\varphi^{\prime}$ (right)

Thus, before computing the inconsistency degree of $\Sigma$, one needs to
check whether its propositional formulas are inconsistent. We show below how
URP checks the inconsistency of $\varphi$. URP with
${{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}P}}$ and
the right-most
${{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\neg{P}}}$
yields the next matchings in the URP numerator:

  * •

$\Pi=(\vee\ \ \neg{P}\ \ \ \\{\wedge\ \ (\vee\ \ \neg{P}\ \ \neg{R}\,)\ \
\,(\vee\ \ \phi_{2}\ \ \\{\wedge\ \ \neg{Q}\ \
{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\neg{P}}\,\\}\,)\,\
\ R\,\\}\,)$

  * •

$(\vee\
\mathcal{C}({\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\neg{P}})\
\mathcal{D}({\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\neg{P}}))=(\vee\
\ \phi_{2}\ \ \\{\wedge\ \ \neg{Q}\ \
{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\neg{P}}\,\\}\,).$

  * •

$\mathcal{C}({\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\neg{P}})=\\{\wedge\
\ \neg{Q}\ \
{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\neg{P}}\,\\}$

  * •

$\mathcal{D}({\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\neg{P}})=\phi_{2}$

Applying URP to $\varphi$ yields:

$\varphi^{\prime}=\langle\ \\{\wedge\ \ (\vee\ \ R\ \phi_{1})\ \ (\vee\ \
\neg{P}\ \ \\{\wedge\ \ (\vee\ \ \neg{P}\ \ \neg{R}\,)\quad(\vee\ \
\phi_{2}\,)\ \ R\,\\}\,)\,\\}:\alpha\ \rangle$

The resulting tree is the right one in Fig. 4. Assume that we proceed now with
a second NC unit-resolution step by picking the same
${{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}P}}$ and
the left-most
${\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\neg{P}}$
(colored blue in Fig. 4, right). Then, the right conjunct of the numerator of
URP is as follows:

  * •

$\Pi=(\vee\
{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\neg{P}}\
(\vee\ \\{\wedge\ \ (\vee\ \neg{P}\ \ \neg{R}\,)\ \ (\vee\ \phi_{2}\,)\ \
R\,\\}\,))$

  * •

$(\vee\
\mathcal{C}({\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\neg{P}})\
\mathcal{D}({\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\neg{P}}))=\Pi$

  * •

$\mathcal{C}({\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\neg{P}})={\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\neg{P}}$

  * •

$\mathcal{D}({\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\neg{P}})=(\vee\
\\{\wedge\ \ (\vee\ \neg{P}\ \ \neg{R}\,)\ \ (\vee\ \phi_{2}\,)\ \ R\,\\}\,)$

By applying URP to $\varphi^{\prime}$, the obtained formula is depicted in
Fig. 5, left:

$\wedge:\alpha$$\vee$
$\phi_{1}$
$\vee$$\wedge$$\vee$$\neg{P}$
$\neg{R}$
$\vee$$\phi_{2}$

$\wedge:\alpha$$\vee$
$\phi_{1}$
$\vee$$\neg{P}$
$\neg{R}$
$\phi_{2}$

Fig. 5. Example 6.3 continued.

After three simplification steps, one gets the formula associated with the
right tree in Fig. 5. Finally, two applications of URP to the two pairs $R$
and $\neg{R}$, and $P$ and $\neg{P}$, lead the calculus to derive
$\langle(\vee):\alpha\rangle$. ∎

In the next example, we illustrate the effects of finding that one of the
propositional formulas of the input base is inconsistent.

######  Example 6.4.

Let $\varphi$ be the formula from Example 6.3 and $\Sigma_{1}$ be $\Sigma$
from Example 6.1 and let us analyze the base
$\Sigma=\Sigma_{1}\cup\\{\langle\varphi:{\bf.6}\rangle\\}$. Then, firstly the
propositional rules of $\mathcal{UR}_{\Sigma}$ are applied to each
propositional Horn-NC in $\Sigma$, and in particular, to
$\langle\varphi:{\bf.6}\rangle$, which, according to Example 6.3, yields
$\langle(\vee):{\bf.6}\rangle$. Then before calling Find, $\Sigma_{1}$ is
reduced to $\Sigma_{1}=\\{\langle P:{\bf.8}\rangle,\ \langle\,(\vee\ \neg P\
\neg Q):{\bf.7}\rangle\\}$ and then Find is called with such $\Sigma_{1}$.
Since $\Sigma_{1}$ is consistent, one can conclude that
$\mathrm{Inc}(\Sigma)={\bf.6}$.

We next give a complete formula and illustrate how $\mathcal{UR}_{\Sigma}$
determines just one inconsistent subset $\Sigma_{1}$ of a Horn-NC base
$\Sigma$ and its degree $\mathrm{Inc}(\Sigma_{1})$. By now, we are not
concerned with finding the maximum inconsistency degree, but just in finding
one inconsistent subset. Later, in Example 6.6, we will illustrate the process
performed by Find to obtain the inconsistency degree $\mathrm{Inc}(\Sigma)$.

######  Example 6.5.

Let us assume that $\Sigma$ is the next possibilistic Horn-NC base:

$\Sigma=\\{\,\langle P:{\bf.8}\rangle,\ \,\langle\,\Pi_{1}:{\bf.6}\rangle,\
\,\langle\,\Pi_{2}:{\bf.5}\rangle,\ \,\langle\,\\{\wedge\ \neg P\ \neg
Q\\}:{\bf.7}\rangle\\}$

wherein the propositional formulas $\Pi_{1}$ and $\Pi_{2}$, both individually
consistent, are as follows:

  * •

$\Pi_{1}=(\vee\ \ \\{\wedge\ \ \neg P\ \ \neg Q\\}\ \ \\{\wedge\ \,Q\ \ P\\})$

  * •

$\Pi_{2}=(\vee\ \ \neg Q\ \ \\{\wedge\ \ R\ \ (\vee\ \ \neg Q\ \ \\{\wedge\ \
S\ \ \neg P\\}\,)\,\\}\,)$

The input base $\Sigma$ is inconsistent and below, we step-by-step provide the
inferences carried out by the calculus $\mathcal{UR}_{\Sigma}$ to derive one
empty formula $\langle\bot:\alpha\rangle$.

  * •

We apply URΣ with $\langle P:{\bf.8}\rangle$ and
$\langle\,\Pi_{1}:{\bf.6}\rangle$ and the next matchings:

– $\ \Pi=\Pi_{1}$

– $\
({{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\vee}}\ \
\mathcal{C}({{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\neg
P}})\ \
\mathcal{D}({{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\neg
P}})\,)=\Pi_{1}$

– $\
\mathcal{C}({{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\neg
P}})=\\{\wedge\ \neg P\ \neg Q\\}$

– $\
\mathcal{D}({{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\neg
P}})=\\{\wedge\ Q\ P\\}$

  * •

Hence, URΣ adds: $\Sigma\leftarrow\Sigma\ \cup\ \langle\,(\vee\ \,\\{\wedge\
Q\ P\\}):{\bf.6}\rangle$

  * •

Simplifying the last formula: $\Sigma\leftarrow\Sigma\ \cup\
\langle\,\\{\wedge\ Q\ P\\}:{\bf.6}\rangle$

  * •

Applying MinD to the last formula: $\Sigma\leftarrow\Sigma\ \cup\ \langle\,Q\
:{\bf.6}\rangle\cup\langle P:{\bf.6}\rangle$

  * •

Since $\langle P:{\bf.8}\rangle,\langle P:{\bf.6}\rangle\in\Sigma$, by MaxN:
$\Sigma\leftarrow\Sigma/\langle P:{\bf.6}\rangle$

  * •

Applying URΣ with $\langle\,Q\ :{\bf.6}\rangle$ and the rightest $\neg Q$ of
$\langle\,\Pi_{2}:{\bf.5}\rangle$:

– $\ \Pi=\Pi_{2}$

– $\
({{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\vee}}\
\mathcal{C}({{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\neg
Q}})\
\mathcal{D}({{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\neg
Q}})\,)=(\vee\
{{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\neg Q}}\
\\{\wedge\ S\ \neg P\\}\,)$

– $\
\mathcal{C}({{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\neg
Q}})={{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\neg
Q}}$

– $\
\mathcal{D}({{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\neg
Q}})=\\{\wedge\ S\ \neg P\\}$

  * •

Thus URΣ adds: $\Sigma\leftarrow\Sigma\ \cup\ \langle\,(\vee\ \,\neg Q\
\,\\{\wedge\ \,R\ \,(\vee\ \,\\{\wedge\ \,S\ \,\neg
P\\}\,)\,\\}\,):{\bf.5}\rangle$

– We denote $\langle\Pi_{3}:{\bf.5}\rangle$ the last added formula.

  * •

Applying URΣ with again $\langle\,Q:{\bf.6}\rangle$ and the last formula
$\langle\Pi_{3}:{\bf.5}\rangle$:

– $\ \Pi=\Pi_{3}$

– $\
({{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\vee}}\ \
\mathcal{C}({{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\neg
Q}})\
\mathcal{D}({{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\neg
Q}})\,)=\Pi_{3}$

– $\
\mathcal{C}({{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\neg
Q}})={{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\neg
Q}}$

– $\
\mathcal{D}({{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\neg
Q}})=\\{\wedge\ \ R\ \ (\vee\ \ \\{\wedge\ \ S\ \ \neg P\\}\,)\,\\}$

  * •

Hence URΣ adds: $\Sigma\leftarrow\Sigma\ \cup\ \langle\,(\vee\ \,\\{\wedge\
\,R\ \ (\vee\ \,\\{\wedge\ \,S\ \,\neg P\\}\,)\,\\}\,):{\bf.5}\rangle$

  * •

Simplifying the last formula: $\Sigma\leftarrow\Sigma\ \cup\
\langle\,\\{\wedge\ \ R\ \ S\ \ \neg P\\}:{\bf.5}\rangle$

  * •

Using the rule InvMinD:

$\Sigma\leftarrow\Sigma\ \cup\
\\{\langle\,R:{\bf.5}\rangle,\langle\,S:{\bf.5}\rangle,\langle\,\neg
P:{\bf.5}\rangle\\}$

  * •

From $\langle\,\neg P:{\bf.5}\rangle$ and the initial $\langle
P:{\bf.8}\rangle$: $\Sigma\leftarrow\Sigma\cup\langle\,(\vee):{\bf.5}\rangle$.

  * •

So the (first) inconsistency degree found is .5. ∎

Next example continues the previous one towards, this time, computing the
proper $\mbox{Inc}(\Sigma)$. This example illustrates the strategy of Find to
do so.

######  Example 6.6.

Let us continue with Example 6.5. Since $\langle\,(\vee):{\bf.5}\rangle$ was
found, for checking whether $\mbox{Inc}(\Sigma)>{\bf.5}$, all possibilistic
formulas whose necessity weight is not bigger than ${\bf.5}$ are useless, that
is, one can obtain the strict .5-cut of $\Sigma$. Thus, the new base is
$\Sigma_{>{\bf.5}}=\Sigma_{1}\cup\Sigma_{2}$, where $\Sigma_{1}$ and
$\Sigma_{2}$ are the strict .5-cut of the initial formulas and of the deduced
formulas, respectively, and which are given below:

$\Sigma_{1}=\\{\,\langle P:{\bf.8}\rangle,\
\,\langle\,\Pi_{1}:{\bf.6}\rangle,\ \,\langle\,\\{\wedge\ \neg P\ \neg
Q\\}:{\bf.7}\rangle\,\\}$ $\Sigma_{2}=\\{\langle\,(\vee\ \,\\{\wedge\ Q\
P\\}):{\bf.6}\rangle,\ \ \langle\,\\{\wedge\ Q\ P\\}:{\bf.6}\rangle,\ \
\langle\,Q\ :{\bf.6}\rangle,\\}$

One can check that the only non-subsumed formula in $\Sigma_{2}$ is
$\langle\,Q\ :{\bf.6}\rangle$. So, $\Sigma_{2}$ is reduced to
$\Sigma_{2}=\\{\langle\,Q\ :{\bf.6}\rangle\\}$. Now, Find newly launches the
process to compute the inconsistency of $\Sigma=\Sigma_{1}\cup\\{\langle\,Q\
:{\bf.6}\rangle\\}$ with ${\bf Inc}={\bf.5}$ and follows the next steps:

  * •

Using $\langle\,Q\ :{\bf.6}\rangle$ and right-most formula in $\Sigma_{1}$
yields: $\langle\,(\vee):{\bf.6}\rangle$.

  * •

The new $\Sigma$ is $\Sigma=\\{\langle P:{\bf.8}\rangle,\langle\,\\{\wedge\
\neg P\ \neg Q\\}:{\bf.7}\rangle\\}$ and the new Inc is .6.

  * •

$\mathcal{UR}_{\Sigma}$ is relaunched and finds
$\langle\,(\vee):{\bf.7}\rangle$.

  * •

The new $\Sigma$ is $\\{\,\langle P:{\bf.8}\rangle\,\\}$ and the new Inc is
.7.

  * •

$\mathcal{UR}_{\Sigma}$ finds $\Sigma$ is consistent.

  * •

Hence Find returns Inc = .7.

Next example illustrates the application of NC Local Unit-resolution, or LUR.

######  Example 6.7.

Consider again the formula $\varphi$ from Example 6.3:

$\langle\ \varphi=\\{\wedge\ \ (\vee\ \ R\ \phi_{1})\ \ (\vee\ \ \neg{P}\ \
\\{\wedge\ \ (\vee\ \ \neg{P}\ \ \neg{R}\,)\quad(\vee\ \ \phi_{2}\ \
\\{\wedge\ \ \neg{Q}\ \
{{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}\neg{P}}}\,\\}\,)\
\ R\,\\}\,)\
{{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}P}}\,\\}:\alpha\
\rangle.$

One can check that its sub-formula

$\phi=(\vee\ \ \neg P\ \ \\{\wedge\ \ (\vee\ \ \neg P\ \
{{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\neg R}})\
\ (\vee\ \ \phi_{2}\ \ \\{\wedge\ \ \neg{Q}\ \
{{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}\neg
P}}\\})\ \
{{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}R}}\\}\,)$

has the pattern of the LUR numerator regarding
${{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\neg R}}$
and ${{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}R}}$.
Thus LUR can be applied and so $\phi$ be replaced, after simplifications, with
$(\vee\ \ \neg P\ \ \\{\wedge\ \ \neg P\ \ (\vee\ \ \phi_{2}\ \ \\{\wedge\ \
\neg Q\ \
{{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}\neg
P}}\\})\ \ R\\})$ in the formula $\varphi$. In this specific example, only one
literal is removed, but in a general case, big sub-formulas may be eliminated.
∎

The next example is devoted to the rule of NC hyper unit-resolution, or HUR.

######  Example 6.8.

Let us reconsider also the formula in previous Example 6.3 (recall that the
$i$ superscript in
${{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\neg{P}^{i}}}$
denotes an specific literal occurrence of
${{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\neg{P}}}$):

$\langle\ \\{\wedge\ \ (\vee\ \ R\ \phi_{1})\ \ (\vee\ \
{{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\neg{P}^{1}}}\
\ \\{\wedge\ \ (\vee\ \
{{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\neg{P}^{2}}}\
\ \neg{R}\,)\quad(\vee\ \ \phi_{2}\ \ \\{\wedge\ \ \neg{Q}\ \
{{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\neg{P}^{3}}}\,\\}\,)\
\ R\,\\}\,)\
{{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}P}}\,\\}:\alpha\
\rangle$

One can apply NC Hyper Unit-Resolution with
${{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}P}}$ and
the three literals
${{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\neg{P}^{i}}}$.
The formula $\Pi$ in the numerator of HUR is the same for the three literals,
so it is noted $\Pi^{1,2,3}$, but the formulas $(\vee\ \
\mathcal{C}(\neg{P}^{i})\ \ \mathcal{D}(\neg{P}^{i}))$ are different and are
given below:

– $\Pi^{1,2,3}=(\vee\ \ \neg{P}\ \ \\{\wedge\ \ (\vee\ \ \neg{P}\ \
\neg{R}\,)\quad(\vee\ \ \phi_{2}\ \ \\{\wedge\ \ \neg{Q}\ \
{{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}\neg{P}}}\,\\}\,)\
\ R\,\\}\,)$

– $(\vee\ \ \mathcal{C}(\neg{P}^{1})\ \ \mathcal{D}(\neg{P}^{1}))=\Pi^{1,2,3}$

– $(\vee\ \ \mathcal{C}(\neg{P}^{2})\ \ \mathcal{D}(\neg{P}^{2}))=(\vee\ \
{{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\neg{P}^{2}}}\
\ \neg{R}\,)$

– $(\vee\ \ \mathcal{C}(\neg{P}^{3})\ \ \mathcal{D}(\neg{P}^{3}))=(\vee\ \
\phi_{2}\ \ \\{\wedge\ \ \neg{Q}\ \
{{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\neg{P}^{3}}}\,\\}\,)$

By applying NC Hyper Unit-Resolution, one gets:

$\langle\ \\{\wedge\ \ (\vee\ \ R\ \phi_{1})\ \ (\vee\ \ \\{\wedge\ \ (\vee\ \
\neg{R}\,)\quad(\vee\ \ \phi_{2}\,)\ \ R\,\\}\,)\
{{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}P}}\,\\}:\alpha\
\rangle$

After simplifying:

$\langle\ \\{\wedge\ \ (\vee\ \ R\ \phi_{1})\ \ \neg{R}\ \ \phi_{2}\ \ R\,\
{{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}P}}\,\\}:\alpha\
\rangle$

Clearly, a simple NC unit-resolution deduces $\langle(\vee):\alpha\rangle$.
Altogether, in this particular example, the rule HUR accelerates considerably
the proof of inconsistency.

##  7 Correctness of $\mathcal{UR}_{\Sigma}$ and Polynomiality of
$\mathcal{\overline{H}}_{\Sigma}$

This section provides the proofs of both, the correctness of
$\mathcal{UR}_{\Sigma}$ to determine the inconsistency degree of
$\mathcal{\overline{H}}_{\Sigma}$ and of the tractability of
$\mathcal{\overline{H}}_{\Sigma}$ (i.e. of Horn-NC-INC, Definition 3.6). Some
proofs, as those of soundness of the simplification rules, are simple and
intuitive and so are omitted. The following formal proofs are provided:

– soundness of quasi-clausal NC unit-resolution (Rule (5));

– soundness of nested NC unit-resolution URΣ;

– correctness of the propositional rules of $\mathcal{UR}_{\Sigma}$;

– correctness of the complete $\mathcal{UR}_{\Sigma}$;

– correctness of the algorithm Find; and

– polynomial complexity of $\mathcal{\overline{H}}_{\Sigma}$.

######  Proposition 7.1.

Rule (5) is sound:

$\langle{{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}\ell}}\,:\,\alpha\rangle\,{{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}\wedge}}\,\langle\,({{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}\vee}}\
\,\mathcal{C}({{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}\neg{\ell}}})\
\,\mathcal{D}({{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}\neg{\ell}}}))\,:\beta\rangle\
\models\
\langle\,\mathcal{D}({{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}\neg{\ell}}}):\mathrm{\bf
min}\\{\alpha,\beta\\}\,\rangle.$

  * Proof.

Denoting
$\mathcal{F}=\langle{{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}\ell}}\,:\,\alpha\rangle\,{{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}\wedge}}\,\langle\,({{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}\vee}}\
\,\mathcal{C}({{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}\neg{\ell}}})\
\,\mathcal{D}({{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}\neg{\ell}}}))\,:\beta\rangle$,
we have:

\- By MinD, $\mathcal{F}\models\ \langle\,({\vee}\ \
{\ell}\wedge\mathcal{C}({\neg{\ell}})\ \
{\ell}\wedge\mathcal{D}({\neg{\ell}})):\mathrm{\bf
min}\\{\alpha,\beta\\}\,\rangle$.

\- Since ${\ell}\wedge\mathcal{C}({\neg{\ell}}\,)\equiv\bot$ then: $\
\mathcal{F}\models\
\langle\,{\ell}\wedge\mathcal{D}({\neg{\ell}}\,):\mathrm{\bf
min}\\{\alpha,\beta\\}\,\rangle$.

\- By MinD, $\mathcal{F}\models\
\langle\,\mathcal{D}({\neg{\ell}}\,):\mathrm{\bf
min}\\{\alpha,\beta\\}\,\rangle$.

$\blacksquare$

######  Proposition 7.2.

Te rule URΣ is sound:

$\langle{{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}\ell}}\,:\,\alpha\rangle\,{{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}\wedge}}\,\langle\,\Pi\succ({{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}\vee}}\
\,\mathcal{C}({{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}\neg{\ell}}})\
\,\mathcal{D}({{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}\neg{\ell}}}))\,:\beta\rangle\
\models\
\langle\,\mathcal{D}({{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}\neg{\ell}}}):\mathrm{\bf
min}\\{\alpha,\beta\\}\,\rangle.$

  * Proof.

By denoting
$\mathcal{F}=\langle{{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}\ell}}\,:\,\alpha\rangle\,{{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}\wedge}}\,\langle\,\Pi\succ({{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}\vee}}\
\,\mathcal{C}({{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}\neg{\ell}}})\
\,\mathcal{D}({{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}\neg{\ell}}}))\,:\beta\rangle$,
we have:

    1. $-$

By MinD,
$\mathcal{F}\models\langle\ell\wedge\Pi\succ({{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}\vee}}\
\,\mathcal{C}({{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}\neg{\ell}}})\
\,\mathcal{D}({{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}\neg{\ell}}}))\,:\mathrm{\bf
min}\\{\alpha,\beta\\}\rangle$.

    2. $-$

Then,
$\mathcal{F}\models\langle\ell\wedge\Pi\succ({{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}\vee}}\
\,\ell\wedge\mathcal{C}({{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}\neg{\ell}}})\
\,\ell\wedge\mathcal{D}({{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}\neg{\ell}}}))\,:\mathrm{\bf
min}\\{\alpha,\beta\\}\rangle$.

    3. $-$

Since ${\ell}\wedge\mathcal{C}({\neg{\ell}}\,)\models\bot$ then, $\
\mathcal{F}\models\langle\ell\wedge\Pi\succ{\ell}\wedge\mathcal{D}({\neg{\ell}}\,):\mathrm{\bf
min}\\{\alpha,\beta\\}\,\rangle$.

    4. $-$

Then,
$\mathcal{F}\models\langle\ell\wedge\Pi\succ\mathcal{D}({\neg{\ell}}\,):\mathrm{\bf
min}\\{\alpha,\beta\\}\,\rangle$.

    5. $-$

By MinD,
$\mathcal{F}\models\langle\Pi\succ\mathcal{D}({\neg{\ell}}\,):\mathrm{\bf
min}\\{\alpha,\beta\\}\,\rangle$.

$\blacksquare$

The next lemma states the correctness of the propositional rules of
$\mathcal{UR}_{\Sigma}$.

######  Lemma 7.3.

Let $\mathcal{UR}_{P}$ be the subset
$\\{\mbox{UR}_{P},{\bf\bot}\vee,{\bf\bot}\wedge,\odot\phi,\odot\odot\\}\subset\mathcal{UR}_{\Sigma}$.
A propositional Horn-NC formula $\varphi$ is inconsistent iff
$\mathcal{UR}_{P}$ with input $\langle\varphi:\alpha\rangle$ derives some
$\langle\bot:\alpha\rangle$.

  * Proof.

We analyze below both directions of the lemma.

$\bullet\ \Rightarrow$ Let us assume that $\varphi$ is inconsistent. Then
$\varphi$ must have a sub-formula verifying the $\mbox{UR}_{P}$ numerator;
otherwise, all complementary pairs of literals $\ell$ and $\neg\ell$ are
included in disjunctions. In this case, since all disjunctions of $\varphi$,
by definition of Horn-NC formula, have at least one negative literal,
$\varphi$ would be satisfied by assigning to all propositions the value $0$,
which contradicts the initial hypothesis. Therefore, $\mbox{UR}_{P}$ is
applied to $\varphi$ with two complementary literals $\ell$ and $\neg\ell$ and
the resulting formula is simplified. The new formula is equivalent to
$\varphi$ and has at least one literal less than $\varphi$. Hence, by
induction on the number of literals of $\varphi$, we obtain that
$\mathcal{UR}_{P}$ ends only when $\langle(\vee):\alpha\rangle$ is derived.

$\bullet\Leftarrow$ Let us assume that $\mathcal{UR}_{P}$ has been iteratively
applied until a formula $\varphi^{\prime}$ different from
$\langle(\vee):\alpha\rangle$ is obtained. Clearly, if the $\mbox{UR}_{P}$
numerator is not applicable then there is not a conjunction of a literal
$\ell$ with a disjunction including $\neg\ell$. Then we have, firstly, since
$\mathcal{UR}_{P}$ is sound, that $\varphi$ and $\varphi^{\prime}$ are
equivalent. Secondly, if $\varphi^{\prime}$ has complementary literals, then
they are integrated in disjunctions. Thus $\varphi^{\prime}$ is satisfied by
assigning the value 0 to all its unassigned propositions, since, by definition
of Horn-NC formula, all disjunctions have at least one negative disjunct.
Therefore, since $\varphi^{\prime}$ is consistent so is $\varphi$.
$\blacksquare$

The next lemma claims the correctness of $\mathcal{UR}_{\Sigma}$.

######  Lemma 7.4.

Let $\Sigma$ be a possibilistic Horn-NC base. $\mathcal{UR}_{\Sigma}$ derives
some empty clause $\langle(\vee):\alpha\rangle$ iff $\Sigma$ is inconsistent,
and if $\mathcal{UR}_{\Sigma}$ derives $\langle(\vee):\alpha\rangle$ then
$\mbox{Inc}(\Sigma)\geq\alpha$.

  * Proof.

The propositional component of possibilistic NC unit-resolution verifies Lemma
7.3, and hence, $\mathcal{UR}_{\Sigma}$ derives an empty formula
$\langle(\vee):\alpha\rangle$ iff the conjunction of the propositional
formulas in the base $\Sigma$ is inconsistent, namely if $\Sigma^{*}$ is
inconsistent. If $\mathcal{UR}_{\Sigma}$ derives
$\langle(\vee):\alpha\rangle$, then by Lemma 7.3, $\mathcal{UR}_{\Sigma}$
detects a subset $\Sigma_{1}\subseteq\Sigma$ which is indeed inconsistent.
Then by Proposition 7.2, the degree $\alpha$ found by $\mathcal{UR}_{\Sigma}$
corresponds to $\mbox{Inc}(\Sigma_{1})$. Since obviously
$\mbox{Inc}(\Sigma_{1})\leq\mbox{Inc}(\Sigma)$, the lemma holds.
$\blacksquare$

The next lemma states the correctness of the algorithm Find.

######  Lemma 7.5.

If Find($\Sigma,0$) returns $\alpha$ then $\mathrm{Inc}(\Sigma)=\alpha$.

  * Proof.

We denote $\Sigma^{\prime}$ and Inc the variables of Find in a given
recursion. Let us prove that the next hypothesis holds in every call to Find:

$\Sigma_{>\mbox{\footnotesize\bf Inc}}=\Sigma^{\prime}\mbox{\ \, and \
}\mbox{Inc}(\Sigma)=\mbox{max}\\{\mbox{Inc}(\Sigma^{\prime}),\mbox{\bf
Inc}\\}$

– We check that the initial call Find($\Sigma,0$) verifies the hypothesis:

\- We have $\Sigma^{\prime}=\Sigma$ and Inc = 0.

\- So indeed we have $\Sigma_{>0}=\Sigma^{\prime}$ and
$\mbox{Inc}(\Sigma)=\mbox{max}\\{\mbox{Inc}(\Sigma^{\prime}),0\\}=\mbox{Inc}(\Sigma)$

– We prove that if the hypothesis holds for $k\geq 1$ then it holds for $k+1$.

– First of all, $\mathcal{UR}_{\Sigma}$ is applied to $\Sigma^{\prime}$.

– By Lemma 7.4, if $\mathcal{UR}_{\Sigma}$ derives $\langle\bot:\alpha\rangle$
then $\mbox{Inc}(\Sigma^{\prime})\geq\alpha$, else $\Sigma^{\prime}$ is
consistent.

– Case $\Sigma^{\prime}$ is consistent: $\mbox{Inc}(\Sigma^{\prime})=0$.

\- By induction hypothesis
$\mbox{Inc}(\Sigma)=\mbox{max}\\{\mbox{Inc}(\Sigma^{\prime}),\mbox{\bf
Inc}\\}={\bf Inc}$

\- So Find correctly returns $\mbox{Inc}(\Sigma)$ and ends.

– Case $\Sigma^{\prime}$ is inconsistent:
$\mbox{Inc}(\Sigma^{\prime})=\alpha>0$.

\- By induction hypothesis $\Sigma^{\prime}=\Sigma_{>\mbox{\footnotesize\bf
Inc}}$, and so $\alpha>\mbox{\bf Inc}$.

\- The next $\Sigma^{\prime}$, noted $\Sigma^{\prime\prime}$, and Inc, noted
Inc’, are $\Sigma^{\prime\prime}=\Sigma^{\prime}_{>\alpha}$ and Inc’=$\alpha$.

We check in $(i)$ and $(ii)$ that the hypothesis holds:

$(i)$ By induction hypothesis:
$\Sigma^{\prime}=\Sigma_{>\mbox{\footnotesize\bf Inc}}$

– Since $\alpha>\mbox{\bf Inc}$ then trivially
$\Sigma^{\prime}_{>\alpha}=\Sigma_{>\alpha}$

– Hence
$\Sigma^{\prime\prime}=\Sigma^{\prime}_{>\alpha}=\Sigma_{>\alpha}=\Sigma_{>\mbox{\footnotesize\bf
Inc'}}$.

$(ii)$ By Lemma 7.4, $\mbox{Inc}(\Sigma^{\prime})\geq\alpha$

– Since $\Sigma^{\prime}=\Sigma_{>\mbox{\footnotesize\bf Inc}}$ and $\alpha>$
Inc then $\mbox{Inc}(\Sigma)\geq\alpha$

– Hence
$\mbox{Inc}(\Sigma)=\mbox{max}\\{\mbox{Inc}(\Sigma_{>\alpha}),\alpha\\}=\mbox{max}\\{\mbox{Inc}(\Sigma^{\prime\prime}),\mbox{\bf
Inc'}\\}$

Altogether, the hypothesis holds until Find finds $\Sigma^{\prime}$ consistent
and then correctly returns $\mbox{Inc}(\Sigma)$. Hence Lemma 7.5 holds.
$\blacksquare$

The next three propositions prove that finding $\mbox{Inc}(\Sigma)$ of any
Horn-NC $\Sigma$ is polynomial.

######  Proposition 7.6.

If $\Sigma$ is a possibilistic Horn-NC base, then $\mathcal{UR}_{\Sigma}$ with
input $\Sigma$ performs at most $n^{2}$ inferences, $n$ being the number of
symbols (size) of $\Sigma$.

  * Proof.

On the one hand, each rule of $\mathcal{UR}_{\Sigma}$ adds a formula
$\langle\varphi:\alpha\rangle$, where $\varphi$ is a sub-formula of a
propositional formula $\Pi$ of a possibilistic formula
$\langle\Pi:\beta\rangle$ in the current base. Hence, the current base always
contains only sub-formulas from $\Sigma$. On the other hand, the weight
$\alpha$ of added formulas $\langle\varphi:\alpha\rangle$ is the minimum of
two weights in the current base. Hence, the weights of formulas in the current
base always come from $\Sigma$. Thus, the maximum number of deduced formulas
is $m\times k$, where $m$ is the number of sub-formulas in $\Sigma$ and $k$ is
the number of different weights in $\Sigma$. Hence, the maximum number of
inferences performed by $\mathcal{UR}_{\Sigma}$ is $m\times k$. If $n$ is the
size of $\Sigma$, then $m,k\leq n$ and so the proposition holds.
$\blacksquare$

######  Proposition 7.7.