# Reconstructing a single-head formula to facilitate logical forgetting

Paolo Liberatore

###### Abstract

Logical forgetting may take exponential time in general, but it does not when
its input is a single-head propositional definite Horn formula. Single-head
means that no variable is the head of multiple clauses. An algorithm to make a
formula single-head if possible is shown. It improves over a previous one by
being complete: it always finds a single-head formula equivalent to the given
one if any.

##  1 Introduction

Logical forgetting is removing some variables from a logical formula while
preserving its information regarding the others [LLM03]. Seen from a different
angle, it is restricting a formula to keep only its information about some of
its variables [Del17].

Each of the two interpretations has its own applications. Removing information
allow reducing memory requirements [EKI19], simplifying reasoning [DW15, EF07,
WSS05] and clarifying the relationship about variables [Del17]. Restricting a
formula on some variables allows formalizing the limited knowledge of agents
[FHMV95, RHPT14], ensuring privacy [GKLW17] and removing inconsistency [LM10].

Initially studied in first-order logic [LR94, ZZ11], logical forgetting has
found its way into many logics such as propositional logic [Boo54, Moi07,
Del17], answer set programming [WZZZ14, GKL16], description logics [KWW09,
EIS+06], modal logics [vDHLM09], logics about actions [EF07, RHPT14], temporal
logic [FAS+20], defeasible logic [AEW12] and belief revision [NCL07].

Contrary to intuition, forgetting may increase size instead of decreasing it
[Lib20b]. This phenomenon is harmful to the many application scenarios where
size reduction is important if not the sole aim of forgetting: increasing
efficiency of reasoning [DW15, EF07, WSS05], summarizing, reusing and
clarifying information [Del17], dealing with information overload [EKI19],
tailoring information to specific applications [EIS+06], dealing with memory
bounds [FHMV95] or more generally with limitations in the ability of reasoning
[RHPT14].

To complicate matters, forgetting is not uniquely determined: a specific
algorithm for forgetting may produce a large formula that is equivalent to a
small one. The latter is as good as the former at representing information,
but better in terms of size. The question is not whether forget increases
size, but whether every possible mechanism for forgetting does. Several
equivalent formulae express forgetting the same variables from the same
formula $F$. The question is whether one of them is smaller than $F$, or than
a target size bound.

Giving an answer to this question is harder than the typical problems in
propositional reasoning: it is in $\Sigma^{p}_{3}$ and is ${\rm D}^{p}$2-hard.
The Horn restriction lowers complexity of one level, to membership in
$\Sigma^{p}_{2}$ and hardness in ${\rm D}^{p}$ [Lib20b].

Such a simplification in complexity is typical to the propositional Horn
restriction [Mak87]. It is one of the reasons that makes it of interest, the
other being its expressivity. Consistency, inference and equivalence only take
polynomial time. At the same time, commonly-used statements like “if a, b and
c then d” and “e, g, and f are impossible at the same time” are allowed. The
Horn restriction is studied in, for example, description logic [KRH13],
default reasoning [EL00], fuzzy logic [BV06], belief revision [ZP12],
transaction logic [BK94] and nonmonotonic reasoning [Got92].

Restricting to the Horn case lowers the complexity of many operations. Is this
the case for forgetting?

A way of forgetting a variable is to resolve all pairs of clauses over that
variable and to remove the resolved clauses. The required space may be
exponential in the number of variables to forget, even if the final result is
polynomially large.

Something better can be done in the definite Horn case: replace the variable
with the body of a clause with the variable in its head. This nondeterministic
algorithm only requires polynomial working space [Lib20a]. It extends from the
definite to the general Horn case [Lib20a].

A restriction that makes this method not only polynomial in space but also in
time is the single-head condition. If clauses do not share heads, the choice
of the clause to replace a variable is moot. What was in general
nondeterministic becomes deterministic. Complexity decreases from
nondeterministic polynomial time to deterministic polynomial time. The problem
is tractable.

Whether a formula is single-head or not is easy to check by scanning the
clauses and storing their heads; if one of them is found again, the formula is
not single-head.

It is easy, but misses the semantical nature of forgetting.

Forgetting variables is restricting information to the other variables, and
information is independent on the syntax. Forgetting the same variables from
two equivalent formulae gives two equivalent formulae. The initial information
is the same, what to forget is the same. What results should be the same,
apart from its syntactic form. Forgetting $c$ from $\\{a\rightarrow
b,b\rightarrow c,c\rightarrow d\\}$ and forgetting it from $\\{a\rightarrow
b,b\rightarrow c,c\rightarrow d,a\rightarrow c\\}$ produces equivalent
formulae since the two formulae are equivalent. Yet, only the former is
single-head. Only the former takes advantage of polynomiality in time. This
needs not to be, since the result is the same. The second formula can be
translated into the first, making forgetting polynomial.

Every formula that is equivalent to a single-head formula is amenable to this
procedure: make it single-head, then forget.

The second step, forgetting, is easy since the formula is single-head. What
about the first?

While checking whether a formula is single-head is straightforward, checking
whether it is equivalent to a single-head formula is not. Many formulae are
equivalent to a given one and are therefore to be checked for multiple heads.
The problem would simplify if it amounted to checking a simple condition on
the formula itself or its models rather than all its equivalent formulae, but
finding such a condition proved difficult [Lib20c].

A polynomial algorithm that often turns a formula in single-head form if
possible is to select the minimal bodies for each given head according to a
certain order. It is polynomial but incomplete: some single-head equivalent
formulae are not recognized as such [Lib20c].

The present article restarts the quest from a different direction: instead of
fixing the heads and searching for the bodies, it fixes the bodies and
searches for the heads. The overall algorithm is complete: it turns a formula
in single-head form if possible. The price is its running time, which may be
exponential.

This may look discouraging since the target is an efficient algorithm for
forgetting. Two points are still in favor of the new algorithm: first, it is
exponential only when it works on equivalent sets of variables; second, each
step can be stopped at any time, making the algorithm incomplete but fast.

The first point derives from the structure of the algorithm: it is a loop over
the bodies of the formula; for each, its equivalent sets of variables are
candidate bodies for clauses of the single-head form. The overall loop
comprises only a polynomial number of steps. Each step is exponential because
a formula may make a set of variables equivalent to exponentially many others.
If not, the algorithm is polynomial in time.

The second point is a consequence of what each step is required to do: change
some clauses of the original formula to make each head only occurs once. If
such an endeavor turns out to be too hard, the original clauses can be just
left unfiltered. Still better, some original clauses may be added to complete
the best set found so far. This part of the output formula will not be single-
head, but the rest may be. The forgetting algorithm may still benefit from the
change, since it is exponential in the number of duplicated heads.

The article is organized as follows. Section 2 restates the definitions and
results obtained in previous articles [Lib20a, Lib20c]. Section 3 presents the
overall algorithm. It repeatedly calls a function implemented in Section 4.
This completes the algorithm, which is correct and complete but not always
polynomial-time. Given that a previous algorithm was incomplete but
polynomial, the question is whether the problem itself is tractable; this is
investigated in Section 5. The Python implementation of the program is
described in Section 6.

##  2 Previously

A summary of the past work on single-head equivalence is in the Introduction.
This section contains the technical definitions and results of previous
articles [Lib20a, Lib20c] used in this article.

The first one is a quite obvious lemma that proves that entailing a variable
is only possible via a clause that has that variable as its head [Lib20a].

###### Lemma 1

If $F$ is a definite Horn formula, the following three conditions are
equivalent, where $P^{\prime}\rightarrow x$ is not a tautology ($x\not\in
P^{\prime}$).

  1. 1.

$F\models P^{\prime}\rightarrow x$;

  2. 2.

$F^{x}\cup P^{\prime}\models P$ where $P\rightarrow x\in F$;

  3. 3.

$F\cup P^{\prime}\models P$ where $P\rightarrow x\in F$.

An order over the sets of variables [Lib20a] is central to the algorithm
presented in the present article.

###### Definition 1

The ordering $\leq_{F}$ that compares two sets of variables where $F$ is a
formula is defined by $A\leq_{F}B$ if and only if $F\models B\rightarrow A$.

The set $BCN(B,F)$ contains all consequences of the set of variables $B$
according to formula $F$ [Lib20a].

###### Definition 2

The set $BCN(B,F)$, where $B$ is a set of variables and $F$ is a formula, is
defined as $BCN(B,F)=BCN(B,F)=\\{x\mid F\cup B\models x\\}$.

The intended meaning of $BCN(B,F)$ is the set of consequences of $B$.
Formally, $BCN(B,F)$ meets its aim. Informally, a consequence is something
that follows from a premise. Some deduction is presumed involved in the
process. Yet, $BCN(B,F)$ may contain variables that do not follow from $B$,
they are just in $B$. No inference ever derives it from $B$.

Excluding all variables of $B$ is not a correct solution: $BCN(B,F)\backslash
B$ is too small. It does not include the variables of $B$ that follow from $B$
thanks for some derivation.

For example, both $x$ and $y$ are in $BCN(B,F)$ if $B=\\{x,y\\}$ and
$F=\\{y\rightarrow z,z\rightarrow y\\}$. Yet, $x$ is in $BCN(B,F)$ only
because it is in $B$. Instead, $y$ can be deduced from $B$ via $y\rightarrow
z$ and $z\rightarrow y$. This distinction proved important to the previous,
incomplete algorithm for single-head equivalence [Lib20c].

###### Definition 3

For every set of variables $B$ and formula $F$, the real consequences of $F$
are $RCN(B,F)=\\{x\mid F\cup(BCN(B,F)\backslash\\{x\\})\models x\\}$.

The set of all consequences of $B=\\{x,y\\}$ is $BCN(B,F)=\\{x,y,z\\}$. The
difference between $x$ and $y$ is that $x$ cannot be recovered once removed
from it while $y$ can. In other words, $B$ derives something that derives $y$
back; it does not for $x$. Therefore, $y$ a real consequence, $x$ is not:
$RCN(B,F)=\\{y,z\\}$.

This example also shows how to determine $RCN(B,F)$ when $F$ is a definite
Horn formula: start from $B$ and add to it all variables $x$ such that
$B^{\prime}\rightarrow x\in F$ with $B^{\prime}\subseteq B$. Only the
variables that are added form $RCN(B,F)$. The algorithm is presented in full
and proved correct in the same article where $RCN(B,F)$ is introduced
[Lib20c]. The algorithm also determines the set of clauses used in the
process: $\\{B^{\prime}\rightarrow x\in F\mid F\models B\rightarrow
B^{\prime}\\}$. The variant of this set where tautologies are excluded is
defined in the present article as $UCL(B,F)$. Since this set only contains the
clauses of $F$, if $F$ does not contain tautologies the difference disappears.

The only variables that may be consequences of a formula without being real
consequences of it are the variables of $B$. This is formally stated by the
following lemma [Lib20c].

###### Lemma 2

For every formula $F$ and set of variables $B$, it holds $BCN(B,F)=A\cup
RCN(B,F)$.

##  3 The reconstruction algorithm

A formula may have multiple clauses with the same head and still be equivalent
to one that has not. Such a formula deceives the algorithm based on replacing
heads with their bodies by sending it on a wild goose chase across multiple
nondeterministic branches that eventually produce the same clause. Turning the
formula into its single-head form wherever possible avoids such a waste of
time.

The approximate algorithm shown in a previous article [Lib20c] produces a
single-head formula that may be equivalent to $F$. It gives no guarantee, in
general: it may fail even if the formula is single-head equivalent.

The algorithm presented in this section does not suffer from this drawback.
When run on formula that has a single-head equivalent form, it finds it. The
trade-off is efficiency: it does not always finish in polynomial time.

###  3.1 Bird’s-eye view of the reconstruction algorithm

The algorithm tries to reconstruct the formula clause by clause. It starts
with an empty formula and adds clauses to it until it becomes equivalent to
the input formula. Not adding clauses with the same head makes the resulting
formula single-head.

An example tells which clauses are added. The aim is to make the formula under
construction equivalent to the input formula. If the input formula contains
$ab\rightarrow x$, the formula under construction has to entail it to achieve
equivalence. This is the same as $x$ being implied by $\\{a,b\\}$.

$ab\rightarrow$$\rightarrow x$

What is in the rectangle? The implication of $x$ from $\\{a,b\\}$ is required
in the formula under construction. This formula aims at replicating the input
formula. It cannot contain clauses not entailed by that. The answer is that
the rectangle contains clauses entailed by the input formula.

Since all clauses are definite Horn, this implication is realized by forward
chaining: $a$ and $b$ derive some variables that derive some others that
derive others that derive $x$. For example, $a$ and $b$ derive $c$ and $d$,
which derive $e$ and $f$ which derive $y$ which derives $x$. Each individual
derivation is realized by a clause.

$ab\rightarrow$$\rightarrow x$$ab\rightarrow c$$ab\rightarrow d$$c\rightarrow
e$$ef\rightarrow y$$y\rightarrow x$$bd\rightarrow f$

The first step of such a derivation has $a$ and $b$ imply another variable by
means of a clause like $ab\rightarrow c$. Without such a clause, forward
chaining does not even start. Nothing derives from $\\{a,b\\}$ without. Not
even a single variable to derive others.

Some clauses in the rectangle are like $ab\rightarrow c$ and $ab\rightarrow
d$, with $\\{a,b\\}$ as their body. Maybe not two, but at least one. Not zero.
At least a clause in the rectangle has body $\\{a,b\\}$. Maybe a subset like
$\\{a\\}$, but this case will be discussed later. For the moment, some clauses
on the left edge of the rectangle have $\\{a,b\\}$ as their bodies.

$ab\rightarrow$$\rightarrow x$$ab\rightarrow c$$ab\rightarrow d$$c\rightarrow
e$$ef\rightarrow y$$y\rightarrow x$$bd\rightarrow f$

A first stage contains $ab\rightarrow c$ and $ab\rightarrow d$; a second
contains the following clauses used in the derivation of $x$. The key is
induction. The formula under construction is assumed to already imply the
clauses in the second stage. Adding $ab\rightarrow c$ and $ab\rightarrow d$
completes the derivation.

The inductive assumption is that the formula under construction implies all
clauses in the second stage. The addition of $ab\rightarrow c$ and
$ab\rightarrow d$ makes it imply $ab\rightarrow x$ as well. Such an induction
is only possible if these two clauses are added only when the others are
already implied. Adding them makes $ab\rightarrow x$ entailed. This entailment
is the induction claim. Which is the induction assumption for the next step.

The induction step that makes $ab\rightarrow x$ entailed requires
$c\rightarrow e$ to be entailed, which is only possible if the induction step
that makes $c\rightarrow e$ entailed is in the past. The same for the other
clauses in the second stage: when the clauses of body $ab$ are added, all
clauses of body $c$, $bd$, etc. are already. Key to induction is the order of
addition of clauses.

How the single-head property is achieved is still untalked of. In the example,
once $c\rightarrow e$ is in, all other sets of variables entailing $e$ should
do so by first entailing $c$. For example, if $ab\rightarrow e$ is in the
input formula, it is entailed by the formula under construction thanks to
$ab\rightarrow c$ and $c\rightarrow e$; no need for duplicated heads. If $ab$
entailed $e$ but not $c$, the input formula is not single-head equivalent.

All of this works flawlessly because of the simplicity of the input formula.
Not in general.

Induction works because the algorithm tries to entail $ab\rightarrow x$ only
when all clauses whose bodies are entailed by $ab$ are already entailed. Such
an assumption requires a caveat: these bodies are entailed by $ab$ but do not
entail it. It does not work on bodies that are not just entailed by $ab$ but
also equivalent to it. Extending the induction assumption to them makes it
circular rather than inductive. On the example: if $gh$ is equivalent to $ab$,
the induction step for $ab$ follows that of $gh$; but the step for $gh$
follows that of $ab$ for the same reason.

Equivalent sets cannot be worked on inductively. Even worse, they cannot be
worked on separately as well. When the step that adds $ab\rightarrow x$ is
over, the following steps rely on its inductive claim. A following step for
the body $ij$ may require $ab\rightarrow x$ to be entailed, if $ij$ entails
$ab$. Because of equivalence, $ij$ also entails $gh$. The induction assumption
also requires the clauses of body $gh$ to be entailed. The clauses of head
$ab$ and $gh$ to be found together.

This also tells what would happen if the first stage of derivation contained
$a\rightarrow c$ instead of $ab\rightarrow c$, a strict subset of $ab$ instead
of $ab$ itself. By monotonicity, $a$ is entailed by $ab$; if it does not
entail it, $a\rightarrow c$ is already in the formula under construction
thanks to the inductive assumption. Otherwise, $ab$ and $a$ are equivalent.
The induction step where $ab\rightarrow x$ is achieved also achieves
$a\rightarrow c$.

Equivalent bodies also require special care to ensure the single-head
property. Searching for the clauses of body $ab$ and $gh$ at the same time may
result in two clauses such as $ab\rightarrow c$ and $gh\rightarrow c$. Such a
solution may as well satisfy the inductive claim, but is not acceptable. As a
previous article illustrates for pages and pages [Lib20c], just adding
$gh\rightarrow c$ and hoping for equivalence to give $ab\rightarrow c$ does
not work; this very clause $ab\rightarrow c$ may be necessary to ensure
equivalence.

The algorithm in this section turns to a mysterious function to produce the
necessary clauses of body $ab$—or equivalent. The next section unveils the
mystery.

###  3.2 Worm’s eye view of the reconstruction algorithm

The key to induction is the entailment between sets of variables. The required
conditions are long to write: “a set variables entails another without being
entailed by it”. Sentences involving one of these segments may still be
readable, but two or three make them unparsable. An order between sets used in
a previous article [Lib20c] shortens wording: $A\leq_{F}B$ if $F\models
B\rightarrow A$. If $A$ entails $B$ according to $F$ but is not entailed by
it, then $A<_{F}B$. If they entail each other, then $A\equiv_{F}B$.

The algorithm sorts the bodies of $F$ according to this order, neglecting
their heads. The minimal bodies are considered first. The set of clauses with
these bodies are turned into single-head form. With this set fixed, the bodies
that are minimal among the remaining ones are processed in the same way. The
procedure ends when no body is left.

If $A$ is the only minimal body, the first step finds all clauses
$A\rightarrow x$ entailed by $A$. If the second-minimal body is $B$, the
second step finds some clauses $B\rightarrow y$; not all of them, since some
may be entailed thanks to the clauses produced in the first step. The same is
done in the remaining steps.

No backtracking is required. The clauses generated by a step are in the final
formula regardless of what happens in the following steps. This is not the
reason why the algorithm may take exponential time.

The reason is that each step may take exponential time. When $A\equiv_{F}B$,
the heads for $A$ and $B$ have to be generated in the same step. Sometimes
this is easy, sometimes it is not. In the worst case, the possibilities
increase exponentially with the number of equivalent sets.

Technically, the algorithm reconstructs the formula starting from the clauses
of minimal bodies:

  * •

the formula is initially empty;

  * •

a body $A$ that only entails equivalent bodies is chosen;

  * •

enough clauses $P\rightarrow x$ with $P\equiv_{F}A$ are selected so that the
reconstructed formula entails all clauses of the given formula with a body
equivalent to $A$;

  * •

a body $B$ that only entails bodies entailed by $A$ or equivalent to $B$ is
chosen;

  * •

enough clauses $P\rightarrow x$ with $P\equiv_{F}B$ are selected so that the
reconstructed formula entails all clauses of the given formula with a body
equivalent to $B$;

  * •

a body $C$ that only entails bodies entailed by $A$ and $B$ or equivalent to
$C$ is chosen;

  * •

…

Since bodies are considered in increasing order, when a body $B$ is considered
all bodies $A<_{F}B$ have already been. This implies that all clauses
$P\rightarrow x$ with $P\equiv_{F}A$ are already entailed by the formula under
construction.

###  3.3 The construction lemma

The reconstruction algorithm looks like a typical backtracking mechanism: some
clauses $P\rightarrow x$ with $P\equiv_{F}A$ are chosen; the same for $B$,
$C$, and so on; choosing clauses for a following set $D$ may prove impossible,
showing that the choice for $A$ was wrong. Backtracking to $A$ is necessary.

It is not.

The reason is that each step generates enough clauses to entail all clauses
with a body equivalent to the given one. Different choices may be possible,
but the result always entails all these clauses. To entail all these clauses,
their heads are required to be in the chosen clauses. Different choices differ
in their bodies, but not in their heads and consequences. If a following
choice proves impossible, backtracking is of no help since it can only replace
a set of clauses with an equivalent one, with the same heads. The same
impossible choice is faced again.

###### Lemma 3

If $F$ is a single-head formula such that $F\models A\rightarrow x$ with
$x\not\in A$ and $F\not\models A\rightarrow B$, then $F$ does not contain
$B\rightarrow x$.

Proof. Since $F\models A\rightarrow x$ and $x\not\in A$, Lemma 1 implies that
$F$ contains a clause $P\rightarrow x$ such that $F\models A\rightarrow P$.
The set $P$ differs from $B$ since $F$ entails $A\rightarrow P$ but not
$A\rightarrow B$. As a result, $B\rightarrow x$ is not the same as
$P\rightarrow x$. Since $F$ contains the latter clause and is single-head, it
does not contain the former.

Why does this lemma negate the need for backtracking? Backtracking kicks in
when adding $B\rightarrow x$ is necessary but another clause $A\rightarrow x$
is already in the formula under construction. Because of the order of the
steps, $B$ is either strictly larger than $A$ or incomparable to it. The
condition $F\not\models A\rightarrow B$ holds in both. The lemma proves that
$B\rightarrow x$ is not in any single-head formula equivalent to $F$. Adding
this clause to the formula under construction is not only useless, it is
impossible if that formula has to be single-head. Which clauses the step for
$A$ added is irrelevant.

###  3.4 One iteration of the reconstruction algorithm

An iteration of the reconstruction algorithm picks a body $B$ only when all
bodies $A<_{F}B$ have already been processed by a previous iteration. As a
result, all clauses $A^{\prime}\rightarrow x$ with $A^{\prime}\equiv_{F}A$ are
already entailed by the formula under construction. This is the fundamental
invariant of the algorithm.

When looking at the iteration for a body $B$, the bodies $A$ such that
$A<_{F}B$ are called strictly entailed bodies to simplify wording. Since $B$
is fixed, “all strictly entailed bodies do something” is simpler than “all
bodies $A$ such that $A<_{F}B$ do something”.

When processing $B$, the formula under construction is the result of the
previous iterations. The set $A$ of a previous iteration cannot be greater or
equal than $B$; therefore, either $A$ is incomparable with $B$ or is less than
it. If $A$ is incomparable with $B$, then $F\not\models B\rightarrow A$; the
clauses of body $A$ or equivalent are not relevant to implications from $B$.
If $A<_{F}B$ then $F\models B\rightarrow A$; the clauses of body $A$ or
equivalent to $A$ help entailing variables from $B$. The construction lemma
ensures that their heads $x$ are not valid candidates as heads for $B$. The
following definitions express these ideas.

###### Definition 4

Given a formula $F$, the strictly entailed bodies of $B$ are the sets $A$ such
that $A\rightarrow x\in F$ for some $x$ and $A<_{F}B$. The clauses and free
heads of such bodies are:

clauses of strictly entailed bodies:

$SCL(B,F)=\\{A\rightarrow x\mid x\not\in A,~{}F\models A\rightarrow
x,~{}F\models B\rightarrow A,~{}F\not\models A\rightarrow B\\}$

heads free from strictly entailed bodies:

$SFREE(B,F)=\\{x\mid\not\exists A\rightarrow x\in SCL(B,F)\\}$

The iteration for a body $B$ produces some clauses $B^{\prime}\rightarrow x$
with $B^{\prime}\equiv B$. The construction lemma limits the choices of the
heads to $x\in SFREE(B,F)$. All clauses of $SCL(B,F)$ are already entailed by
the formula under construction. They are the only ones relevant to finding new
clauses $B^{\prime}\rightarrow x$. The goal of the iteration is to entail the
following clauses.

###### Definition 5

Given a set of variables $B$ and a formula $F$, the clauses of equivalent
bodies are:

$BCL(B,F)=\\{A\rightarrow x\mid x\not\in A,F\models A\rightarrow x,~{}F\models
B\rightarrow A,~{}F\models A\rightarrow B\\}$

The algorithm progressively builds a formula equivalent to the given one. It
is initially empty. Every step hinges around the body $B$ of a clause. The
main invariant is that the formula under construction already entails
$SCL(B,F)$; the aim is to make it entail $BCL(B,F)$ as well. This makes the
invariant true again in the following steps, since $BCL(B,F)$ is part of
$SCL(C,F)$ if $B<_{F}C$. The $SFREE(B,F)$ set simplifies this task by
restricting the possible heads of the new clauses.

Every step adds some new clauses to the formula; which ones they are is
explained in a later section. This one is about the overall algorithm. To it,
what matters of a single step is only what it produces, not how. What it
produces is formalized as follows.

###### Definition 6

A valid iteration is a function $ITERATION(B,F)$ that satisfies the following
two conditions for every set of variables $B$ and formula $F$:

choice:

$ITERATION(B,F)$ is a set of non-tautological clauses $B^{\prime}\rightarrow
x$ such that

  * •

$F\models B^{\prime}\rightarrow x$,

  * •

$F\models B\equiv B^{\prime}$ and

  * •

$x\in SFREE(B,F)$;

entailment:

$SCL(B,F)\cup ITERATION(B,F)\models BCL(B,F)$.

The first condition (choice) limits the possible clauses
$B^{\prime}\rightarrow x$ generated at each step. The second (entailment)
requires them to satisfy the invariant for the next steps (entailment of
$BCL(B,F)$) given the invariant for the current (entailment of $SCL(B,F)$).

A minimal requirement for the steps of the algorithm is that they succeed when
the formula is already single-head. In spite of its weakness, this property is
useful for proving that the algorithm works on single-head equivalent
formulae.

###### Lemma 4

If $F$ is a single-head formula, $ITERATION(B,F)={}\\{B^{\prime}\rightarrow
x\in F\mid x\not\in B^{\prime},~{}F\models B\equiv B^{\prime}\\}$ is a valid
iteration function.

Proof. The given function $ITERATION(B,F)$ is shown to satisfy both the choice
and the entailment condition, the two parts of the definition of a valid
iteration function (Definition 6).

The choice condition concerns the individual clauses of $ITERATION(B,F)$. They
are not tautological by construction. The other requirements are proved one by
one for each $B^{\prime}\rightarrow x\in ITERATION(B,F)$.

  * •

The first is $F\models B^{\prime}\rightarrow x$. It holds because
$B^{\prime}\rightarrow x\in F$ is part of the definition of this function
$ITERATION(B,F)$.

  * •

The second is $F\models B\equiv B^{\prime}$. It is part of the definition of
this function $ITERATION(B,F)$.

  * •

The third is $x\in SFREE(B,F)$. Its converse $x\not\in SFREE(B,F)$ means that
$SCL(B,F)$ contains a clause $A\rightarrow x$. The definition of $A\rightarrow
x\in SCL(B,F)$ is $x\not\in A$, $F\models A\rightarrow x$, $F\models
B\rightarrow A$ and $F\not\models A\rightarrow B$. The latter implies
$F\not\models A\rightarrow B^{\prime}$ since $F\models B\equiv B^{\prime}$.
Lemma 3 proves that $F\models A\rightarrow x$, $x\not\in A$ and $F\not\models
A\rightarrow B^{\prime}$ imply $B^{\prime}\rightarrow x\not\in F$, which
contradicts $B^{\prime}\rightarrow x\in F$.

The given function $ITERATION(B,F)$ also satisfies the entailment condition of
Definition 6: $SCL(B,F)\cup ITERATION(B,F)\models BCL(B,F)$. This is implied
by $SCL(B,F)\cup ITERATION(B,F)\models SCL(B,F)\cup BCL(B,F)$, which is
defined by $SCL(B,F)\cup ITERATION(B,F)\models B^{\prime}\rightarrow x$ if
$x\not\in B^{\prime}$, $F\models B^{\prime}\rightarrow x$, $F\models
B\rightarrow B^{\prime}$ and either $F\not\models B^{\prime}\rightarrow B$ or
$F\models B^{\prime}\rightarrow B$. Either one choice of alternative is always
true, which simplifies the condition to $SCL(B,F)\cup ITERATION(B,F)\models
B^{\prime}\rightarrow x$ if $x\not\in B^{\prime}$, $F\models
B^{\prime}\rightarrow x$ and $F\models B\rightarrow B^{\prime}$. What is
actually proved is a more general condition: for every $G\subseteq F$,
$SCL(B,F)\cup ITERATION(B,F)\models B^{\prime}\rightarrow x$ holds if
$x\not\in B^{\prime}$, $G\models B^{\prime}\rightarrow x$ and $F\models
B\rightarrow B^{\prime}$. The introduction of $G$ allows for induction over
the size of $G$.

If $G$ is empty, it entails $B^{\prime}\rightarrow x$ only if $x\in
B^{\prime}$. Such a clause does not satisfy the other requirement $x\not\in
B^{\prime}$. The condition is met. This is the base case of induction.

The induction step requires proving the claim for an arbitrary $G\subseteq F$
assuming it for every formula smaller than $G$.

The claim is that $G\subseteq F$, $x\not\in B^{\prime}$, $G\models
B^{\prime}\rightarrow x$ and $F\models B\rightarrow B^{\prime}$ imply
$SCL(B,F)\cup ITERATION(B,F)\models B^{\prime}\rightarrow x$. The induction
assumption is the same for every $G^{\prime}\subset G$.

The premises $x\not\in B^{\prime}$ and $G\models B^{\prime}\rightarrow x$
allow applying Lemma 1: $G^{x}\models B^{\prime}\rightarrow B^{\prime\prime}$
holds for some clause $B^{\prime\prime}\rightarrow x\in G$.

A consequence of $B^{\prime\prime}\rightarrow x\in G$ is
$B^{\prime\prime}\rightarrow x\in F$ since $G\subseteq F$. For the same
reason, $G^{x}\models B^{\prime}\rightarrow B^{\prime\prime}$ implies
$F\models B^{\prime}\rightarrow B^{\prime\prime}$. With the other assumption
$F\models B\rightarrow B^{\prime}$, transitivity implies $F\models
B\rightarrow B^{\prime\prime}$. The converse implication
$B^{\prime\prime}\rightarrow B$ may be entailed by $F$ or not. If $F\models
B^{\prime\prime}\rightarrow B$ holds then either $x$ is in $B^{\prime\prime}$
or $B^{\prime\prime}\rightarrow x$ is in $ITERATION(B,F)$; in both cases,
$B^{\prime\prime}\rightarrow x$ is entailed by $SCL(B,F)\cup ITERATION(B,F)$.
If $F\not\models B^{\prime\prime}\rightarrow B$ then either $x$ is in
$B^{\prime\prime}$ or $B^{\prime\prime}\rightarrow x$ is in $SCL(B,F)$; in
both cases, $B^{\prime\prime}\rightarrow x$ is entailed by $SCL(B,F)\cup
ITERATION(B,F)$. The conclusion of this paragraph is $SCL(B,F)\cup
ITERATION(B,F)\models B^{\prime\prime}\rightarrow x$.

Induction proves that $SCL(B,F)\cup ITERATION(B,F)$ also entails
$B^{\prime}\rightarrow B^{\prime\prime}$. This condition is the same as
$SCL(B,F)\cup ITERATION(B,F)\models B^{\prime}\rightarrow b$ for every $b\in
B^{\prime\prime}$. Since $G^{x}$ entails $B^{\prime}\rightarrow
B^{\prime\prime}$, it entails $B^{\prime}\rightarrow b$ for every $b\in
B^{\prime\prime}$. If $b\in B^{\prime}$ then $B^{\prime}\rightarrow b$ is a
tautology and is therefore entailed by $SCL(B,F)\cup ITERATION(B,F)$.
Otherwise, $b\not\in B^{\prime}$. Since $B^{\prime\prime}\rightarrow x$
contains $x$, it is not in $G^{x}$; since $G$ contains
$B^{\prime\prime}\rightarrow x$ instead, $G^{x}$ is a proper subset of $G$.
The induction assumption is the same as the induction claim with $G^{x}$ in
place of $G$, that is, $G^{x}\subseteq F$, $x\not\in B^{\prime}$,
$G^{x}\models B^{\prime}\rightarrow b$ and $F\models B\rightarrow B^{\prime}$
imply $SCL(B,F)\cup ITERATION(B,F)\models B^{\prime}\rightarrow b$. Since all
premises hold, the claim holds as well: $SCL(B,F)\cup ITERATION(B,F)\models
B^{\prime}\rightarrow b$. This is the case for every $b\in B^{\prime\prime}$.
A consequence is $SCL(B,F)\cup ITERATION(B,F)\models B^{\prime}\rightarrow
B^{\prime\prime}$.

The conclusion $SCL(B,F)\cup ITERATION(B,F)\models B^{\prime}\rightarrow
B^{\prime\prime}$ joins $SCL(B,F)\cup ITERATION(B,F)\models
B^{\prime\prime}\rightarrow x$ to prove $SCL(B,F)\cup ITERATION(B,F)\models
B^{\prime}\rightarrow x$. This is the induction claim.

The specific function $ITERATION(B,F)$ of this lemma gives only clauses of
$F$. It depends on the syntax of $F$. Yet, the validity of an iteration
function is semantical: only depends on entailments, equivalences and the
three functions $SCL(B,F)$, $SFREE(B,F)$ and $BCL(B,F)$, which are all defined
in terms of entailments. Therefore, if $ITERATION(B,F)$ is valid, the same
function applied to another formula $ITERATION(B,F^{\prime})$ is still valid
if $F\equiv F^{\prime}$.

###### Lemma 5

If $ITERATION(B,F)$ is a valid iteration function and $F\equiv F^{\prime}$,
then $ITERATION(B,F^{\prime})=ITERATION(B,F)$ is a valid iteration function.

Proof. Since $ITERATION(B,F)$ is valid iteration function, it produces a set
of clauses $B^{\prime}\rightarrow x$ such that $x\not\in B^{\prime}$,
$F\models B\rightarrow x$, $F\models B\equiv B^{\prime}$, $x\in SFREE(B,F)$
and all of them plus $SCL(B,F)$ entail all clauses $B^{\prime}\rightarrow x$
with $F\models B\equiv B^{\prime}$ that are entailed by $F$. In turn,
$SCL(B,F)$ is defined as the set of clauses $B^{\prime\prime}\rightarrow x$
such that $F\models B^{\prime\prime}\rightarrow x$, $F\models B\rightarrow
B^{\prime\prime}$ and $F\not\models B^{\prime\prime}\rightarrow x$. Finally,
$SFREE(B,F)$ is defined as the set of variables $x$ such that no clause
$B^{\prime\prime}\rightarrow x\in SCL(B,F)$.

All these conditions are based on what $F$ entails. Since $F$ is equivalent to
$F^{\prime}$, they also hold when $F^{\prime}$ is in place of $F$. Therefore,
$ITERATION(B,F^{\prime})=ITERATION(B,F)$ is also a valid iteration function.

The two lemmas together prove that if $F$ is single-head equivalent then it
has a valid iteration function: the one for a single-head formula that is
equivalent to $F$.

###### Lemma 6

If $F$ is equivalent to the single-head formula $F^{\prime}$, then
$ITERATION(B,F)=\\{B^{\prime}\rightarrow x\in F^{\prime}\mid F^{\prime}\models
B\equiv B^{\prime}\\}$ is a valid iteration function.

Proof. By Lemma 4, $ITERATION(B,F^{\prime})$ is a valid iteration function for
$F^{\prime}$. By Lemma 5, it is also valid for $F$.

As a result, every single-head equivalent formula has a valid iteration
function.

###### Corollary 1

Every single-head equivalent formula has a valid iteration function.

The proofs of the three lemmas show how to find a valid iteration function:
switch from the single-head equivalent formula to a single-head formula that
is equivalent to it and then extract the necessary clauses from it.

This mechanism works in theory, and is indeed used in proofs that requires a
valid iteration function to exists. It does not work in practice, since the
single-head formula equivalent to the given one is not known. Rather the
opposite: the whole point of valid iteration functions is to be used in
reconstruction algorithm to find a single-head formula equivalent to the given
one. The iteration function is a means to the aim of finding a single-head
formula, not the other way around.

In practice, finding a valid iteration function is no easy task. An entire
following section is devoted to that. For the moment, a valid iteration
function is assumed available.

###  3.5 The reconstruction algorithm

Assuming the availability of a valid iteration function $ITERATION(B,F)$, the
reconstruction algorithm is as follows.

######  Algorithm 1 (Reconstruction algorithm)

  1. 1.

$G=\emptyset$

  2. 2.

$P=P(X)$ # set of all subsets of $X$

  3. 3.

while $P\not=\emptyset$:

    1. (a)

choose a $\leq_{F}$-minimal $B\in P$
(a set such that $A<_{F}B$ does not hold for any $A\in P$)

    2. (b)

$G=G\cup ITERATION(B,F)$

    3. (c)

$P=P\backslash\\{B^{\prime}\mid F\models B\equiv B^{\prime}\\}$

  4. 4.

return $G$

The algorithm is non-deterministic, but works for every possible
nondeterministic choices. It is not deterministic because many sets $B$ may be
minimal each time. The final result depends on these choices because
$ITERATION(B,F)$ may differ from $ITERATION(B^{\prime},F)$ even if
$B\equiv_{F}B^{\prime}$. Yet, an equivalent single-head formula is found
anyway, if any.

As an example, a valid iteration function for $F=\\{a\rightarrow
b,b\rightarrow a,bc\rightarrow d\\}$ has the values
$ITERATION(\\{a,c\\},F)=\\{bc\rightarrow d\\}$ and
$ITERATION(\\{b,c\\},F)=\\{ac\rightarrow d\\}$. The reconstruction algorithm
produces either $bc\rightarrow d$ or $ac\rightarrow d$ depending on whether it
chooses $\\{a,c\\}$ or $\\{b,c\\}$ as the set $B$ of an iteration of its main
loop. Either way, the result is single-head and equivalent to $F$.

The following lemmas state some properties of the algorithm that are
independent on the nondeterministic choices. For example, proving termination
means that the algorithm terminates for all possible nondeterministic choices.

###### Lemma 7

The reconstruction algorithm (Algorithm 1) always terminates.

Proof. The set $P$ becomes smaller at each iteration, since a choice of $B$ is
always possible if $P$ is not empty because $\leq_{F}$ is a partial order. As
a result, at some point $P$ becomes empty and the algorithm terminates.

The second property of the reconstruction algorithm is that it never
calculates $ITERATION(B,F)$ for equivalent sets $B$. Still better, it
calculates $ITERATION(B,F)$ exactly once for each $B$ among its equivalent
ones. This is proved by the following two lemmas.

###### Lemma 8

For every set of variables $B^{\prime}$, the reconstruction algorithm
(Algorithm 1) calculates $ITERATION(B,F)$ for some $B$ such that $F\models
B\equiv B^{\prime}$.

Proof. Initially, $B^{\prime}\in P$ since $P$ contains all sets of variables.
The algorithm terminates by Lemma 7. It only terminates when $P$ is empty.
Therefore, $B^{\prime}$ is removed from $P$ during the run of the algorithm.
Removal is only done by $P=P\backslash\\{B^{\prime}\mid F\models B\equiv
B^{\prime}\\}$. This operation is preceded by $G=G\cup ITERATION(B,F)$.

###### Lemma 9

The reconstruction algorithm (Algorithm 1) does not calculate both
$ITERATION(B,F)$ and $ITERATION(B^{\prime},F)$ if $F\models B\equiv
B^{\prime}$.

Proof. Let $B$ and $B^{\prime}$ be two sets such that the reconstruction
algorithm calculates $ITERATION(B,F)$ and $ITERATION(B^{\prime},F)$. This
implies that the algorithm chooses $B$ in an iteration and $B^{\prime}$ in
another. By symmetry, the iteration of $B$ can be assumed to come first. This
iteration ends with $P=P\backslash\\{B^{\prime}\mid F\models B\equiv
B^{\prime}\\}$. When the iteration of $B^{\prime}$ begins, no set equivalent
to $B$ according to $F$ is in $P$ any longer. Since $B^{\prime}$ is in $P$, it
is not equivalent to $B$. This is a contradiction.

When the reconstruction algorithm extracts a set $B$ from $P$, all sets $A$
with $A<_{F}B$ have been removed in a past iteration. During that, $G$ was
increased to entail all clauses $A\rightarrow x$ entailed by $F$, which make
$SCL(B,F)$ because of $A<_{F}B$. That $G$ entails $SCL(B,F)$ is the
fundamental invariant of the algorithm.

###### Lemma 10

If $ITERATION(B,F)$ is a valid iteration function, $G\models SCL(B,F)$ holds
during the whole execution of the reconstruction algorithm (Algorithm 1).

Proof. The proof links the values of the variables at different iterations.
The values of $P$, $B$ and $G$ at the $i$-th iteration of the algorithm are
denoted $P_{i}$, $B_{i}$ and $G_{i}$. More precisely, these are the values
right after Step 3a of the $i$-th iteration.

The claim $G\models SCL(B,F)$ is proved by induction over the number of
iterations of the loop.

In the first iteration, $P_{1}$ contains all sets of variables, $G_{1}$ is the
empty set and $B_{1}$ is a set of $P_{1}$ such that $P_{1}$ contains no set
$A<_{F}B_{1}$. The values of $P_{1}$ and $B_{1}$ imply that no set such that
$A<_{F}B_{1}$ exists. As a result, $SCL(B_{1},F)$ is empty and therefore
entailed even by the empty formula $G_{1}$.

The induction claim is $G_{i}\models SCL(B_{i},F)$; the induction assumption
is $G_{j}\models SCL(B_{j},F)$ for every $j<i$.

The claim $G_{i}\models SCL(B_{i},F)$ is $G_{i}\models A\rightarrow x$ if
$x\not\in A$, $F\models A\rightarrow x$ and $A<_{F}B$. The set $B_{i}$ is an
element of $P_{i}$ such that $P_{i}$ contains no element that is strictly less
than $B_{i}$. Since $A$ is strictly less than $B_{i}$, it is not in $P_{i}$.
Going back to the first iteration, $P_{1}$ contains all sets of variables,
including $A$. Therefore, $A$ is removed at some iteration $j<i$. The only
removal instruction is $P_{j+1}=P_{j}\backslash\\{B^{\prime}\mid F\models
B_{j}\equiv B^{\prime}\\}$. It removes $A$; therefore, $F\models B_{j}\equiv
A$ holds. With the assumptions that $A\rightarrow x$ is not tautologic and is
entailed by $F$, it proves that $A\rightarrow x$ belongs to $BCL(B_{j},F)$.

The induction assumption is $G_{j}\models SCL(B_{j},F)$. A consequence is that
$G_{j}\cup ITERATION(B_{j},F)$ entails $SCL(B_{j},F)\cup ITERATION(B_{j},F)$.
By definition of a valid iteration function, the latter entails
$BCL(B_{j},F)$, which includes $A\rightarrow x$. This clause is therefore
entailed by $G_{j}\cup ITERATION(B_{j},F)$, the same as $G_{j+1}$.

Since $j<i$ and $G$ monotonically increases, $G_{j+1}\subseteq G_{i}$. As a
result, $G_{i}\models A\rightarrow x$, which is the claim.

The reconstruction algorithm generates a formula that is equivalent to $F$.
This holds for every valid iteration function and nondeterministic choices.

###### Lemma 11

If $ITERATION(B,F)$ is a valid iteration function, the formula produced by the
reconstruction algorithm is equivalent to $F$.

Proof. The algorithm returns $G$, which is only added clauses of
$ITERATION(B,F)$. All of them are entailed by $F$ by the definition of valid
iteration functions. This proves that the formula returned by the algorithm
contains only clauses entailed by $F$.

It is now proved to imply all clauses $B^{\prime}\rightarrow x$ entailed by
$F$. By Lemma 8, the reconstruction algorithm calculates $ITERATION(B,F)$ for
some $B$ such that $F\models B\equiv B^{\prime}$. A consequence of the
invariant $G\models SCL(B,F)$ proved by Lemma 10 is that $G\cup
ITERATION(B,F)$ entails $SCL(B,F)\cup ITERATION(B,F)$, which entails
$B^{\prime}\rightarrow x$ by the definition of valid iteration. By
transitivity, $G\cup ITERATION(B,F)$ entails $B^{\prime}\rightarrow x$. After
$G=G\cup ITERATION(B,F)$, it is $G$ that entails $B^{\prime}\rightarrow x$.
Since $G$ is never removed clauses, at the end of the algorithm $G$ still
entails $B^{\prime}\rightarrow x$.

The algorithm is correct: it always terminates and always outputs a formula
equivalent to the given one. What is missing is its completeness: if the input
formula is equivalent to a single-head formula, that formula is output for
some valid iteration function.

###### Lemma 12

If $F$ is equivalent to a single-head formula $F^{\prime}$, for some valid
iteration function the reconstruction algorithm (Algorithm 1) returns
$F^{\prime}$.

Proof. By Lemma 6, $ITERATION(B,F)={}\\{B^{\prime}\rightarrow x\in
F^{\prime}\mid F^{\prime}\models B\equiv B^{\prime}\\}$ is a valid iteration.
The algorithm always terminates thanks to Lemma 11. It returns only clauses
from $ITERATION(B,F)$; since these are all clauses of $F^{\prime}$, the return
value is a subset of $F^{\prime}$.

The claim is proved by showing that all clauses of $F^{\prime}$ are returned.
Let $B^{\prime}\rightarrow x\in F^{\prime}$. By Lemma 8, the algorithm
calculates $ITERATION(B,F)$ for some $B$ such that $F\models B\equiv
B^{\prime}$. By construction, $B^{\prime}\rightarrow x$ is in
$ITERATION(B,F)$. The algorithm returns the union of all sets $ITERATION(B,F)$
it calculates, and $B^{\prime}\rightarrow x$ is in this union.

This lemma tells that every single-head formula equivalent to the input can be
returned by the reconstruction algorithm using the appropriate iteration
function. Yet, an inappropriate iteration function may make it return a
formula that is still equivalent to the original but is not single-head. An
additional property of the iteration function is required to avoid such an
outcome.

###### Lemma 13

If $ITERATION(B,F)$ is a valid iteration function whose values never contain
each two clauses with the same head then the reconstruction algorithm
(Algorithm 1) returns a single-head formula if and only if $F$ is equivalent
to a single-head formula.

Proof. Let $F^{\prime}$ be the formula returned by the reconstruction
algorithm on $F$. By Lemma 11, $F\equiv F^{\prime}$.

If $F^{\prime}$ is single-head, then $F$ is single-head equivalent by
definition.

Otherwise, $F^{\prime}$ is not single-head. The following proof shows that $F$
is equivalent to no single-head formula.

Let $B\rightarrow x$ and $C\rightarrow x$ be two clauses returned by the
algorithm. They were added to $G$ in different iterations, since by assumption
$ITERATION(B,F)$ does not contain two clauses with the same head. Let
$B^{\prime}$ and $C^{\prime}$ be the values of $B$ in the iterations that
produce them:

$\displaystyle B\rightarrow x$ $\displaystyle\in$ $\displaystyle
ITERATION(B^{\prime},F)\mbox{ where }F\models B\equiv B^{\prime}$
$\displaystyle C\rightarrow x$ $\displaystyle\in$ $\displaystyle
ITERATION(C^{\prime},F)\mbox{ where }F\models C\equiv C^{\prime}$

By Lemma 9, the reconstruction algorithm does not determine both
$ITERATION(B^{\prime},F)$ and $ITERATION(C^{\prime},F)$ if $F\models
B^{\prime}\equiv C^{\prime}$. Therefore, $F\not\models B\equiv C$.

Let $F^{\prime}$ be a single-head formula that is equivalent to $F$, and
$A\rightarrow x$ be its only clause with head $x$. Because of its equivalence
with $F$, it entails both $B\rightarrow x$ and $C\rightarrow x$. Since these
clauses are produced by a valid iteration function, they are not tautologic:
$x\not\in B$ and $x\not\in C$. Lemma 1 tells that $F^{\prime}$ contains
$B^{\prime\prime}\rightarrow x$ and $C^{\prime\prime}\rightarrow x$ such that
$F^{\prime}\models B\rightarrow B^{\prime\prime}$ and $F^{\prime}\models
C\rightarrow C^{\prime\prime}$. Since the only clause of $F^{\prime}$ that has
$x$ in the head is $A\rightarrow x$, both $B^{\prime\prime}$ and
$C^{\prime\prime}$ coincide with $A$. As a result, $F^{\prime}$ entails
$B\rightarrow A$ and $C\rightarrow A$.

Since $F$ is equivalent to $F^{\prime}$, it also does. This is the same as
$A\leq_{F}B$ and $A\leq_{F}C$. These orderings are not strict. Otherwise,
$A<_{F}B$ implies $A<_{F}B^{\prime}$, which implies $A\rightarrow x\in
SCL(B^{\prime},F)$, which implies $x\not\in SFREE(B^{\prime},F)$, which
contradicts $B\rightarrow x\in ITERATION(B^{\prime},F)$ since the latter
includes $x\in SFREE(B^{\prime},F)$. The same applies to $A<_{F}C$. As a
result, $F\models A\equiv B$ and $F\models A\equiv C$. The consequence
$F\models B\equiv C$ contradicts $F\not\models B\equiv C$, which was
previously proved.

This lemma completes the proof of soundness and correctness of the
reconstruction algorithm: it terminates with a single-head formula, if any; if
any exists, it returns it.

###  3.6 Efficiency of the reconstruction algorithm

The reconstruction algorithm works flawlessly in theory, but in practice its
iterations may be exponentially many because so many are the sets of
variables. A small change solves the problem: instead of all sets of
variables, only process the bodies of clauses of the formula. The algorithm
produces the same result because it runs like using a tie-breaking rule: if
more than one set is minimal, prefer one such that $ITERATION(B,F)=\emptyset$;
if none is such, choose a set that is the body of a clause of $F$. The
following two lemmas show this rule valid.

###### Lemma 14

If $ITERATION(B,F)\not=\emptyset$ then $F\models B\equiv B^{\prime\prime}$
holds for some clause $B^{\prime\prime}\rightarrow x\in F$.

Proof. Let $B^{\prime}\rightarrow x$ be a clause of $ITERATION(B,F)$. The
definition of valid iteration includes $x\not\in B^{\prime}$, $F\models
B^{\prime}\equiv B$, $F\models B^{\prime}\rightarrow x$ and $x\in SFREE(B,F)$.

From $F\models B^{\prime}\rightarrow x$ and $x\not\in B^{\prime}$ Lemma 1
implies that $F$ contains a clause $B^{\prime\prime}\rightarrow x$ such that
$F\models B^{\prime}\rightarrow B^{\prime\prime}$. The converse implication
$F\models B^{\prime\prime}\rightarrow B^{\prime}$ may hold or not. If it does,
then $F$ contains a clause $B^{\prime\prime}\rightarrow x$ with $F\models
B^{\prime}\equiv B^{\prime\prime}$. Since $F\models B\equiv B^{\prime}$, it
follows $F\models B\equiv B^{\prime\prime}$ and the claim is proved.

The other case $F\not\models B^{\prime\prime}\rightarrow B^{\prime}$ is shown
to lead to contradiction. Since $F\models B\equiv B^{\prime}$, the conditions
$F\not\models B^{\prime\prime}\rightarrow B^{\prime}$ and $F\models
B^{\prime}\rightarrow B^{\prime\prime}$ extend from $B^{\prime}$ to $B$. This
change turns them into $F\not\models B^{\prime\prime}\rightarrow B$ and
$F\models B\rightarrow B^{\prime\prime}$. This is the definition of
$B^{\prime\prime}<_{F}B$. Since $B^{\prime\prime}\rightarrow x$ is in $F$, it
is not a tautology and is entailed by $F$. With $B^{\prime\prime}<_{F}B$,
these conditions define $B^{\prime\prime}\rightarrow x\in SCL(B,F)$. This
implies $x\not\in SFREE(B,F)$, which conflicts with $x\in SFREE(B,F)$.

The choice of the minimal set $B$ in the construction algorithm is non-
deterministic. All lemmas proved so far hold for every possible
nondeterministic choices. Therefore, they also hold when restricting the
choices in whichever way. The following lemma tells that the candidate sets
are of two kinds: those which would generate an empty set of clauses, and
those equivalent to the body of a clause in the original formula.

###### Lemma 15

At every step of the reconstruction algorithm (Algorithm 1) if $P$ is not
empty it contains either a $\leq_{F}$-minimal set $B$ such that
$ITERATION(B,F)=\emptyset$ or a $\leq_{F}$-minimal set $B$ such that
$B\rightarrow x\in F$.

Proof. Since $P$ is not empty, it has at least a minimal element $B$ because
$\leq_{F}$ is a partial order. If $ITERATION(B,F)$ is empty, the claim is
proved. Otherwise, $ITERATION(B,F)\not=\emptyset$, and Lemma 14 applies: $F$
contains a clause $B^{\prime\prime}\rightarrow x$ such that $F\models B\equiv
B^{\prime\prime}$. Its body $B^{\prime\prime}$ is $<_{F}$-minimal in $P$
because it is equivalent to $B$, which is minimal. Remains to prove that
$B^{\prime\prime}$ is in $P$.

By contradiction, $B^{\prime\prime}\not\in P$ is assumed. Since $P$ initially
contains all sets of variables, $B^{\prime\prime}$ was removed at some point.
The only operation removing elements from $P$ removes all sets equivalent to a
given one. Since it removes $B^{\prime\prime}$ it also removes $B$ since it is
equivalent to $B^{\prime\prime}$. This contradicts the assumption that $B$ is
in $P$.

If $ITERATION(B,F)$ is empty the iteration that chooses $B$ is irrelevant to
the final result since $G$ remains the same. The sets equivalent to $B$ could
just be removed from $P$. The other case is that $B$ is equivalent to a body
$B^{\prime\prime}$ of a clause of $F$. Since $B$ is minimal, also
$B^{\prime\prime}$ is minimal. Therefore, the algorithm could as well choose
$B^{\prime\prime}$ instead of $B$. This means that the algorithm may be
limited to choosing sets of variables that are bodies of clauses of $F$. The
other sets either do not change $G$ or can be replaced by them.

######  Algorithm 2 (Precondition-reconstruction algorithm)

  1. 1.

$G=\emptyset$

  2. 2.

$P=\\{B\mid B\rightarrow x\in F\mbox{ for some variable x}\\}$

  3. 3.

while $P\not=\emptyset$:

    1. (a)

choose a $<_{F}$-minimal $B\in P$
(a set such that $A<_{F}B$ does not hold for any $A\in P$)

    2. (b)

$G=G\cup ITERATION(B,F)$

    3. (c)

$P=P\backslash\\{B^{\prime}\mid F\models B\equiv B^{\prime}\\}$

  4. 4.

return $G$

The algorithm is almost the same as the basic reconstruction algorithm
(Algorithm 1). The only difference is that $P$ is no longer initialized with
all sets of variables, but only with the bodies of the clauses of $F$. Its
initial size is reduced from exponential to linear. Since each iterations
removes at least $B$, it makes $P$ strictly decrease. They are therefore
linearly many. The algorithm is still not polynomial-time since
$ITERATION(B,F)$ may not be polynomial.

This new, efficient version of the reconstruction algorithm is like the
original one with a restriction of the nondeterministic choices: if
$ITERATION(B,F)=\emptyset$ holds for some minimal sets $B$ of $P$, one of them
is chosen; otherwise, the body of a clause of $F$ is chosen. Lemma 15
guarantees that $P$ always contains a minimal set of either kind.

The difference is that the original algorithm removes all sets $B^{\prime}$
such that $F\models B\equiv B^{\prime}$ when $ITERATION(B,F)=\emptyset$; the
new algorithm virtually removes $B$ only. The following lemma shows that the
other sets $B^{\prime}$ also satisfy $ITERATION(B^{\prime},F)=\emptyset$, and
are therefore removed right after $B$.

###### Lemma 16

If $ITERATION(B,F)=\emptyset$ and $F\models B\equiv B^{\prime}$ then
$ITERATION(B^{\prime},F)=\emptyset$.

Proof. The proof shows contradictory the existence of a clause
$B^{\prime\prime}\rightarrow x$ in $ITERATION(B^{\prime},F)$. The definition
of a valid iteration function includes $x\not\in B^{\prime\prime}$, $F\models
B^{\prime\prime}\rightarrow x$, $F\models B\equiv B^{\prime\prime}$ and $x\in
SFREE(B,F)$. The first three conditions define $B^{\prime\prime}\rightarrow
x\in BCL(B^{\prime},F)$.

Since $BCL(B^{\prime},F)$ and $SFREE(B^{\prime},F)$ are defined from what $F$
entails, they coincide with $BCL(B,F)$ and $SFREE(B,F)$ since $F\models
B\equiv B^{\prime}$. This implies $B^{\prime\prime}\rightarrow x\in BCL(B,F)$
and $x\in SFREE(B,F)$.

The definition of $ITERATION(B,F)$ includes $SCL(B,F)\cup
ITERATION(B,F)\models BCL(B,F)$. Since $ITERATION(B,F)$ is empty, this is the
same as $SCL(B,F)\models BCL(B,F)$. As a result, $SCL(B,F)$ implies
$B^{\prime\prime}\rightarrow x$ while not containing any positive occurrence
of $x$ since $x\in SFREE(B,F)$. This is only possible if
$B^{\prime\prime}\rightarrow x$ is tautologic, but $x\in B^{\prime\prime}$
contradicts $x\not\in B^{\prime\prime}$.

The restriction of the nondeterministic choices does not affect the lemmas
about Algorithm 1 proved so far. While not explicitly mentioned, they do not
assume anything about the nondeterministic choices. As a result, they hold
regardless of them. They hold even restricting the nondeterministic choice in
whichever way.

As a result, the new algorithm always terminates, always returns a formula
equivalent to the given one, and that formula is single-head if and only if
any is equivalent to the original, provided that $ITERATION(B,F)$ does not
contain two clauses of the same head for any $B$.

The modified reconstruction algorithm performs the loop a number of times
equal to the number of clauses of the input formula. More precisely, to the
number of different bodies in the formula; still, a linear number of times. If
each iteration turns out to be polynomial, establishing single-head
equivalence would be proved polynomial.

The problem is indeed in $ITERATION(B,F)$. A brute-force implementation is to
loop over all sets of clauses $B^{\prime}\rightarrow x$ with
$B^{\prime}\equiv_{F}B$ and $x\in SFREE(B,F)$, checking if one satisfies the
conditions of validity. Unfortunately, the sets $B^{\prime}$ may be
exponentially many. This obvious solution is unfeasible.

Whether $ITERATION(B,F)$ can be determined in polynomial time is an open
problem. The following section gives an algorithm that may run in polynomial
time but is exponential-time in the worst case.

###  3.7 Formulae that are not single-head equivalent

All is good when the formula is single-head equivalent: an appropriate valid
iteration function makes the reconstruction algorithm return a single-head
formula that is equivalent to the given one. This is what happens when the
formula is single-head equivalent. What if it is not?

An easy and wrong answer is that the algorithm returns a formula that is not
single-head. A closer look at the lemmas shows that this is not always the
case.

Lemma 11 tells that the reconstruction algorithm returns a formula that is
equivalent to the given one, but has a requirement: a valid iteration
function. That one exists is only guaranteed for single-head formulae, not in
general. If the formula is not single-head equivalent then either:

  * •

no valid iteration function exists;

  * •

a valid iteration function exists; it makes the algorithm generate a formula
equivalent to the given one by Lemma 11 and therefore not single-head.

Lemma 11 splits the second case in two: either the iteration function has some
values containing two clauses with the same head or it does not. All three
cases are possible.

An example of a formula that has no valid iteration function is
$F=\\{a\rightarrow b,b\rightarrow c,c\rightarrow b\\}$, in the following
figure and in the inloop.py test file of the singlehead.py program. While
$ITERATION(\\{b\\},F)$ and $ITERATION(\\{c\\},F)$ satisfy the definition of
validity if equal to $\\{b\rightarrow c,c\rightarrow b\\}$, no value for
$ITERATION(\\{a\\},F)$ does. Indeed, $SCL(\\{a\\},F)=\\{b\rightarrow
c,c\rightarrow b\\}$, which implies $SFREE(\\{a\\},F)=\\{a\\}$. As a result,
$ITERATION(\\{a\\},F)$ could only be empty. This is not possible because
$BCL(\\{a\\},F)$ contains $a\rightarrow c$ and $b\rightarrow c$, which are not
entailed by $SCL(\\{a\\},F)$.

$a$$b$$c$

An example of a formula that has a valid iteration function but all of them
have values with two clauses with the same head is $F=\\{x\rightarrow
a,a\rightarrow d,x\rightarrow b,b\rightarrow c,{}ac\rightarrow x,bd\rightarrow
x\\}$. This formula is in the disjointnotsingle.py test file of the
singlehead.py program. The following figure shows it. A valid iteration
function is $ITERATION(\\{a\\},F)=\\{a\rightarrow d\\}$,
$ITERATION(\\{b\\},F)=\\{b\rightarrow c\\}$,
$ITERATION(\\{x\\},F)={}ITERATION(\\{a,b\\},F)={}ITERATION(\\{a,c\\},F)={}ITERATION(\\{d,b\\},F)={}\\{x\rightarrow
a,x\rightarrow b,ac\rightarrow x,bd\rightarrow x\\}$, but the last values
contain two clauses with the same head $x$. This is always the case. In
particular, if $B=\\{x\\}$ then $ITERATION(B,F)$ is required to entail
$x\rightarrow a$, $x\rightarrow b$, $ac\rightarrow x$ and $bd\rightarrow x$,
but $SCL(B,F)=\\{a\rightarrow d,b\rightarrow c\\}$ does not help at all. Three
heads $x$, $a$ and $b$ do not suffice for four bodies.

$a$$c$$b$$d$$x$$D$$C$$B$$A$

An example of a formula that is not single-head equivalent but has a valid
iteration function that never returns a set containing two clauses with the
same head is $F=\\{a\rightarrow c,b\rightarrow c\\}$, in the following figure
and in the samehead.py test file of the singlehead.py program. Its only valid
iteration function is defined by $ITERATION(\\{a\\},F)=\\{a\rightarrow c\\}$
and $ITERATION(\\{b\\},F)=\\{b\rightarrow c\\}$. The reconstruction algorithm
either processes $\\{a\\}$ first and $\\{b\\}$ second or vice versa. In both
cases it adds both $ITERATION(\\{a\\},F)$ and $ITERATION(\\{b\\},F)$ to the
resulting formula, which ends up containing two clauses with head $c$.

$b$$a$$c$

The algorithm as implemented in the singlehead.py program does not deal with
these three cases separately. It needs not. The optimizations in the search
for an iteration function turn all three cases into the first, where no valid
iteration function exists.

The reason is that $ITERATION(B,F)$ is not calculated in advance, but during
the iteration for $B$. A number of candidate sets of clauses are tried.
Excluding the ones with duplicated heads is actually a simplification. So is
excluding the ones that contain some heads of another value $ITERATION(A,F)$
calculated before, which happens in two cases: when no valid iteration
function exists and when the output formula would not be single-head.

##  4 The iteration function

The reconstruction algorithm uses a function $ITERATION(B,F)$ at each
iteration. Only its properties have been given so far. If $F$ is single-head
equivalent such a function is easily proved to exist, but how to calculate it
is an entirely different story. This long section is exclusively devoted to
this problem.

At least, the value of the function $ITERATION(B,F)$ for $B$ is independent of
that for $B^{\prime}$. Even if $B\equiv_{F}B^{\prime}$, but also if
$B\not\equiv_{F}B^{\prime}$, it is not required to be the same. This is a
simplification because the computation of $ITERATION(B,F)$ is only affected by
the set of variables $B$, not by any other set $B^{\prime}$.

The requirements on $ITERATION(B,F)$ are listed in Definition 6: is a set of
non-tautological clauses $B^{\prime}\rightarrow x$ such that $F\models
B^{\prime}\rightarrow x$, $B^{\prime}\equiv_{F}B$, $x\in SFREE(B,F)$ and
$SCL(B,F)\cup ITERATION(B,F)\models BCL(B,F)$.

The algorithm presented in this section is implemented in the Python program
singlehead.py: it first determines the heads of the clauses; it then
calculates the set of all possible bodies to be associated with them; for each
association, the resulting set is checked. The first two steps automatically
guarantee the first three conditions, the second checks the fourth.

The heads are uniquely determined. This is not the case for the bodies, nor it
is the case for their associations with the heads. Efficiency depends on how
many alternatives can be excluded in advance, and how fast they can be
discarded if they are not valid.

###  4.1 Heads in search of bodies

The heads of the clauses of $ITERATION(B,F)$ are uniquely determined. The
condition of validity implies an exact set of heads; two valid iteration
functions do not differ on their heads. If $ITERATION(B,F)$ is also required
not to contain duplicated heads, it must contain exactly a clause for each
head.

The starting point is $BCN(B,F)=\\{x\mid F\models B\rightarrow x\\}$, the set
of variables entailed by $F$ and $B$. A valid iteration function
$ITERATION(B,F)$ contains only clauses with head in $BCN(B,F)$. Not the other
way around, because:

  * •

$ITERATION(B,F)$ does not contain heads in $SFREE(B,F)$ but $BCN(B,F)$ does;

  * •

$ITERATION(B,F)$ does not contain heads that are in all sets equivalent to
$B$, but $BCN(B,F)$ does; if a clause $B^{\prime}\rightarrow x$ is in
$ITERATION(B,F)$ then $B^{\prime}\equiv_{F}B$; if $x$ is in all sets
equivalent to $B$ then $x\in B^{\prime}$; the clause $B^{\prime}\rightarrow x$
is true but tautological.

The second point may look moot. As a matter of facts, it is not. An example
clarifies why $ITERATION(B,F)$ cannot include tautologies. The formula is
$F=\\{ab\rightarrow c,ac\rightarrow b,d\rightarrow a\\}$, in the following
figure and in the equiall.py test file. The sets $\\{a,b\\}$ and $\\{a,c\\}$
are equivalent. The clauses $ab\rightarrow a$ and $ac\rightarrow a$ are
tautological. While they look harmless, useless but harmless, they are not.
Once in $ITERATION(\\{a,b\\},F)$, they conflict with $ITERATION(\\{d\\},F)$,
which needs $d\rightarrow a$. The formula returned by the reconstruction
algorithm would not be single-head while $F$ is single-head equivalent, being
single-head. Variables like $a$ are not possible heads for $\\{a,b\\}$
although they are in $BCN(\\{a,b\\},F)$ and may be in $SFREE(\\{a,b\\},F)$.
Excluding tautologies excludes them.

$d$$b$$a$$c$

Finding such variables is easy using the real consequences [Lib20c]:
$RCN(B,F)=\\{x\mid F\cup(BCN(B,F)\backslash\\{x\\})\models x\\}$. They are the
variables that follow from $B$ because of some clauses of $F$, not just
because they are in $B$.

###### Lemma 17

If $x\in BCN(B,F)\backslash RCN(B,F)$ and $F\models B\equiv B^{\prime}$, then
$x\in B^{\prime}$.

Proof. The contrary of the claim is proved contradictory: $x\not\in
B^{\prime}$.

Since $x$ is in $BCN(B,F)\backslash RCN(B,F)$, it is in $BCN(B,F)$ but not in
$RCN(B,F)$.

The first condition $x\in BCN(B,F)$ is defined as $F\cup B\models x$. With the
assumption $F\models B\equiv B^{\prime}$, it implies $F\cup B^{\prime}\models
x$.

The second condition $x\not\in RCN(B,F)$ is defined as
$F\cup(BCN(B,F)\backslash\\{x\\})\not\models x$. The assumption $F\models
B\equiv B^{\prime}$ implies $F\models B\rightarrow B^{\prime}$, which in turn
implies $B^{\prime}\subseteq BCN(B,F)$. Because of the additional assumption
$x\not\in B^{\prime}$, this containment strengthens to $B^{\prime}\subseteq
BCN(B,F)\backslash\\{x\\}$. Since $F\cup(BCN(B,F)\backslash\\{x\\})\not\models
x$, the entailment $F\cup B^{\prime}\not\models x$ follows by monotonicity,
contradicting $F\cup B^{\prime}\models x$.

This lemma tells that a variable in $BCN(B,F)$ but not in $RCN(B,F)$ belongs
to all sets $B^{\prime}$ that are equivalent to $B$ according to $F$. The
following lemma proves something in the opposite direction: the variables in
$RCN(B,F)$ may be heads of $ITERATION(B,F)$.

###### Lemma 18

If $x\in RCN(B,F)$ then $B^{\prime}\rightarrow x\in BCL(B,F)$ for some
$B^{\prime}$.

Proof. Since $F\cup B$ implies every variable in $BCN(B,F)$ by definition, it
implies $BCN(B,F)$. A consequence of the deduction theorem is $F\models
B\rightarrow BCN(B,F)$. Every variable in $B$ is entailed by $F\cup B$ and is
therefore in $BCN(B,F)$. A consequence of $B\subseteq BCN(B,F)$ is $F\models
BCN(B,F)\rightarrow B$. Equivalence is therefore proved: $F\models B\equiv
BCN(B,F)$.

The assumption $x\in RCN(B,F)$ is defined as
$F\cup(BCN(B,F)\backslash\\{x\\})\models x$. Combined with the tautological
entailment $F\cup(BCN(B,F)\backslash\\{x\\})\models
BCN(B,F)\backslash\\{x\\}$, it implies
$F\cup(BCN(B,F)\backslash\\{x\\})\models{}BCN(B,F)\backslash\\{x\\}\cup\\{x\\}$.
This is the same as $F\cup(BCN(B,F)\backslash\\{x\\})\models BCN(B,F)$, which
is the same as $F\models BCN(B,F)\backslash\\{x\\}\rightarrow BCN(B,F)$. The
converse implication is a consequence of monotony. This proves the equivalence
$F\models BCN(B,F)\backslash\\{x\\}\equiv BCN(B,F)$. By transitivity of
equivalence, $F\models B\equiv BCN(B,F)\backslash\\{x\\}$.

The set $B^{\prime}$ required by the claim of the lemma is
$BCN(B,F)\backslash\\{x\\}$. The final consequence of the last paragraph is
$F\models B\equiv B^{\prime}$. Another entailment proved is
$F\cup(BCN(B,F)\backslash\\{x\\})\models x$, which is the same as $F\models
B^{\prime}\rightarrow x$. The last requirement for $B^{\prime}\rightarrow x$
to be in $BCL(B,F)$ is $x\not\in B^{\prime}$, which is the case because
$B^{\prime}$ is by construction the result of removing $x$ from another set.

This is not exactly the reverse of the previous lemma, in that it does not
precisely prove that $RCN(B,F)$ contains the variables that are in some sets
equivalent to $B$ but not all. Yet, it allows for a simple way for determining
the heads of the clauses in $ITERATION(B,F)$.

###### Lemma 19

The heads of the clauses in $ITERATION(B,F)$ for a valid iteration function is
$HEADS(B,F)=RCN(B,F)\cap SFREE(B,F)$.

Proof. The proof comprises two parts: first, if $B^{\prime}\rightarrow x\in
ITERATION(B,F)$ then $x\in HEADS(B,F)$; second, if $x\in HEADS(B,F)$ then
$B^{\prime}\rightarrow x\in ITERATION(B,F)$ for some set of variables
$B^{\prime}$.

The first part assumes $B^{\prime}\rightarrow x\in ITERATION(B,F)$. The
definition of valid iteration includes $x\not\in B^{\prime}$, $F\models
B\equiv B^{\prime}$, $F\models B^{\prime}\rightarrow x$ and $x\in SFREE(B,F)$.
A consequence of $F\models B\equiv B^{\prime}$ is that every element of
$B^{\prime}$ is entailed by $F\cup B$, and is therefore in $BCN(B,F)$. This
proves the containment $B^{\prime}\subseteq BCN(B,F)$. Since $x$ is not in
$B^{\prime}$, this containment strengthens to $B^{\prime}\subseteq
BCN(B,F)\backslash\\{x\\}$. The assumption $F\models B^{\prime}\rightarrow x$
implies $F\cup B^{\prime}\models x$. Since $B^{\prime}\subseteq
BCN(B,F)\backslash\\{x\\}$, this implies
$F\cup(BCN(B,F)\backslash\\{x\\})\models x$. This entailment defines $x\in
RCN(B,F)$. Since $x\in SFREE(B,F)$ also holds, the claim $x\in HEADS(B,F)$
follows.

The second part of the proof assumes $x\in HEADS(B,F)$. This is defined as
$x\in RCN(B,F)$ and $x\in SFREE(B,F)$. By Lemma 18, the first implies
$B^{\prime}\rightarrow x\in BCL(B,F)$ for some $B^{\prime}$. By the assumption
of validity of the iteration function, $SCL(B,F)\cup ITERATION(B,F)$ implies
$B^{\prime}\rightarrow x$. By Lemma 1, $SCL(B,F)\cup ITERATION(B,F)$ contains
a clause $B^{\prime\prime}\rightarrow x$. Since $x\in SFREE(B,F)$, this clause
is not in $SCL(B,F)$, and is therefore in $ITERATION(B,F)$.

The name of this function $HEADS(B,F)$ needs a clarification. The aim of
$ITERATION(B,F)$ is to reproduce $BCL(B,F)$. Since $HEADS(B,F)$ are the heads
of $ITERATION(B,F)$, they are the heads needed to reproduce $BCL(B,F)$. Not.

A part of the definition of $ITERATION(B,F)$ is that its heads are all in
$SFREE(B,F)$. This restriction presumes the formula single-head equivalent: it
only works if variables that are not heads in $SCL(B,F)$ suffice as heads of
clauses that reproduce $BCL(B,F)$. If they do not, $ITERATION(B,F)$ is unable
to imply $BCL(B,F)$. The following formula exemplifies such a situation.

$F=\\{a\rightarrow x,x\rightarrow b,b\rightarrow x\\}$

The heads of $SCL(\\{a\\},F)$ are $\\{b,x\\}$. The other variables are
$SFREE(\\{a\\},F)=\\{a\\}$. Therefore, $HEADS(\\{a\\},F)=\emptyset$ since
$a\not\in RCN(\\{a\\},F)$. The heads of $SCL(\\{a\\},F)$ and
$ITERATION(\\{a\\},F)$ are disjoint by definition, this is not the problem.
The problem is that the available heads $HEADS(\\{a\\},F)=\emptyset$ are
insufficient for building clauses that entail $BCL(B,F)$.

The first step for obtaining $ITERATION(B,F)$ is generating its heads. Finding
the bodies and attaching them to these heads is the hard part of the
reconstruction algorithm. Finding the heads is not.

###  4.2 Every body on its own heads

A side effect of Lemma 19 is an equivalent condition to single-head
equivalence. The following is a preliminary lemma.

###### Lemma 20

If a valid iteration function is such that $ITERATION(B,F)$ does not contain
multiple clauses with the same head for any $B$, the return value of the
reconstruction algorithm is single-head if and only if $HEADS(B,F)$ and
$HEADS(B^{\prime},F)$ do not overlap for any $B$ and $B^{\prime}$ such that
$F\not\models B\equiv B^{\prime}$.

Proof. One direction of the claim is that if the reconstruction algorithm
returns two clauses with the same head then $HEAD(B,F)\cap
HEAD(B^{\prime},F)\not=\emptyset$ for some $B$ and $B^{\prime}$ such that
$F\not\models B\equiv B^{\prime}$. The reconstruction algorithm returns the
union of all sets $ITERATION(B,F)$ it calculates. Since this union contains
two clauses of the same head, one comes from $ITERATION(B,F)$ and one from
$ITERATION(B^{\prime},F)$ because no single set $ITERATION(B,F)$ contains
multiple clauses with the same head. Lemma 9 tells that the reconstruction
algorithm does not determine both $ITERATION(B,F)$ and
$ITERATION(B^{\prime},F)$ if $F\models B\equiv B^{\prime}$. This proves
$F\not\models B\equiv B^{\prime}$. The heads of $ITERATION(B,F)$ and
$ITERATION(B^{\prime},F)$ are respectively $HEADS(B,F)$ and
$HEADS(B^{\prime},F)$ by Lemma 19. These sets overlap because $ITERATION(B,F)$
contains a clause with the same head as one of $ITERATION(B^{\prime},F)$. This
proves $HEADS(B,F)\cap HEADS(B^{\prime},F)\not=\emptyset$ with $F\not\models
B\equiv B^{\prime}$.

The other direction of the claim is that $HEADS(B,F)\cap
HEADS(B^{\prime},F)\not=\emptyset$ with $F\not\models B\equiv B^{\prime}$
implies that the reconstruction algorithm returns two clauses with the same
head. Lemma 8 states that the reconstruction algorithm determines
$ITERATION(B^{\prime\prime},F)$ for some $B^{\prime\prime}$ such that
$F\models B\equiv B^{\prime\prime}$. The heads of the clauses in
$ITERATION(B^{\prime\prime},F)$ are $HEADS(B^{\prime\prime},F)$, which is the
same as $HEADS(B,F)$ because $F\models B\equiv B^{\prime\prime}$. For the same
reason, the reconstruction algorithm also determines
$ITERATION(B^{\prime\prime\prime},F)$ with $F\models B^{\prime}\equiv
B^{\prime\prime\prime}$, and its heads are $HEADS(B^{\prime},F)$. Let $x\in
HEADS(B,F)\cap HEADS(B^{\prime},F)$. Both $ITERATION(B^{\prime\prime},F)$ and
$ITERATION(B^{\prime\prime\prime},F)$ contain a clause of head $x$. The body
cannot be the same because the first is equivalent to $B^{\prime\prime}$ and
the second to $B^{\prime\prime\prime}$, and these sets are respectively
equivalent to $B$ and $B^{\prime}$, which are not equivalent by assumption. As
a result, these two clauses have the same head but different bodies.

The condition that the sets $HEADS(B,F)$ are disjoint is logical, not
algorithmic. It is independent of the reconstruction algorithm. It depends on
the definition of $HEADS(B,F)$ which is based on $RCN(B,F)$ and $SFREE(B,F)$,
both defined in terms of entailments. It turns the overall search for a
single-head formula equivalent to $F$ into the local search for the clauses of
$ITERATION(B,F)$.

###### Lemma 21

A formula $F$ is equivalent to a single-head formula if and only if a valid
iteration function is such that $ITERATION(B,F)$ does not contain two clauses
with the same head for any $B$ and $HEADS(B,F)\cap HEADS(B^{\prime},F)$ is
empty for every $B$ and $B^{\prime}$ such that $F\not\models B\equiv
B^{\prime}$.

Proof. The long statement of the lemma is shortened by naming its conditions:
(a) a valid iteration function is such that $ITERATION(B,F)$ does not contain
two clauses with the same head for any $B$; (b) $HEADS(B,F)\cap
HEADS(B^{\prime},F)$ is empty for every $B$ and $B^{\prime}$ such that
$F\not\models B\equiv B^{\prime}$. The claim is that $F$ is single-head
equivalent if and only if both (a) and (b) hold.

The first direction of the claim assumes (a) and (b) and proves $F$ single-
head equivalent. Lemma 20 proves that the return value of the reconstruction
algorithm is single-head from (a) and (b). Lemma 11 proves that the
reconstruction algorithm returns a formula equivalent to $F$ when it uses a
valid iteration function, which is part of (a). This proves that $F$ is
single-head equivalent, as required.

The other direction of the claim assumes $F$ single-head equivalent and proves
(a) and (b).

Since $F$ is equivalent to a single-head formula $F^{\prime}$, Lemma 6
applies: $ITERATION(B,F)=\\{B^{\prime}\rightarrow x\in F^{\prime}\mid
F^{\prime}\models B\equiv B^{\prime}\\}$ is a valid iteration function.

It is proved to meet condition (a) by contradiction. Let
$B^{\prime\prime}\rightarrow x$ and $B^{\prime\prime\prime}\rightarrow x$ be
two different clauses of $ITERATION(B,F)$. They are in $F^{\prime}$ because
$ITERATION(B,F)$ only contains clauses of $F^{\prime}$. This implies that
$F^{\prime}$ is not single-head, while it is assumed to be.

Condition (b) is proved by contradiction. Its converse is $x\in HEADS(B,F)$
and $x\in HEADS(B^{\prime},F)$ with $F\not\models B\equiv B^{\prime}$. Lemma
19 proves that the heads of $ITERATION(B,F)$ and $ITERATION(B^{\prime},F)$ are
respectively $HEADS(B,F)$ and $HEADS(B^{\prime},F)$. Therefore, a clause
$B^{\prime\prime}\rightarrow x$ is in $ITERATION(B,F)$ and a clause
$B^{\prime\prime\prime}\rightarrow x$ is in $ITERATION(B^{\prime},F)$. Both
sets comprise only clauses of $F^{\prime}$ by construction. Therefore, both
clauses are in $F^{\prime}$. The definition of iteration function includes
$F\models B\equiv B^{\prime\prime}$ and $F\models B^{\prime}\equiv
B^{\prime\prime\prime}$. The assumption $F\not\models B\equiv B^{\prime}$
implies $F\not\models B^{\prime\prime}\equiv B^{\prime\prime\prime}$, which
implies $B^{\prime\prime}\not=B^{\prime\prime\prime}$. Two clauses of the same
head but different bodies are in $F^{\prime}$, which was assumed single-head.

The condition as stated by the lemma is infeasible to check since
exponentially many sets of variables exist. However, only the sets that are
bodies of clauses of the formula need to be checked.

###### Lemma 22

A formula $F$ is equivalent to a single-head formula if and only if there
exists a valid $ITERATION(B,F)$ that never produces two clauses with the same
head and $HEADS(B,F)\cap HEADS(B^{\prime},F)$ is empty for every clauses
$B\rightarrow x$ and $B^{\prime}\rightarrow y$ of $F$ with $F\not\models
B\equiv B^{\prime}$.

Proof. If $F$ is single-head equivalent, $HEADS(B,F)\cap HEADS(B^{\prime},F)$
is empty for every pair of sets $B$ and $B^{\prime}$ that are not equivalent
according to $\equiv_{F}$ by Lemma 21. It is therefore empty in the particular
case where $B$ and $B^{\prime}$ are bodies of clauses of $F$. This is one
direction of the claim.

The other direction requires proving that $F$ is single-head equivalent from
the other properties mentioned in the claim. The first condition includes the
existence of a valid iteration function $ITERATION(B,F)$. The second is that
$HEADS(B,F)\cap HEADS(B^{\prime},F)$ is empty whenever $F\not\models B\equiv
B^{\prime}$ and $B$ and $B^{\prime}$ are bodies of clauses of $F$. When a
valid iteration function exists, the second extends to the case where $B$ and
$B^{\prime}$ that are not bodies of clauses of $F$. The claim follows by Lemma
21.

By Lemma 14, either $ITERATION(B,F)=\emptyset$ or $F\models B\equiv
B^{\prime\prime}$ hold for some clause $B^{\prime\prime}\rightarrow x\in F$.
If $ITERATION(B,F)$ is empty so is $HEADS(B,F)$ because the latter is the set
of the heads of the former by Lemma 19. In this case, $HEADS(B,F)\cap
HEADS(B^{\prime},F)=\emptyset$ follows. The same holds for $B^{\prime}$ by
symmetry. The claim is therefore proved if either $B$ or $B^{\prime}$ are not
each $\equiv_{F}$-equivalent to a body of $F$.

Remains to prove it if both $B$ and $B^{\prime}$ are equivalent to a body of
$F$ each. Let $B^{\prime\prime}$ and $B^{\prime\prime\prime}$ be these bodies.
Since $B$ and $B^{\prime}$ are $\equiv_{F}$-equivalent, so are
$B^{\prime\prime}$ and $B^{\prime\prime}$. Since $F\models
B^{\prime\prime}\equiv B^{\prime\prime\prime}$ and $HEADS(B,F)$ is defined
from what $F$ entails, it coincides with $HEADS(B^{\prime\prime\prime},F)$.
For the same reason, $HEADS(B^{\prime},F)$ coincides with
$HEADS(B^{\prime\prime\prime\prime},F)$. Since $B^{\prime\prime}$ and
$B^{\prime\prime\prime}$ are bodies of clauses of $F$,
$HEADS(B^{\prime\prime},F)\cap HEADS(B^{\prime\prime\prime},F)=\emptyset$
holds by assumption. It implies $HEADS(B,F)\cap
HEADS(B^{\prime},F)=\emptyset$, the claim.

###  4.3 Head-on

Lemma 19 tells the heads of the clauses that may be in $ITERATION(B,F)$, but
also helps to find their bodies: since the heads are known and the clauses are
consequences of $F$, the bodies are found by bounding resolution to the heads.

###### Lemma 23

If $F\models B^{\prime}\rightarrow x$ and $x\not\in B^{\prime}$, a clause with
head $x$ and body contained in $B^{\prime}$ is obtained by repeatedly
resolving a non-tautological clause of $F$ with clauses of $F^{x}$.

Proof. Lemma 1 applied to $F\models B^{\prime}\rightarrow x$ and $x\not\in
B^{\prime}$ proves $F^{x}\models B^{\prime}\rightarrow B$ for some
$B\rightarrow x\in F$. This is the clause of $F$ in the statement of the
lemma. The rest of the proof shows that it is not a tautology and that it
resolves with a sequence of clauses of $F^{x}$, resulting in a subclause of
$B^{\prime}\rightarrow x$.

The clause $B\rightarrow x$ is first proved not to be a tautology. The
entailment $F^{x}\models B^{\prime}\rightarrow B$ is the same as
$F^{x}\cup\\{B^{\prime}\\}\models B$. The formula $F^{x}\cup\\{B^{\prime}\\}$
does not contain $x$ by the definition of $F^{x}$ and the assumption that
$B^{\prime}\rightarrow x$ is not a tautology ($x\not\in B^{\prime}$). Since it
is definite Horn and does not contain $x$ it satisfied by the model that sets
all variables to true but $x$: all clauses are satisfied since they contain at
least a positive variable, which is not $x$. This model does not satisfy $x$,
proving $F^{x}\cup\\{B^{\prime}\\}\models x$ impossible and disproving $x\in
B$.

Remains to show how to resolve $B\rightarrow x$ with the clauses of $F^{x}$.
It immediately follows from a property proved by induction.

The induction is on the size of a formula $G$. The property is: if $G$ entails
$B^{\prime}\rightarrow C$ then $C\cup D\rightarrow x$ resolves with some
clauses of $G$ into $B^{\prime\prime}\cup D\rightarrow x$ where
$B^{\prime\prime}$ is a subset of $B^{\prime}$. The clause $C\cup D\rightarrow
x$ is not required to be in $G$.

Since induction is on the size of $G$, the base case is that $G$ is empty. An
empty formula implies $B^{\prime}\rightarrow C$ only if $C\subseteq
B^{\prime}$. The claim holds with a zero-length resolution, since $C\cup
D\rightarrow x$ already satisfies $C\subseteq B^{\prime}$. This proves the
base case of induction.

The inductive case is for an arbitrary formula $G$.

If $C$ is a subset of $B^{\prime}$, the claim again holds because a zero-
length resolution turns $C\cup D\rightarrow x$ into itself, which satisfies
$C\subseteq B^{\prime}$.

If $C$ is not a subset of $B^{\prime}$, then $C\backslash B^{\prime}$ contains
some variables. Let $c\in C\backslash B^{\prime}$ be one of them: $c\in C$ and
$c\not\in B^{\prime}$. The first condition $c\in C$ makes $G\models
B^{\prime}\rightarrow C$ include $G\models B^{\prime}\rightarrow c$. The
second condition $c\not\in B^{\prime}$ and this conclusion are the premises of
Lemma 1, which proves $G^{c}\models B^{\prime}\rightarrow E$ for some clause
$E\rightarrow c\in G$.

Since $c\in C$, this clause $E\rightarrow c$ of $G$ resolves with $C\cup
D\rightarrow x$ into $C\backslash\\{c\\}\cup E\cup D\rightarrow x$. The
entailment $G^{c}\models B^{\prime}\rightarrow E$ allows applying the
inductive assumption: $C\backslash\\{c\\}\cup E\cup D\rightarrow x$ resolves
with clauses of $G^{c}$ into $C\backslash\\{c\\}\cup
B^{\prime\prime\prime}\cup D\rightarrow x$, where
$B^{\prime\prime\prime}\subseteq B^{\prime}$.

Overall, $C\cup D\rightarrow x$ resolves with a clause of $G$ into
$C\backslash\\{c\\}\cup E\cup D\rightarrow x$, which then resolves with
clauses of $G^{b}\subseteq G$ into $C\backslash\\{c\\}\cup
B^{\prime\prime\prime}\cup D\rightarrow x$ where
$B^{\prime\prime\prime}\subseteq B^{\prime}$. The last clause is similar to
the first $C\cup D\rightarrow x$ in that its head is the same and its body
minus $D$ is still implied by $B^{\prime}$. Indeed, $G\models
B^{\prime}\rightarrow C\backslash\\{c\\}\cup B^{\prime\prime\prime}$ follows
from $G\models B^{\prime}\rightarrow C$ and $B^{\prime\prime\prime}\subseteq
B^{\prime}$. Yet, the variables of $C\backslash\\{c\\}\cup
B^{\prime\prime\prime}$ not in $B^{\prime}$ are one less than those of $C$.

Applying the same mechanism to another variable of $C\backslash\\{c\\}\cup
B^{\prime\prime\prime}$ not in $B^{\prime}$ if any is therefore possible, and
results in another sequence of resolutions that replace that variable with
variables of $B^{\prime}$. Since the number of variables not in $B^{\prime}$
strictly decreases, the process terminates with a clause containing zero of
them. The resulting clause is $B^{\prime\prime}\cup D\rightarrow x$ with
$B^{\prime\prime}\subseteq B^{\prime}$.

This proves the induction claim.

The premise of the induction claim is $G\models B^{\prime}\rightarrow C$; its
conclusion is that $C\cup D\rightarrow x$ resolves with clauses of $G$ into
$B^{\prime\prime}\cup D\rightarrow x$ with $B^{\prime\prime}\subseteq
B^{\prime}$.

The premise is satisfied by $F^{x}\models B^{\prime}\rightarrow B$, obtained
in the first paragraph of the proof. The conclusion is that
$B\cup\emptyset\rightarrow x$ resolves with clauses of $F^{x}$ into
$B^{\prime\prime}\cup\emptyset\rightarrow x$ with $B^{\prime\prime}\subseteq
B^{\prime}$. Since the first paragraph of the proof also states $B\rightarrow
x\in F$, all parts of the lemma are proved.

The goal is still to find the clauses of $ITERATION(B,F)$. A previous result
shows that their heads are $HEADS(B,F)$ if the formula is single-head
equivalent. This lemma restricts its bodies. It does not restrict them enough,
however.

For example, since $abc\rightarrow d$ is a clause of $F=\\{a\rightarrow
b,ac\rightarrow d,abc\rightarrow d\\}$, it is the result of a zero-length
resolution starting from itself. Yet, $ac\rightarrow d$ is obtained in the
same way. It implies $abc\rightarrow d$, making it redundant. If a set of
clauses containing $ab\rightarrow d$ fails at being $ITERATION(B,F)$, the same
test with $abc\rightarrow d$ in its place fails as well.

The inclusion of $abc\rightarrow d$ among the clauses to test is a problem for
two reasons:

  * •

the bodies generated this way are associated to the heads in $HEADS(B,F)$ to
form the candidates for a valid iteration function; the number of these
combinations increases exponentially with the number of bodies;

  * •

as explained later, a candidate set for $ITERATION(B,F)$ is checked using the
result of this bounded form of resolution; namely, its result on $F$ and its
result on the formula under construction plus the candidate set are compared;
this comparison can be done syntactically, but only if all clauses in the
candidate set are minimal.

Retaining only the clauses of minimal bodies solves both problems:

$HCLOSE(H,F)=\\{B\rightarrow x\mid F\models B\rightarrow x,~{}x\in H\backslash
B,~{}\not\exists B^{\prime}\subset B~{}.~{}F\models B^{\prime}\rightarrow
x\\}$

This set can be generated by removing all clauses containing others from the
result of the resolution procedure hinged on $H$. The reconstruct.py program
does it by an obvious function $minimal(C)$ that returns the clauses of $C$
whose body does not strictly contain others. The algorithm that generates
$HCLOSE(B,F)$ calls it multiple times to reduce the set of clauses it works
on.

###### Algorithm 3

$hclose(H,F)$

  1. 1.

$C=\\{B\rightarrow x\in F\mid x\in H\backslash B\\}$

  2. 2.

$C=minimal(C)$

  3. 3.

$R=\emptyset$

  4. 4.

$T=C\backslash R$

  5. 5.

while $T\not=\emptyset$:

    1. (a)

for $B\rightarrow x\in T$:

       * for $B^{\prime\prime}\rightarrow y\in F$:

         * if $B^{\prime}\rightarrow x\in resolve(B^{\prime\prime}\rightarrow y,B\rightarrow x)$ and $x\not\in B^{\prime}$:

           * $C=C\cup\\{B^{\prime}\rightarrow x\\}$

    2. (b)

$C=minimal(C)$

    3. (c)

$R=R\cup T$

    4. (d)

$T=C\backslash R$

  6. 6.

return $C$

Since the main loop of this algorithm is a “while” statement on a set $T$ that
is changed in its iterations, its termination is not obvious. The following
lemma proves it.

###### Lemma 24

The hclose() algorithm (Algorithm 3) always terminates.

Proof. If a clause is in $T$, it is added to $R$ in the next iteration of the
main loop by the instruction $R=R\cup T$ and removed from $T$ by
$T=C\backslash R$.

The clause remains in $R$ because this set is never removed elements. It is
never inserted again in $T$ since this set is only changed by $T=C\backslash
R$. This proves that $T$ does not contain the same clause in two different
iterations.

The number of clauses deriving from resolution from a fixed formula is finite.
Since all clauses added to $T$ derive from resolution, if the iterations
overcome this finite number, $T$ is empty in at least one of them. This
condition terminates the loop.

Let $HCLOSEALL(H,F)$ be like $HCLOSE(H,F)$ without minimality:
$HCLOSEALL(H,F)=\\{B\rightarrow x\mid{}F\models B\rightarrow x,~{}{}x\in
H\backslash B\\}$.

The minimal subclauses of $HCLOSEALL(H,F)$ equivalently define $HCLOSE(H,F)$.

###### Lemma 25

The minimal subclauses of $HCLOSEALL(H,F)$ are $HCLOSE(H,F)$.

Proof. The definition of $B\rightarrow x\in HCLOSE(H,F)$ is $F\models
B\rightarrow x$, $x\in H\backslash B$ and no subclause $B^{\prime}\rightarrow
x$ of $B\rightarrow x$ is entailed by $F$. The same clause $B\rightarrow x$ is
minimal in $HCLOSEALL(H,F)$ if $F\models B\rightarrow x$, $x\in H\backslash B$
and no subclause $B^{\prime}\rightarrow x$ of $B\rightarrow x$ is in
$HCLOSEALL(H,F)$. The definition $B^{\prime}\rightarrow x\in HCLOSEALL(H,F)$
comprises $F\models B^{\prime}\rightarrow x$ but also $x\in H\backslash
B^{\prime}$. The latter is however not a restriction: if
$B^{\prime}\rightarrow x$ is a subclause of $B\rightarrow x$, which satisfies
$x\in H\backslash B$, it also satisfies $x\in H\backslash B^{\prime}$ since
$B^{\prime}\subseteq B$.

This set $HCLOSEALL(H,F)$ is not interesting by itself. It is only used as an
indirect means to prove the correctness of the algorithm. The first step in
that direction proves that the algorithm only produces clauses of
$HCLOSEALL(H,F)$. Not all of them, though. Yet, for each clause of
$HCLOSEALL(H,F)$ it produces a subclause. Since the only subclause in
$HCLOSEALL(H,F)$ of a minimal clause of $HCLOSEALL(H,F)$ is itself, this
proves that the algorithm generates it. Finally, the last statement
$C=minimal(C)$ excludes all clauses that are not minimal.

The first step of the proof proves that Algorithm 3 only returns clauses of
$HCLOSEALL(H,F)$.

###### Lemma 26

Every clause produced by the hclose() algorithm (Algorithm 3) is in
$HCLOSEALL(H,F)$.

Proof. The clauses in $HCLOSEALL(H,F)$ are defined by being entailed by $F$,
by having their head in $H$ and not being tautologies. The claim is proved by
showing the all clauses in $C$ satisfy these conditions throughout the
execution of the algorithm.

The set $C$ is initialized by $C=\\{B\rightarrow x\in F\mid x\in H\backslash
B\\}$, and $x\in H\backslash B$ implies $x\not\in B$. It is then changed only
by $C=C\cup\\{B^{\prime}\rightarrow x\\}$, which is only executed if $x\not\in
B^{\prime}$. This proves that $C$ never contains tautologies.

The other two properties are proved by showing that they are initially
satisfied and are never later falsified: every clause in $C$ is entailed by
$F$ and its head is in $H$.

The set $C$ is initialized by $C=\\{B\rightarrow x\in F\mid x\in H\backslash
B\\}$. All clauses in $F$ are entailed by $F$, and $x\in H\backslash B$
includes $x\in H$.

A clause $B^{\prime}\rightarrow x$ is added to $C$ only if it is the result of
resolving a clause $B\rightarrow x$ of $C$ with a clause
$B^{\prime\prime}\rightarrow y$ of $F$. Since all clauses of $C$ are entailed
by $F$, so is $B^{\prime}\rightarrow x$. Since all clauses of $C$ have head in
$H$, the head $x$ of $B^{\prime}\rightarrow x$ is in $H$.

This proves that every clause in $C$ is in $HCLOSEALL(H,F)$. Since the
algorithm returns $C$, it only returns clauses of $HCLOSEALL(H,F)$.

The algorithm returns clauses of $HCLOSEALL(H,F)$, but not all of them. As
expected, since $C$ is minimized. Yet, a subclause of every clause of
$HCLOSEALL(H,F)$ is returned.

###### Lemma 27

A subclause of every clause in $HCLOSEALL(H,F)$ is returned by the hclose()
algorithm (Algorithm 3).

Proof. The definition of $B^{\prime}\rightarrow x\in HCLOSEALL(H,F)$ is
$F\models B^{\prime}\rightarrow x$ and $x\in H\backslash B^{\prime}$. The
latter implies $x\not\in B^{\prime}$. Lemma 23 proves that a subclause of
$B^{\prime}\rightarrow x$ is obtained by iteratively resolving a clause
$B\rightarrow x\in F$ such that $x\not\in B$ with clauses of $F^{x}$.

The algorithm initializes $C$ with the non-tautological clauses of $F$ with
head in $H$. This includes $B\rightarrow x$ since $x$ is in $H$ but not in
$B$. The algorithm then iteratively adds to $C$ the resolvent of clauses of
$C$ with clauses of $F$, but also removes clauses by $C=minimize(C)$.

For each clause in the derivation, one of its subclauses is proved to be in
$C$ in the last step of the algorithm.

This property is proved iteratively: for the first clause of the derivation,
and then for every resolvent.

The first clause $B\rightarrow x$ of the derivation is shown to satisfy this
property. Being a clause of $F$ such that $x\in H\backslash B$, it is added to
$C$ by $C=\\{B\rightarrow x\mid{}F\models B\rightarrow x,~{}x\in H\backslash
B\\}$. The only instruction removing clauses from $C$ is $C=minimal(C)$, which
only removes clauses that strictly contain other clauses of $C$. In turn,
these contained clauses are removed only if $C$ contains strict subclauses of
them. By induction on the size of the subclause, $C$ contains a subclause of
$B\rightarrow x$ at the end of the execution of the algorithm.

An arbitrary clause $B^{\prime\prime}\rightarrow x$ of the derivation is
inductively assumed to satisfy the property: one of its subclauses
$B^{\prime\prime\prime}\rightarrow x$ is in $C$ at the end of execution. The
claim is proved on the following clause in the derivation.

Let $D\rightarrow b$ with $b\in B^{\prime\prime}$ be the clause of $F^{x}$
that resolves with $B^{\prime\prime}\rightarrow x$. Their resolvent is
$B^{\prime\prime}\backslash\\{b\\}\cup D\rightarrow x$. Since
$B^{\prime\prime\prime}\rightarrow x$ is a subclause of
$B^{\prime\prime}\rightarrow x$, its body $B^{\prime\prime\prime}$ is a subset
of $B^{\prime\prime}$. It may contain $b$ or not.

If $B^{\prime\prime\prime}$ does not contain $b$ then
$B^{\prime\prime\prime}\subseteq B^{\prime\prime}\backslash\\{b\\}$, and
$B^{\prime\prime\prime}\rightarrow x$ is itself a subclause of
$B^{\prime\prime}\backslash\\{b\\}\cup D\rightarrow x$, and is by assumption
in $C$ at the end of execution.

If $B^{\prime\prime\prime}$ contains $b$ then
$B^{\prime\prime\prime}\rightarrow x$ resolves with $D\rightarrow b$,
producing $B^{\prime\prime\prime}\backslash\\{b\\}\cup D\rightarrow x$. This
is a subclause of $B^{\prime\prime}\backslash\\{b\\}\cup D\rightarrow x$ since
$B^{\prime\prime\prime}\subseteq B^{\prime\prime}$. A subclause of this
resolvent is proved to be in $C$ at the end of execution.

Since $B^{\prime\prime\prime}\rightarrow x$ is in $C$, it has been added by
either $C=\\{B\rightarrow x\mid F{}\models B\rightarrow x,~{}x\in H\backslash
B\\}$ or $C=C\cup\\{B^{\prime}\rightarrow x\\}$. In the first case,
$B^{\prime\prime\prime}\rightarrow x$ is also copied to $T$. In the second,
since $R$ accumulates the values of $T$, either $T$ already contained
$B^{\prime\prime\prime}\rightarrow x$ at some previous point or contains it
after $T=C\backslash R$. Either way, at some point
$B^{\prime\prime\prime}\rightarrow x$ is in $T$. At the next iteration, it is
resolved with all clauses of $F$, including $D\rightarrow b$. This clause does
not contain $x$ since it is in $F^{x}$. Neither does $B^{\prime\prime\prime}$
since $B^{\prime\prime\prime}\rightarrow x$ is in $C$, which is never added a
tautology. Their resolvent $B^{\prime\prime\prime}\backslash\\{b\\}\cup
D\rightarrow x$ is therefore not a tautology and is therefore added to $C$. It
is removed if and when $C$ contains one of its proper subclauses. Which is
only removed if and when $C$ contains one of its proper subclauses. This
inductively proves that a subclause of
$B^{\prime\prime\prime}\backslash\\{b\\}\cup D\rightarrow x$, which is a
subclause of $B^{\prime\prime}\backslash\\{b\\}\cup D\rightarrow x$, is in $C$
at the end of execution.

This shows that a subclause of every clause in the derivation is in the final
value of $C$. This includes the final clause of the derivation:
$B^{\prime}\rightarrow x$. Since $B^{\prime}\rightarrow x$ is an arbitrary
clause of $HCLOSEALL(H,F)$, this proves that a subclause of every clause of
$HCLOSEALL(H,F)$ is produced by the algorithm.

The rest of the proof of correctness of Algorithm 3 is easy.

###### Lemma 28

The hclose() algorithm (Algorithm 3) generates exactly the minimal subclauses
of $HCLOSEALL(H,F)$.

Proof. For every clause $B^{\prime}\rightarrow x$ of $HCLOSEALL(H,F)$, the
algorithm generates one of its subclauses by Lemma 27. Since it is generated
by the algorithm, this subclause $B^{\prime\prime}\rightarrow x$ is in
$HCLOSEALL(H,F)$ by Lemma 26. Since $B^{\prime}\rightarrow x$ is minimal, none
of its proper subsets is in $HCLOSEALL(H,F)$. Therefore, the subclause
$B^{\prime\prime}\rightarrow x$ of $B^{\prime}\rightarrow x$ is not a proper
subclause: it coincides with $B^{\prime}\rightarrow x$. This proves that the
algorithm generates every minimal clause of $HCLOSEALL(H,F)$.

In the other direction, since the algorithm returns all minimal clauses of
$HCLOSEALL(H,F)$, it cannot return any non-minimal one. Indeed, if
$B^{\prime}\rightarrow x\in HCLOSEALL(H,F)$ contains another clause of
$HCLOSEALL(H,F)$, it also contains a minimal clause of $HCLOSEALL(H,F)$. By
Lemma 26, this minimal clause is in $C$ at the end of the algorithm.
Therefore, $B^{\prime}\rightarrow x$ is removed from $C$ by $C=minimal(C)$ and
is not returned.

Since the minimal subclauses of $HCLOSEALL(H,F)$ are exactly $HCLOSE(H,F)$ by
Lemma 25, the correctness of the algorithm is proved.

###### Corollary 2

The hclose() algorithm (Algorithm 3) returns $HCLOSE(H,F)$.

Having shown how $HCLOSE(H,F)$ can be calculated, it can be used to determine
$ITERATION(B,F)$, which is then used within the reconstruction algorithm to
determine a single-head formula equivalent to a given one if any. How it is
used is the theme of the next section.

###  4.4 Body search

When searching for the value of $ITERATION(B,F)$, Lemma 19 provides half of
the answer: its heads are exactly $HEADS(B,F)$. What about its bodies? The
definition of a valid iteration function only constraints them to come from
$BCL(B,F)$. It is not much of a constraint: being a set of consequences,
$BCL(B,F)$ is not bounded by the size of $F$. Not all of it is necessary,
though: if a valid iteration function exists, one such that $ITERATION(B,F)$
is contained in $HCLOSE(HEADS(B,F),UCL(B,F))$ exists as well. Proving this
statement is the aim of this section.

The first two lemmas are proved with an arbitrary subset of $SCL(B,F)\cup
BCL(B,F)$, which $UCL(B,F)$ is then proved to be.

###### Lemma 29

For every $H$ and every formula $F^{\prime}\subseteq SCL(B,F)\cup BCL(B,F)$,
it holds $HCLOSE(H,F^{\prime})\subseteq SCL(B,F)\cup BCL(B,F)$.

Proof. The condition $B^{\prime}\rightarrow x\in SCL(B,F)\cup BCL(B,F)$ is the
same as $B^{\prime}\rightarrow x\in SCL(B,F)$ or $B^{\prime}\rightarrow x\in
BCL(B,F)$. This is an alternative. The first case is $x\not\in B^{\prime}$,
$F\models B^{\prime}\rightarrow x$, $F\models B\rightarrow B^{\prime}$ and
$F\not\models B^{\prime}\rightarrow B$. The second is $x\not\in B^{\prime}$,
$F\models B^{\prime}\rightarrow x$, $F\models B\rightarrow B^{\prime}$ and
$F\models B^{\prime}\rightarrow B$. The two alternative subconditions
$F\not\models B^{\prime}\rightarrow B$ and $F\models B^{\prime}\rightarrow B$
cancel each other. This proves $B^{\prime}\rightarrow x\in SCL(B,F)\cup
BCL(B,F)$ equivalent to $x\not\in B^{\prime}$, $F\models B^{\prime}\rightarrow
x$ and $F\models B\rightarrow B^{\prime}$.

The premise of the lemma $F^{\prime}\subseteq SCL(B,F)\cup BCL(B,F)$ is the
same as $x\not\in B^{\prime}$, $F\models B^{\prime}\rightarrow x$ and
$F\models B\rightarrow B^{\prime}$ for every clause $B^{\prime}\rightarrow x$
of $F^{\prime}$. The claim is the same for every clause $B^{\prime}\rightarrow
x$ of $HCLOSE(H,F^{\prime})$.

The definition of $B^{\prime}\rightarrow x\in HCLOSE(H,F^{\prime})$ includes
$x\in H\backslash B^{\prime}$, which implies $x\not\in B^{\prime}$, the first
requirement for $B^{\prime}\rightarrow x\in SCL(B,F)\cup BCL(B,F)$. It also
includes $F^{\prime}\models B^{\prime}\rightarrow x$. Since $F^{\prime}$ is
contained in $SCL(B,F)\cup BCL(H,F)$, which only contains clauses entailed by
$F$, it is entailed by $F$. A consequence of $F\models F^{\prime}$ and
$F^{\prime}\models B^{\prime}\rightarrow x$ is $F\models B^{\prime}\rightarrow
x$. This is the second requirement for $B^{\prime}\rightarrow x\in
SCL(B,F)\cup BCL(B,F)$.

Only $F\models B\rightarrow B^{\prime}$ remains to be proved. Since $F$
entails $F^{\prime}$, which contains $B^{\prime}\rightarrow x$, it also
entails $B^{\prime}\rightarrow x$. A subclause of $B^{\prime}\rightarrow x$ is
obtained by resolving clauses of $F$. The claim $F\models B\rightarrow
B^{\prime}$ is iteratively proved on all clauses in such a derivation. The
base case is proved because $F\models F^{\prime}$ and $F^{\prime}\subseteq
SCL(B,F)\cup BCL(B,F)$ imply $F\models B\rightarrow B^{\prime}$ for every
clause $B^{\prime}\rightarrow x\in F^{\prime}$.

The induction step assumes $F\models B\rightarrow B^{\prime\prime}$ and
$F\models B\rightarrow B^{\prime\prime\prime}$ for two clauses
$B^{\prime\prime}\rightarrow x$ and $B^{\prime\prime\prime}\rightarrow y$
obtained from resolution. They resolve if either $x\in B^{\prime\prime\prime}$
or $y\in B^{\prime\prime}$. The result is respectively
$((B^{\prime\prime}\backslash\\{x\\})\cup B^{\prime\prime\prime})\rightarrow
y$ or
$(B^{\prime\prime}\cup(B^{\prime\prime\prime}\backslash\\{y\\}))\rightarrow
x$. In both cases the body of the resulting clause is a subset of
$B^{\prime\prime}\cup B^{\prime\prime\prime}$. The claim is proved because of
$F\models B\rightarrow B^{\prime\prime}$ and $F\models B\rightarrow
B^{\prime\prime\prime}$.

A specific value for $H$ strengthens the containment proved by the lemma.

###### Lemma 30

For every formula $F^{\prime}\subseteq SCL(B,F)\cup BCL(B,F)$, it holds
$HCLOSE(HEADS(B,F),F^{\prime})\subseteq BCL(B,F)$.

Proof. Since $F^{\prime}\subseteq SCL(B,F)\cup BCL(B,F)$, Lemma 29 proves
$HCLOSE(H,F^{\prime})\subseteq SCL(B,F)\cup BCL(B,F)$ for every set of
variables $H$. The claim is proved by showing that $H=HEADS(B,F)$ forbids
clauses of $SCL(B,F)$ in $HCLOSE(H,F^{\prime})$.

By contradiction, $B^{\prime}\rightarrow x$ is assumed to be a clause of
$SCL(B,F)$ that is also in $HCLOSE(HEADS(B,F),F^{\prime})$. The definition of
$HCLOSE(HEADS(B,F),F^{\prime})$ includes $x\in HEADS(B,F)$. Since
$HEADS(B,F)=RCN(B,F)\cap SFREE(B,F)$, it holds $x\in SFREE(B,F)$. This is
defined as the set of variables that are the head of no clause of $SCL(B,F)$,
contradicting the assumption $B^{\prime}\rightarrow x\in SCL(B,F)$.

A set contained in $SCL(B,F)\cup BCL(B,F)$ is $UCL(B,F)$, as proved by the
following lemma.

###### Lemma 31

For every formula $F$ and set of variables $B$, it holds
$UCL(B,F)=F\cap(SCL(B,F)\cup BCL(B,F))$.

Proof. The set $UCL(B,F)$ is defined as the set of clauses
$B^{\prime}\rightarrow x$ of $F$ such that $x\not\in B$ and $F\models
B\rightarrow B^{\prime}$. The entailment defines $B^{\prime}\leq_{F}B$, which
is the same as either $B^{\prime}<_{F}B$ or $B^{\prime}\equiv_{F}B$. Since
every clause of $F$ is entailed by $F$, every clause $B^{\prime}\rightarrow x$
of $UCL(B,F)$ satisfies $x\not\in B^{\prime}$, $F\models B^{\prime}\rightarrow
x$ and either $B^{\prime}<_{F}B$ or $B^{\prime}\equiv_{F}B$. Therefore, it is
either in $SCL(B,F)$ or in $BCL(B,F)$.

In the reverse direction, every clause of $SCL(B,F)$ and every clause of
$BCL(B,F)$ satisfies $x\not\in B^{\prime}$ and $F\models B\rightarrow
B^{\prime}$. This is the definition of $UCL(B,F)$ if the clause is also in
$F$.

Lemma 30 proves $HCLOSE(HEADS(B,F),F^{\prime})\subseteq BCL(B,F)$ for every
subset $F^{\prime}$ of $SCL(B,F)\cup BCL(B,F)$. The last lemma proves that
$UCL(B,F)$ is such a subset. Combining the two lemmas produce the following
corollary.

###### Corollary 3

For every formula $F$ and set of variables $B$, it holds
$HCLOSE(HEADS(B,F),UCL(B,F))\subseteq BCL(B,F)$.

This corollary proves that $HCLOSE(HEADS(B,F),UCL(B,F))$ is a subset of
$BCL(B,F)$ and being a subset of $BCL(B,F)$ is a part of the definition of
$ITERATION(B,F)$. The other parts are now proved to be met by
$HCLOSE(HEADS(B,F),UCL(B,F))$ as well.

This claim requires some preliminary lemmas. The first is the monotonicity of
$UCL(B,F)$ with respect to containment of the formula.

###### Lemma 32

If $F^{\prime}\subseteq F$ then $UCL(B,F^{\prime})\subseteq UCL(B,F)$.

Proof. The definition of $B^{\prime}\rightarrow x\in UCL(B,F^{\prime})$ is
$B^{\prime}\rightarrow x\in F^{\prime}$, $x\not\in B^{\prime}$ and
$F^{\prime}\models B\rightarrow B^{\prime}$. The first condition implies
$B^{\prime}\rightarrow x\in F$ because $F^{\prime}\subseteq F$. The third
implies $F\models B\rightarrow B^{\prime}$ by monotonicity of entailment. The
conditions in the definition of $B^{\prime}\rightarrow x\in UCL(B,F)$ all
hold.

This lemma allows proving that $UCL(B,F)$ is the part of $F$ that matters when
checking entailment from $B$.

###### Lemma 33

The following two conditions are equivalent: $F\models B\rightarrow x$ and
$UCL(B,F)\models B\rightarrow x$.

Proof. If $x\in B$ then $B\rightarrow x$ is a tautology. It is therefore
entailed by both $F$ and $UCL(B,F)$ and the claim is proved. The rest of the
proof covers the case $x\not\in B$.

If $UCL(B,F)$ implies $B\rightarrow x$ also $F$ does, since $UCL(B,F)$ is a
subset of $F$.

Remains to prove the converse. The assumption is $F\models B\rightarrow x$ and
the claim is $UCL(B,F)\models B\rightarrow x$.

This is proved by induction on the size of $F$.

The base case is $F=\emptyset$, where $F\models B\rightarrow x$ implies $x\in
B$, a case already proved to satisfy the claim.

The induction step proves that $F\models B\rightarrow x$ implies
$UCL(B,F)\models B\rightarrow x$ assuming the same implication for every
$F^{\prime}$ strictly smaller than $F$.

The claim is already proved when $x\in B$. Otherwise, $x\not\in B$ and
$F\models B\rightarrow x$ imply by Lemma 1 that $F$ contains a clause
$B^{\prime}\rightarrow x$ such that $F^{x}\models B\rightarrow B^{\prime}$. If
$x\in B^{\prime}$ then $B^{\prime}\rightarrow x$ is a tautology and is
therefore entailed by $UCL(B,F)$. Otherwise, $x\not\in B^{\prime}$. The
condition $B^{\prime}\rightarrow x\in F$ implies $F\models
B^{\prime}\rightarrow x$. The condition $F^{x}\models B\rightarrow B^{\prime}$
implies $F\models B\rightarrow B^{\prime}$. Otherwise, all conditions for
$B^{\prime}\rightarrow x$ being in $UCL(B,F)$ are met. Therefore, $UCL(B,F)$
entails $B^{\prime}\rightarrow x$.

By definition, $F^{x}\models B\rightarrow B^{\prime}$ is the same as
$F^{x}\models B\rightarrow b$ for every $b\in B^{\prime}$. Since $F^{x}$ is
smaller than $F$ because it does not contain $B^{\prime}\rightarrow x$ at
least, the induction assumption applies: $UCL(B,F^{x})\models B\rightarrow b$.
Since $F^{x}\subseteq F$, Lemma 32 tells that $UCL(B,F^{x})\subseteq
UCL(B,F)$. By monotonicy of entailment, $UCL(B,F)\models B\rightarrow b$
follows. This holds for every $b\in B^{\prime}$, implying $UCL(B,F)\models
B\rightarrow B^{\prime}$.

This conclusion $UCL(B,F)\models B\rightarrow B^{\prime}$ with the previous
one $UCL(B,F)\models B^{\prime}\rightarrow x$ implies $UCL(B,F)\models
B\rightarrow x$.

Since $F\models B\rightarrow x$ defines $x\in BCN(B,F)$ and $UCL(B,F)\models
B\rightarrow x$ defines $x\in BCN(B,UCL(B,F))$, an immediate consequence is
the equality of these two sets.

###### Lemma 34

For every formula $F$ and set of variables $B$ it holds
$BCN(B,F)=BCN(B,UCL(B,F))$.

Proof. By Lemma 33, $F\models B\rightarrow x$ is the same as $UCL(B,F)\models
B\rightarrow x$. The first condition defines $x\in BCN(B,F)$, the second $x\in
BCN(B,UCL(B,F))$.

Contrary to the other functions defined in this article, $UCL(B,F)$ only
contains clauses of $F$. A clause that is not in $F$ is never in $UCL(B,F)$
even if it is entailed by it. This set is the restriction of $F$ to the case
where $B$ is true. Only the clauses in $UCL(B,F)$ matter when deriving
something from $F\cup B$. They are the only clauses that matter to $BCN(B,F)$,
$RCN(B,F)$, $SCL(B,F)$ and $BCL(B,F)$. If $UCL(B,F)$ replaces $F$, these do
not change. More generally, if something is defined in terms of what $F$ and
$B$ entail, it is unaffected by the removal of all clauses not in $UCL(B,F)$
from $F$.

This claim requires a preliminary result: $UCL()$ is monotonic with respect to
entailment of the set of variables.

###### Lemma 35

If $F\models A\rightarrow B$ then $UCL(B,F)\subseteq UCL(A,F)$.

Proof. By definition, $B^{\prime}\rightarrow x\in UCL(B,F)$ is $x\not\in
B^{\prime}$, $F\models B\rightarrow B^{\prime}$ and $B^{\prime}\rightarrow
x\in F$. The second condition $F\models B\rightarrow B^{\prime}$ implies
$F\models A\rightarrow B^{\prime}$ since $F\models A\rightarrow B$ is assumed.
With $x\not\in B^{\prime}$ and $B^{\prime}\rightarrow x\in F$, this condition
defines $B^{\prime}\rightarrow x\in UCL(A,F)$.

Lemma 33 generalizes from clauses whose body is equal to the given set of
variables to clauses whose body is entailed by it.

###### Lemma 36

If $F\models A\rightarrow B$, then $F\models B\rightarrow x$ is equivalent to
$UCL(A,F)\models B\rightarrow x$.

Proof. A consequence of $UCL(A,F)\models B\rightarrow x$ is $F\models
B\rightarrow x$ since $UCL(A,F)$ is a subset of $F$. The first direction of
the claim is proved even if $F\models A\rightarrow B$ does not hold.

The other direction is that $F\models B\rightarrow x$ implies $UCL(A,F)\models
B\rightarrow x$ if $F\models A\rightarrow B$. By Lemma 33, the assumption
$F\models B\rightarrow x$ implies $UCL(B,F)\models B\rightarrow x$. This is
not the claim yet because it contains $UCL(B,F)$ instead of $UCL(A,F)$.
However, Lemma 35 proves $UCL(B,F)\subseteq UCL(A,F)$ from $F\models
A\rightarrow B$. Monotonicity implies $UCL(A,F)\models B\rightarrow x$.

This lemma proves that checking whether $F$ entails $B\rightarrow x$ where
$F\models A\rightarrow B$ can be safely restricted from $F$ to its subset
$UCL(A,F)$. This set is determined by the algorithm for $RCN(A,F)$ at almost
no additional cost, and may reduce the number of clauses to consider. This
reduction is dramatic on large formulae that contain only a small fraction of
clauses whose bodies are entailed by $A$.

This result applies to the search for bodies of $ITERATION(B,F)$.

###### Lemma 37

If $ITERATION(B,F)$ is a valid iteration function and $B^{\prime}\rightarrow
x\in ITERATION(B,F)$, then $HCLOSE(HEADS(B,F),UCL(B,F))$ contains a clause
$B^{\prime\prime}\rightarrow x$ with $B^{\prime\prime}\subseteq B^{\prime}$.

Proof. The definition of $B^{\prime}\rightarrow x\in ITERATION(B,F)$ includes
$F\models B^{\prime}\rightarrow x$ and $F\models B\equiv B^{\prime}$.
Equivalence implies entailment: $F\models B\rightarrow B^{\prime}$. Lemma 36
applies: $F\models B^{\prime}\rightarrow x$ implies $UCL(B,F)\models
B^{\prime}\rightarrow x$.

Lemma 19 proves $x\in HEADS(B,F)$.

By definition, $HCLOSE(HEADS(B,F),UCL(B,F))$ does not include a clause
$B^{\prime}\rightarrow x$ such that $UCL(B,F)\models B^{\prime}\rightarrow x$
and $x\in HEADS(B,F)$ only if $UCL(B,F)\models B^{\prime\prime}\rightarrow x$
with $B^{\prime\prime}\subset B^{\prime}$. Since the head of this clause is in
$HEADS(B,F)$, the same applies to it: it is not in
$HCLOSE(HEADS(B,F),UCL(B,F))$ if a proper subclause of it has the same
property. This inductively proves that a subclause
$B^{\prime\prime}\rightarrow x$ of $B^{\prime}\rightarrow x$ is in
$HCLOSE(HEADS(B,F),UCL(B,F))$.

Corollary 3 prove that searching for a valid $ITERATION(B,F)$ can be
restricted to the subsets of $HCLOSE(HEADS(B,F),UCL(B,F))$.

###### Lemma 38

If $ITERATION(B,F)$ is a valid iteration function then another valid iteration
function with the same heads in the same number of clauses is a subset of
$HCLOSE(HEADS(B,F),UCL(B,F))$.

Proof. Lemma 37 shows that $B^{\prime}\rightarrow x\in ITERATION(B,F)$ implies
$B^{\prime\prime}\rightarrow x\in HCLOSE(HEADS(B,F),UCL(B,F))$ for some
$B^{\prime\prime}\subseteq B^{\prime}$. This containment implies
$B^{\prime\prime}\rightarrow x\models B^{\prime}\rightarrow x$. As a result,
replacing $B^{\prime}\rightarrow x$ with $B^{\prime\prime}\rightarrow x$ in
$ITERATION(B,F)$ results in a formula entailing $ITERATION(B,F)$, and
therefore still entailing $BCL(B,F)$. This is the entailment part of the
definition of a valid iteration function.

This replacement also maintains the choice part. By Corollary 3,
$HCLOSE(HEADS(B,F),UCL(B,F))\subseteq BCL(B,F)$. This proves $x\not\in
B^{\prime}$, $F\models B^{\prime}\rightarrow x$ and $F\models B\equiv
B^{\prime}$. Remains to prove $x\in SFREE(B,F)$. It holds because the
definition of $B^{\prime}\rightarrow x\in HCLOSE(HEADS(B,F),UCL(B,F))$
includes $x\in HEADS(B,F)$, which includes $x\in SFREE(B,F)$, which implies
$B^{\prime}\rightarrow x\not\in SCL(B,F)$.

This replacement maintains the heads of the clauses because it replaces a
clause with another having the same head.

This lemma proves that searching for $ITERATION(B,F)$ can be restricted to the
subsets of $HCLOSE(HEADS(B,F),UCL(B,F))$. This avoids the inclusion of clauses
containing others; a further minimization is shown in the next section.

###  4.5 Implied by strictly implied subsets

Lemma 38 bounds the search for a valid iteration function to the subsets of
$HCLOSE(HEADS(B,F),UCL(B,F))$. Still, the number of such subsets may be
exponential. Lemma 19 further bounds the search: the heads of $ITERATION(B,F)$
are not just in $HEADS(B,F)$, they are exactly $HEADS(B,F)$. The subsets that
do not contain a head in $HEADS(B,F)$ can be skipped. So can the subsets that
contain duplicated heads, since the aim is to find a single-head formula. Yet,
these reductions do not always make the number of candidate subsets
polynomial. Every further restriction helps.

Some considerations on $HCLOSE(HEADS(B,F),UCL(B,F))$ provide a direction. It
constrains clauses to be entailed by $UCL(B,F)$, to have head in $HEADS(B,F)$
and a minimal body with respect to set containment. The first two are
necessary because of the definition of validity and because of Lemma 19, but
why minimality?

A non-minimal body is never necessary because $B^{\prime\prime}\rightarrow x$
entails $B^{\prime}\rightarrow x$ if $B^{\prime\prime}\subset B^{\prime}$.
Everything $B^{\prime}\rightarrow x$ entails is also entailed by
$B^{\prime\prime}\rightarrow x$. Both clauses are acceptable for being in
$ITERATION(B,F)$, they both consume the same head $x$, but
$B^{\prime\prime}\rightarrow x$ entails everything $B^{\prime}\rightarrow x$
entails. The latter can be disregarded since the former is a valid substitute
of it in every respect.

The goal is a set of clauses that entails $BCL(B,F)$ with $SCL(B,F)$. If
$B^{\prime\prime}\subset B^{\prime}$, then $SCL(B,F)\cup
IT\cup\\{B^{\prime\prime}\rightarrow x\\}$ implies $SCL(B,F)\cup
IT\cup\\{B^{\prime}\rightarrow x\\}$. What really matters is this implication.
When it holds, $BCL(B,F)$ is entailed by the implicant if it is entailed by
the implicate. The implication is a consequence of set containment, but is not
equivalent to it. It may hold even if set containment does not.

The implication involves the set $IT$, but is used to restrict the possible
clauses to include in $IT$, when $IT$ is not fixed yet. What can be checked
then is whether $SCL(B,F)\cup\\{B^{\prime\prime}\rightarrow x\\}$ implies
$SCL(B,F)\cup\\{B^{\prime}\rightarrow x\\}$. This is the same as
$SCL(B,F)\cup\\{B^{\prime\prime}\rightarrow x\\}\models B^{\prime}\rightarrow
x$, which holds if $SCL(B,F)\cup B^{\prime}\models B^{\prime\prime}$. A body
$B^{\prime}$ can be replaced by another $B^{\prime\prime}$ it entails with
$SCL(B,F)$.

###### Lemma 39

If $ITERATION(B,F)$ is a valid iteration function, $B^{\prime}\rightarrow x\in
ITERATION(B,F)$, $B^{\prime\prime}\rightarrow x\in BCL(B,F)$ and $SCL(B,F)\cup
B^{\prime}\models B^{\prime\prime}$ hold, another valid iteration function is
$ITERATION^{\prime}(B,F)=ITERATION(B,F){}\backslash\\{B^{\prime}\rightarrow
x\\}\cup\\{B^{\prime\prime}\rightarrow x\\}$.

Proof. All clauses in $ITERATION^{\prime}(B,F)$ but
$B^{\prime\prime}\rightarrow x$ are in $ITERATION(B,F)$. They satisfy the
condition of choice of the definition of validity, which is now proved for
$B^{\prime\prime}\rightarrow x$. The assumption $B^{\prime\prime}\rightarrow
x\in BCL(B,F)$ implies $F\models B^{\prime\prime}\rightarrow x$ and $F\models
B\equiv B^{\prime\prime}$. The condition $x\in SFREE(B,F)$ follows from
$B^{\prime}\rightarrow x\in ITERATION(B,F)$. This proves the condition of
choice.

Remains to prove the entailment condition: $SCL(B,F)\cup
ITERATION^{\prime}(B,F)\models BLC(B,F)$. By assumption, $SCL(B,F)\cup
B^{\prime}\models B^{\prime\prime}$. As a result, $SCL(B,F)\cup
ITERATION^{\prime}(B,F)\cup B^{\prime}$, being equal to $SCL(B,F)\cup
ITERATION(B,F){}\backslash\\{B^{\prime}\rightarrow
x\\}{}\cup\\{B^{\prime\prime}\rightarrow x\\}{}\cup B^{\prime}$, entails
$SCL(B,F)\cup ITERATION(B,F){}\backslash\\{B^{\prime}\rightarrow
x\\}{}\cup\\{B^{\prime\prime}\rightarrow x\\}{}\cup B^{\prime\prime}$, which
entails $x$. By the deduction theorem, $SCL(B,F)\cup
ITERATION^{\prime}(B,F)\models B^{\prime}\rightarrow x$. Since $SCL(B,F)\cup
ITERATION^{\prime}(B,F)$ implies the only clause of $ITERATION(B,F)$ it does
not contain, it implies it all: $SCL(B,F)\cup ITERATION^{\prime}(B,F)\models
SCL(B,F)\cup ITERATION(B,F)$. Since $ITERATION(B,F)$ is a valid iteration
function, it satisfies $SCL(B,F)\cup ITERATION(B,F)\models BCL(B,F)$. By
transitivity, $SCL(B,F)\cup ITERATION^{\prime}(B,F)\models BCL(B,F)$.

If $B^{\prime}\rightarrow x$ and $B^{\prime\prime}\rightarrow x$ are both in
$HCLOSE(HEADS(B,F),UCL(B,F))$, the first can be disregarded if $SCL(B,F)\cup
B^{\prime}\models B^{\prime\prime}$. This reduces the set of candidates
subsets of $HCLOSE(HEADS(B,F),UCL(B,F))$.

This is similar to what Lemma 38 allows when $B^{\prime\prime}\subset
B^{\prime}$, but with an important difference: the reverse containment
$B^{\prime}\subset B^{\prime\prime}$ is not possible, the reverse implication
from $B^{\prime\prime}$ to $B^{\prime}$ is. If $SCL(B,F)\models
B^{\prime}\equiv B^{\prime\prime}$, Lemma 39 allows
$B^{\prime\prime}\rightarrow x$ to replace $B^{\prime}\rightarrow x$ but also
the other way around. Such an equivalence is not possible under set
containment: $B^{\prime}\subset B^{\prime\prime}$ contradicts
$B^{\prime\prime}\subset B^{\prime}$. If a body is minimal according to set
containment, no other body can take its place; a body that is minimal
according to implication can be replaced by an equivalent one. While uniquely
defining $HCLOSE(H,F)$ is possible, extending it to minimality by entailment
is not. Not uniquely. This is why the following definition only gives a
condition of minimality rather than uniquely defining a set like
$HCLOSE(H,F)$.

###### Definition 7

$MINBODIES(U,S)$ is an arbitrary function that returns a subset $R$ of $U$
such that $B^{\prime}\rightarrow x\in U$ implies $S\cup B^{\prime}\models
B^{\prime\prime}$ for some clause $B^{\prime\prime}\rightarrow x\in R$.

The function $minbodies(U,S)$ in singlehead.py meets this definition. It works
on whole clauses $B^{\prime}\rightarrow x$ and $B^{\prime\prime}\rightarrow x$
instead of their bodies $B^{\prime}$ and $B^{\prime\prime}$ only. It starts
from a clause of $U$ and repeatedly checks whether its body and $S$ entail the
body of another clause of $U$ with the same head. The trace of clauses in this
and in all runs avoid loops and repeated search.

The function is called with $U=HCLOSE(HEADS(B,F),UCL(B,F))$ and
$S=UCL(B,F)\cap SCL(B,F)$. The resulting subset of
$HCLOSE(HEADS(B,F),UCL(B,F))$ may still include some clauses that could be
removed for two reasons.

How inference is checked.

Lemma 39 allows neglecting a clause if its body and $SCL(B,F)$ entails another
body. But the function $minbodies(U,S)$ in singlehead.py does not check
$SCL(B,F)\cup B^{\prime}\models B^{\prime\prime}$ for every set
$B^{\prime\prime}$. For simplicity, it only checks whether a single variable
in $B^{\prime}$ resolves with a single clause of $UCL(B,F)\cap SCL(B,F)$ to
produce $B^{\prime\prime}$.

Using resolution instead of entailment is not a limitation because the only
difference is that resolution may produce a subclause of an entailed clause.
This difference disappears since $B^{\prime}\rightarrow x$ is subset-minimal:
none of its subsets are entailed.

Whether resolving a variable in $B^{\prime}$ with a clause in $UCL(B,F)\cap
SCL(B,F)$ once is sufficient is another story. A preliminary analysis suggests
that this is not a limitation, and a resolution derivation of
$B^{\prime\prime}$ from $SCL(B,F)\cup B^{\prime}$ can always be restructured
so that the last step is always the resolution of a body of
$HCLOSE(HEADS(B,F),UCL(B,F))$ with a clause of $UCL(B,F)\cap SCL(B,F)$. This
would prove by iteration that such a derivation is a sequence of steps like
the ones the program follows. Yet, this is unproven.

How minimal elements are searched for.

The function $minbodies(U,S)$ in singlehead.py follows implications among
bodies, avoiding the ones it already visited. The following example
(minbodies.py) shows that it may return a non-minimal body this way.

$F=\\{bh\rightarrow c,ch\rightarrow b,ch\rightarrow d,x\rightarrow
h,bde\rightarrow x\\}$

The first four clauses make $UCL(B,F)\cap SCL(B,F)$ when $B=\\{b,d,e\\}$. They
imply $bhe\rightarrow che$, $che\rightarrow bhe$ and $che\rightarrow cde$.
These three bodies $bhe$, $che$ and $cde$ are equivalent according to $F$, but
$cde$ is only entailed by the other two according to $UCL(B,F)\cap SCL(B,F)$.

$che$$bhe$$cde$

The only necessary clause is $cde\rightarrow x$, since its body $cde$ is
implied by the other two $che$ and $bhe$ but not the other way around. Yet,
minbodies(U, S) may also produce $bhe\rightarrow x$.

If searching starts from $che$, it moves to $bhe$ and stops there because the
only other body it directly entails it is $che$, which it skips as already
analyzed. The clause $bhe\rightarrow x$ is therefore produced even if its body
entails $cde$ and not the other way around.

The problem is still due to single resolutions in place of inference, but not
only. The only necessary body $cde$ could be found from $bhe$ even using a
single resolution at time by not avoiding the bodies already visited like
$che$. This is not done for its computational costs.

These issues may make the function return some clauses that are not minimal.
This only affects the running time of the algorithm, not its correctness. It
increases the number of candidates for $ITERATION(B,F)$ and ultimately the
overall running time, but since all necessary clauses are included the result
is correct anyway.

###  4.6 The algorithm, at last

The overall algorithm for checking whether a formula is single-head equivalent
assembles the pieces built so far. It is the reconstruction algorithm
(Algorithm 3) where $ITERATION(B,F)$ is not given but calculated employing
$HEADS()$, $HCLOSE()$ and $MINBODIES()$.

The reconstruction algorithm iterates over the bodies of the clauses in the
formula, sorted by entailment. It starts from the bodies that entail no other
and continues to the ones entailing only the ones already processed. For every
body $B$, it calculates $ITERATION(B,F)$ and adds it to the formula under
construction $G$. The only missing bit of this algorithm is $ITERATION(B,F)$.
It is found by iterating over the sets of clauses it may contain until a set
that entails $BCL(B,F)$ with $SCL(B,F)$ is found.

######  Algorithm 4 (Singlehead-autoreconstruction algorithm)

  1. 1.

$F=\\{B\rightarrow x\in F\mid x\not\in B\\}$

  2. 2.

$G=\emptyset$

  3. 3.

$P=\\{B\mid\exists x.B\rightarrow x\in F\\}$

  4. 4.

while $P\not=\emptyset$

    1. (a)

choose a $<_{F}$-minimal $B\in P$
(a set such that $A<_{F}B$ does not hold for any $A\in P$)

    2. (b)

$H=HEADS(B,F)$

    3. (c)

$M=HCLOSE(H,UCL(B,F))$

    4. (d)

$T=MINBODIES(M,UCL(B,F)\cap SCL(B,F))$

    5. (e)

$E={\sf false}$

    6. (f)

for all $IT=\\{C_{1}\rightarrow h_{1},\ldots,C_{m}\rightarrow h_{m}\mid
H=\\{h_{1},\ldots,h_{m}\\},~{}\forall i~{}.~{}h_{i}\not\in C_{i},~{}\exists
y_{1},\ldots,y_{m}~{}.~{}C_{1}\rightarrow y_{1},\ldots,C_{m}\rightarrow
y_{m}\in T\\}$

      1. i.

if $SCL(B,F)\cup IT\models BCL(B,F)$

        1. A.

$E={\sf true}$

        2. B.

break

    7. (g)

if $\neg E$

      1. i.

fail

    8. (h)

$G=G\cup IT$

    9. (i)

$P=P\backslash\\{B^{\prime}\mid F\models B\equiv B^{\prime}\\}$

  5. 5.

return $G$

The overall structure is the same as the reconstruction algorithm (Algorithm
2): a single-head formula $G$ aims at replicating $F$ by accumulating
$ITERATION(B,F)$ during a loop over the bodies $B$ of $F$ sorted by
$\leq_{F}$. The difference is that $ITERATION(B,F)$ is not given but found by
iterating over sets of clauses $IT$.

This search is the main contributor to complexity in the algorithm, since
exponentially many such sets may exists. This is why a number of hacks for
efficiency are implemented:

  * •

instead of checking all subsets of $BCL(B,F)$, only the subsets of
$HCLOSE(HEADS(B,F),UCL(B,F))$ are considered;

  * •

this set is further reduced by $MINBODIES()$;

  * •

rather than looping over sets of clauses, each variable in $HEADS(B,F)$ is
attached a body coming from $MINBODIES()$; this is correct because all these
bodies are equivalent; it is convenient because it automatically excludes all
sets of clauses with missing or duplicated heads;

  * •

$RCN(B,F)$ and $UCL(B,F)$ are determined and stored for all bodies of $F$ once
at the beginning.

The algorithm is further improved by other optimizations described in separate
sections because of the length of their proofs. The rest of this section is
about the correctness of Algorithm 4 itself.

###### Lemma 40

All non-tautological clauses with head in $HEADS(B,F)$ and body in
$HCLOSE(HEADS(B,F),UCL(B,F))$ are in $BCL(B,F)$.