# The Horn Non-Clausal Class and its Polynomiality

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

###### Abstract

The expressiveness of propositional non-clausal (NC) formulas is exponentially
richer than that of clausal formulas. Yet, clausal efficiency outperforms non-
clausal efficiency. Indeed, a major weakness of the latter is that, while Horn
clausal formulas, along with Horn algorithms, are crucial for the high
efficiency of clausal reasoning, no Horn-like formulas in non-clausal form had
been proposed.

To overcome such weakness, we first define the hybrid class $\mathbb{H_{NC}}$
of Horn Non-Clausal (Horn-NC) formulas by adequately lifting the Horn pattern
to NC form, and argue that $\mathbb{H_{NC}}$, along with future Horn-NC
algorithms shall increase non-clausal efficiency just as the Horn class has
increased clausal efficiency.

Secondly, we: (i) give the compact, inductive definition of $\mathbb{H_{NC}}$;
(ii) prove that syntactically $\mathbb{H_{NC}}$ subsumes the Horn class but
semantically both classes are equivalent; and (iii) characterize the non-
clausal formulas belonging to $\mathbb{H_{NC}}$.

Thirdly, we define the Non-Clausal Unit-Resolution calculus, or
UR${}_{\mbox{nc}}$, and prove that it checks the satisfiability of
$\mathbb{H_{NC}}$ in polynomial time. This fact, to our knowledge, makes
$\mathbb{H_{NC}}$ the first characterized polynomial class in NC reasoning.

Finally, we prove that $\mathbb{H_{NC}}$ is linearly recognizable, and also
that it is both strictly more succinct and exponentially richer than the Horn
class.

We discuss that in NC automated reasoning, e.g. satisfiability solving,
theorem proving, logic programming, etc., can directly benefit from
$\mathbb{H_{NC}}$ and UR${}_{\mbox{nc}}$ and that, as a by-product of its
proved properties, $\mathbb{H_{NC}}$ arises as a new alternative to analyze
Horn functions and implication systems.

Field: Automated Reasoning in Propositional Logic.

Keywords: NNF; Unit Resolution; DPLL; Satisfiability; Theorem Proving; Logic
Programming; Tractability; Horn functions; Implication Systems.

##  1 Introduction

The expressive power of non-clausal (NC) formulas is exponentially richer
(formally specified in Section 5) than that of clausal formulas and they have
found much use in heterogeneous fields and practical settings such as
diagnosis [47], algebric theorems [116], linear monadic decomposition [78],
symbolic model checking [157], formal verification [57], supervisory control
[40], circuit verification [56], linear quantifier elimination [123],
quantified boolean formulas [61], constraint problems [154], theorem proving
[126], ontologies [4], knowledge compilation [49], heuristics [16],
satisfiability modulo theory [95], MaxSAT [110], encodings [121], modal logics
[68], nested expressions [128], description logics [99], many-valued logics
[159], learning [1], deductive databases [54], minimum unsatisfiability [33],
compiling linear constrains [145], constraint handling rules [74], dynamic
systems [131], DPLL [146], linear constraint solving [8], linear arithmetic
games [65], aggregates [34], equilibrium logic [127], model generation [92],
constrained Horn clauses [101], Horn clause verification [150], constraint
logic programs [149], NC resolution [119], Skolemisation [102], numeric
planning [133], stochastic search [118] and hard problems [121].

On the other side, the Horn clausal formulas are pivotal in our approach. Such
formulas can be read naturally as instructions for a computer and are central
for deductive databases, declarative programming, automated reasoning and
artificial intelligence. Modeling and computing with Horn languages have
received a great deal of attention since 1943 [115, 87] and they are the core
of countless contemporary research fields spread across many logics and a
variety of reasoning problems.

Regarding specifically the conjunctive rôle of Horn formulas and Horn-SAT
algorithms in propositional logic, its linearity [55, 91, 117, 135, 72, 60]
for both satisfiability checking Horn formulas and simplifying non-Horn ones
is likely its most significant, well-known virtue. The valuable contribution
of Horn efficiency to the global efficiency of clausal reasoning is evidenced
by the fact that highly-efficient DPLL solvers embed a Horn-SAT-like algorithm
so-called Unit Propagation111So the terms Horn-SAT algorithm and Unit
Propagation will be used interchangeably.[53]. Hence, finding polynomial
clausal super-classes of the Horn class has been a key issue for several
decades in the quest for improving clausal reasoning; some found classes are:
hidden Horn [107, 7], generalized Horn [37], Q-Horn [28], extended-Horn [38],
SLUR [134], Quad [44], UP-Horn [66] and more. The Related Work gives a
chronological account of such clausal classes and their interrelations.

Despite those many clausal classes, so far no attempt is known to lift the
Horn pattern to the non-clausal level, i.e. no NC class is recognized to be
the NC analogous to the Horn class. Perhaps, the Horn pattern was considered
inherently clausal and not extensible to non-clausal form. In this paper, we
bridge that gap by introducing the hybrid class $\mathbb{H_{NC}}$ of Horn-NC
formulas, which results by suitably amalgamating the Horn-clausal and the NC
formulas, or equivalently, by appropriately lifting the Horn-clausal pattern
to NC form.

Firstly, the syntactical Horn-NC pattern is established by lifting the clausal
restriction: a formula is Horn if all its clauses have (any number of negative
literals and) at most one positive literal, to the NC level, which gives rise
to the recursive non-clausal restriction: an NC formula is Horn-NC if all its
disjunctions have any number of negative disjuncts and at most one non-
negative disjunct. Accordingly, $\mathbb{H_{NC}}$ is the class of Horn-NC
formulas. Note that $\mathbb{H_{NC}}$ naturally subsumes the Horn class. After
such simple definition of $\mathbb{H_{NC}}$, we go deeper into the details and
give its detailed definition compactly and inductively.

Secondly, we prove the relationships between $\mathbb{H_{NC}}$ and the classes
Horn and NC. Concretely, we show that $\mathbb{H_{NC}}$ and the Horn class are
related in that (i) $\mathbb{H_{NC}}$ syntactically subsumes the Horn class
but both classes are logically equivalent; and $\mathbb{H_{NC}}$ and the NC
class are related in that (ii) $\mathbb{H_{NC}}$ contains all NCs whose
clausal form is Horn. The Venn diagram in Fig. 1 below relates
$\mathbb{H}_{\mathbb{NC}}$ to the classes Horn ($\mathbb{H}$), NC
($\mathbb{N_{C}}$) and Clausal ($\mathbb{C}$).

Thirdly, we provide Non-Clausal Unit-Resolution, or UR${}_{\mbox{nc}}$, prove
its completeness for $\mathbb{H_{NC}}$ and that it allows to test the
satisfiability of $\mathbb{H_{NC}}$ in polynomial time. This claim makes
$\mathbb{H_{NC}}$, so far as we know, the first characterized tractable NC
class. Such polynomiality allows to easily prove that Horn-NC-SAT is
P-complete.

$\ \mathbb{N_{C}}$$\mathbb{C}$$\mathbb{H_{NC}}$$\mathbb{H}$

Fig. 1. The Horn$\cdot$NC, Horn, NC and clausal classes.

Fourthly, we demonstrate the following additional properties of
$\mathbb{H_{NC}}$: (i) $\mathbb{H_{NC}}$ is linearly recognizable, i.e.
deciding whether an NC is Horn-NC takes linear time; (ii) $\mathbb{H_{NC}}$ is
more succinct [75] than the Horn class, i.e. some Horn-NC formulas are
exponentially smaller than their equivalent Horn formulas; and (iii)
syntactically, $\mathbb{H_{NC}}$ is exponentially richer than the Horn class,
i.e. for each Horn formula there are exponentially many Horn-NCs.

We summarize and illustrate our aforementioned contributions through the NC
formula $\varphi$ below, whose suffix notation will be detailed in Subsection
2 and wherein $A,B,\ldots$ and $\overline{A},\overline{B},\ldots$ are positive
and negative literals, respectively, and $\phi_{1}$, $\phi_{2}$ and $\phi_{3}$
are NCs:

$\varphi=\\{\wedge\ \,A\ \,(\vee\ \ \overline{B}\ \ \\{\wedge\ \ (\vee\ \
\overline{D}\ \ \overline{C}\ \ A)\ \ (\vee\ \ \phi_{1}\ \ \\{\wedge\ \
\phi_{2}\ \ {\overline{A}}\\})\ \,B\\}\,)\ \ \phi_{3}\\}$

We will show that $\varphi$ is Horn-NC when $\phi_{1}$, $\phi_{2}$ and
$\phi_{3}$ are Horn-NC and at least one of $\phi_{1}$ or $\phi_{2}$ is
negative. In that case we will show that:

$\bullet$ $\varphi$ can be tested for satisfiability in polynomial time.

$\bullet$ $\varphi$ can be recognized as Horn-NC in linear time.

$\bullet$ $\varphi$ is logically equivalent to a Horn formula.

$\bullet$ Applying $\wedge/\vee$ distributivity to $\varphi$ yields a Horn
formula.

$\bullet$ There are exponentially many Horn-NCs equivalent to $\varphi$.

$\bullet$ $\varphi$ is exponentially smaller than its equivalent Horn formula.

In a nutshell, $\mathbb{H_{NC}}$ gathers benefits from possessing a salient
expressive power and from enjoying appealing properties for efficient
reasoning. Hence, it is reasonable to expect that $\mathbb{H_{NC}}$ in tandem
with fast future Horn-NC algorithms could be relevant in NC reasoning to the
extent to which $\mathbb{H_{NC}}$ could be regarded the NC analogous to the
Horn clausal class.

A direct benefit of this work is that $\mathbb{H_{NC}}$ and UR${}_{\mbox{nc}}$
pave the way to develop NC DPLL reasoners able to emulate the efficiency of
their clausal counterparts. We also argue that $\mathbb{H_{NC}}$ and
UR${}_{\mbox{nc}}$ allow logic programing and in general, knowledge-based
systems: $(i)$ enriching their syntax from simple Horn rules to Horn-NC rules
where heads and bodies are NCs with slight restrictions; and $(ii)$ answering
queries with an efficiency comparable to the clausal efficiency as, both,
Horn-NCs can be tested for satisfiability polynomially and have only one
minimal model (as aforementioned, they are equivalent to a Horn formula).

As a by-product of its properties, $\mathbb{H_{NC}}$ can potentially draw
interest from other fields such as Boolean functions and implicational
(closure) systems. Indeed, $\mathbb{H_{NC}}$ can serve to analyze the Boolean
functions representable by Horn formulas [43], since $\mathbb{H_{NC}}$ is
equivalent to the Horn class, is easily recognizable and its formulas are much
smaller than their clausal representations. Regarding implicational systems
[23], instead of clausal implications related to Horn formulas, general NC
implications related to Horn-NCs can be envisioned. Further applications using
the $\mathbb{H_{NC}}$ properties are given in the related work.

The Future Work section outlines a substantial number of research directions
which pivot on two research axes: (i) $\mathbb{H_{NC}}$ and UR${}_{\mbox{nc}}$
can be smoothly extended beyond propositional logic to richer logics and
adapted to different reasoning problems; and (ii) our work can be used as a
lever to develop the NC paradigm; for example, our definition of
UR${}_{\mbox{nc}}$ is the basis to conceive a new definition of Non-Clausal
Resolution.

This paper continues as follows. Section 2 presents background and
terminology. Section 3 defines $\mathbb{H_{NC}}$ and relates $\mathbb{H_{NC}}$
to the classes NC and Horn. Section 4 introduces UR${}_{\mbox{nc}}$ and proves
the tractability of $\mathbb{H_{NC}}$. Section 5 demonstrates further
properties of $\mathbb{H_{NC}}$. Section 6 and 7 focus on related work and
future work, respectively. The last section summarizes the main contributions.

##  2 Background, Notation and Terminology

This section presents background on propositional non-clausal logic (the
reader is referred to e.g. [20] for a more complete background) and introduces
our notation and terminology.

######  Definition 2.1.

Positive literals are noted $\\{A,B,\ldots\\}$ and negative ones
$\\{\overline{A},\overline{B},\ldots\\}$. $\mathbb{L}$ is the set of literals.
A clause is a disjunction of literals. A clause with at most one positive
literal is Horn. A conjunction of clauses is a clausal formula. A conjunction
of Horn clauses is a Horn formula. $\mathbb{C}$ and $\mathbb{H}$ are the sets
of clausal and Horn formulas, respectively.

######  Definition 2.2.

The NC alphabet is formed by the sets of: constants {T, F}, literals
$\mathbb{L}$, connectives {$\neg,\vee,\wedge\\}$ and auxiliary symbols: (, ),
{ and }.

For the sake of readability of NC formulas, we employ: (1) the prefix notation
because it requires only one connective $\vee$ or $\wedge$ per formula, while
infix notation requires $k-1$ ($k$ is the arity of $\vee$ and $\wedge$); and
(2) two formula delimiters, $\\{\wedge\,\ldots\,\\}$ for conjunctions and
$(\vee\,\ldots\,)$ for disjunctions (Definition 2.3), to distinguish them
inside nested NCs. The negation normal form formulas (NNFs) do not use the
connective $\neg$. We give next our notation for NNFs.

######  Definition 2.3.

The set $\mathbb{N_{NF}}$ of NNF formulas is defined in the usual way:

  * •

$\\{{\bf T,\,F}\\}\cup\mathbb{L}\,\subset\,\mathbb{N_{NF}}$.

  * •

If for all $i\in\\{1,\ldots k\\}$, $\varphi_{i}\in\mathbb{N_{NF}}$ then
$\\{\wedge\
\varphi_{1}\ldots\varphi_{i}\ldots\varphi_{k}\\}\in\mathbb{N_{NF}}$.

  * •

If for all $i\in\\{1,\ldots k\\}$, $\varphi_{i}\in\mathbb{N_{NF}}$ then
$\,(\vee\ \varphi_{1}\ldots\varphi_{i}\ldots\varphi_{k})\in\mathbb{N_{NF}}$.

– $\\{\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.

– $\langle\odot\,\varphi_{1}\ldots\varphi_{i}\ldots\varphi_{k}\rangle$ 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}$ and $\varphi_{3}$ below are NNF while $\varphi_{2}$ and
$\varphi_{4}$ are not.

  * –

$\varphi_{1}=(\vee\ \ \\{\wedge\ \ \overline{A}\ \ {\bf T}\,\\}\ \ \\{\wedge\
\ (\vee\ \ \overline{A}\ \ C\,)\ \ {\bf T}\ \ \\{\wedge\ \ D\ \ (\vee\ \ A\ \
\overline{B}\,)\,\\}\,\\}\,)$.

  * –

$\varphi_{2}=\\{\wedge\ \ D\ \ \neg(\vee\ \ \\{\wedge\ \ \overline{A}\ \
B\,\\}\ \ {\bf F}\ \ (\vee\ \ A\ \ C\,)\,)\,\\}.$

  * –

$\varphi_{3}=\\{\wedge\ \ \varphi_{1}\ \ (\vee\ \ \\{\wedge\ \ A\ \
\overline{C}\\}\ \ \overline{B})\ \ (\vee\ \ \varphi_{1}\ \ {\bf F}\ \
A)\,\\}.$

  * –

$\varphi_{4}=(\vee\ \ \varphi_{2}\ \ \\{\wedge\ \ A\ \ (\vee\ \ \varphi_{1}\ \
\overline{D}\ \ \varphi_{3})\,\\}\ \ \\{\wedge\ \ \varphi_{2}\ \ B\ \ (\vee\ \
\varphi_{1}\ \ \varphi_{3})\,\\}\,)$ ∎

######  Definition 2.5.

The set $\mathbb{N_{C}}$ of NC formulas is built inductively as
$\mathbb{N_{NF}}$ but over the whole NC alphabet, namely including also the
connective $\neg$ (we omit the formal details).

######  Example 2.6.

$\varphi_{2}$ and $\varphi_{4}$ in Example 2.4, which were not in
$\mathbb{N_{NF}}$, are in $\mathbb{N_{C}}$.

######  Definition 2.7.

Sub-formulas are inductively defined as follows. The unique sub-formula of an
atom ($\\{{\bf T,\,F}\\}\cup\mathbb{L}$) is the atom itself. The sub-formulas
of $\varphi$ are $\varphi$ itself more the sub-formulas of either (i)
$\varphi^{\prime}$, if $\varphi=\neg\varphi^{\prime}$, or (ii) the
$\varphi_{i}$’s, if $\varphi=\langle\odot\
\varphi_{1}\ldots\varphi_{i}\ldots\varphi_{k}\rangle$.

######  Definition 2.8.

NCs are representable by trees if: (i) each atom is a leaf node and each
occurrence of connectives is an internal node; and (ii) the arcs are given by:
(a) each sub-formula $\neg\varphi$ is an arc linking the nodes of $\neg$ and
of the connective of $\varphi$; and (b) each sub-formula $\langle\odot\
\varphi_{1}\ldots\varphi_{i}\ldots\,\varphi_{k}\rangle$ is a $k$-ary hyper-arc
linking the nodes of $\odot$ and the nodes of, for every $i$, $\varphi_{i}$ if
$\varphi_{i}$ is an atom and of its connective otherwise.

######  Example 2.9.

The tree representing $\varphi_{2}$ in Example 2.4 is given in Fig. 2.

Y1.0e0]pt$\wedge$Y1.0e0]pt$\overline{C}$Y1.0e0]pt$\neg$Y1.0e0]pt$\vee$Y1.0e0]pt$\wedge$Y1.0e0]pt$\overline{A}$Y1.0e0]pt$B$Y1.0e0]ptFY1.0e0]pt$\vee$Y1.0e0]pt$\overline{A}$Y1.0e0]pt$\overline{C}$

Fig. 2. Tree of $\varphi_{2}$.

∎

There exist different, bi-dimensional graphical models [24, 93] Our approach
also applies when NCs are modeled and implemented as directed acyclic graphs
(DAGs), which are more general than trees and allow for important savings in
both space and time.

######  Definition 2.10.

An NC formula $\varphi$ is modeled by a DAG when each sub-formula $\phi$ is
modeled by a unique DAG $D_{\phi}$ and each $\phi$-occurrence by a pointer to
(the root of) $D_{\phi}$.

######  Example 2.11.

Each sub-formula $\varphi_{1}$ to $\varphi_{3}$ in $\varphi_{4}$ from Example
2.4 requires one DAG and two sub-formula pointers.

An interpretation $\mathcal{I}$ maps $\mathbb{N_{C}}$ onto $\\{0,1\\}$ and
maps constants as follows: $\mathcal{I}({\bf F})=\mathcal{I}(\,(\vee)\,)=0$
and $\mathcal{I}({\bf T})=\mathcal{I}(\,\\{\wedge\\}\,)=1.$ As the
interpretation of negated, conjunctive and disjunctive formulas is well-known,
by space reasons we omit their formal definitions.

######  Definition 2.12.

An interpretation $\mathcal{I}$ is a model of $\varphi$ if
$\mathcal{I}(\varphi)=1.$ If $\varphi$ has a model then it is satisfiable and
otherwise unsatisfiable. $\varphi$ and $\varphi^{\prime}$ are equivalent,
noted $\varphi\equiv\varphi^{\prime}$, if $\forall\mathcal{I}$,
$\mathcal{I}(\varphi)=\mathcal{I}(\varphi^{\prime})$. $\varphi^{\prime}$ is
logical consequence of $\varphi$, noted $\varphi\models\varphi^{\prime}$, if
$\forall\mathcal{I}$, $\mathcal{I}(\varphi)\leq\mathcal{I}(\varphi^{\prime})$.

######  Definition 2.13.

We define: SAT, Horn-SAT, NC-SAT and Horn-NC-SAT are the problems of testing
the satisfiability of clausal, Horn, NC and Horn-NC formulas, respectively.

Complexity. SAT [42] and NC-SAT are NP-complete, Horn-SAT is linear [55, 91,
117, 135, 60]. Here, the Horn-NC class is defined and proved that Horn-NC-SAT
is polynomial.

######  Definition 2.14.

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

$\bullet$ Replace: $\\{\wedge\ {\bf F}\ \varphi\,\\}\leftarrow{\bf F}$;
$(\vee\ {\bf T}\ \varphi\,)\leftarrow{\bf T}$; $\\{\wedge\ {\bf T}\
\varphi\,\\}\leftarrow\varphi$; $(\vee\ \,{\bf F}\ \varphi\,)$ $\leftarrow$
$\varphi$

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

##  3 The Horn-NNF and Horn-NC Classes

We give first the definition of $\mathbb{H_{NF}}$ and then that of
$\mathbb{H_{NC}}$. We will use the following abbreviations: HNF for Horn-NNF
and HNC for Horn-NC.

###  3.1 The Horn-NNF formulas: $\mathbb{H_{NF}}$

######  Definition 3.1.

Negative formulas are NNF formulas having solely negative literals.
$\mathbb{{N_{G}}}$ is the set of negative NNF formulas.

######  Example 3.2.

An example of negative formula is $(\vee\ \ \\{\wedge\ \,\overline{A}\
\,\overline{C}\,\\}\ \ \\{\wedge\ \,\overline{E}\ \,(\vee\ \,\overline{A}\
\,\overline{B}\,)\,\\}\,)$. ∎

Next we lift the the Horn pattern to the non-clausal level as follows:

######  Definition 3.3.

An NNF is HNF all its disjunctions have any number of negative disjuncts and
at most one non-negative disjunct. We denote $\mathbb{H_{NF}}$ the class of
HNF formulas.

Clearly Horn formulas are HNF, namely $\mathbb{H}\subset\mathbb{H_{NF}}$.

Remark. As Definition 3.3 is not concerned with how NNFs are represented, our
approach also applies when NNFs are represented by DAGs and not just by trees.
Yet, for the sake of simplicity, we will use NNFs representable by trees
throughout this article.

######  Example 3.4.

Let us consider $\varphi_{1}$ and $\varphi_{2}$ below. As $\varphi_{1}$ has
two disjuncts and only one is non-negative, $\varphi_{1}$ is HNF. Yet
$\varphi_{2}$ has two non-negative disjuncts and so it is not HNF.

  * •

$\varphi_{1}=(\vee\ \ \\{\wedge\ \ \overline{B}\ \ \overline{D}\\}\ \
\\{\wedge\ \ C\ \ A\,\\}\,)\qquad\varphi_{2}=(\vee\ \ \\{\wedge\ \
\overline{B}\ \ D\\}\ \ \\{\wedge\ \ C\ \ \overline{A}\,\\}\,).$ ∎

######  Example 3.5.

Below we consider $\varphi$ and $\varphi^{\prime}$ resulting from $\varphi$ by
switching its left-most $\overline{A}$ for A. All the disjunctions of
$\varphi$, i.e. $(\vee\ \overline{A}\ C)$, $(\vee\ A\ \overline{B})$ and
$\varphi$ itself, have exactly one non-

  * •

$\varphi=(\vee\quad\overline{A}\ \ \\{\wedge\ \ (\vee\ \ \overline{A}\ \
C\,)\quad\\{\wedge\ \ D\ \ (\vee\ \ A\ \ \overline{B}\,)\,\\}\,\\}\,)$.

  * •

$\varphi^{\prime}=(\vee\quad A\ \ \\{\wedge\ \ (\vee\ \ \overline{A}\ \
C\,)\quad\\{\wedge\ \ D\ \ (\vee\ \ A\ \ \overline{B}\,)\,\\}\,\\}\,)$.

negative disjunct; so $\varphi$ is HNF. Yet, $\varphi^{\prime}=(\vee\ A\
\phi)$, $\phi$ being non-negative; so, as $\varphi^{\prime}$ has two non-
negative disjuncts, $\varphi^{\prime}$ is not HNF. ∎

######  Proposition 3.6.

All sub-formulas of an HNF formula are HNF.

The proof follows immediately from Definition 3.3. Note that the converse does
not hold since there are non-HNF formulas all of whose sub-formulas are HHF.

Towards a fine-grained definition of $\mathbb{{H}_{NF}}$, first we inductively
specify $\mathrm{{HNF}}$ conjunctions (Lemma 3.7) and $\mathrm{{HNF}}$
disjunctions (Lemma 3.9), and then we compactly specify $\mathbb{{H}_{NF}}$ by
embedding both specifications into an inductive function (Definition 3.12).

Conjunctions of Horn clausal formulas are Horn too, and a similar kind of
Horn-like compliance also holds in NC form, viz. conjunctions of HNF formulas
are HNF too.

######  Lemma 3.7.

Conjunctions of $\mathrm{{HNF}}$ formulas are $\mathrm{{HNF}}$ as well,
formally

$\\{\wedge\
\varphi_{1}\,\ldots\,\varphi_{i}\ldots\,\varphi_{k}\\}\in\mathbb{{H}_{NF}}\mbox{\em\
\ iff \ \ for }1\leq i\leq k,\ \varphi_{i}\in\mathbb{{H}_{NF}}.$

The proof is straightforward.

######  Example 3.8.

If $\mathrm{H}_{1}$ is Horn and $\varphi\in\mathbb{{H}_{NF}}$, then
$\\{\wedge\ \mathrm{H}_{1}\ (\vee\ \overline{D}\ A\,)\
\varphi\\}\in\mathbb{{H}_{NF}}$ ∎

It is not hard to check that the definition of HNF disjunction in Definition
3.3 can be equivalently expressed in the next recursive manner: an NNF
disjunction is HNF if it has any number of negative disjuncts and one HNF
disjunct, which leads to:

######  Lemma 3.9.

A disjunctive NNF $\varphi=(\vee\
\varphi_{1}\ldots\varphi_{i}\ldots\varphi_{k})$ with $k\geq 1$ disjuncts
belongs to $\mathbb{{H}_{NF}}$ iff it has one $\mathrm{{HNF}}$ and $k-1$
negative disjuncts, formally

$(\vee\
\varphi_{1}\ldots\varphi_{i}\ldots\varphi_{k})\in\mathbb{{H}_{NF}}\mbox{\em\ \
iff there is}\ i\ \mbox{\em s.t.}\ \varphi_{i}\in\mathbb{{H}_{NF}}\ \mbox{\em
and}\ \mbox{\em for all }j\neq i,\varphi_{j}\in\mathbb{{N_{G}}}.$

  * Proof.

If. Since the sub-formulas $\forall j,j\neq i,\varphi_{j}$ have no positive
literals, the non-negative disjunctions of $\varphi=(\vee\
\varphi_{1}\ldots\varphi_{i}\ldots\varphi_{k})$ are those in $\varphi_{i}$
plus $\varphi_{i}$ and $\varphi$ themselves. Given that by hypothesis
$\varphi_{i}\in\mathbb{H}_{\mathbb{NF}}$ and that $\forall j,j\neq
i,\varphi_{j}$ have no positive literals, then $\varphi=(\vee\
\varphi_{1}\ldots\varphi_{i}\ldots\varphi_{k})$ satisfies Definition 3.3, and
so $\varphi\in\mathbb{H}_{\mathbb{NF}}$. Iff. It is done by contradiction: if
(i) $\varphi_{i}\notin\mathbb{H}_{\mathbb{NF}}$ or (ii) $\exists i,j,i\neq
j,\varphi_{i},\varphi_{j}\notin\mathbb{{N_{G}}}$, then $(\vee\
\varphi_{1}\ldots\varphi_{i}\ldots\varphi_{k})\notin\mathbb{H}_{\mathbb{NF}}$.
A similar proof is given in Theorem 3.31 and so, by space reasons, we omit the
details. $\blacksquare$

From Lemma 3.9, we have: (A) non-recursive $\mathrm{{HNF}}$ disjunctions are
Horn clauses; (B) NNF disjunctions with all negative disjuncts are
$\mathrm{{HNF}}$; and (C) NNF disjunctions with $k\geq 2$ non-negative
disjuncts are not $\mathrm{{HNF}}$. Next, we reexamine Examples 3.4 and 3.5
but this time bearing Lemma 3.9 in mind.

######  Example 3.10.

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

  * •

$\varphi_{1}=(\vee\ \\{\wedge\ \overline{B}\ \overline{D}\\}\ \\{\wedge\ C\
A\,\\}\,).$

– Clearly $\\{\wedge\ \overline{B}\ \overline{D}\\}\in\mathbb{{N_{G}}}$ and by
Lemma 3.7, $\\{\wedge\ C\ A\,\\}\in\mathbb{{H}_{NF}}$.

– According to Lemma 3.9, $\varphi_{1}\in\mathbb{{H}_{NF}}$.

  * •

$\varphi_{2}=(\vee\ \\{\wedge\ \overline{B}\ D\\}\ \ \\{\wedge\ C\
\overline{A}\,\\}\,)$.

– Clearly $\\{\wedge\ \overline{B}\ D\\}\notin\mathbb{N_{G}}$ and $\\{\wedge\
C\ \overline{A}\,\\}\notin\mathbb{{N_{G}}}$; by Lemma 3.9,
$\varphi_{2}\notin\mathbb{{H}_{NF}}$. ∎

######  Example 3.11.

Let us consider again $\varphi$ and $\varphi^{\prime}$ in Example 3.5
recalling that $\varphi^{\prime}$ results from $\varphi$ by just switching its
left-most $\overline{A}$ for $A$.

  * •

By Lemma 3.9, $(\vee\ \overline{A}\ C)\in\mathbb{{H}_{NF}}$ and $(\vee\ A\
\overline{B})\in\mathbb{{H}_{NF}}$.

  * •

By Lemma 3.7, $\\{\wedge\ \ D\ \,(\vee\ A\
\overline{B})\\}\in\mathbb{{H}_{NF}}$.

  * •

By Lemma 3.7, $\phi=\\{\wedge\ (\vee\ \overline{A}\ C\,)\ \\{\wedge\ \ D\
\,(\vee\ A\ \overline{B})\\}\\}\in\mathbb{{H}_{NF}}$.

  * •

We have: $\varphi=(\vee\ \overline{A}\ \,\phi\,)$. Since
$\overline{A}\in\mathbb{{N_{G}}}$ and $\phi\in\mathbb{{H}_{NF}}$, by Lemma
3.9, $\varphi\in\mathbb{{H}_{NF}}$.

  * •

We have: $\varphi^{\prime}=(\vee\ A\ \phi\,)$. Since
$A,\phi\notin\mathbb{{N_{G}}}$, by Lemma 3.9,
$\varphi^{\prime}\notin\mathbb{{H}_{NF}}$. ∎

By merging Lemmas 3.7 and 3.9, $\mathbb{{H}_{NF}}$ is compactly and
inductively defined as follows.

######  Definition 3.12.

We inductively define the set of formulas $\mathbb{\overline{H}_{NF}}$
exclusively from the rules below, wherein $k\geq 1$ and $\mathbb{L}$ is the
set of literals.

  * (1)

$\mathbb{L}\subset\mathbb{\overline{H}_{NF}}.$

  * (2)

$\mathrm{If}\ \ \forall i,\,\varphi_{i}\in\mathbb{\overline{H}_{NF}}\ \
\mathrm{then}\ \ \\{\wedge\
\varphi_{1}\,\ldots\,\varphi_{i}\ldots\varphi_{k}\\}\in\mathbb{\overline{H}_{NF}}.$

  * (3)

$\mathrm{If}\ \ \varphi_{i}\in\mathbb{\overline{H}_{NF}}\ \,\mathrm{and}\
\,\forall j\neq i$, $\varphi_{j}\in\mathbb{{N_{G}}}\ \,\mathrm{then}\ \,(\vee\
\varphi_{1}\ldots\varphi_{i}\ldots\,\varphi_{k})\in\mathbb{\overline{H}_{NF}}.$

We prove next that $\mathbb{\overline{H}_{NF}}$ coincides with
$\mathbb{{H}_{NF}}$, that is, Definition 3.12 corresponds to the recursive and
compact definition of $\mathbb{{H}_{NF}}$. Besides, the specification in
Definition 3.12 yields an optimal strategy to decide whether an NNF is
$\mathrm{{HNF}}$, which is proven in Subsection 5.1. In fact, a recognition
algorithm is designed and its linear behavior proved.

######  Theorem 3.13.

We have: $\mathbb{\overline{H}_{NF}}=\mathbb{{H}_{NF}}$.

  * Proof.

We prove first $\mathbb{\overline{H}_{NF}}\subseteq\mathbb{{H}_{NF}}$ and then
$\mathbb{\overline{H}_{NF}}\supseteq\mathbb{{H}_{NF}}$. The first relation
$\mathbb{\overline{H}_{NF}}\subseteq\mathbb{{H}_{NF}}$ is proven by structural
induction, where (1) $\mathbb{L}\subset\mathbb{{H}_{NF}}$ holds trivially, as
follows.

(2) The non-recursive $\mathbb{\overline{H}_{NF}}$ conjunctions are literal
conjunctions, which trivially verify Definition 3.3 and so are in
$\mathbb{{H}_{NF}}$. Further, assuming that for an induction step
$\mathbb{\overline{H}_{NF}}\subseteq\mathbb{{H}_{NF}}$ holds and that
$\varphi_{i}\in\mathbb{\overline{H}_{NF}},1\leq i\leq k$, then any formula
$\\{\wedge\ \varphi_{1}\,\ldots\,\varphi_{i}\ldots\varphi_{k}\\}$ added in (2)
to $\mathbb{\overline{H}_{NF}}$ belongs also to $\mathbb{{H}_{NF}}$ by Lemma
3.7. So $\mathbb{\overline{H}_{NF}}\subseteq\mathbb{{H}_{NF}}$ holds.

(3) Assuming that for a given recursive level
$\mathbb{\overline{H}_{NF}}\subseteq\mathbb{{H}_{NF}}$ holds, in the next
recursion, only disjunctions $\varphi$ in (3) are added to
$\mathbb{\overline{H}_{NF}}$. But the condition of (3) and that of Lemma 3.9
are equal; so by Lemma 3.9, $\varphi$ is in $\mathbb{{H}_{NF}}$ too. Therefore
$\mathbb{\overline{H}_{NF}}\subseteq\mathbb{{H}_{NF}}$ holds.

$\bullet$ $\mathbb{{H}_{NF}}\subseteq\mathbb{\overline{H}_{NF}}$. Given that
the structures to define $\mathbb{{N}_{NF}}$ and $\mathbb{\overline{H}_{NF}}$
in Definition 2.3 and Definition 3.12, respectively, are equal, the potential
inclusion of each NNF formula $\varphi$ in $\mathbb{\overline{H}_{NF}}$ is
systematically considered. Further, the statement: if
$\varphi\in\mathbb{{H}_{NF}}$ then $\varphi\in\mathbb{\overline{H}_{NF}}$, is
proven by structural induction on the depth of formulas and by using a
reasoning similar to that of the previous
$\mathbb{\overline{H}_{NF}}\subseteq\mathbb{{H}_{NF}}$ case and also by using
Lemmas 3.7 and 3.9. $\blacksquare$

######  Example 3.14.

We regard again $\varphi$ and $\varphi^{\prime}$ from Example 3.11:

  * •

By (3), $(\vee\ \overline{A}\ C)\in\mathbb{{H}_{NF}}$. $(\vee\ A\
\overline{B})\in\mathbb{{H}_{NF}}$.

  * •

By (2), $\\{\wedge\ \ D\ \,(\vee\ A\ \overline{B})\\}\in\mathbb{{H}_{NF}}$.
$\phi=\\{\wedge\ (\vee\ \overline{A}\ C\,)\ \\{\wedge\ \ D\ \,(\vee\ A\
\overline{B})\\}\\}\in\mathbb{{H}_{NF}}$.

  * •

By (3), $\varphi=(\vee\ \overline{A}\ \,\phi\,)\in\mathbb{{H}_{NF}}$.
$\varphi^{\prime}=(\vee\ A\ \phi\,)\notin\mathbb{{H}_{NF}}$. ∎

######  Example 3.15.

We now analyze a more complete NNF, concretely the one from the Introduction.
Let us consider $\varphi$ below wherein $\phi_{1},\phi_{2}$ and $\phi_{3}$ are
NCs:

$\varphi=\\{\wedge\ \,A\ \,(\vee\ \ \overline{B}\ \ \\{\wedge\ \ (\vee\ \
\overline{D}\ \ \overline{C}\ \ A)\ \ (\vee\ \ \phi_{1}\ \ \\{\wedge\ \
\phi_{2}\ \ {\overline{A}}\\})\ \,B\\}\,)\ \ \phi_{3}\\}$

We check under which conditions verified by $\phi_{1},\phi_{2}$ and
$\phi_{3}$, $\varphi$ is indeed HNF. The disjunctions of $\varphi$ and the
proper $\varphi$ can be rewritten as follows:

  * •

$\omega_{1}=(\vee\ \ \overline{D}\ \ \overline{C}\ \ A)$. $\omega_{2}=(\vee\ \
\phi_{1}\ \ \\{\wedge\ \ \phi_{2}\ \ {\overline{A}}\\})$.

  * •

$\omega_{3}=(\vee\ \ \overline{B}\ \ \\{\wedge\ \ \omega_{1}\ \ \omega_{2}\
\,B\\}\,).$ $\varphi=\\{\wedge\ A\ \omega_{3}\ \phi_{3}\\}.$

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

  * •

$\omega_{1}$: Trivially, $\omega_{1}$ is Horn.

  * •

$\omega_{2}$: $\omega_{2}$ is HNF if $\phi_{1},\phi_{2}\in\mathbb{H_{NF}}$ and
if at least one of $\phi_{1}$ or $\phi_{2}$ is negative.

  * •

$\omega_{3}$: $\omega_{3}$ is HNF if $\omega_{2}\in\mathbb{H_{NF}}$ (as
$\omega_{1}\in\mathbb{H_{NF}}$).

  * •

$\varphi$: $\varphi$ is HNF if $\omega_{2}\in\mathbb{H_{NF}}$ (see previous
line) and $\phi_{3}\in\mathbb{H_{NF}}$.

Recapitulating, the second ($\omega_{2}$) and fourth ($\varphi$) conditions
entail that $\varphi$ is HNF only if $\phi_{1}$, $\phi_{2}$ and $\phi_{3}$ are
HNF and if at least one of $\phi_{1}$ or $\phi_{2}$ is negative. Since the
first condition is subsumed by Proposition 3.6, we can conclude that $\varphi$
is HNF only if its sub-formulas are HNF and if at least one of $\phi_{1}$ or
$\phi_{2}$ is negative. ∎

###  3.2 Relating $\mathbb{H_{NF}}$ to the Horn and NNF Classes

We prove that $\mathbb{{H}_{NF}}$ and the Horn class are semantically
equivalent and specify the NNF fragment that forms $\mathbb{{H}_{NF}}$. To
facilitate the reading of the section, the proofs of the theorems are
relegated to Subsection 3.4. A new simple concept is introduced next.

######  Definition 3.16.

For every $\varphi\in\mathbb{N_{NF}}$, we define $cl(\varphi)$ as the unique
clausal formula that results from applying $\vee/\wedge$ distributivity to
$\varphi$ until a clausal formula, viz. $cl(\varphi)$, is obtained. We will
call $cl(\varphi)$ the clausal form of $\varphi$.

######  Example 3.17.

Applying $\vee/\wedge$ distributivity to $\varphi_{1}$ in Example 3.4, one
obtains:

$cl(\varphi_{1})=\\{\wedge\ \ (\vee\ \overline{B}\,\ \,C)\ \ (\vee\
\,\overline{B}\ A)\ \ (\vee\ \overline{D}\ \,C\,)\ \ (\vee\ \ \overline{D}\
\,A)\,\\}.$ ∎

######  Proposition 3.18.

We have $\varphi\equiv cl(\varphi)$.

The proof is trivial. We next show, in Theorem 3.19, Corollary 3.20 and
Theorem 3.21, that $cl(\varphi)$ allows to relate $\mathbb{{H}_{NF}}$ to the
classes Horn and NNF.

######  Theorem 3.19.

The clausal form of all HNF formulas is Horn, i.e.
$\forall\varphi\in\mathbb{H_{NF}}:cl(\varphi)\in\mathbb{H}.$

  * Proof.

See Subsection 3.4. $\blacksquare$

Theorem 3.19 and Proposition 3.18 yield the next semantical characterization
of $\mathbb{H_{NF}}$.

######  Corollary 3.20.

The classes $\mathbb{H_{NF}}$ and $\mathbb{H}$ are semantically equivalent:
each formula in a class is equivalent to another formula in the other class.

  * Proof.

On the one hand, by Proposition 3.18 and Theorem 3.19, for every HNF formula
$\varphi$, we have $\forall\varphi\in\mathbb{H_{NF}}:\varphi\equiv
cl(\varphi)\in\mathbb{H}$. On the other hand,
$\mathbb{H}\subset\mathbb{H_{NF}}$. $\blacksquare$

Corollary 3.20 entails that $\mathbb{H_{NF}}$ can represent the same Boolean
functions that the Horn class, viz. the Horn functions [43] (see Section
LABEL:sec:Applcac). The next theorem specifies which NNF formulas are included
in $\mathbb{{H}_{NF}}$.

######  Theorem 3.21.

All NNF formulas $\varphi$ whose clausal form is Horn are HNF, namely:

$\forall\varphi\in\mathbb{N_{NF}}\ \,\mbox{if}\ \,cl(\varphi)\in\mathbb{H}\ \
\mbox{then}\ \ \varphi\in\mathbb{{H}_{NF}}.$

  * Proof.

See Subsection 3.4. $\blacksquare$

######  Example 3.22.

For $\varphi_{1}$ and $\varphi_{2}$ from Example 3.4,
$cl(\varphi_{1})\in\mathbb{H}$ and $cl(\varphi_{2})\notin\mathbb{H}$; only
$\varphi_{1}$ is HNF. For $\varphi$ and $\varphi^{\prime}$ from Example 3.5,
$cl(\varphi)\in\mathbb{H}$ and $cl(\varphi^{\prime})\notin\mathbb{H}$; so only
$\varphi$ is HNF.

Next Theorem 3.23 puts together previous Theorems 3.19 and 3.21 and provides a
concise definition of the class of HNF formulas.

######  Theorem 3.23.

The next statement holds: $\forall\varphi\in\mathbb{N_{NF}}:\
\varphi\in\mathbb{{H}_{NF}}$ iff $cl(\varphi)\in\mathbb{H}.$

Fig. 3 exemplifies Theorem 3.23. The classes $\mathbb{{H}_{NF}}$,
$\mathbb{H}$, $\mathbb{N_{NF}}$ and $\mathbb{C}$ are depicted and each
$\varphi$ linked to its $cl(\varphi)$ with either a red or a blue line. Red
lines: $cl(\varphi_{1})$ to $cl(\varphi_{3})$ are in $\mathbb{H}$; so
$\varphi_{1}$ to $\varphi_{3}$ are HNF. Blue lines: $cl(\phi_{1})$ to
$cl(\phi_{3})$ are not in $\mathbb{H}$; so $\phi_{1}$ to $\phi_{3}$ are not
HNF.

HCHNFNNF$cl(\varphi_{1})$$\varphi_{1}$
$\phi_{1}$$cl(\phi_{1})$$cl(\varphi_{2})$$\varphi_{2}$
$cl(\phi_{2})$$\phi_{2}$$cl(\varphi_{3})$$\varphi_{3}$
$\phi_{3}$$cl(\phi_{3})$

Fig. 3. Exemplifying Theorem 3.23.

Theorem 3.23 gives indeed a concise definition of $\mathbb{H_{NF}}$ but
recognizing HNFs through Theorem 3.23 is unfeasible as computing $cl(\varphi)$
takes exponential time and space. However the detailed syntactical Definition
3.12 of $\mathbb{H_{NF}}$ will allow us (Section 5) to design an algorithmic
strategy to recognize HNFs in linear time.

###  3.3 The Horn-NC Formulas

Next define $\mathbb{H_{NC}}$ by simply applying De Morgan’s laws to
Definition 3.3 of $\mathbb{H_{NF}}$.

######  Definition 3.24.

An NC formula $\varphi$ is in $\varphi\in\mathbb{H_{NC}}$ if: (A) all its
disjunctions under the scope of no $\neg$ connective or of an even number of
$\neg$ connectives have at most one non-negative disjunct; and (B) all its
conjunctions under the scope of an odd number of $\neg$ connectives have at
most one non-positive conjunct.

######  Example 3.25.

One can check that $\varphi_{2}$ from Example 2.4 is HNC.

######  Definition 3.26.

We define the set of formulas $\mathbb{\overline{H}_{NC}}$ exclusively from
the rules below:

  * •

$\mathbb{{H}_{NF}}\subset\mathbb{\overline{H}_{NC}}$.

  * •

If $(\vee\
\varphi_{1}\ldots\varphi_{k-1}\,\varphi_{k})\in\mathbb{\overline{H}_{NC}}$
then $\neg\\{\wedge\
\neg\varphi_{1}\ldots\neg\varphi_{k-1}\,\neg\varphi_{k}\\}\in\mathbb{\overline{H}_{NC}}$.

  * •

If $\\{\wedge\
\varphi_{1}\ldots\varphi_{k-1}\,\varphi_{k}\\}\in\mathbb{\overline{H}_{NC}}$
then $\neg(\vee\
\neg\varphi_{1}\ldots\neg\varphi_{k-1}\,\neg\varphi_{k})\in\mathbb{\overline{H}_{NC}}$.

######  Theorem 3.27.

We have that: $\mathbb{{H}_{NC}}=\mathbb{\overline{H}_{NC}}$.

  * Proof.

It follows from Definition 3.24 of $\mathbb{{H}_{NC}}$ and Definition 3.26 of
$\mathbb{\overline{H}_{NC}}$, indeed both result from applying De Morgan’s
laws to $\mathbb{{H}_{NF}}$. $\blacksquare$

######  Example 3.28.

Applying De Morgan’s laws to the HNF $\\{\wedge\ \ C\ \ \\{\wedge\ \ (\vee\ \
A\ \ \overline{B}\,)\ \ \\{\wedge\ \ \overline{A}\ \
\overline{C}\,\\}\,\\}\,\\}$ yields $\varphi_{2}$ in Example 2.4 (ruling out
F); so $\varphi_{2}$ is $\mathrm{{HNC}}$. ∎

######  Definition 3.29.

For every $\varphi\in\mathbb{N_{C}}$, we define $cl^{*}(\varphi)$ as the
unique clausal formula that results from applying De Morgan’s laws and
$\wedge/\vee$ distributivity to $\varphi$ until a clausal formula, viz.
$cl^{*}(\varphi)$, is obtained.

Theorem 3.30 syntactically and semantically characterizes $\mathbb{H_{NC}}$
just as Theorems 3.19, Theorem 3.21 and Corollary 3.20 characterized
$\mathbb{H_{NF}}$.

######  Theorem 3.30.

We have that the next relationships between $\mathbb{H_{NC}}$ and
$\mathbb{N_{NC}}$ and $\mathbb{H}$:

  * •

$\forall\varphi\in\mathbb{N_{NC}}:$ $\varphi\in\mathbb{H_{NC}}$ iff
$cl^{*}(\varphi)\in\mathbb{H}$.

  * •

$\mathbb{H_{NC}}$ and $\mathbb{H}$ are semantically equivalent.

  * Proof.

As Definition 3.29 of $cl^{*}(\varphi)$ is obtained by just applying De
Morgan’s laws to Definition 3.16 of $cl(\varphi)$, the statements in Theorem
3.30 follow immediately from the same ones proved for $\mathbb{H_{NF}}$ in
Theorem 3.19, Theorem 3.21 and Corollary 3.20, respectively. $\blacksquare$

###  3.4 Formal Proofs

Before proving Theorems 3.19 and 3.21, Theorem 3.31 is required. So, we prove
successively: Theorem 3.31, Theorem 3.19 and Theorem 3.21.

######  Theorem 3.31.

Let $\varphi$ be an NNF disjunction $(\vee\
\varphi_{1}\ldots\varphi_{i}\ldots\varphi_{k}\,)$. $cl(\varphi)\in\mathbb{H}$
iff $\varphi$ has $k-1$ negative disjuncts and one disjunct s.t.
$cl(\varphi_{i})\in\mathbb{H}$, formally:

$cl(\,(\vee\
\varphi_{1}\ldots\varphi_{i}\ldots\varphi_{k}\,)\,)\in\mathbb{H}\mathrm{\ \
iff\ \ }(1)\ \exists i,\mbox{\,s.t.}\ cl(\varphi_{i})\in\mathbb{{H}}\
\mbox{\,and}\ \,(2)\ \forall j,j\neq i,\varphi_{j}\in\mathbb{N_{G}}.$

  * Proof.

If-then. By refutation: let $cl(\,(\vee\
\varphi_{1}\ldots\varphi_{i}\ldots\varphi_{k})\,)\in\mathbb{H}$ and prove that
if (1) or (2) are violated, then $cl(\varphi)\notin\mathbb{H}$.

    1. $\bullet$

(1) $\exists i$ s.t. $cl(\varphi_{i})\notin\mathbb{{H}}$.

$-$ If we take the case $k=1$, then $\varphi=\varphi_{1}$.

$-$ But $cl(\varphi_{1})\notin\mathbb{H}$ implies
$cl(\varphi)\notin\mathbb{H}$.

    2. $\bullet$

(2) $\exists j,j\neq i,\varphi_{j}\notin\mathbb{N_{G}}$.

$-$ Suppose that, besides $\varphi_{i}$, one $\varphi_{j},\,j\neq i$, has
positive literals too.

$-$ We take a simple case, concretely $k=2,\,\varphi_{1}=A$ and
$\varphi_{2}=B$.

$-$ So, $\varphi=(\vee\ \varphi_{1}\ \varphi_{2})=(\vee\ A\ B)$, which implies
$cl(\varphi)\notin\mathbb{H}$.

$\bullet$ Only-If. For simplicity and without loss of generality, we assume
that

$(\vee\
\varphi_{1}\ldots\varphi_{i}\ldots\varphi_{k-1})=\varphi^{-}\in\mathbb{N_{G}}\mbox{
and }\varphi_{k}\in\mathbb{H_{NF}}$, and prove:

$cl(\varphi)=cl(\,(\vee\ \
\varphi_{1}\ldots\varphi_{i}\ldots\varphi_{k-1}\,\varphi_{k})\,)=cl(\,(\vee\
\varphi^{-}\ \varphi_{k})\,)\in\mathbb{H}.$

$-$ To obtain $cl(\varphi)$, one must obtain first $cl(\varphi^{-})$ and
$cl(\varphi_{k})$, and so

$(i)\ \ cl(\varphi)=cl(\,(\vee\ \ \varphi^{-}\ \varphi_{k})\,)=cl(\,(\vee\ \
cl(\varphi^{-})\ \ cl(\varphi_{k})\,)\,).$

$-$ By definition of $\varphi^{-}\in\mathbb{N_{G}}$,

$(ii)\ \ cl(\varphi^{-})=\\{\wedge\ D^{-}_{1}\ldots
D^{-}_{m-1}\,D^{-}_{m}\\}$; the $D^{-}_{i}$’s are negative clauses.

$-$ By definition of $\varphi_{k}\in\mathbb{H_{NF}}$,

$(iii)\ \ cl(\varphi_{k})=\mathrm{H}=\\{\wedge\ h_{1}\ \ldots
h_{n-1}\,h_{n}\\}$; the $h_{i}$’s are Horn clauses.

$-$ By ($i$) to ($iii$),

$cl(\varphi)=cl(\,(\vee\ \ \\{\wedge\ D^{-}_{1}\
\,\ldots\,D^{-}_{m-1}\,D^{-}_{m}\\}\ \ \\{\wedge\ h_{1}\ \ldots
h_{n-1}\,h_{n}\,\\}\,)\,).$

$-$ Applying $\vee\//\wedge$ distributivity to $cl(\varphi)$ and noting
$C_{i}=(\vee\ D^{-}_{1}\ h_{i}\,)$,

$cl(\varphi)=cl(\,\\{\wedge\ \ \\{\wedge\ C_{1}\ldots C_{i}\ldots C_{n}\\}\ \
(\vee\ \,\\{\wedge\ D^{-}_{2}\ldots D^{-}_{m-1}\,D^{-}_{m}\,\\}\ \
\mathrm{H}\,)\,\\}\ ).$

$-$ Since the $C_{i}=(\vee\ D^{-}_{1}\ h_{i}\,)$’s are Horn clauses,

$cl(\varphi)=cl(\,\\{\wedge\ \ \mathrm{H}_{1}\ \ (\vee\ \ \\{\wedge\
D^{-}_{2}\ldots D^{-}_{m-1}\,D^{-}_{m}\,\\}\ \ \mathrm{H}\,)\,\\}\ ).$

$-$ For $j<m$ we have,

$cl(\varphi)=cl(\ \\{\wedge\ \mathrm{H}_{1}\
\ldots\mathrm{H}_{j-1}\mathrm{H}_{j}\ \ (\vee\ \ \\{\wedge\ D^{-}_{j+1}\ldots
D^{-}_{m-1}\,D^{-}_{m}\\}\ \ \mathrm{H}\,)\,\\}\ ).$

$-$ For $j=m$, $cl(\varphi)=\\{\wedge\ \mathrm{H}_{1}\
\ldots\mathrm{H}_{m-1}\,\mathrm{H}_{m}\
\mathrm{H}\,\\}=\mathrm{H}^{\prime}\in\mathbb{H}.$

$-$ Hence $cl(\varphi)\in\mathbb{H}$. $\blacksquare$

Theorem 3.19. We have
$\forall\varphi\in\mathbb{{H}_{NF}}:cl(\varphi)\in\mathbb{H}$.

  * Proof.

We consider Definition 3.12 of $\mathbb{{H}_{NF}}$. The proof is done by
structural induction on the depth $r(\varphi)$ of any $\varphi$ in
$\mathbb{{H}_{NF}}$, formally defined below, where $\ell_{i}$ is a literal:

$r(\varphi)=\left\\{\begin{array}[]{l l l}0&\varphi=\langle\odot\ \ell_{1}\
\ldots\ell_{k-1}\ \ell_{k}\rangle\ \mbox{or}\ \varphi=\ell.\\\
1+max\,\\{r(\varphi_{1}),\ldots,r(\varphi_{k-1}),\,r(\varphi_{k})\\}&\varphi=\langle\odot\
\varphi_{1}\ \ldots\varphi_{k-1}\ \varphi_{k}\rangle.\\\ \end{array}\right.$

$\bullet$ Base Case: $r(\varphi)=0.$

If $r(\varphi)=0$ clearly $\varphi\in\mathbb{H}$, and so
$cl(\varphi)\in\mathbb{H}$.

$\bullet$ Induction hypothesis: $\forall\varphi,\ r(\varphi)\leq n,\ \
\varphi\in\mathbb{{H}_{NF}}\mbox{ \ entails \ }cl(\varphi)\in\mathbb{H}.$

$\bullet$ Induction proof: $r(\varphi)=n+1$. By Definition 3.12, lines (2) and
(3), we have:

(2) $\varphi=\\{\wedge\
\varphi_{1}\ldots\varphi_{i}\ldots\varphi_{k}\\}\in\mathbb{{H}_{NF}}$, where
$k\geq 1$.

$-$ By definition of $r(\varphi)$, $r(\varphi)=n+1$ entails $1\leq i\leq k,\
r(\varphi_{i})\leq n.$

$-$ By induction hypothesis, $\varphi_{i}\in\mathbb{{H}_{NF}}\mbox{\, and
\,}r(\varphi_{i})\leq n\mbox{ \ entail \ }cl(\varphi_{i})\in\mathbb{H}$.

$-$ It is obvious that, $cl(\varphi)=\\{\wedge\ \ cl(\varphi_{1})\ \ldots\
cl(\varphi_{i})\ldots cl(\varphi_{k})\,\\}.$

$-$ Therefore, $cl(\varphi)=\\{\wedge\
\mathrm{H}_{1}\ldots\mathrm{H}_{i}\ldots\mathrm{H}_{k}\\}=\mathrm{H}\in\mathbb{H}$.

(3) $\varphi=(\vee\ \varphi_{1}\ldots\varphi_{i}\ldots\varphi_{k-1}\
\varphi_{k})\in\mathbb{{H}_{NF}}$, where $k\geq 1$.

$-$ By Definition 3.12, line (3), $0\leq i\leq k-1,\
\varphi_{i}\in\mathbb{N_{G}}$ and $\varphi_{k}\in\mathbb{{H}_{NF}}.$

$-$ By definition of $r(\varphi)$, $r(\varphi)=n+1$ entails
$r(\varphi_{k})\leq n.$

$-$ By induction hypothesis, $d(\varphi_{k})\,\leq n$ and
$\varphi_{k}\,\in\mathbb{{H}_{NF}}$ entail $cl(\varphi_{k})\,\in\mathbb{H}.$

$-$ By Theorem 3.31, only-if, $0\leq i\leq k-1,\ \varphi_{i}\in\mathbb{N_{G}}$
and $cl(\varphi_{k})\in\mathbb{H}$ entail:

$cl(\,(\vee\ \varphi_{1}\ldots\varphi_{i}\ldots\varphi_{k-1}\
\varphi_{k})\,)\in\mathbb{H}$. $\blacksquare$

Theorem 3.21. $\forall\varphi\in\mathbb{N_{NF}}$: if
$cl(\varphi)\in\mathbb{H}$ then $\varphi\in\mathbb{{H}_{NF}}$.

  * Proof.

It is done by structural induction on the depth $d(\varphi)$ of $\varphi$
defined as follows:

$d(\varphi)=\left\\{\begin{array}[]{l l l}0&\varphi\in\mathbb{C}.\\\
1+max\,\\{d(\varphi_{1}),\ldots,d(\varphi_{i}),\ldots\,,d(\varphi_{k})\\}&\varphi=\langle\odot\
\varphi_{1}\ldots\varphi_{i}\ldots\varphi_{k}\rangle.\\\ \end{array}\right.$

$\bullet$ Base case: $d(\varphi)=0$ and $cl(\varphi)\in\mathbb{H}$.

$-$ $d(\varphi)=0$ entails $\varphi\in\mathbb{C}$.

$-$ If $\varphi\notin\mathbb{H}$, then $cl(\varphi)\notin\mathbb{H}$,
contradicting the assumption.

$-$ Hence $\varphi\in\mathbb{H}$ and so by Definition 3.12,
$\varphi\in\mathbb{{H}_{NF}}$.

$\bullet$ Inductive hypothesis: $\forall\varphi\in\mathbb{N_{NF}},\
d(\varphi)\leq n,\ cl(\varphi)\in\mathbb{H}\mbox{ \ entail \
}\varphi\in\mathbb{{H}_{NF}}.$

$\bullet$ Induction proof: $d(\varphi)=n+1$.

By Definition 2.3 of $\mathbb{N_{NF}}$, cases $(i)$ and $(ii)$ below arise.

$(i)$ $cl(\varphi)=cl(\,\\{\wedge\
\varphi_{1}\ldots\varphi_{i}\ldots\,\varphi_{k}\\}\,)\in\mathbb{H}$ and $k\geq
1$.

$-$ Since $\varphi$ is a conjunction, $1\leq i\leq
k,\,cl(\varphi_{i})\in\mathbb{H}.$

$-$ By definition of $d(\varphi)$, $d(\varphi)=n+1$ entails $1\leq i\leq
k,\,d(\varphi_{i})\leq n.$

$-$ By induction, $1\leq i\leq k,\ \,d(\varphi_{i})\leq n,\
cl(\varphi_{i})\in\mathbb{H}$ $\mbox{\ entails\
}\varphi_{i}\in\mathbb{{H}_{NF}}.$

$-$ By Definition 3.12, line (2), $1\leq i\leq k,\
\varphi_{i}\in\mathbb{{H}_{NF}}$ entails $\varphi\in\mathbb{{H}_{NF}}$.

$(ii)$ $cl(\varphi)=cl(\,(\vee\
\varphi_{1}\ldots\varphi_{i}\ldots\varphi_{k-1}\ \varphi_{k})\,)\in\mathbb{H}$
and $k\geq 1$.

$-$ By Theorem 3.31, if-then, $0\leq i\leq k-1,\ \varphi_{i}\in\mathbb{N_{G}}$
and $cl(\varphi_{k})\in\mathbb{H}.$

$-$ By definition of $d(\varphi)$, $d(\varphi)=n+1$ entails
$d(\varphi_{k})\leq n.$

$-$ By induction hypothesis, $d(\varphi_{k})\,\leq n$ and
$cl(\varphi_{k})\in\mathbb{H}$ entail $\varphi_{k}\,\in\mathbb{{H}_{NF}}.$

$-$ By Definition 3.12, line (3), $0\leq i\leq k-1,\
\varphi_{i}\in\mathbb{N_{G}}$ and $\varphi_{k}\in\mathbb{{H}_{NF}}$ entail:

$(\vee\ \varphi_{1}\ldots\varphi_{i}\ldots\varphi_{k-1}\
\varphi_{k})=\varphi\in\mathbb{{H}_{NF}}$. $\blacksquare$

##  4 NC Unit-Resolution and the Tractability of $\mathbb{{H}_{NC}}$

We define Non-Clausal Unit Resolution, noted UR${}_{\mbox{nc}}$ and prove
that, both, UR${}_{\mbox{nc}}$ is complete for $\mathbb{{H}_{NF}}$ and that
the satisfiability of $\mathbb{{H}_{NF}}$ is tested polynomially. The calculus
UR${}_{\mbox{nc}}$ encompasses the main rule, called UR, and several
simplification rules. Albeit the latter are straightforward, UR is quite
elaborate and so is presented progressively.

Remark. If $\varphi$ is a disjunctive HNF with $k\geq 2$ disjuncts, then, by
Definition 3.3, $\varphi$ has at least one negative disjunct, and so,
assigning 0 to all its propositions satisfies $\varphi$. Hence, to avoid such
simple case we will consider that the input $\varphi$ is a conjunctive HNF.

At first, we introduce UR just for almost-clausal HNFs. Assume HNF formulas
with the almost-clausal pattern shown below and 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}\overline{\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}\overline{\ell}}}\
\phi_{j+1}\,\ldots\,\phi_{k})\ \varphi_{i+1}\,\ldots\,\varphi_{n}\\}$

These formulas are almost-clausal because if the $\varphi$’s and $\phi$’s were
clauses and literals, respectively, then they would be clausal. Trivially such
formulas are equivalent to the next ones:
$\\{{{\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}\\}$. Thus, one can derive the simple
inference rule on the left, below. By noting
$\mathcal{D}({{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\overline{\ell}}})=(\vee\
\,\phi_{1}\,\ldots\,\phi_{j}\,\phi_{j+1}\,\ldots\,\phi_{n})$, such rule can be
concisely written as indicated on the right:

$\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}\overline{\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})}{{\mbox{\,UR}}}\qquad\quad\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}}\
\,{{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\overline{\ell}}}\
\,\mathcal{D}({{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\overline{\ell}}})\,)}{\mathcal{D}({{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\overline{\ell}}})}{{\mbox{\,UR}}}$

We now extend our analysis from formulas with the previous pattern
${{\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}}\
\,{{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\overline{\ell}}}\
\,\mathcal{D}({{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\overline{\ell}}})\,)$
to those with pattern
${{\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}}\
\mathcal{C}({{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\overline{\ell}}})\
\mathcal{D}({{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\overline{\ell}}})\,)$
where
$\mathcal{C}({{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\overline{\ell}}})$
is the maximal sub-formula linked to
${{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\ell}}$
that becomes false when
${{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\overline{\ell}}}$
is false, i.e.
$\mathcal{C}({{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\overline{\ell}}})$
is the maximal sub-formula equivalent to a conjunction
${{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\overline{\ell}}}\wedge\psi$.
For instance, if $\varphi$ has the sub-formula $(\vee\ \varphi_{1}\ \\{\wedge\
\phi_{1}\ \\{\wedge\
{{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\overline{\ell}}}\
(\vee\ \phi_{2}\ \overline{A})\ \phi_{3}\\}\\}\ \varphi_{2}\,)$, we take
$\mathcal{C}({{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\overline{\ell}}})=\\{\wedge\
\phi_{1}\ \\{\wedge\
{{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\overline{\ell}}}\
(\vee\ \phi_{2}\ \overline{A})\ \phi_{3}\\}\\}$ because: (a)
$\mathcal{C}({{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\overline{\ell}}})$
verifies
${{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\overline{\ell}}}\wedge\psi={{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\overline{\ell}}}\wedge\\{\wedge\
\phi_{1}\ \,(\vee\ \phi_{2}\ \overline{A})\ \,\phi_{3}\,\\}$; and (b) no
bigger sub-formula verifies (a). It is easily checked that, the augmented UR
for the pattern
${{\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}}\
\,\mathcal{C}({{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\overline{\ell}}})\
\,\mathcal{D}({{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\overline{\ell}}})\,)$
is ${{\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}}\
\,\mathcal{C}({{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\overline{\ell}}})\
\,\mathcal{D}({{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\overline{\ell}}})\,)\vdash\mathcal{D}({{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\overline{\ell}}})$.

######  Example 4.1.

Let us consider the formula below where the $\phi_{i}$’s are HNF formulas:

$\varphi=\\{{{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\wedge}}\
\ {{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}A}}\ \
(\vee\ \ \overline{C}\ \ \\{\wedge\ \
{{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\overline{A}}}\
\ (\vee\ \ E\ \ \overline{D})\,\\}\ \ \phi_{1}\,)\ \ (\vee\ \ D\ \ \\{\wedge\
\ \phi_{2}\ \ \overline{A}\,\\}\,)\ \ \phi_{3}\,\\}.$

If we take the left-most
${{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\overline{A}}}$,
then $\varphi$ has a sub-formula with pattern
${{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}A}}\
{{\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}}\
\mathcal{C}({{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\overline{A}}})\
\mathcal{D}({{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\overline{A}}})\,)$,
in which
$\mathcal{C}({{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\overline{A}}})=\\{\wedge\
{{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\overline{A}}}\
\ (\vee\ E\ \overline{D})\,\\}$ and
$\mathcal{D}({{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\overline{A}}})=(\vee\
\overline{C}\ \phi_{1}).$ By applying UR to $\varphi$, we obtain:

$\varphi^{\prime}=\\{{{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\wedge}}\
\ {{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}A}}\ \
(\vee\ \ \overline{C}\ \phi_{1})\ \ (\vee\ \ D\ \ \\{\wedge\ \ \phi_{2}\ \
\overline{A}\,\\}\,)\ \ \phi_{3}\,\\}.$ ∎

The pattern of the almost-clausal HNFs can be rewritten
$\\{{{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\wedge}}\
\Pi\
{{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\ell}}\
({{\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}\overline{\ell}}})\
\mathcal{D}({{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\overline{\ell}}})\,)\
\Pi^{\prime}\\}$, where $\Pi$ and $\Pi^{\prime}$ represent concatenations of
formulas, i.e. $\Pi=\varphi_{1}\ldots\varphi_{i-1}$ and
$\Pi^{\prime}=\varphi_{i+1}\ldots\varphi_{k}$. Then it is not hard to check
that the general nested HNFs to which the rule UR can indeed be applied, must
have the next syntactical pattern222The notation $\langle\odot\
\varphi_{1}\ldots\varphi_{k}\rangle$ was introduced in Definition 2.3,
bottom.:

$\\{\wedge\ \Pi_{0}\
{{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\ell}}\
\langle\odot_{1}\ \,\Pi_{1}\ \ \ldots\ \ \langle\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}\overline{\ell}}})\
\mathcal{D}({{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\overline{\ell}}})\,)\
\,\Pi^{\prime}_{k}\,\rangle\ \ \ldots\ \ \Pi^{\prime}_{1}\,\rangle\
\Pi_{0}^{\prime}\,\\}$

where the $\Pi_{j}$’s and $\Pi_{j}^{\prime}$’s are concatenations of HNF
formulas, namely $\Pi_{j}=\varphi_{j_{1}}\ldots\varphi_{j_{i-1}}$ and
$\Pi^{\prime}_{j}=\varphi_{j_{i+1}}\ldots\varphi_{j_{n_{j}}},$ and the rule UR
can be expressed as follows:

$\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}}\
\langle\odot_{1}\
\Pi_{1}\ldots\langle\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}\overline{\ell}}})\
\
\mathcal{D}({{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\overline{\ell}}})\,)\
\ \Pi^{\prime}_{k}\,\rangle}\ldots\,\Pi^{\prime}_{1}\rangle}{\langle\odot_{1}\
\Pi_{1}\ldots\langle\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}\overline{\ell}}})\
\ \Pi^{\prime}_{k}\,\rangle}\ldots\,\Pi^{\prime}_{1}\rangle}{\ \mbox{UR}}$

UR means: if the input has a literal
${{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\ell}}$
conjunctively linked to a sub-formula with the pattern of the right conjunct
in the numerator, then the latter can be replaced with the formula in the
denominator. In practice, applying UR is equivalent to remove
$\mathcal{C}({{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\overline{\ell}}})$.
If we denote $\Pi$ the right conjunct of the numerator and by
$\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}\overline{\ell}}})\
\mathcal{D}({{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\overline{\ell}}})\,)$
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}\overline{\ell}}})\
\mathcal{D}({{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\overline{\ell}}})\,)$
is a sub-formula of $\Pi$, then UR can be expressed:

$\displaystyle\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}}\
\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}\overline{\ell}}})\
\
\mathcal{D}({{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\overline{\ell}}})\,)}{\Pi\cdot\mathcal{D}({{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\overline{\ell}}})}{\mbox{\,UR}}$

######  Example 4.2.

Let us consider that the following formula is HNF:

$\varphi=\\{\wedge\ \ (\vee\ \ C\ \phi_{1})\ \ (\vee\ \ \overline{A}\ \
\\{\wedge\ \ (\vee\ \ \overline{A}\ \ \overline{C}\,)\quad(\vee\ \ \phi_{2}\ \
\\{\wedge\ \ \overline{B}\ \
{{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\overline{A}}}\,\\}\,)\
\ C\,\\}\,)\
{{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}A}}\,\\}.$

Its associated DAG (tree, in this is case) is depicted in Fig. 5, left.

$\wedge$$\vee$
$\phi_{1}$
$\vee$$\overline{A}$
$\wedge$$\vee$$\overline{A}$
$\overline{C}$
$\vee$$\phi_{2}$
$\wedge$$\overline{B}$
$\overline{A}$

$\wedge$$\vee$
$\phi_{1}$
$\vee$$\overline{A}$
$\wedge$$\vee$$\overline{A}$
$\overline{C}$
$\vee$$\phi_{2}$

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

For ${{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}A}}$
and the right-most
${{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\overline{A}}}$,
the formulas in UR are the following:

$\bullet$ $\Pi=(\vee\ \ \overline{A}\ \ \\{\wedge\ \ (\vee\ \ \overline{A}\ \
\overline{C}\,)\quad(\vee\ \ \phi_{2}\ \ \\{\wedge\ \ \overline{B}\ \
{{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\overline{A}}}\,\\}\,)\
\ C\,\\}\,)$

$\bullet$ $(\vee\
\mathcal{C}({\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\overline{A}})\
\mathcal{D}({\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\overline{A}}))=(\vee\
\ \phi_{2}\ \ \\{\wedge\ \ \overline{B}\ \
{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\overline{A}}\,\\}\,)$

$\bullet$
$\mathcal{C}({\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\overline{A}})=\\{\wedge\
\ \overline{B}\ \
{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\overline{A}}\,\\}$
and
$\mathcal{D}({\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\overline{A}})=\phi_{2}$.

Then, applying UR to $\varphi$ leads $\varphi^{\prime}$ below and whose tree
is the right one in Fig. 5:

$\varphi^{\prime}=\\{\wedge\ \ (\vee\ \ C\ \phi_{1})\ \ (\vee\ \ \overline{A}\
\ \\{\wedge\ \ (\vee\ \ \overline{A}\ \ \overline{C}\,)\quad(\vee\ \
\phi_{2}\,)\ \ C\,\\}\,)\
{{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}A}}\,\\}$ ∎

$\bullet$ Simplification Rules. The simplification rules given below must
accompany UR. The first two rules simplify formulas by (upwards) propagating
$(\vee)$ from sub-formulas to formulas; $\varphi$ is the input HNF, and as
before, $\varphi\cdot\phi$ means that $\phi$ is a sub-formula of $\varphi$:

$\frac{\varphi\cdot({{\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}\,)}{\varphi\cdot({{\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}\,)}{{\bf
F}_{\vee}}\qquad\frac{\varphi\cdot\\{{{\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}\,\\}}{\varphi\cdot(\,{{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}\vee}}\,)}{{\bf
F}_{\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. $\langle\odot\
\phi_{1}\,\rangle$, and the second one removes a connective that is inside
another equal connective:

$\frac{\varphi\cdot\langle{{\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}\,\langle\odot_{2}\
\phi_{1}\,\rangle\,\varphi_{i+1}\ldots\varphi_{k}\,\rangle}{\varphi\cdot\langle{{\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}\,\rangle}{\
\odot\phi}$

$\frac{\varphi\cdot\langle{{\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}\,\langle\odot_{2}\
\phi_{1}\ldots\phi_{n}\,\rangle\,\varphi_{i+1}\ldots\varphi_{k}\,\rangle,\odot_{1}=\odot_{2}}{\varphi\cdot\langle{{\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}\,\rangle}{\
\odot\odot}$

######  Example 4.3.

We continue with Example 4.2. Picking the left-most
${\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\overline{A}}$
(colored blue in Fig. 5, right), we have
$\mathcal{C}({\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\overline{A}})={\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\overline{A}}$,
$\mathcal{D}({\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\overline{A}})=(\vee\
\\{\wedge\ \ (\vee\ \overline{A}\ \ \overline{C}\,)\ \ (\vee\ \phi_{2}\,)\ \
C\,\\}\,)$, and $\Pi=(\vee\
\mathcal{C}({\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\overline{A}})\
\mathcal{D}({\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\overline{A}}))$.
By applying UR to $\varphi^{\prime}$, the obtained formula is given in Fig. 6,
left. After two applications of $\odot\phi$ and one of $\odot\odot$, one gets
the formula associated with the right tree in Fig. 6. Finally, two
applications of UR to the two pairs C and $\overline{C}$, and A and
$\overline{A}$, and then one application of ${\bf F}_{\wedge}$ leads the
calculus UR${}_{\mbox{nc}}$ to derive $(\vee)$.

$\wedge$$\vee$
$\phi_{1}$
$\vee$$\wedge$$\vee$$\overline{A}$
$\overline{C}$
$\vee$$\phi_{2}$

$\wedge$$\vee$
$\phi_{1}$
$\vee$$\overline{A}$
$\overline{C}$
$\phi_{2}$

Fig. 6. Example 4.3

######  Definition 4.4.

We define UR${}_{\mbox{nc}}$ as the calculus formed by the UR rule and the
above described simplification rules, i.e.
UR${}_{\mbox{nc}}=\\{\mathrm{UR},{\bf F}_{\vee},{\bf
F}_{\wedge},\odot\phi,\odot\odot\\}$.

######  Lemma 4.5.

An HNF $\varphi$ is unsatisfiable iff UR${}_{\mbox{nc}}$ applied to $\varphi$
derives $(\vee)$.

The proof is rather straightforward and contains some tedious details, and so
it is omitted by space reasons.

######  Lemma 4.6.

HNF-SAT is polynomial.

  * Proof.

The number of UR and simplification rules performed is at most the number of
literals and connectives in $\varphi$, respectively,. On the other hand, it is
not difficult to find data structures to execute polynomially each rule in
UR${}_{\mbox{nc}}$. Hence, the lemma holds. $\blacksquare$

######  Proposition 4.7.

HNF-SAT is P-complete.

  * Proof.

It follows straightforwardly from HNF-SAT is polynomial, by Lemma 4.6, and
HNF-SAT includes Horn-SAT, which is P-complete [46, 31]. $\blacksquare$

Final Remark. We believe that it will be not hard to find data structures to
devise an HNF-SAT algorithm based on UR${}_{\mbox{nc}}$ with linear
complexity. Since the HNF-SAT algorithm is NC Unit-Propagation, on its basis,
effective NC DPLL solvers can be developed.

###  4.1 Beyond NC Unit-Resolution

(1) NC Hyper-Unit-Resolution. The given definition of the NC Unit-Resolution
rule can be extended to obtain NC Hyper-Unit-Resolution (HUR). Assume that the
$\varphi$ contains a conjunction of
${\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\ell}$ with
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}\overline{\ell}^{1}}})\
\
\mathcal{D}({{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\overline{\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}\overline{\ell}^{2}}})\
\
\mathcal{D}({{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\overline{\ell}^{2}}})\,)$,
where $\overline{\ell}^{i}$ denotes a specific occurrence of
$\overline{\ell}$. The simultaneous application of NC unit-resolution with two
sub-formulas is formally expressed as follows:

$\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}}\
\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}\overline{\ell}^{1}}})\
\
\mathcal{D}({{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\overline{\ell}^{1}}})\,)\
{{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\wedge}}\
\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}\overline{\ell}^{2}}})\
\
\mathcal{D}({{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\overline{\ell}^{2}}})\,)}{\Pi^{1}\succ\mathcal{D}({{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\overline{\ell}^{1}}})\wedge\,\Pi^{2}\succ\mathcal{D}({{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\overline{\ell}^{2}}})}{\mbox{\em}}$

If the sub-formula
$\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}\overline{\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}\overline{\ell}^{i}}}))$
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}\overline{\ell}}})\rangle^{i}$,
then HUR for $k$ sub-formulas is formally expressed as follows:

$\displaystyle\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}}\
\langle\Pi,\mathcal{CD}({{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\overline{\ell}}})\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}\overline{\ell}}})\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}\overline{\ell}}})\rangle^{k}}{\langle\Pi,\mathcal{D}({{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\overline{\ell}}})\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}\overline{\ell}}})\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}\overline{\ell}}})\rangle^{k}}{\mbox{
\ \text@underline{HUR}}}$

Since the
${{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}\overline{\ell}^{i}}}$’s
are pairwise different, so are the sub-formulas $\mathcal{CD}^{i}$ and
$\mathcal{D}^{i}$ in HUR. However, the formulas $\Pi^{i}$ are not necessarily
different as it is shown next:

######  Example 4.8.

Let us reconsider also the formula in previous Example 4.2:

$\varphi=\\{\wedge\ \ (\vee\ \ C\ \phi_{1})\ \ (\vee\ \
{{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\overline{A}^{1}}}\
\ \\{\wedge\ \ (\vee\ \
{{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\overline{A}^{2}}}\
\ \overline{C}\,)\quad(\vee\ \ \phi_{2}\ \ \\{\wedge\ \ \overline{B}\ \
{{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\overline{A}^{3}}}\,\\}\,)\
\ C\,\\}\,)\
{{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}A}}\,\\}.$

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

– $\Pi^{1,2,3}=(\vee\ \
{{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\overline{A}^{1}}}\
\ \\{\wedge\ \ (\vee\ \
{{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\overline{A}^{2}}}\
\ \overline{C}\,)\quad(\vee\ \ \phi_{2}\ \ \\{\wedge\ \ \overline{B}\ \
{{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\overline{A}^{3}}}\,\\}\,)\
\ C\,\\}\,)$

– $(\vee\ \
\mathcal{C}({{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\overline{A}^{1}}})\
\
\mathcal{D}({{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\overline{A}^{1}}}))=\Pi^{1,2,3}$

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

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

Applying NC Hyper Unit-Resolution yields: $\\{\wedge\ \ (\vee\ R\ \phi_{1})\ \
(\vee\ \ \\{\wedge\ \ (\vee\ \neg{R})\ \ (\vee\ \phi_{2})\ \ R\\})\
{{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}P}}\,\\}$

After simplifying: $\\{\wedge\ \ (\vee\ \ C\ \phi_{1})\ \ \overline{C}\ \
\phi_{2}\ \ C\,\
{{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}A}}\,\\}$.
Clearly, a simple NC unit-resolution deduces $(\vee)$. Altogether, the rule
HUR accelerates considerably the proof of unsatisfiability. ∎

Remark. An NC hyper unit-resolution rule even more general than HUR can be
devised to handle simultaneously $k\geq 1$ unit-clauses, $\ell_{k}$, so that
for each $\ell_{k}$, $i\geq 1$ sub-formulas
$\Pi^{k,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^{k,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^{k,i}}}))$
can be covered. That is, one can compute simultaneously $k\geq 1$ applications
of HUR (but for space reasons, we omit its formal definition).

(2) NC Local-Unit-Resolution. The UR rule can also be applied to sub-formulas
in order to accelerate the searching of proofs, i.e. to allow for shorter
proofs. Thus, if a sub-formula $\phi$ of $\varphi$ has the pattern of UR, UR
can be applied to $\phi$. Namely, applying UR to any sub-formula of $\varphi$
with pattern
$\phi={{\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}\overline{\ell}}})\
\mathcal{D}({{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\overline{\ell}}})\,)$
can be authorized and $\phi$ replaced 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}\overline{\ell}}})$.
So, Local NC Unit-Resolution, LUR, is formalized as follows:

$\displaystyle\frac{\varphi\cdot(\,{{\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}\overline{\ell}}})\
\
\mathcal{D}({{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\overline{\ell}}})\,)\,)}{\varphi\cdot(\,{{\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}\overline{\ell}}})\,)}{\mbox{\,LUR}}$

LUR means: if the input $\varphi$ has a sub-formula with pattern
${{\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}\overline{\ell}}})\
\
\mathcal{D}({{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\overline{\ell}}})\,)$,
the latter can be replaced 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}\overline{\ell}}})$,
or analogously, the formula
$\mathcal{C}({{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\overline{\ell}}})$
can be eliminated.

######  Example 4.9.

Consider again Example 4.2. Its sub-formula $\\{\wedge\ \ (\vee\ \
\overline{A}\ \
{{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\overline{C}}}\,)\
\ (\vee\ \ \phi_{2}\ \ \\{\wedge\ \ \overline{B}\ \
{{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}\overline{A}}}\,\\}\\\
\,)\ \
{{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}C}}\,\\}$
has the pattern
${{\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}\overline{\ell}}})\
\mathcal{D}({{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\overline{\ell}}})\,)$,
and so LUR can be applied to $\varphi$ as follows:
$\varphi\cdot(\,{{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}C}}\wedge\Pi\cdot(\vee\
\ \overline{A}\ \
{{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\overline{C}}}\,)\,)\vdash\varphi\cdot(\,{{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}C}}\wedge\Pi\cdot\overline{A}\,)$.
After applying LUR, one obtains:

$\\{\wedge\ \ (\vee\ \ C\ \phi_{1})\ \ (\vee\ \
{{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}\overline{A}}}\
\ \\{\wedge\ \
{{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}\overline{A}}}\quad(\vee\
\ \phi_{2}\ \ \\{\wedge\ \ \overline{B}\ \
{{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}\overline{A}}}\,\\}\,)\
\ C\,\\}\,)\
{{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}A}}\,\\}.$

Now applying HUR with
${{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}A}}$ and
the first two
${{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\overline{A}}}$’s,
one determines that $\varphi$ is unsatisfiable. ∎

######  Proposition 4.10.

If applying LUR to any NNF formula $\varphi$ results in $\varphi^{\prime}$
then $\varphi$ and $\varphi^{\prime}$ are logically equivalent.

The proof follows straightforwardly from the soundness of UR.

Observe that HUR and LUR habilitate shorter proofs. For instance, for Example
4.2, only one LUR and one HUR are enough to derive $(\vee)$. Thus, their
suitable management can make increase the overall deductive efficiency.

###  4.2 Application to Logic Programming

The introduction of NC formulas in the field of logic programming, concretely
within answer set programming, was done in [111]. Programs containing NCs in
their bodies and heads are called nested programs and have been employed in
many issues e.g. normal forms [30], extension to other logics [122], allowing
for highly-expressive predicates (aggregates) [34], etc. However, nested
definite programs, the equivalent to classical definite programs, have not
been characterized. We show that the HNF formulas are indeed the base of the
nested definite programs.

######  Definition 4.11.

An HNF rule is an expression $\Pi^{+}\rightarrow\Phi$ wherein $\Pi^{+}$ is an
NNF having only positive literals and $\Phi$ is an arbitrary HNF. An HNF
program is a set of HNF rules.

######  Example 4.12.

The nest rule is an HNF rule because its body is a positive NNF and its head
is an HNF:

$\\{\wedge\ A\ D\\}\ (\vee\ E\ \\{\wedge\ D\ C\\})\ \longrightarrow\
\\{\wedge\ \ (\vee\ \ \overline{A}\ \ C\,)\quad\\{\wedge\ \ D\ \ (\vee\ \ A\ \
\overline{B}\,)\,\\}\,\\}$ ∎

######  Proposition 4.13.

An HNF logic program is an HNF formula.

  * Proof.

Clearly a rule $(\vee\ \neg\Pi^{+}\ \Phi)$ satisfies Definition 3.3 and hence
so does a conjunction of them, i.e. an HNF logic program. $\blacksquare$

######  Lemma 4.14.

Let $\mathcal{P}$ be a proposition set, Lp an HNF logic program and $\varphi$
any arbitrary NNF. Deciding whether $\mathcal{P}\wedge Lp\models\varphi$ is
polynomial.

  * Proof.

By Lemma 4.6, one can polynomially check whether $\mathcal{P}\wedge Lp$ is
satisfiable. If so, by applying UR${}_{\mbox{nc}}$ one can polynomially
determine the positive literals that follow logically from $\mathcal{P}\wedge
Lp$, i.e. its minimal model. Finally, one can also polynomially check whether,
for such minimal model, $\varphi$ evaluates to 1 and so whether
$\mathcal{P}\wedge Lp\models\varphi$. $\blacksquare$

Given Corollary 3.20, each HNF program is equivalent to a clausal definite
program, thus one can say that the HNF programs are the nested definite
programs. On the other side, Example 4.12 visualizes the potentiality of
$\mathbb{{H}_{NF}}$ to enrich declarative rules in logic programming. As
mentioned previously, we think that future work will allow to find data-
structure to linearly test the satisfiability of $\mathbb{{H}_{NF}}$. This
would imply that the complexity of propositional HNF logic programs is linear,
that is, expressiveness can be significantly augmented while keeping the same
linear complexity of clausal logic programming [46, 31, 155]. Besides, HNF
logic programs are much smaller than their equivalent Horn programs.

##  5 Additional Properties of $\mathbb{H_{NC}}$

This section proves three additional properties of $\mathbb{H_{NC}}$.

###  5.1 Linear Recognition of $\mathbb{H_{NC}}$

We present a recognition algorithm, HNF, to determine whether an NNF is HNF
and also prove its correctness and linearity. Checking whether an NC $\varphi$
is HNC is performed by first translating $\varphi$ into an equivalent NNF
$\varphi^{\prime}$, and then, by applying HNF to $\varphi^{\prime}$. That
translation can be achieved in linear-time by merely pushing in the negations.

$\bullet$ HNF’s Principle. We call disjunctions and conjunctions of literals,
e.g. $(\vee\ \overline{A}\ B)$, flat-formulas. HNF uses two fresh literals,
$\ell^{+}$ and $\ell^{-}$, treating them as positive and negative,
respectively, and replaces flat-formulas of the input with $\ell^{+}$ or
$\ell^{-}$ as described below:

$(1)$ The strategy to bottom-up replace flat-formulas is as follows. In a
given step, HNF replaces the flat-formulas with $\ell^{+}$ or $\ell^{-}$. So,
sub-formulas containing only literals and flat-formulas are flattened and so
recursively replaced in the next step.

$(2)$ Below in (a)-(e), we enumerate the five possible cases encountered to
replace a given flat-formula $\phi$ with either $\ell^{+}$ or $\ell^{-}$.
$pos(\phi)$ is the number of positive literals of $\phi$. If case (a) holds,
then HNF halts and signals that the input is non-HNF.

  * $\bullet$

If $\phi$ is a clause, then HNF operates as follows:

    1. (a)

$pos(\phi)>1$ $\longrightarrow$ halts and returns non-HNF.

    2. (b)

$pos(\phi)=1$ $\longrightarrow$ replaces $\phi$ with $\ell^{+}$.

    3. (c)

$pos(\phi)=0$ $\longrightarrow$ replaces $\phi$ with $\ell^{-}$.

  * $\bullet$

If $\phi$ is a conjunction, then HNF acts as follows:

    1. (d)

$pos(\phi)>0$ $\longrightarrow$ replaces $\phi$ with $\ell^{+}$.

    2. (e)

$pos(\phi)=0$ $\longrightarrow$ replaces $\phi$ with $\ell^{-}$.

$(3)$ HNF returns three possible labels either non-HNF, $\ell^{-}$ or
$\ell^{+}$ whose meanings are $\varphi\notin\mathbb{H_{NF}}$,
$\varphi\in\mathbb{N_{G}}$, and $\varphi\in\mathbb{H_{NF}}/\mathbb{N_{G}}$
(non-negative HNF), respectively. Hence, the correctness of HNF amounts to:
HNF($\varphi$) returns ”non-HNF” iff $\varphi$ is not HNF.

$\bullet$ Pseudo-Code. The required data-structure is: An NNF is implemented
by associating to each sub-formula $\varphi$: (1) a pointer $[\varphi]$ that
points to the address where the linked structure of symbols constituting
$\varphi$ begins, i.e. to the root of DAG Dφ. Dφ is stored only once and each
$\varphi$-occurrence in the NNF is replaced with $[\varphi]$; and (2) an
integer $pos(\varphi)$ that, when $\varphi$ is flattened, is set to the number
of positive literals in $\varphi$. The pseudo-code of HNF is given above; the
right column indicates cases (a)-(e) in the above HNF’s principle
corresponding to the line in question.

HNF$(\,[\varphi]\,)$.

If $[\varphi]=(\vee\ \ell_{1}\,\,\ldots\ell_{i}\ldots\,\ell_{k})$ then do:

$pos(\,\varphi\,)\leftarrow$ number of positive-literals in $\varphi$.

if $pos(\,\varphi\,)>1$ then halt and return non-HNF. : (a)

if $pos(\,\varphi\,)=1$ then return($\ell^{+}$). : (b)

if $pos(\,\varphi\,)=0$ then return($\ell^{-}$). : (c)

If $[\varphi]=\\{\wedge\ \ell_{1}\,\ldots\,\ell_{i}\ldots\,\ell_{k}\\}$ then
do:

$pos(\,\varphi\,)\leftarrow$ number of positive-literals in $\varphi$.

if $pos(\,\varphi\,)>0$ then return($\ell^{+}$). : (d)

if $pos(\,\varphi\,)=0$ then return($\ell^{-}$). : (e)

else for $1\leq i\leq k,\,\varphi_{i}\neq\ell_{i}$ do:
$[\varphi_{i}]\leftarrow$ HNF( $[\varphi_{i}]$ ).

Return HNF( $[\varphi]$ ).

######  Example 5.1.

Next, we run HNF on $\varphi$ below. Its flat-formulas are $\phi_{1}=(\vee\
\overline{A}\ E)$,

$\varphi=\\{\wedge\ \ \overline{C}\ \ (\vee\ \ \overline{A}\ E\,)\ \ (\vee\ \
(\vee\ \ \\{\wedge\ \ \overline{F}\ \overline{C}\,\\}\ \ \overline{E}\,)\ \
\\{\wedge\ \ A\ B\,\\}\,)\,\\}.$

$\phi_{2}=\\{\wedge\ \overline{F}\ \overline{C}\\}$ and $\phi_{3}=\\{\wedge\
A\ B\\}$, and their associated replacements are:

  1. 1.

$pos(\phi_{1})=1$ $\longrightarrow$ case (b) $\longrightarrow$ $\phi_{1}$ is
replaced with $\ell^{+}$.

  2. 2.

$pos(\phi_{2})=0$ $\longrightarrow$ case (e) $\longrightarrow$ $\phi_{2}$ is
replaced with $\ell^{-}$.

  3. 3.

$pos(\phi_{3})=2$ $\longrightarrow$ case (d) $\longrightarrow$ $\phi_{3}$ is
replaced with $\ell^{+}$.

– After the replacements, one obtains: $\\{\wedge\ \ \overline{C}\ \ \ell^{+}\
\ (\vee\ \ (\vee\ \ \ell^{-}\ \overline{E}\,)\ \ \ell^{+}\,)\,\\}.$

– Replacing its flat-formula $(\vee\ \ell^{-}\ \overline{E}\,)$ with
$\ell^{-}$ yields: $\\{\wedge\ \ \ \overline{C}\ \ \ell^{+}\ \ (\vee\ \
\ell^{-}\ \ell^{+}\,)\,\\}.$

– Replacing its flat-formula $(\vee\ \ell^{-}\ \ell^{+}\,)$ with $\ell^{+}$
yields: $\\{\wedge\ \ \overline{C}\ \ \ell^{+}\ \ \ell^{+}\,\\}.$

– Here, HNF returns $\ell^{+}$, indicating that $\varphi$ is non-negative HNF.
∎

######  Example 5.2.

We now run HNF on the formula: $\\{\wedge\ \ \overline{C}\ \ (\vee\ \
\\{\wedge\ \ A\ \ \overline{C}\,\\}\ \ E\,)\,\\}.$

– Replacing $\\{\wedge\ \ A\ \ \overline{C}\,\\}$ with $\ell^{+}$ leads to
$\\{\wedge\ \ \overline{C}\ \ (\vee\ \ \ell^{+}\ \ E\,)\,\\}.$

– As $pos(\vee\ \ell^{+}\ E)>1$, condition (a) holds and HNF halts returning
non-HNF. ∎

######  Theorem 5.3.

Correctness of HNF: $\varphi$ is non-HNF iff  HNF($\varphi$) returns non-HNF.

  * Proof.

We denote $nn(\phi_{init})$ the number of non-negative disjuncts of any
initial disjunctive sub-formula $\phi_{init}$ of the input $\varphi$.

$\bullet$ Steps (b) to (e). A flat-formula $\phi$ is replaced with $\ell^{+}$
iff $\phi$ has some positive literal. Assume that $\phi^{\prime}$ is the
father of $\phi$. As both $\ell^{+}$ and $\phi$ are non-negative,
$nn(\phi^{\prime})=nn(\phi)$. Since sub-formulas are recursively flattened,
all initial $nn(\phi_{init})$ are recursively preserved. Hence if
$\phi_{flat}$ is the initial $\phi_{init}$ after having been flattened, then
$pos(\phi_{flat})=nn(\phi_{init})$.

$\bullet$ Step (a). Assume that (a) sometime holds. If HNF halts and returns
non-HNF, then some $pos(\phi_{flat})>1$ is encountered. But
$pos(\phi_{flat})=nn(\phi_{init})$ and $pos(\phi_{flat})>1$ entail that
$\exists\phi_{init},\ nn(\phi_{init})>1$, and so, by Definition 3.3, the input
$\varphi$ is not HNF. Hence, if HNF returns non-HNF, $\varphi$ is non-HNF. On
the contrary, supposing that the hypothesis (a) is never met, then by
following a reasoning dual to the previous, one obtains that if HNF returns
$\ell^{+}$ or $\ell^{-}$, then $\varphi$ is HNF. $\blacksquare$

######  Theorem 5.4.

Linearity of HNF: HNF$(\varphi)$ ends in time $O(size(\varphi))$.

  * Proof.

The running time of HNF is the sum of the times for building and scanning
(applying cases (a)-(e)) the DAG associated to $\varphi$. Building: pointers
are initialized and counters allocated; both in constant time; so building is
linear. Scanning: $(i)$ arcs are traversed at most once upwards and once
downwards. $(ii)$ when a sub-formula is flattened, HNF counts its positive
literals and set $pos(\phi)$ accordingly, which is done at most once and takes
$O(k)$ time, $k$ being the arity of $\phi$; so $(ii)$ is linear. $(iii)$
replacing a flat-formula with $\ell^{+}$ or $\ell^{-}$ is done at most once
and in constant time. Hence, the overall cost is linear. $\blacksquare$

###  5.2  Succinctness and Syntactical Richeness

Succinctness was introduced in [75] and is given in Definition 5.5. It
measures spatial efficiency of formula classes for knowledge modeling and has
been used in many works.

######  Definition 5.5.

Let $\mathbb{X}$ and $\mathbb{Y}$ two formula classes. $\mathbb{X}$ is at
least as succinct as $\mathbb{Y}$, noted $\mathbb{X}\leq\mathbb{Y}$, iff for
every $\varphi\in\mathbb{Y}$ there exists $\varphi^{\prime}\in\mathbb{X}$ s.t.
$\varphi\equiv\varphi^{\prime}$ and the size of $\varphi^{\prime}$ is
polynomially bounded in that of $\varphi$. $\mathbb{X}$ is strictly more
succinct than $\mathbb{Y}$ iff $\mathbb{X}\leq\mathbb{Y}$ and
$\mathbb{Y}\nleq\mathbb{X}$.

######  Proposition 5.6.

$\mathbb{H_{NC}}$ is strictly more succinct than $\mathbb{H}$.

  * Proof.

Clearly $\mathbb{H_{NC}}\leq\mathbb{H}$ because
$\mathbb{H_{NC}}\supseteq\mathbb{H}$. To prove that
$\mathbb{H}\nleq\mathbb{H_{NC}}$, it is enough to take any DNF
$\varphi\in\mathbb{H_{C}}$ with $k$ conjuncts and $n$ literals per conjunct.
Thus $cl(\varphi)\equiv\varphi\in\mathbb{H}$ and the size of $cl(\varphi)$ is
$k^{n}$. $\blacksquare$

We now deal with syntactical richness and consider that class $\mathbb{X}$ is
richer than $\mathbb{Y}$ simply if $\mathbb{X}$ subsumes $\mathbb{Y}$. As
formulas express interrelations among variables, richer classes having more
formulas supply more syntactical options to express interrelations among
variables and so have superior syntactical capabilities for knowledge
modeling. Clearly $\mathbb{H_{NC}}$ is richer than $\mathbb{H}$, but we check
that it is even exponentially richer.

######  Definition 5.7.

Let $\mathbb{X}$ and $\mathbb{Y}$ be two formula classes. $\mathbb{X}$ is
exponentially richer than $\mathbb{Y}$ iff:

  1. $($i$)$

$\mathbb{X}\supset\mathbb{Y}$.

  2. $($ii$)$

$\forall\varphi^{\prime}\in\mathbb{Y}$ there are exponentially many
$\varphi\in\mathbb{X}$ s.t. $\varphi\equiv\varphi^{\prime}$.

######  Proposition 5.8.

$\mathbb{H_{NC}}$ is exponentially richer than $\mathbb{H}$.

The proof is straightforward. Note, however, that the previous proposition
does not imply that $\mathbb{H_{NF}}$ is exponentially richer than
$\mathbb{H}$.

##  6 Related Work

Given that $\mathbb{H_{NC}}$ results from merging the NC and Horn formulas, we
review the main literature relative to both of kind of formulas.

###  6.1 Non-Clausal Reasoning

Logic Programming. This area has been discussed in Subsection 4.2.

Satisfiability. Given the growing efficiency of clausal DPLL solvers,
enhancing NC reasoning tended toward translating NCs into equisatisfiable
clausal ones via Tseitin-like [148] translators, and then, applying DPLL
solvers. Yet, the benefits of translations were questioned [146, 121, 56],
which advocated both, developing approaches computing original NCs and
incorporating structural information in the search. On the other side, a
number of approaches for NC satisfiability exist: NC Resolution [119], NC DPLL
[125, 73, 146, 94], path dissolution and anti-links [132], connection calculi
[126], regular, connected tableaux [80], NC tableaux-like with reductions
[76], SLD-resolution [141] and general matings [93]. The experimental results
showed the relative good performance of DPLL. Although several NC DPLL solvers
have been implemented, NC unit resolution had not been published. On the other
side, a rule called NC unit-dissolution is introduced in [120], but this is
done within the framework of other general rule (Dissolution) and it is not
formalized. Our work led to formally define NC unit-resolution for the first
time, prove its completeness for $\mathbb{H_{NC}}$ and it allowed to
demonstrate the polynomiality of $\mathbb{H_{NC}}$.

Incomplete Solvers. For clausal problems, GSAT [140] demonstrated that an
incomplete solver can solve many hard problems much more efficiently than
complete solvers. Several authors have generalized these techniques to NCs.
Sebastiani [136] suggested how to modify GSAT to be applied to NCs. Kautz et
al. [96] introduced DAGSat for clausal formulas, but allowed handling of NCs
without an increase in size. Later, Stachniak [142] introduced polWSAT an
evolution of WalkSAT [139] to handle NCs. The authors in [118] present a new
way of expressing the scoring function for evaluating partial interpretations
and their solver outperforms previous complete and incomplete NC solvers. Yet,
as HNCs are polynomial, designing incomplete NC solvers for them has limited
interest. UR${}_{\mbox{nc}}$ could be relevant to develop incomplete NC-SAT
solvers.

Quantified Boolean Formulas. An extension of the SAT problem increasingly
present in research and applications, is featuring universal and existential
quantifiers for boolean variables giving rise to the QBFs. In particular,
developing efficient solvers for QBFs in NC form is a concern of contemporary
research as evidenced by the reported performances, e.g. [113, 61, 14].
However, to the best of our knowledge, no results presented here concerning
$\mathbb{H_{NC}}$ and UR${}_{\mbox{nc}}$ have been initialized for QBFs in NC.

Max-SAT. Some reasoning problems have been intensively studied for clausal but
hardly for NC, and sometimes, even no truly NC definition exists. MaxSAT is an
example. The reached efficiency for MaxSAT [108] contrasts with the
nonexistence of a proper definition for NC-MaxSAT. A recent work [110] defines
NC-MaxSAT as the problem of, given $k$ NCs
{$\varphi_{1},\,\varphi_{2},\ldots,\varphi_{k}$}, determining the greatest
$i$, $i\leq k$, of simultaneously satisfiable formulas. In such definition the
only envisaged formula inter-dependence is the one derived from the shared
literals which is, however, rather clausal-like. The proper NC inter-
dependence is the one derived from the connexions among formulas and sub-
formulas. Applications of clausal Unit Propagation include its use for
improving the lower-bound during the solving of MaxSAT [109]. Thus
UR${}_{\mbox{nc}}$ seems essential to compute efficiently NC-MaxSAT.

Theorem Proving. Automated reasoning in NC and FOL has been an active research
field since the 1960s and is still the object of considerable research and
progress, e.g. [80, 85, 126, 63]. On the other side, DPLL for clausal FOL has
already been developed [18, 17]. Extending NC FOL with equality logic is a
former [13] as well a recent [124] concern. Although our approach has been
initially oriented towards propositional logic, it is extensible to FOL.
Concretely, we plan to propose a FOL NC DPLL by lifting UR${}_{\mbox{nc}}$ to
FOL (Future Work), which means, moreover, to generalize to clausal approach in
[18, 17].

Resolution. In the seminal work by N. Murray [119], NC Resolution for
propositional and FOL was defined in a combined functional and classical
manner and has been applied to different contexts, e.g. [13, 141]. Each proper
NC Resolution is followed by some functional-logical simplifications of the
formula. The completeness of NC Resolution under a linear restriction was
proved by the authors in [80]. Although NC Resolution was specified in 1982,
paradoxically no NC Unit-Resolution version had been published. NC Hyper-
resolution had not been defined either to our knowledge. The available
definition of NC Resolution suffers form some drawbacks e.g. not clearly
defining the potential resolution steps or requiring complex completeness
proofs [80]. We plan to present a new definition of NC Resolution (see future
work).

Knowledge Compilation. It consists in translating an original formula into
another equivalent one during the off-line phase. Whereas the original and
target formulas are semantically equivalent, the target class present desired
syntactical conditions permitting computing the clausal entailment test
polynomially. This way, the on-line exponential complexity, usually present
during query-answering, is confined to the off-line phase and later amortized
over all on-line queries answered polynomially. NNF sub-classes, such as DNNF,
d-NNF or the well-known BDD and OBDD [50], were introduced as target ones by
A. Darwiche [48, 49]. $\mathbb{H_{NC}}$ is polynomial for satisfiability
checking, i.e. for clausal entailment, but $\mathbb{H_{NC}}$ is incomplete
since not all NNFs are of course equivalent to, and so representable by, an
HNC. So, $\mathbb{H_{NC}}$ does not qualify as a target class. Yet in [64],
the class formed by the disjunctions of Horn formulas, or
$\mathbb{H}$-[$\vee$], is introduced as a target class. learly, the class of
disjunctions of HNCs, or $\mathbb{H_{NC}}$-[$\vee$], subsumes
$\mathbb{H}$-[$\vee$] and is strictly more succinct, likewise
$\mathbb{H_{NC}}$ is strictly more succinct than $\mathbb{H}$. Towards using
$\mathbb{H_{NC}}$-[$\vee$] as a target class, the next questions should be
analyzed: how to compile knowledge into $\mathbb{H_{NC}}$-[$\vee$]; which is
its complexity for consistency, clausal entailment, implicants, etc. [50]; and
finally, its succinctness should be compared with existing target classes.

###  6.2 Horn Formulas

Due to the ubiquity of Horn formulas in knowledge representation and automated
reasoning, and by space reasons, our related work is unavoidably incomplete.
It focuses first on their presence in knowledge representation and then in
automated reasoning.

####  6.2.1 Knowlegde Representation.

Propositional logic. As alluded to in the introduction, finding polynomial
clausal super-classes of the Horn class has been a key issue on increasing
clausal efficiency since 1978 [107]. Most of such extensions are presented
below chronologically along with their relationships. Our research has allowed
to lift the Horn formulas to NC and prove that tractable reasoning also exists
in NC, but we think that this is just a first outcome and that some Horn
extensions pointed out below can also be NC lifted. For instance, one can
conceive the renomable-HNC formulas as those NCs whose clausal form is
renomable-Horn.

$\bullet\ \mathsf{Unit\ Propagation}$. The so-called Unit Propagation was
proved complete for Horn-SAT in [84, 70, 117]. Further publications [90, 55,
135] get this universally understood. The linearity of Horn algorithms [55,
91, 117, 135, 72, 60] gave rise to efficient implementation of Unit
Propagation. Deciding if a model of a Horn formula is unique is also linear
[129].

$\bullet\ \mathsf{Hidden\ Horn}$. A given formula is hidden Horn [107, 7] if a
change in the polarity of some variables leads to an equivalent Horn formula.
Recognizing hidden Horn formulas is linear [7, 37] and since Horn-SAT is
linear, so is SAT-checking them.

$\bullet\ \mathsf{S_{0},\ Hierarchy\ \varphi_{K}}$. Another Horn extension was
proposed in [160], called $S_{0}$, and later Generalized Horn in [37], and
successively broadened in [6, 69]. Recognizing and SAT-checking $S_{0}$
formulas are quadratic [6, 69]. Reference [69] defines recursively a hierarchy
$\Sigma_{0}\subseteq\Sigma_{1}\ldots\subseteq\Sigma_{k}\ldots$ over the non-
clausal classes $\Sigma_{k}$, where $\Sigma_{0}$ are the Horn formulas and
$\Sigma_{1}$ is $S_{0}$. This hierarchy was strengthened in [130] whose
classes $\Pi_{k}$ subsume the classes $\Sigma_{k}$. SAT-checking $\Sigma_{k}$
and $\Pi_{k}$ formulas is polynomial but recognizing the renamings of
$\Sigma_{k}$ formulas, $k>1$, is $\mathcal{NP}$-complete [62].

$\bullet\ \mathsf{Q\cdot Horn}$. The Q-Horn formulas [28] subsume the Horn,
hidden Horn and the Quadratic (2-CNF) formulas. Q-Horn formulas are recognized
and SAT-checked linearly [28, 29].

$\bullet\ \mathsf{Extended\ Horn}$. The extended-Horn formulas were introduced
in [38] based on a theorem in [36]. Their definition relies on Unit
Propagation and matrix multiplication. Hidden extended-Horn formulas are
defined in the same way as hidden Horn from Horn. SAT-checking extended-Horn
formulas is linear; however, no polynomial recognition of the extended-Horn
formulas is known.

$\bullet\ \mathsf{Hierarchy\ \Omega}$. The hierarchy $\Omega$ of classes
proposed in [45] contains the classes Horn, reverse-Horn (clauses have at most
one negative literal) and hidden-Horn. The classes in $\Omega$ are recognized
and SAT-checked polynomially.

$\bullet\ \mathsf{SLUR}$. The definition of the SLUR (Single Lookahead Unit
Resolution) formulas [134, 15] is based on an algorithm rather than on
properties of formulas. SAT-checking a formula $\varphi$ is divided in two
phases. First unsatisfiability is sought by applying Unit Propagation (UP). If
such seeking fails, then $\varphi$ is assumed to be satisfiable and a
satisfying assignment is guessed using UP-lookahead to avoid obviously false
assignments. The class SLUR contains those formulas where the algorithm
succeeds in the first phase or finds a satisfying assignment in the second
phase. The class SLUR subsumes the hidden-Horn, extended-Horn and other
classes [144]. SLUR and Q-Horn are incomparable [67]. The SLUR formulas are
efficiently SAT-checked but recognizing them is coNP-complete [153].

$\bullet\ \mathsf{Quad}$. The class Quad [44] includes the Horn and the
Quadratic (2-CNF) formulas. Quad is not subsumed by the hierarchy $\Omega$,
and Q-Horn and Quad are incomparable. Recognizing and SAT-checking Quad
formulas take quadratic time.

$\bullet\ \mathsf{Autarkies}$. If a partial assignment satisfies all those
clausewe thinks of $\varphi$ affected by it, i.e., no new clauses are created,
the resulting formula is an autarky, e.g. the simplest autarkies are the pure
literals. Therefore, $\varphi$ is satisfiable iff its autarky is. The class of
autarkies include Q-Horn and is incomparable with the class SLUR [151].
Finding the specific linear autarkies is polynomial [104] and there exist
partial autarkies  that applied repeatedly result in a unique, autarky-free
formula.

$\bullet\ \mathsf{Matched}$. The matched formulas were analyzed initially in
[147] in order to provide a benchmark for testing some previously published
formulas but were considered rather useless. However, although the class
matched is incomparable with Q-Horn and SLUR, w.r.t. frequency of occurrence
on random formulas, reference [67] verified that matched is far more common
than both those classes together. Matched formulas are always satisfiable and
trivially SAT-checkable.

$\bullet\ \mathsf{Minimally\ Unsatisfiable}$. Several classes of unsatisfiable
formulas are identified in [105]. A formula is minimally unsatisfiable if it
is unsatisfiable and removing any clause results in a satisfiable formula
[33]. Minimally unsatisfiable formulas are SAT-checked polynomially.

$\bullet\ \mathsf{Various\ results}$ [152]. The next results are provided in
[152]: (i) none of the classes $S_{0}$, Q-Horn and extended Horn subsumes any
other; (ii) a new class is defined that subsumes $S_{0}$; and (iii) originated
in that new class, a hierarchy of classes is proposed that generalizes
$\Omega$ (see hierarchy $\Omega$ above) and the classes $S_{0}$ and Q-Horn.
Recognizing and SAT-checking the newly described, hierarchical classes are
both polynomial.

$\bullet\ \mathsf{CC\cdot balanced}$. The CC-balanced formulas have been
studied in [41] and the motivation for this class is when Linear Programming
relaxations of SAT-checking have non-integer solutions. Recognizing and SAT-
checking CC-balanced formulas are linear.

$\bullet\ \mathsf{UP\cdot Horn}$. The UP-Horn formulas [66] include the Horn
and the non-Horn formulas resulting in Horn formulas after applying the Unit
Propagation. Thus, recognizing and SAT-checking UP-Horn formulas are
polynomial.

$\bullet\ \mathsf{SLUR\ hierarchies}$. SLUR($i$) [153] is a hierarchy on top
of the class SLUR. Level $i$-th consists in making the SLUR algorithm to
consider simultaneously $i$ literals and their corresponding $2^{i}$
assignments. SLUR*($i$) [15] is a hierarchy more general than SLUR($i$) and
relies on allowing DPLL to backtrack at most $i$ levels. The class $SLUR_{K}$
is introduced in [77] and proved that it strongly subsumes previous
hierarchies SLUR($i$) and SLUR*($i$). The authors in [77] develop another
polynomial SAT class $UC_{K}$ based on the class Unit-refutation Complete,
$UC$ [52], and prove a major result, concretely that $SLUR_{K}=UC_{K}$.

$\bullet\ \mathsf{Various\ results}$ [3]. Reference [3] presents some new
polynomial fragments based on Unit Propagation: (i) the polynomial class in
[147], formed by formulas whose variables may appear at most twice, is
extended; (ii) some series of benchmarks from the DIMACS repository and from
SAT competitions are shown to belong to UP-Horn; and (iii) some set relations
between the classes Quad and UP-Horn are established.

Beyond Propositional Logic. Horn formulas are used in a large variety of
artificial intelligence logics. Hence, we make reference just to some logics
somewhat close to propositional logic and whose NC lifting is discussed in
Future Work.

$\bullet$ $\mathsf{Regular\ Many\cdot Valued}$ and $\mathsf{Possibilistic\
Logics.}$ The regular many-valued Horn formulas [79] and the possibilistic
Horn formulas [106, 58, 59] have been lifted to NC in [88, 89].

$\bullet$ $\mathsf{Linear\ Arithmetic\ Logic.}$ In linear arithmetic logic [8,
9], an atom is a disequality, e.g. $4x_{1}+x_{3}\neq 3$, or a weak inequality,
e.g. $3x_{1}+x_{4}\leq 10$. A Horn arithmetic clause is a disjunction of any
number of disequalities and at most one weak inequality. An example of a Horn
arithmetic clause is given below. Satisfiability of Horn arithmetic formulas
is polynomial [103]. Future work section considers the extension of this class
to NC form.

$(3x_{1}+x_{5}-4x_{3}\leq 7)\vee(2x_{1}+3x_{2}-4x_{3}\neq
4)\vee(x_{2}+x_{3}+x_{5}\neq 7)$

$\bullet$ $\mathsf{Horn\ Constraint\ Systems.}$ Different classes of numerical
Horn formulas are studied in [143]. The authors consider the next setting: if
${\bf x}$ and ${\bf a}$ are vectors and ${\bf A}$ is a matrix, a system of
constraints ${\bf A\cdot x\geq a}$ is called Horn constraint system if: (a)
the entries in A are in $\\{0,1,-1\\}$; (b) each row of A contains at most one
positive entry; (c) x is a real vector; and (d) a is a integral vector. A
comprehensive account of a variety of theses Horn constraint systems and their
corresponding complexity is given in [158]. Whether or not these classes can
be extended to NC form is an open issue for us.

$\bullet$ $\mathsf{\L ukasiewicz\ Logic.}$ The authors in [27] defined Horn
formulas in the infinite-valued Łukasiewicz logic and proved that their
satisfiability problem is NP-complete. However, it was proven to be polynomial
for the 3-valued case [25]. Further tractable and intractable subclasses are
given in [26]. Future work section regards this class to be extended to NC.

####  6.2.2 Automated Reasoning

The models of Horn formulas form a lattice333A fact observed first by McKinsey
[115] (see also [87]) and this mathematical tool is also the underlying
structure within a large number of domains: lattice theory, hypergraph theory,
data bases, concept analysis, artificial intelligence, knowledge spaces,
Semantic Web, etc. This fact entails that many concepts and algorithms have
been developed for Horn formulas in different realms and there exist bijective
links between the elements belonging to different fields [23]. See [2, 156,
22] for comprehensive surveys. Thus, we give a short overview of some selected
reasoning problems which are tighter connected with $\mathbb{H_{NC}}$.

Horn Functions. Noting $\mathcal{B}=\\{0,1\\}$, a Boolean function
$f_{\mathcal{B}}$ is a mapping $\mathcal{B}^{n}\rightarrow\mathcal{B}$.
$f_{\mathcal{B}}$ is modeled by a formula $\varphi$ iff $f_{\mathcal{B}}$
assumes 1 exactly on the 0-1 vectors corresponding to the models of $\varphi$
and 0 elsewhere. The next claims are well-known [81, 82, 43].

$-$ $f_{\mathcal{B}}$ is representable by numerous formulas.

$-$ $f_{\mathcal{B}}$ is representable by a clausal formula.

$-$ $f_{\mathcal{B}}$ represents a unique Boolean function.

If $f_{\mathcal{B}}$ is a Horn function $f_{\mathcal{H}}$ and is defined on
$(x_{1},x_{2},\ldots,x_{n})$, then $f_{\mathcal{H}}$ fulfills [43]:

$-$ The set of models of $f_{\mathcal{H}}$ is closed under componentwise
conjunction.

$-$ $f_{\mathcal{H}}$ is representable by a Horn formula.

$-$ The true points of $f_{\mathcal{H}}$ form a closure system on
$\\{x_{1},x_{2},\ldots,x_{n}\\}$.

Given a $f_{\mathcal{H}}$, obtaining its Horn formula is done in [21]. Horn
functions are also representable by non-Horn formulas and to decide whether an
arbitrary clausal formula represents a Horn function is co-NP-complete [43]. A
prime implicant, fundamental in Boolean functions, of $f_{\mathcal{B}}$ is a
clause $C$: (i) whose models include those of $f_{\mathcal{B}}$ and (ii) no
sub-clause of $C$ satisfies (i). Any $f_{\mathcal{B}}$ is representable by the
conjunction of its prime implicants. Searching all prime implicants of any
$f_{\mathcal{B}}$ is NP-complete. The prime implicates of any
$f_{\mathcal{H}}$ are Horn clauses. A main application of Horn functions is
finding the Horn representation of any $f_{\mathcal{H}}$ with minimal size,
which has several applications, e.g. compacting knowledge bases [83]. The
steps to find the required prime implicants of any $f_{\mathcal{B}}$ are: (1)
obtaining the prime implicants of $f_{\mathcal{B}}$ and (2) finding which
prime implicants can be discarded. The minimization problem is NP-hard, for
general and also for Horn funtions [82]. Horn functions are a sub-class of
other more general Boolean functions such as the renamable-Horn and the Q-Horn
functions [43] representable by Horn-renamable and Q-Horn formulas,
respectively (see Subsection 6.2.1).

Given that Horn functions [43] are representable by a Horn formula and
Corollary 3.20 states that both $\mathbb{H_{NC}}$ and the Horn class are
semantically equivalent, $\mathbb{H_{NC}}$ can serve for the analysis of Horn
functions. In fact, $\mathbb{H_{NC}}$ turns out to be an attractive option to
the Horn class taking into account that, as proved in Section 5,
$\mathbb{H_{NC}}$ is linearly recognizable and its HNC formulas can be even
exponentially smaller than their clausal Horn representations.

Implicational (Closure) Systems. They are used to express strong implications
between attributes in databases (functional depdendencies) and relational data
[51], but are relevant in many domains. We refer to [2, 156, 22] for recent
overviews. A formal context $\mathbb{K}$ is a 3-tuple $(G,M,I)$, where $G$ are
objects, $M$ are attributes and $I$ is a binary table indicating which objects
have which of the attributes [71]. A formal concept is a 2-tuple
$(O_{i},A_{i})$ where $O_{i}$ is a set of objects and $A_{i}$ is a set of
attributes and means that every object in $O_{i}$ has every attribute in
$A_{i}$. If an object is not in $O_{i}$ then there is an attribute in $A_{i}$
which that object does not have; and for every attribute that is not in
$A_{i}$ there is an object in $O_{i}$ that does not have that attribute. An
implication $A\rightarrow B$ means each object having all attributes in $A$
also have all attributes in $B$. An implication system $\Sigma$ defined on a
set $S$ is a binary relation on $\mathcal{P}(S)$ and consists of a set of
implication rules $A\rightarrow B$, where $A,B\in\mathcal{P}(S)$. The family
$\mathcal{F}$ that satisfies all implication rules in $\Sigma$ is:

$\mathcal{F}_{\Sigma}=\\{X\subseteq S:A\subseteq X\ \mbox{imply}\ B\subseteq
X\ \mbox{for all}\ A\rightarrow B\in\Sigma\\}$

$(\mathcal{F}_{\Sigma},\subseteq)$ is a closed set lattice where a closure of
$X\subseteq S$ is obtained via the operator $\varphi_{\Sigma}$:

$\bullet\ \varphi_{\Sigma}(X)=\pi(X)\cup\pi^{2}(X)\cup\pi^{3}(X)\cup\ldots$
(up to saturation) with

$\bullet\ \pi(X)=X\cup\bigcup\,\\{B:A\subseteq X\ \mbox{and}\ A\rightarrow
B\in\Sigma\\}$

An algorithm to obtain $\varphi_{\Sigma}(X)$ is in [43]. There are tight
connections between Horn functions and implication systems [23]. Implication
systems can be viewed from a logic-based perspective as follows. $A\rightarrow
B$ holds in $\mathbb{K}$ if each object that belongs to attributes in $A$ also
belongs to atributes in $B$. Any $\Sigma$ is complete for $\mathbb{K}$ if, for
all $A\rightarrow B$: $\mathbb{K}\models A\rightarrow B\ \ \mbox{iff}\ \
\Sigma\vdash A\rightarrow B$. $\Sigma$ and $\Sigma^{\prime}$ are equivalent if
$\varphi_{\Sigma}(X)=\varphi_{\Sigma^{\prime}}(X)$. $A\rightarrow B$ follows
from $\Sigma$, noted $\Sigma\models A\rightarrow B$, if $\Sigma\cup
A\rightarrow B$ is equivalent to $\Sigma$. Then, we have [156]: $\Sigma\models
A\rightarrow B\quad\mbox{iff}\quad B\subseteq\varphi_{\Sigma}(A)$. The
possibility of managing implications by inference systems is one of its
outstanding features. Equivalent systems are obtained with inference rules
whose aim is to turn the original system into an equivalent system fulfilling
some desired properties. Thus, many methods to compact implication system have
been proposed and the first was formed by the Armstrong rules [5].

Implication systems with the HNF syntax can be contemplated. Classical
implications can be extended with HNF implications as those of Definition 4.11
and Example 4.12. This would allow for compacter representations of
implication systems, which is one of their desired properties, viz.
optimality. However, compacter syntactical forms have more complex structures
and so defining inferences with HNF implications makes difficult to ensure
their completeness. Another interesting issue is that of directness.
Directness with HNF implications amounts to, given any arbitrary set $X$, find
$\varphi_{\Sigma}(X)$ with just one traversal of the HNF system. A polynomial
algorithm based on UR${}_{\mbox{nc}}$ could be devised for getting
$\varphi_{\Sigma}(X)$ in an HNF direct implication-system, and likely even
with linear complexity.

Directed Hypergraphs. A directed hypergraph is an pair $(E,\mathcal{H})$, $E$
being a vertex set and $\mathcal{H}$ a hyper-edge set. Hypergraphs have been
applied in many domains including implication systems. Horn formulas can be
mapped into a directed hypergraph e.g., [12] and Horn-SAT can be proved to be
P-complete via P-completeness of the reachability problem in directed
hypergraphs. Assuming that a Horn formula is satisfiable and a new clause is
inserted, the satisfiability question is answered in $O(1)$ time and inserting
a new clause of length $q$ in $O(q)$ amortized time [11]. If $m$ clauses of a
unsatisfiable Horn formula are deleted, the time needed to maintain the
satisfiability state and its minimum model is $O(n\times m)$, $n$ being the
number of variables [10]. We think that a reachability notion can be roughly
defined on the DAG of any $\varphi\in\mathbb{H_{NC}}$ as follows: (i)
initially only positive-literal nodes in unit clauses are reachable; (ii) a
negative-literal node is reachable if its dual positive-literal node is
reachable; (iii) a negative $\vee$-node (resp. $\wedge$-node) is reachable if
all (resp. one) of its negative disjunct nodes are reachable; and (iv) the
non-negative disjunct node in a $\vee$-node is reachable if all its negative
disjunct nodes are reachable; and (v) all conjunct nodes of a reachable non-
negative $\wedge$-node are reachable. Thus $\varphi$ is unsatisfiable iff the
node F is reachable on the DAG of $\varphi$. The satisfiability of
$\mathbb{H_{NC}}$ also is P-complete because both it is polynomial and
contains Horn-SAT. The mentioned problems studied for the clausal scenario
when clauses are inserted or deleted from a (un)satisfiable formula, such as
maintaining the minimum model of an HNC, are worthwhile issues to be tackled.

Horn Approximations. An alternative to knowledge compilation has been
developed in [137, 98, 138, 114] and consists in compiling a formula $\varphi$
into two Horn formulas $H_{lb}$ and $H_{ub}$ so that many queries performed
under $\varphi$ can be performed under $H_{lb}$ and $H_{ub}$ polynomially.
Thus, the goal is finding $H_{lb}$ and $H_{ub}$ whose models
$\mathcal{M}(H_{lb})$ and $\mathcal{M}(H_{ub})$ verify
$\mathcal{M}(H_{lb})\subseteq\mathcal{M}(\varphi)\subseteq\mathcal{M}(H_{ub})$.
Then one disposes of: (i) sound approximation:
$\mathcal{M}(H_{ub})\models\phi$ implies $\varphi\models\phi$, and (ii)
complete approximation: $\mathcal{M}(H_{lb})\not\models\phi$ implies
$\varphi\not\models\phi$. To maximize these concepts, the tightest
approximations must be sought, which are: (i) $H_{glb}$ s.t.
$\mathcal{M}(H_{lb})\subseteq\mathcal{M}(H_{glb})\subseteq\mathcal{M}(\varphi)$
for all $H_{lb}$; and (ii) $H_{lub}$ s.t.
$\mathcal{M}(\varphi)\subseteq\mathcal{M}(H_{lub})\subseteq\mathcal{M}(H_{ub})$
for all $H_{ub}$. Finding Horn approximations is mildly harder than solving
the original clause entailment, i.e. it is $\mathrm{P^{NP[O(logn)]}}$-hard
[35]. Determining HNFs $\varphi_{1}$ and $\varphi_{2}$ verifying the
requirements for $H_{glb}$ and $H_{lub}$ is clearly harder than determining
the proper $H_{glb}$ and $H_{lub}$ as clausal formulas have simpler
syntactical structure than NC formulas. However, some simple HNFs can be
considered to start with, e.g. a conjunction of disjunctions formed by
negative literals and one conjunction of positive literals, which amounts to
compact Horn clauses sharing the same negative literals. Besides, as HNFs are
much smaller than their Horn clausal counterparts and also clause entailment
(unsatisfiability) with HNFs is polynomial, HNFs will allow accelerating on-
line answering.

Abduction. Abduction is the problem of, given a Horn function $f_{H}$ and a
assumption set $\mathcal{S}$ of propositions, generating an explanation for a
literal $\ell$, which is a subset $\mathcal{E}\subseteq\mathcal{S}$ verifying:
(i) $f_{H}\wedge\mathcal{E}$ is satisfiable, and (ii)
$f_{H}\wedge\mathcal{E}\models\ell$. The complexity of abduction depends on
the representation of $f_{H}$: if $f_{H}$ is represented by its characteristic
models, then abduction is polynomial [97], wheras it is NP-complete if $f_{H}$
is represented by OBDDs [86]. The complexity of abduction when Boolean
functions are presented by HNC formulas should be studied, but it is likely
polynomial because the above conditions (i) and (ii) are checked polynomially,
taking into account that $\mathbb{H_{NC}}$ is polynomial for satisfiability
testing.

Petri Nets. There are tight relations between rule-based systems and Petri
Nets [161, 39, 112]. Petri Nets are used to verify properties of rule-based
systems such as inconsistency, redundancy and circularity rules. A transition
$T$ having several input places $P_{1},P_{2},\ldots,P_{j-1}$ and several
output places $P_{j},P_{j+1},\ldots,P_{k}$ is modeled by rule (1) below:

(1) $P_{1}\wedge\ldots\wedge P_{j-1}\longrightarrow P_{j}\wedge\ldots\wedge
P_{k}$ (2) $T_{1}\vee\ldots\vee T_{j-1}\longrightarrow T_{j}\wedge\ldots\wedge
T_{k}$

A place $P$ preceded by several transitions $T_{1},T_{2},\ldots,T_{j-1}$ and
followed by several transitions $T_{j},T_{j+1},\ldots,T_{k}$ is modeled by
rule (2) above. As rules (1)-(2) are not Horn, a normalization process [161]
must be applied, which of course significantly increases the size of the
obtained knowledge base. However, both rules are indeed HNF according to
Definition 4.11, and so, they can be polynomially tackled with
UR${}_{\mbox{nc}}$-based inferences.

##  7 Future Work

Our presented approach can be extended smoothly to heterogeneous logics,
accommodated to different reasoning settings, and used as a base towards
developing the NC paradigm. Future research, that is likely to receive our
attention, is divided into two axes.

###  7.1 $\mathbb{H_{NC}}$ and UR${}_{\mbox{nc}}$ for Several Logics

We will define $\mathbb{H_{NC}}$ and UR${}_{\mbox{nc}}$ for several logics and
validate each UR${}_{\mbox{nc}}$ by proving its completeness for its
corresponding $\mathbb{H_{NC}}$. Then, based on UR${}_{\mbox{nc}}$, we will
design Horn-NC-SAT algorithms, which are useful e.g. in DPLL reasoners.

Propositional logic. Since $\mathbb{H_{NC}}$ should play in NC a rôle similar
to the rôle played by Horn in clausal efficiency, worthy research efforts
remain to devise a highly-efficient Horn-NC-SAT algorithm. As Horn-SAT is
linear, proving that Horn-NC-SAT is also linear would suggest that reaching
clausal efficiency in some NC settings is conceivable. We have shown that
Horn-NC-SAT is polynomial and we believe that its linearity can be proved.

Logic Programming. This topic has been discussed in Subsection 4.2.

Quantified Boolean Formulas (QBFs). Building solvers for QBFs in NC is a
contemporary research concern, e.g. [113, 61, 14]. We will extend the
presented $\mathbb{H_{NC}}$ to QBFs and define the QBF-Horn-NC class. Then, we
will determine UR${}_{\mbox{nc}}$ for QBF-NCs, basic for DPLL. The complexity
of QBF-Horn-NC is an open question knowing that QBF-Horn is quadratic [32].

Regular Many-Valued Logic and Possibilistic Logic. Our approach has been
extended to these logics in [88, 89].

Linear-Arithmetic Logic. In Related Work, Arithmetic-Horn formulas have been
presented and mentioned that its associated SAT problem is polynomial [103].
Thus, we will define the Arithmetic-Horn-NC class. Then, we will try to prove
that Arithmetic-Horn-NC-SAT is polynomial as its clausal counterpart is [103].
For that purpose, we will require first to stipulate UR${}_{\mbox{nc}}$ for
linear-arithmetic logic.

Łukasiewicz Logic. As evoked in Related Work, the satisfiability problem of
the class $\mathcal{L}_{\infty}$-Horn is NP-complete [27] and polynomial [25]
for the 3-valued case, $\mathcal{L}_{3}$-Horn. Our goal will be to lift
$\mathcal{L}_{3}$-Horn to NC, determining thus, the $\mathcal{L}_{3}$-Horn-NC
class, $\mathcal{L}_{3}$-$\mathbb{H_{NC}}$. Then we will analyze whether
tractability is preserved in NC, that is, whether
$\mathcal{L}_{3}$-$\mathbb{H_{NC}}$ is polynomial. For that, a former step is
to define UR${}_{\mbox{nc}}$ for $\mathcal{L}_{3}$. Posteriorly, we will deal
with the infinite-valued case.

###  7.2 Developing the NC Paradigm

Tractability. This research line will be resumed by uplifting some of the
polynomial Horn-clausal extensions reviewed in Related Work. Concretely, we
will first attempt to determine the renamable-Horn-NC and SLUR-NC classes.
Indeed, uplifting polynomial clausal classes may be an open research direction
towards amplifying NC tractability.

Satisfiability. It was empirically verified (Related Work) that DPLL
outperforms the other published methods. $\mathbb{H_{NC}}$ and
UR${}_{\mbox{nc}}$ are the base of NC DPLL solvers. Hence, we plan: (1)
devising a fast Unit-Propagation based on UR${}_{\mbox{nc}}$ and easing its
suitable integration into the NC-DPLL structure; and (2) lifting polynomial
classes surveyed in Related Work to NC form.

MaxSAT. As evoked in Related Work, NC MaxSAT has not been properly defined. At
least the next three optimization factors can be considered, $\varphi$ being
the input: (i) the number of satisfiable clauses in $cl(\varphi)$; (ii) the
number of satisfiable sub-formulas in $\varphi$; and (iii) a weighted factor
resulting from combining both previous factors. We will analyze such variants,
compare them and solve NC-MaxSAT.

Signed Many-Valued Logic. Polarity of literals is the underlying
characterization of the Horn pattern; yet, it does not apply in signed many-
valued logic [19, 79]. However, a realistic possibility to make tractability
appear in signed logic consists in extending polynomial Horn super-classes to
signed logic. We think that the simplicity, wide range and relevance of the
SLUR formulas (Related Work) make them good candidates to begin with. Then, we
will attempt to lift the found clausal subclasses to NC.

Resolution. N. Murray in the 1980s [119] proposed NC Resolution in a combined
functional and classical manner. Thus, we plan to make the next contributions:
(1) determining a new definition of NC Resolution, making it as deterministic
as clausal Resolution is, and proving also its refutation completeness. We
will pursue this objective following the principle employed in this article
which led us to define UR${}_{\mbox{nc}}$; and (2) NC Hyper-Resolution has not
been defined yet, and thus we will attempt to bridge such gap.

Q-Resolution. Resolution QBFs is called Q-Resolution [100]. Thus, we plan
lifting Q-Resolution to NC and so defining NC-Q-Resolution. Yet, in view of
the aforementioned difficulties to prove the completeness of (non-quantified)