Proof. The premise of the lemma is that $B^{\prime}\rightarrow x$ is a clause
such that $x\not\in B^{\prime}$, $x\in HEADS(B,F)$ and $B^{\prime}\rightarrow
y\in HCLOSE(HEADS(B,F),UCL(B,F))$ for some variable $y$.

Corollary 3 proves that every clause of $HCLOSE(HEADS(B,F),UCL(B,F))$ is in
$BCL(B,F)$. The definition of $B^{\prime}\rightarrow y\in BCL(B,F)$ includes
$B^{\prime}\equiv_{F}B$, which is also part of the definition of
$B^{\prime}\rightarrow x\in BCL(B,F)$. Another part is $x\not\in B^{\prime}$,
which holds because $B^{\prime}\rightarrow x$ is by assumption not a
tautology.

The only missing part is $F\models B^{\prime}\rightarrow x$. The definition of
$x\in HEADS(B,F)$ includes $x\in RCN(B,F)$, which implies $x\in BCN(B,F)$ by
Lemma 2: $F\models B\rightarrow x$. Since the previously proved fact
$B^{\prime}\equiv_{F}B$ is defined as $F\models B^{\prime}\equiv B$, this
entailment is the same as $F\models B^{\prime}\rightarrow x$, the missing part
of the definition of $B^{\prime}\rightarrow x\in BCL(B,F)$.

Since $IT$ comprises only clauses meeting the condition of the previous lemma,
they satisfy its consequence.

###### Lemma 41

All sets $IT$ in the autoreconstruction algorithm (Algorithm 4) are contained
in $BCL(B,F)$.

Proof. By construction, $IT$ is made of non-tautological clauses with heads in
$HEADS(B,F)$ and bodies in $MINBODIES(HCLOSE(HEADS(B,F),UCL(B,F)),UCL(B,F)\cap
SCL(B,F))$. The latter is a subset of its first argument
$HCLOSE(HEADS(B,F),UCL(B,F))$ by definition. Therefore, all clauses of $IT$
have heads in $HEADS(B,F)$ and bodies in $HCLOSE(HEADS(B,F),UCL(B,F))$ and are
not tautologies. Lemma 40 prove that they are in $BCL(B,F)$.

Since all sets $IT$ are subsets of $BCL(B,F)$, its clauses meet most of the
choice part of the definition of a valid iteration function: $x\not\in
B^{\prime}$, $F\models B^{\prime}\rightarrow x$ and $F\models B\equiv
B^{\prime}$. They also meet the remaining one, $x\in SFREE(B,F)$, since $x\in
HEADS(B,F)$.

The entailment part of the definition of validity is not meet in general, but
only if the iteration of the external loop ends.

###### Lemma 42

At the end of every iteration of the external loop (Step 4) of the
autoreconstruction algorithm (Algorithm 4), $IT$ satisfies the conditions for
a valid iteration function $ITERATION(B,F)$.

Proof. Lemma 41 proves that $IT$ only contains clauses of $BCL(B,F)$. By
construction, the heads of $IT$ are in $HEADS(B,F)$, a subset of $SFREE(B,F)$.
The choice condition for $IT$ being a valid iteration function is met.

The entailment condition is $SCL(B,F)\cup IT\models BCL(B,F)$. This may or may
not happen for a specific set $IT$. However, if no set $IT$ satisfies
$SCL(B,F)\cup IT\models BCL(B,F)$ in the internal loop, the algorithm fails.
Therefore, the entailment condition for $IT$ holds if the iteration of the
external loop ends.

While $IT$ is a valid iteration function if the algorithm does not fail, the
same could be achieved by making the algorithm fail for all sets $IT$. It is
also essential that the algorithm does not fail if a valid iteration function
exists.

###### Lemma 43

If $F$ has a valid iteration function such that $ITERATION(B,F)$ is single-
head, then $IT$ is equal to the value of a valid iteration function
$ITERATION(B,F)$ at some iteration of the internal loop (Step 4f) of the
autoreconstruction algorithm (Algorithm 4).

Proof. Lemma 38 proves that if $F$ has a valid iteration function it also has
one such that $ITERATION(B,F)$ is a subset of $HCLOSE(HEADS(B,F),UCL(B,F))$
and has the same heads in the same number of clauses. Lemma 39 further
restricts this property to the subsets of
$MINBODIES(HCLOSE(HEADS(B,F),UCL(B,F)),UCL(B,F)\cap SCL(B,F))$. Since this is
a valid iteration function, its heads are $HEADS(B,F)$ by Lemma 19.

This proves that if $F$ has a valid iteration function such that
$ITERATION(B,F)$ is single-head, also has one such that $ITERATION(B,F)$ have
bodies from $MINBODIES(HCLOSE(HEADS(B,F),UCL(B,F)),UCL(B,F)\cap SCL(B,F))$ and
single-head heads in $HEADS(B,F)$. This other one is still a valid iteration
function; therefore, it contains no tautology. Since the internal loop (Step
4f) of the algorithm tries all tautology-free associations of these heads with
these bodies, it finds it.

The following lemma has an awkward statement but is necessary to avoid
repeating the same argument in multiple proofs.

###### Lemma 44

If the autoreconstruction algorithm (Algorithm 4) terminates, the sequence of
values of $G$ is the same as in the reconstruction algorithm (Algorithm 1) for
some nondeterministic choices and the following valid iteration function.

$ITERATION(B,F)=\left\\{\begin{array}[]{ll}IT&\mbox{at the end of the
iteration of $B^{\prime}$}\\\ &\mbox{if $B$ is equivalent to a body
$B^{\prime}$ in $F$}\\\ \emptyset&\mbox{otherwise}\end{array}\right.$

Proof. The iteration function is valid: Lemma 42 proves the conditions of
validity when $B$ is a body in $F$, and these conditions carry over to
equivalent sets because they are semantical; Lemma 14 applied in reverse
proves that the value of every valid iteration function $ITERATION(B,F)$ is
empty if $B$ is not equivalent to a body in $F$.

The allowed choices for the precondition $B$ in Algorithm 4 are the same as in
Algorithm 2. Lemma 42 proves that $IT$ is the value of some valid iteration
function $ITERATION(B,F)$ at the end of every iteration of Algorithm 4. Since
$G$ is initially empty and is added respectively $IT$ or $ITERATION(B,F)$ at
every step, the values of $G$ are the same in the two algorithms.

Lemma 15 proves that Algorithm 1 can always choose a set $B$ such that
$ITERATION(B,F)=\emptyset$ if $P$ does not contain a $<_{F}$-minimal body of
$F$. Therefore, Algorithm 1 can always choose a set $B$ so that it does not
change $G$ when it cannot choose a set $B$ like Algorithm 2 does. The sequence
of values of $G$ is the same because the choices of the first kind do not
change it and the choices of the second kind change it in the same way.

The correctness of the algorithm can now be proved.

###### Theorem 1

The autoreconstruction algorithm (Algorithm 4), returns a single-head formula
equivalent to the input formula if and only if the input formula has any.

Proof. The proof comprises three steps: first, if $F$ is single-head
equivalent, the algorithm does not fail; second, the output formula (if any)
is equivalent to $F$; third, if $F$ is single-head equivalent the output
formula is single-head. These three facts imply that the algorithm outputs a
single-head version of $F$ if any. The second implies that if $F$ is not
single-head equivalent the output formula is not single-head, if the algorithm
does not fail.

The first step is that the algorithm does not fail if $F$ is single-head
equivalent. If $F$ is single-head equivalent, it has a valid iteration
function whose values are all single-head by Lemma 6. This is the precondition
of Lemma 43, which proves that $IT$ holds the value of a valid iteration
function at some iteration of the internal loop of the algorithm. The
definition of validity includes $SCL(B,F)\cup IT\models BCL(B,F)$. This
entailment makes $E$ true, avoiding failure.

The second step is that the output formula is equivalent to the input formula.
Lemma 44 proves that the values of $G$ in the algorithm are the same as the
values in Algorithm 1 for a valid iteration function and some nondeterministic
choices. This includes the last value, which is returned. Algorithm 1 returns
a formula equivalent to $F$ by Lemma 11.

The third step is that the output formula (if any) is single-head if the input
formula is single-head equivalent. The algorithm has been proved to terminate
two paragraphs above; this is the precondition of Lemma 44, which proves the
validity of a certain iteration function. Its possible values are $\emptyset$
and the value of $IT$ at the end of some iteration of the algorithm. Both are
single-head: $\emptyset$ because it contains no clause, $IT$ by construction.
Since the output formula is the same as that of Algorithm 1 with this
iteration function by Lemma 44, and this iteration function has only single-
head values, Lemma 13 applies: the output is single-head since $F$ is by
assumption equivalent to a single-head formula.

If the formula $F$ is single-head equivalent the algorithm terminates and
outputs a single-head formula equivalent to it. Otherwise, the algorithm does
not output a single-head formula; it may output a formula that is not single-
head or nothing at all because it fails.

###  4.7 Tautologies

The autoreconstruction algorithm (Algorithm 4) exploits $RCN(B,F)$ and
$UCL(B,F)$. A previous article shows an algorithm rcnucl() for calculating
$RCN(B,F)$ and $\\{B^{\prime}\rightarrow x\in F\mid F\models B\rightarrow
B^{\prime}\\}$. The second is almost $UCL(B,F)$ but does not exclude
tautologies. Since $F$ is removed all tautologies in the first step of the
autoreconstruction algorithm, this missing condition is moot as implied by
$B^{\prime}\rightarrow x\in F$.

Some optimizations below exploit $UCL(B,G\cup IT)$. The rcnucl() algorithm
determines it if $G\cup IT$ does not contain tautologies, which is proved by
the following lemma.

###### Lemma 45

The set $G\cup IT$ does not contain tautologies during the execution of the
autoreconstruction algorithm (Algorithm 4).

Proof. The sets assigned to $IT$ do not contain tautology because their
definition includes $h_{i}\not\in C_{i}$. Since $G$ is initially empty, is
only changed by the instruction $G=G\cup IT$ and $IT$ does not contain
tautology, it does not either.

###  4.8 Wild-goose chase

The algorithm requires $SCL(B,F)$ and $BCL(B,F)$. Being sets of consequences
of $F$, they may be exponentially large. Their direct use is best avoided. The
implementation of the algorithm in singlehead.py exploits three variants to
this aim:

  1. 1.

in place of $HEADS(B,F)$, whose definition involves the set of heads of
$SCL(B,F)$, it uses the difference between $RCN(B,F)$ and the heads of $G$,
the formula under construction;

  2. 2.

in place of $UCL(B,F)\cap SCL(B,F)$ it uses $UCL(B,F)\cap U$ where $U$ is the
union of $UCL(B,F)$ for all bodies $B$ of $F$ used in the previous iterations
of the algorithm;

  3. 3.

$SCL(B,F)\cup IT\models BCL(B,F)$ is checked as $HCLOSE(RCN(B,G\cup
IT),UCL(B,G\cup IT))=HCLOSE(RCN(B,F),UCL(B,F))$.

In all three optimizations $G$ takes the place of $SCL(B,F)$. This is correct
as long as the algorithm mimics the reconstruction algorithm with a valid
iteration function.

###### Lemma 46

At every iteration of the autoreconstruction algorithm (Algorithm 4),
$G\models SCL(B,F)$.

Proof. By Lemma 44, the values of $G$ in the autoreconstruction algorithm are
the same as in Algorithm 1 for some nondeterministic choices and a valid
iteration function. Lemma 10 proves $G\models SCL(B,F)$.

The algorithm works by iteratively rebuilding the formula from the ground
up—from a body $A$ that do not entail any other to a body $B$ that only
entails $A$ and so on. Each floor is built over the lower ones. If they are
not, it cannot. They have to be finished and solid. In logical terms,
processing $B$ requires $A$ to have already been processed, and its
consequences already being entailed.

The first lemma states that the order of processing of bodies is correct.

###### Lemma 47

If $B$ is chosen in a given iteration of the autoreconstruction algorithm
(Algorithm 4) and $A^{\prime}$ is the body of a clause in $F$ such that
$A^{\prime}<_{F}B$, then a set $A$ such that $A\equiv_{F}A^{\prime}$ was
chosen in a previous iteration.

Proof. The algorithm only chooses sets of variables that are minimal in $P$.
This means that when $B$ is chosen, the set $A^{\prime}$ is not in $P$. Since
$A^{\prime}$ is the body of a clause in $F$, it was initially in $P$. As a
result, $A^{\prime}$ has been removed in a previous iteration. Let $A$ be the
set of variables chosen in that iteration. Since $P$ is only removed elements
by the statement $P=P\backslash\\{B^{\prime}\mid B\cup F\models B\equiv
B^{\prime}\\}$, it holds $F\models A\equiv A^{\prime}$, which is the same as
$A\equiv_{F}A^{\prime}$.

If the algorithm is erecting a building, it needs all floors below $B$ before
building $B$. Floor $B$ is not made in mid-air, it is made over them. The next
lemma proves the converse: no floor that should be over $B$ is built before
it.

###### Lemma 48

If $A$ is chosen in an iteration of the autoreconstruction algorithm
(Algorithm 4) that precedes the iteration in which $B$ is chosen, then
$B\not\leq_{F}A$.

Proof. Since $B$ is chosen after $A$, it is in $P$ when $A$ is chosen and at
the end of that iteration. Since the algorithm only chooses minimal elements
of $P$, it does not choose $A$ if $B<_{F}A$. Since $B$ is still in $P$ at the
end of the iteration, after $P=P\backslash\\{B^{\prime}\mid F\models B\equiv
B^{\prime}\\}$, then $A\equiv_{F}B$ does not hold either. Since $B$ is not
strictly less than $A$ and not equivalent to it, it is not less than or equal
to it: $B\not\leq_{F}A$.

Adding $IT$ to $G$ makes $G$ entail every clause in $BCL(B,F)$ at the end of
each iteration. As expected and wanted. What would be neither expected nor
wanted is going overboard and adding clauses that are not in $BCL(B,F)$, or
even worse not entailed by $F$. After all, the final aim is to reconstruct $F$
in a controlled way. Controlled means single-head, but equivalence with $F$ is
essential: not producing anything not entailed by $F$.

This unwanted situation is first excluded for $G$.

###### Lemma 49

At every iteration of the autoreconstruction algorithm (Algorithm 4) $G$ is a
subset of $\cup\\{BCL(A,F)\mid B\not\leq_{F}A\\}$.

Proof. Let $A^{\prime}\rightarrow x$ a clause of $G$. The set $G$ is initially
empty, and it is only changed by $G=G\cup IT$ at the end of every iteration of
the external loop. Therefore, $A^{\prime}\rightarrow x$ is in $IT$ at the end
of an iteration. Let $A$ be the element of $P$ chosen in Step 4a at the
beginning of that iteration. Lemma 48 proves $B\not\leq_{F}A$. Lemma 41 proves
$IT\subseteq BCL(A,F)$.

Since $G$ is not too large and $IT$ is built appropriately as shown by Lemma
41, their union $G\cup IT$ is also correct.

###### Lemma 50

At every iteration of the algorithm, $F\models G\cup IT$ holds.

Proof. Lemma 41 proves that $IT$ is a subset of $BCL(B,F)$, which is a set of
consequences of $F$. Lemma 49 proves that $G$ is contained in the union of
some sets $BCL(A,F)$, which again only contain consequences of $F$. As a
result, all clauses of $G\cup IT$ are entailed by $F$.

###  4.9 Head back

The autoreconstruction algorithm uses $HEADS(B,F)=RCN(B,F)\cap SFREE(B,F)$ as
the heads of the clauses of $IT$. Since $SFREE(B,F)$ is defined in terms of
$SCL(B,F)$, which is a set of consequences of $F$, it is expensive to
determine. The implemented algorithm replaces it with $RCN(B,F)$ minus the
heads of the clauses in $G$.

This is not always correct. Formula $F=\\{a\rightarrow x,b\rightarrow x\\}$ is
a counterexample. The set $B$ chosen in the first iteration may be $\\{a\\}$,
and the algorithm sets $G=\\{a\rightarrow x\\}$. The second set $B$ is then
$\\{b\\}$. By definition, $SFREE(B,F)$ is the set of all variables that are
not heads of $SCL(B,F)$, the clauses entailed by $F$ whose body are less than
$B$; the only variable $B=\\{b\\}$ entails is $x$, and no clause in $F$
contains $x$ negative; therefore, $SCL(B,F)=\emptyset$ and
$SFREE(B,F)=\\{a,b,x\\}$. While $HEADS(B,F)=RCN(B,F)\cap
SFREE(B,F)=\\{x\\}\cap\\{a,b,x\\}=\\{x\\}$, the heads of $IT$ in the
implemented algorithm are $RCN(B,F)\backslash\\{x\mid\exists B.B\rightarrow
x\in G\\}={}\emptyset$.

Granted, the counterexample formula is not single-head equivalent. And not by
chance: the actual and computed heads only differ on formulae that are not
single-head equivalent. Rather than insisting on the correct set of heads,
efforts are better spent on proving that the final outcome of each iteration
is correct: even when the algorithm uses the wrong sets of heads, it still
disproves the formula single-head equivalent. This is exactly what happens for
the counterexample formula: the set of heads for $IT$ is empty while
$BCL(B,F)$ contains $b\rightarrow x$. The iteration ends in failure, as
required. This holds in general, not just in the counterexample.

The first step in this direction is that the heads of $RCN(B,F)$ minus the
heads of $G$ are all in $HEADS(B,F)$.

###### Lemma 51

During the execution of the reconstruction algorithm (Algorithm 4)
$H=RCN(B,F)\backslash\\{x\mid\exists B^{\prime}.B^{\prime}\rightarrow x\in
G\\}$ is a subset of $HEADS(B,F)$.

Proof. The claim is proved by showing that every variable not in $HEADS(B,F)$
is not in $H$ either.

If $x$ is not in $HEADS(B,F)$ then it is either not in $RCN(B,F)$ or not in
$SFREE(B,F)$. In the first case, $x$ is not in $H$ because $H$ is a subset of
$RCN(B,F)$. In the second case, $x$ is proved not to be in $H$ by showing that
it is the head of a clause of $G$.

The definition of $x\in SFREE(B,F)$ is that a clause $A^{\prime}\rightarrow x$
is in $SCL(B,F)$. Being in $SCL(B,F)$ it is not a tautology: $x\not\in
A^{\prime}$. By Lemma 46, $G$ entails all of $SCL(B,F)$, including
$A^{\prime}\rightarrow x$. This entailment and $x\not\in A^{\prime}$ are the
preconditions of Lemma 1, which tells that $G$ contains a clause
$A^{\prime\prime}\rightarrow x$. Since $x$ is the head of a clause of $G$, it
is not in $H$.

This lemma proves that $H$ is a subset of $HEADS(B,F)$. An expected
consequence is that the sets $IT$ built over $H$ are also sets that can be
built over $HEADS(B,F)$. This is however not the case because $MINBODIES(U,S)$
is not necessarily monotonic with respect to its first argument. Yet, the
change would preserve the property proved by Lemma 50: $F$ entails these sets.

###### Lemma 52

At every step of the autoreconstruction algorithm (Algorithm 4), $F$ implies
every clause with head in $H=RCN(B,F)\backslash\\{x\mid\exists
B^{\prime}.B^{\prime}\rightarrow x\in G\\}$ and body in
$MINBODIES(HCLOSE(H,UCL(B,F)),UCL(B,F)\cap SCL(B,F))$.

Proof. By Lemma 51, $H$ is a subset of $HEADS(B,F)$. By definition,
$MINBODIES(HCLOSE(H,UCL(B,F)),UCL(B,F)\cap SCL(B,F))$ is a subset of its first
argument $HCLOSE(H,UCL(B,F))$. The definition of this set includes $H$ only as
$x\in H\backslash B$, which implies $x\in HEADS(B,F)\backslash B$ since
$H\subseteq HEADS(B,F)$: every clause of $HCLOSE(H,UCL(B,F))$ is in
$HCLOSE(HEADS(B,F),UCL(B,F))$. This implies that
$MINBODIES(HCLOSE(H,UCL(B,F)),UCL(B,F)\cap SCL(B,F))$ is a subset of
$HCLOSE(HEADS(B,F),UCL(B,F))$. Lemma 40 proves that all non-tautological
clauses with heads in $HEADS(B,F)$ and bodies in $HCLOSE(HEADS(B,F),UCL(B,F))$
are contained in $BLC(B,F)$ and are therefore entailed by $F$; the
tautological ones are entailed because they are tautologies.

These two lemmas allow proving the main property of this section: $RCN(B,F)$
minus the heads of $G$ is a correct replacement of $HEADS(B,F)$ in the
autoreconstruction algorithm. More precisely, if they are not the same the
autoreconstruction algorithm gives the correct answer anyway.

###### Lemma 53

If $H=RCN(B,F)\backslash\\{x\mid\exists B^{\prime}.B^{\prime}\rightarrow x\in
G\\}$ is not equal to $HEADS(B,F)$, the formula $F$ is not single-head
equivalent and the autoreconstruction algorithm (Algorithm 4) running with
this modified definition of $H$ fails.

Proof. The modified and the original algorithms are identical as long as
$H=RCN(B,F)\backslash\\{x\mid\exists B^{\prime}.B^{\prime}\rightarrow x\in
G\\}$ and $HEADS(B,F)$ coincide. Up to the first moment these sets differ, the
two algorithms are the same. Therefore, they possess the same properties. For
example, $F\models G$ as proved in Lemma 50. At the first iteration where $H$
and $HEADS(B,F)$ differ, the modified algorithm is proved to fail, but this is
correct because the formula is not single-head equivalent. The rest of the
proof is about this first iteration where $H$ and $HEADS(B,F)$ differ.

The starting point is $H\subseteq HCLOSE(H,F)$ as proved by Lemma 51. The
proof comprises four steps that follow from the assumption that $H$ and
$HEADS(B,F)$ differ:

  1. 1.

some variables $x$ of $HEADS(B,F)$ are the head of some clauses of $G$

  2. 2.

if $x$ is a variable of $HEADS(B,F)$ but not of $H$, and
$A^{\prime}\rightarrow x\in G$ for some $A^{\prime}$ then both $F\not\models
A^{\prime}\rightarrow B$ and $F\not\models B\rightarrow A^{\prime}$ hold;

  3. 3.

the algorithm fails;

  4. 4.

$F$ is not equivalent to any single-head formula.

The first step proves that if $HEADS(B,F)$ and $H$ differ then some variables
of $HEADS(B,F)$ are the head of some clauses of $G$.

Since $H$ is subset of $HEADS(B,F)$, these two sets can only differ if
$HEADS(B,F)$ contains a variable not in $H$. Being in $HEADS(B,F)$, such a
variable is in $RCN(B,F)$. Since it is not $H$, which is $RCN(B,F)$ minus the
heads of $G$, it is the head of a clause of $G$.

The second step proves that if $x$ is a variable of $HEADS(B,F)\backslash H$,
then all clauses $A^{\prime}\rightarrow x\in G$ satisfy $F\not\models
A^{\prime}\rightarrow B$ and $F\not\models B\rightarrow A^{\prime}$.

By Lemma 49, $G$ is a subset of $\cup\\{BCL(A,F)\mid B\not\leq_{F}A\\}$.
Therefore, $A^{\prime}\rightarrow x$ is in $BCL(A,F)$ for some $A$ such that
$B\not\leq_{F}A$. By definition of $BCL(A,F)$ the equivalence
$A\equiv_{F}A^{\prime}$ holds. With $B\not\leq_{F}A$, it proves
$B\not\leq_{F}A^{\prime}$. This is the first property to prove: $F\not\models
A^{\prime}\rightarrow B$.

Since $x$ is in $HEADS(B,F)$, it is in $SFREE(B,F)$. By definition, no clause
$A^{\prime}\rightarrow x$ with head $x$ is in $SCL(B,F)$ exists. The
definition of $A^{\prime}\rightarrow x\in SCL(B,F)$ is $x\not\in A^{\prime}$,
$F\models A^{\prime}\rightarrow x$ and $A^{\prime}<_{F}B$. If the first two
conditions are true, the third is false. Since $A^{\prime}\rightarrow x$ is in
$G$, it is in $\cup\\{BCL(A,F)\mid B\not\leq_{F}A\\}$ by Lemma 49; since
$BCL(A,F)$ does not include tautologies by definition, $x$ is not in
$A^{\prime}$. Since $A^{\prime}\rightarrow x\in G$ and $F\models G$ by Lemma
50, $F\models A^{\prime}\rightarrow x$. As a result, $A^{\prime}<_{F}B$ is
false. Since $A^{\prime}<_{F}B$ means $A^{\prime}\leq_{F}B$ and
$B\not\leq_{F}A^{\prime}$, its negation is either $A^{\prime}\not\leq_{F}B$ or
$B\leq_{F}A^{\prime}$. The second cannot because $B\not\leq_{F}A^{\prime}$, as
proved above. Therefore, $A^{\prime}\not\leq B$. This implies $F\not\models
B\rightarrow A^{\prime}$, the second property to prove.

The third step proves that if $HEADS(B,F)$ and $H$ differ the algorithm fails
if it uses $H$ in place of $HEADS(B,F)$.

As proved in the first step, if $HEADS(B,F)$ and $H$ differ then a variable
$x$ in $HEADS(B,F)$ is the head of a clause of $G$. Since $HEADS(B,F)$ is a
subset of $RCN(B,F)$, this variable $x$ is in $RCN(B,F)$. By Lemma 18, a
clause $B^{\prime}\rightarrow x$ is in $BCL(B,F)$.

By contradiction, the algorithm is assumed not to fail. Since the algorithm
fails if $E$ is false, and $E$ is set true only when $SCL(B,F)\cup IT\models
BCL(B,F)$ holds, this entailment is the case for some $IT$. Since $G$ entails
$SCL(B,F)$ by Lemma 46, this implies $G\cup IT\models B^{\prime}\rightarrow
x$. The other premise $x\not\in B^{\prime}$ of Lemma 1 holds since
$B^{\prime}\rightarrow x$ is in $BCL(B,F)$, which does not contain tautologies
by definition. The lemma proves the existence of a clause
$B^{\prime\prime}\rightarrow x\in G\cup IT$ such that $G\cup IT\models
B^{\prime}\rightarrow B^{\prime\prime}$. The former can be rewritten as:
either $B^{\prime\prime}\rightarrow x\in G$ or $B^{\prime\prime}\rightarrow
x\in IT$. The alternative $B^{\prime\prime}\rightarrow x\in IT$ is false since
the heads of $IT$ are exactly $H$, and $H$ does not contain any head of $G$ by
construction. As a result, $B^{\prime\prime}\rightarrow x\in G$. As proved in
the previous step, for all clauses $B^{\prime\prime}\rightarrow x\in G$ it
holds $F\not\models B\rightarrow B^{\prime\prime}$. Since
$B^{\prime}\rightarrow x\in BCL(B,F)$ includes $F\models B\equiv B^{\prime}$,
this is the same as $F\not\models B^{\prime}\rightarrow B^{\prime\prime}$.
Since $F$ entails $G$ by Lemma 50 and all clauses of $IT$ by Lemma 52, the
previously proved property $G\cup IT\models B^{\prime}\rightarrow
B^{\prime\prime}$ implies $F\models B^{\prime}\rightarrow B^{\prime\prime}$.

This is a contradiction. The assumption was that the algorithm does not fail.
Therefore, the algorithm fails.

This failure would be a problem if the formula were single-head equivalent,
but this is proved not to be the case. This is the fourth and final step of
the proof.

By assumption, $HEADS(B,F)$ and $H$ differ. The first step of the proof proves
$x\in HEADS(B,F)$ and $A^{\prime}\rightarrow x\in G$ for a clause
$A^{\prime}\rightarrow x$. The second step proves $F\not\models B\rightarrow
A^{\prime\prime}$ and $F\not\models A^{\prime\prime}\rightarrow B$ for all
clauses $A^{\prime\prime}\rightarrow x\in G$ with head in $HEADS(B,F)$,
including $A^{\prime}\rightarrow x$. Since $G$ does not contain tautologies by
Lemma 45, $x$ is not in $A^{\prime}$. Since $F$ entails $G$ by Lemma 50, it
entails its clause $A^{\prime}\rightarrow x$.

Since $x$ is in $HEADS(B,F)$, it is also in $RCN(B,F)$ by definition. By Lemma
18, $BCL(B,F)$ contains a clause $B^{\prime}\rightarrow x$. This is defined as
$x\not\in B^{\prime}$, $F\models B^{\prime}\rightarrow x$ and $F\models
B\equiv B^{\prime}$.

The proof is by contradiction: $F^{\prime}$ is assumed to be a single-head
formula equivalent to $F$. Because of equivalence, everything entailed by $F$
is entailed by $F^{\prime}$. In particular, $F^{\prime}$ entails
$B^{\prime}\rightarrow x$ and $A^{\prime}\rightarrow x$. Since $x$ is neither
in $B^{\prime}$ nor in $A^{\prime}$, Lemma 1 applies: $F$ contains two clauses
$B^{\prime\prime}\rightarrow x$ and $A^{\prime\prime}\rightarrow x$ such that
$F^{\prime}\models B^{\prime}\rightarrow B^{\prime\prime}$ and
$F^{\prime}\models A^{\prime}\rightarrow A^{\prime\prime}$. Since $F$ is
removed tautologies in the first step of the algorithm, these are not
tautologies: $x\not\in A^{\prime\prime}$ and $x\not\in B^{\prime\prime}$.
Since $F^{\prime}$ is single-head, $A^{\prime\prime}$ and $B^{\prime\prime}$
are the same. Let $C=A^{\prime\prime}=B^{\prime\prime}$. What holds for
$A^{\prime\prime}$ or $B^{\prime\prime}$ also holds for $C$. Namely, $x\not\in
C$, $C\rightarrow x\in F^{\prime}$, $F^{\prime}\models B^{\prime}\rightarrow
C$ and $F^{\prime}\models A^{\prime}\rightarrow C$. Membership implies
entailment: $F^{\prime}\models C\rightarrow x$. By equivalence, $F$ entails
the same formulae: $C\rightarrow x$, $B^{\prime}\rightarrow C$ and
$A^{\prime}\rightarrow C$.

If $F\models C\rightarrow B$, since $F\models A^{\prime}\rightarrow C$ and
$F\models B\equiv B^{\prime}$, then $F\models A^{\prime}\rightarrow B$, which
is not the case. As a result, $F\not\models C\rightarrow B$. Since $F\models
B\equiv B^{\prime}$, the entailment $F\models B^{\prime}\rightarrow C$ implies
$F\models B\rightarrow C$. All conditions for $C\rightarrow x\in SCL(B,F)$ are
met: $x\not\in C$, $F\models C\rightarrow x$, $F\models B\rightarrow C$ and
$F\not\models C\rightarrow B$.

Since $G$ implies $SCL(B,F)$ by Lemma 46, it implies $C\rightarrow x$. Since
$x$ is not in $C$, Lemma 1 proves that $G$ contains a clause
$C^{\prime}\rightarrow x$ such that $G\models C\rightarrow C^{\prime}$, which
implies $F\models C\rightarrow C^{\prime}$ because $F$ implies $G$ by Lemma
50. Since $F\models B^{\prime}\rightarrow C$ and $F\models B\equiv
B^{\prime}$, this implies $F\models B\rightarrow C^{\prime}$. This is a
contradiction since $x\in HEADS(B,F)$ and $C^{\prime}\rightarrow x\in G$ imply
$F\not\models B\rightarrow C^{\prime}$ as proved in the second step of the
proof.

In summary, even if $H$ differs from $HEADS(B,F)$ the algorithm is still
right: it fails, which is what it should do since the formula is not single-
head equivalent. This allows using $H$ instead of $HEADS(B,F)$, saving the
calculation of $SCL(B,F)$.

A positive side effect of the change is that success is no longer ambiguous.
If $F$ is not single-head equivalent, the original algorithm may fail or
return a formula that is not single-head. The modified version fails, period.

###### Lemma 54

If $F$ is not equivalent to any single-head formula, Algorithm 4 with the
variant $H=RCN(B,F)\backslash\\{x\mid\exists B^{\prime}.B^{\prime}\rightarrow
x\in G\\}$ fails.

Proof. A difference between $RCN(B,F)\backslash\\{x\mid\exists
B^{\prime}.B^{\prime}\rightarrow x\in G\\}$ and $HEADS(B,F)$ makes the
modified algorithm fail, as shown by Lemma 53. The claim is therefore proved
in this case. Remains to prove it when $RCN(B,F)\backslash\\{x\mid\exists
B^{\prime}.B^{\prime}\rightarrow x\in G\\}$ always coincides with
$HEADS(B,F)$.

This is proved by contradiction: the algorithm is assumed not to fail and
$RCN(B,F)\backslash\\{x\mid\exists B^{\prime}.B^{\prime}\rightarrow x\in G\\}$
to always coincide with $HEADS(B,F)$; the input formula is proved single-head
equivalent.

Since $RCN(B,F)\backslash\\{x\mid\exists B^{\prime}.B^{\prime}\rightarrow x\in
G\\}$ is the same as $HEADS(B,F)$, the modified algorithm is the same as the
original (Algorithm 4). Since the modified algorithm does not fail, the
original does not fail either. By Theorem 1, the output formula of the
original algorithm is equivalent to $F$. This is therefore also the output
formula of the modified algorithm. The input formula is proved single-head
equivalent by showing that the output formula is single-head.

The claim is proved by inductively showing that $G$ never contains two clauses
with the same head $x$. It initially holds because $G$ is empty. It is
inductively assumed at the beginning of every iteration and proved at the end.
Two cases are considered: $G$ does not contain a clause with head $x$ at the
beginning of the iteration, or it does.

The first case is that $G$ does not contain a clause of head $x$. The only
instruction that changes $G$ is $G=G\cup IT$. Since $G$ does not contain any
clause of head $x$ and $IT$ may at most contain one by construction, $G\cup
IT$ may at most contain one clause of head $x$. This is the inductive claim.

The second case is that $G$ contains a clause of head $x$. It implies that $x$
is not in $H=RCN(B,F)\backslash\\{x\mid\exists
B^{\prime}.B^{\prime}\rightarrow x\in G\\}$. Since $H$ is the set of heads of
$IT$, this set does not contain any clause of head $x$. The instruction
$G=G\cup IT$ does not add any clause of head $x$ to $G$, which still contains
only one clause of head $x$ after it.

In the other way around, if the algorithm succeeds the input formula is
single-head equivalent. The converse is proved by Theorem 1. In the modified
version of the algorithm, success and failure alone tell whether the input
formula is single-head or not.

###  4.10 Old bodies

The algorithm uses $UCL(B,F)\cap SCL(B,F)$ as the second argument of
$MINBODIES()$. The first component $UCL(B,F)$ is already known: it is
calculated in advance together with $RCN(B,F)$ for all bodies $B$ in $F$. The
second component $SCL(B,F)$ is instead a problem because it is not bounded by
the size of $F$. The intersection can be rewritten as
$\\{B^{\prime}\rightarrow x\in UCL(B,F)\mid B^{\prime}<_{F}B\\}$, which
however requires two entailment tests for each clause: $F\models B\rightarrow
B^{\prime}$ and $F\not\models B^{\prime}\rightarrow B$.

A more efficient way to obtain it is to accumulate all clauses $UCL(B,F)$
along the way in a set $U$. During the iteration for $B$, this set $U$
contains all clauses of $F$ with a body that is strictly less than $B$. It may
also contain other clauses, but intersecting with $UCL(B,F)$ removes them.

The algorithm requires only small, localized changes: at the beginning, $U$ is
empty; at the end of each step, $UCL(B,F)$ is added to $U$ by $U=U\cup
UCL(B,F)$; finally, $UCL(B,F)\cap U$ replaces $UCL(B,F)\cap SCL(B,F)$.

###### Lemma 55

If $B^{\prime}\rightarrow x\in UCL(B,F)$, then $B^{\prime}\rightarrow x\in
SCL(B,F)$ if and only $B^{\prime}\rightarrow x\in U$, where $U$ is the union
of $UCL(A,F)$ for all sets $A$ used in the previous iterations of the
autoreconstruction algorithm (Algorithm 4).

Proof. The proof comprises two parts: $B^{\prime}\rightarrow x\in UCL(B,F)\cap
U$ implies $B^{\prime}\rightarrow x\in SCL(B,F)$, and $B^{\prime}\rightarrow
x\in UCL(B,F)\cap SCL(B,F)$ implies $B^{\prime}\rightarrow x\in U$.

The first part starts from the assumptions $B^{\prime}\rightarrow x\in
UCL(B,F)$ and $B^{\prime}\rightarrow x\in U$. The first condition is defined
as $B^{\prime}\rightarrow x\in F$, $F\models B\rightarrow B^{\prime}$ and
$x\not\in B^{\prime}$, the second as $B^{\prime}\rightarrow x\in UCL(A,F)$
with $A$ chosen before $B$. That $A$ was chosen before $B$ has two
consequences: first, $B<_{F}A$ is not the case as otherwise $A$ would not have
been minimal in $P$ when it was chosen; second, $B\equiv_{F}A$ does not hold
either, as otherwise $B$ would have been removed from $P$ in the iteration for
$A$. Since neither $B<_{F}A$ nor $B\equiv_{F}A$ hold, $B\leq_{F}A$ does not
hold either. By definition, $F\not\models A\rightarrow B$ follows. The
condition $B^{\prime}\rightarrow x\in UCL(A,F)$ implies $F\models A\rightarrow
B^{\prime}$. If $F\models B^{\prime}\rightarrow B$ then by transitivity
$F\models A\rightarrow B$, which contradicts $F\not\models A\rightarrow B$.
Therefore, the converse $F\not\models B^{\prime}\rightarrow B$ holds. The
conditions $F\not\models B^{\prime}\rightarrow B$, $F\models B\rightarrow
B^{\prime}$, $B^{\prime}\rightarrow x\in F$ and $x\not\in B^{\prime}$ imply
$B^{\prime}\rightarrow x\in SCL(B,F)$.

The reverse direction is proved by assuming $B^{\prime}\rightarrow x\in
UCL(B,F)$ and $B^{\prime}\rightarrow x\in SCL(B,F)$. These conditions imply
$x\not\in B^{\prime}$, $B^{\prime}\rightarrow x\in F$, $F\models B\rightarrow
B^{\prime}$ and $F\not\models B^{\prime}\rightarrow B$. The latter two define
$B^{\prime}<_{F}B$. Since $B^{\prime}$ is the precondition of a clause of $F$,
it is initially in $P$. When $B$ is chosen it is no longer in $P$, as
otherwise $B$ would not be minimal in $P$. Therefore, $B^{\prime}$ has been
removed from $P$ in a previous step. Let $A$ be the set of variables chosen at
that step. The only instruction that removes elements from $P$ is
$P=P\backslash\\{B^{\prime}\mid F\models A\equiv B\\}$. Therefore, $F\models
A\equiv B^{\prime}$. Equivalence implies entailment: $F\models A\rightarrow
B^{\prime}$; with $x\not\in B^{\prime}$ and $B^{\prime}\rightarrow x\in F$,
this is the definition of $B^{\prime}\rightarrow x\in UCL(A,F)$. Therefore,
$B^{\prime}\rightarrow x$ is added to $U$ at the end of the iteration. Since
$U$ is never removed element, it still contains that clause at the iteration
when $B$ is chosen.

The instruction $T = MINBODIES(M,UCL(B,F)\cap SCL(B,F))$ can therefore be
replaced by $T = MINBODIES(M,UCL(B,F)\cap U)$ with the only additional cost of
accumulating $UCL(B,F)$ in $U$. This is correct because the lemma proves that
as long as clauses of $UCL(B,F)$ are concerned, there is no difference between
$SCL(B,F)$ and $U$.

###  4.11 Cherry picking

The check $SCL(B,F)\cup IT\models BCL(B,F)$ is the most expensive operation in
the inner loop of the algorithm. As a dominating operation, it should be as
efficient as possible. Instead, it requires two sets that are not even bounded
by the size of the original formula: $SCL(B,F)$ and $BCL(B,F)$; they contain
consequences of $F$, not only clauses of $F$. This section reformulates the
check to remove $SCL(B,F)$, the next $BCL(B,F)$.

Since the formula under construction $G$ entails $SCL(B,F)$ by Lemma 46, it
could be used in its place. But while $G$ contains a subset equivalent to
$SCL(B,F)$, it also contains other clauses. In particular, it contains clauses
that are not in $BCL(B,G)$ and are therefore irrelevant when the precondition
is $B$. This is a setback in efficiency when $F$ contains many bodies that do
not entail each other. Restricting to $UCL(B,G)$ excludes the extra clauses,
but is not correct in general.

$F=\\{ab\rightarrow c,c\rightarrow d\\}$

The algorithm chooses $B=\\{c\\}$ as the first body since it is entailed by
the other $\\{a,b\\}$ but not the other way around. The first iteration ends
with $G=\\{c\rightarrow d\\}$. The algorithm then moves onto $B=\\{a,b\\}$.
The set $UCL(B,G)$ contains the clauses of $G$ whose body is entailed by $B$
according to $G$. The key here is “according to $G$”: since $G$ does not
contain $ab\rightarrow c$, the clause $c\rightarrow d$ does not have its body
entailed by $B=\\{b,c\\}$. Since it is the only clause of $G$, it follows that
$UCL(B,G)$ is empty. Since $IT$ cannot contain a clause with head $d$, the
clause $ab\rightarrow d\in BCL(B,F)$ cannot be entailed by $UCL(B,G)\cup IT$.

The problem is “according to $G$”. The formula under construction is still too
weak. Selecting clauses from $G$ is correct, but using $G$ for deciding body
entailment is not. The clause $c\rightarrow d$ is expected to come out from
this selection because its body $c$ is entailed by $B=\\{a,b\\}$ and is
therefore relevant to the reconstruction of the clauses whose body is entailed
by $B$. However, $c$ is entailed by $B$ only according to $F$, not to $G$.

The solution is to use $G$ as the source of clauses and $F$ for entailment
between bodies. The first results are established on this modified selection
function.

$UCL(B,G,F)=\\{B^{\prime}\rightarrow x\in G\mid F\models B\rightarrow
B^{\prime}\\}$

The condition $x\not\in B^{\prime}$ is not necessary because $G$ is already
proved not to contain tautologies by Lemma 45.

This set is equivalent to $SCL(B,F)$. This is proved in two parts: first,
$UCL(B,G,F)$ is a subset of $SCL(B,F)$; second, it entails it.

###### Lemma 56

At every iteration of the algorithm (Algorithm 4), $UCL(B,G,F)\subseteq
SCL(B,F)$ holds.

Proof. The definition of $A^{\prime}\rightarrow x\in UCL(B,G,F)$ is
$A^{\prime}\rightarrow x\in G$ and $F\models B\rightarrow A^{\prime}$. By
Lemma 49, $A^{\prime}\rightarrow x\in G$ implies $A^{\prime}\rightarrow x\in
BCL(A,F)$ for some $A$ such that $B\not\leq_{F}A$. The definition of
$A^{\prime}\rightarrow x\in BCL(A,F)$ is $x\not\in A^{\prime}$, $F\models
A^{\prime}\rightarrow x$ and $F\models A\equiv A^{\prime}$. Since
$B\not\leq_{F}A$, the latter implies $B\not\leq_{F}A^{\prime}$, which means
$F\not\models A^{\prime}\rightarrow B$. All parts of the definition of
$A^{\prime}\rightarrow x\in SCL(B,F)$ are proved: $x\not\in A^{\prime}$,
$F\models A^{\prime}\rightarrow x$, $F\models B\rightarrow A^{\prime}$ and
$F\not\models A^{\prime}\rightarrow B$.

This lemma trivially implies $SCL(B,F)\models UCL(B,G,F)$. The converse
entailment requires a preliminary lemma that shows that $G$ and $UCL(B,G,F)$
are the same when checking entailment of clauses whose body is entailed by
$B$.

###### Lemma 57

For every two formulae $F$ and $G$, if $G\models A\rightarrow x$, $F\models G$
and $F\models B\rightarrow A$ then $UCL(B,G,F)\models A\rightarrow x$.

Proof. Proved by induction on the number of variables of $G$. The base case is
when $G$ only contains a single variable. The only definite clauses of one
variable are $x\rightarrow x$ and $\emptyset\rightarrow x$. The first is a
tautology and is therefore entailed by $UCL(B,G,F)$. The second is in
$UCL(B,G,F)$ since $F\models B\rightarrow\emptyset$.

The induction conclusion is that $UCL(B,G,F)\models A\rightarrow x$ follows
from $G\models A\rightarrow x$, $F\models G$ and $F\models B\rightarrow A$. If
$x$ is in $A$ then $A\rightarrow x$ is a tautology and is therefore entailed
by $UCL(B,G,F)$. Otherwise, $x\not\in A$ and $G\models A\rightarrow x$ are the
premises of Lemma 1, which proves the existence of a clause
$A^{\prime}\rightarrow x\in G$ such that $G^{x}\models A\rightarrow
A^{\prime}$. Since $F$ entails $G$ it also entails its subset $G^{x}$ and its
consequences, including $A\rightarrow A^{\prime}$. This entailment $F\models
A\rightarrow A^{\prime}$ forms with $A^{\prime}\rightarrow x\in G$ the
definition of $A^{\prime}\rightarrow x\in UCL(B,G,F)$.

Since $G^{x}$ entails $A\rightarrow A^{\prime}$, it entails $A\rightarrow a$
for every $a\in A^{\prime}$. The other two assumptions of the induction
hypothesis have already been proved: $F\models G^{x}$ and $F\models
B\rightarrow A$. Its conclusion is $UCL(B,G^{x},F)\models A\rightarrow a$.
Since this is the case for each $a\in A^{\prime}$, $UCL(B,G^{x},F)\models
A\rightarrow A^{\prime}$ follows. By construction, $UCL(B,G^{x},F)$ is a
subset of $UCL(B,G,F)$ since the formula $F$ that dictates with clauses of $G$
or $G^{x}$ are selected is the same and $G^{x}$ is a subset of $G$. As a
result, $UCL(B,G,F)\models UCL(B,G^{x},F)$. Therefore, $UCL(B,G,F)\models
A\rightarrow A^{\prime}$. Along with $A^{\prime}\rightarrow x\in UCL(B,G,F)$,
this implies $UCL(B,G,F)\models A\rightarrow x$.

This lemma allows proving the converse entailment of Lemma 56.

###### Lemma 58

At every iteration of the algorithm, $UCL(B,G,F)\models SCL(B,F)$.

Proof. Let $A\rightarrow x\in SCL(B,F)$. The claim is that $UCL(B,G,F)\models
A\rightarrow x$. By Lemma 46, $A\rightarrow x\in SCL(B,F)$ implies $G\models
A\rightarrow x$. The definition of $A\rightarrow x\in SCL(B,F)$ includes
$F\models B\rightarrow A$. Since $F\models G\cup IT$ by Lemma 50, also
$F\models G$ holds. All preconditions of Lemma 57 are met. Its conclusion is
$UCL(B,G,F)\models A\rightarrow x$.

The final destination of this three lemmas is proving that $UCL(B,G,F)$ and
$SCL(B,F)$ are equivalent in the algorithm. This is an obvious consequence of
the above lemmas, and is formally stated in the following.

###### Lemma 59

At every iteration of the autoreconstruction algorithm (Algorithm 4),
$UCL(B,G,F)\equiv SCL(B,F)$ holds.

Proof. By Lemma 56, $UCL(B,G,F)\subseteq SCL(B,F)$, which implies
$SCL(B,F)\models UCL(B,G,F)$. Lemma 58 proves the other direction:
$UCL(B,G,F)\models SCL(B,F)$. Implication in both directions is equivalence.

This lemma could directly be applied to the program by checking
$UCL(B,G,F)\cup IT\models BCL(B,F)$ instead of $SCL(B,F)\cup IT\models
BCL(B,F)$ and modifying the function that calculates $UCL(B,F)$ by the
addition of a third argument. This is however not necessary. While $SCL(B,F)$
is not equivalent to $G$, the whole formula $SCL(B,F)\cup IT$ can be replaced
by $UCL(B,G\cup IT)$.

These formulae are not equivalent. Yet, they are the same as long as
entailment of $BCL(B,F)$ is concerned. This is proved in two parts: first,
$UCL(B,G\cup IT)\models BCL(B,F)$ implies $SCL(B,F)\cup IT\models BCL(B,F)$;
second, the converse.

The assumption of the first part is $UCL(B,G\cup IT)\models BCL(B,F)$. Its
claim is $SCL(B,F)\cup IT\models BCL(B,F)$. The first step is that $IT$ can be
factored out from $UCL(B,G\cup IT)$.

###### Lemma 60

At every iteration of the autoreconstruction algorithm (Algorithm 4),
$SCL(B,F)\cup IT\equiv UCL(B,G\cup IT,F)$ holds.

Proof. An immediate consequence of the definition is $UCL(B,G\cup
IT,F)=UCL(B,G,F)\cup UCL(B,IT,F)$.

By Lemma 59, $UCL(B,G,F)$ is equivalent to $SCL(B,F)$.

Since $IT\subseteq BCL(B,F)$ by Lemma 41, it holds $F\models B\rightarrow
B^{\prime}$ for all clauses $B^{\prime}\rightarrow x$ of $IT$. As a result,
$UCL(B,IT,F)$ contains all of them: $UCL(B,IT,F)=IT$.

Since $SCL(B,F)\cup IT$ is equivalent to $UCL(B,G\cup IT,F)$, if the latter is
equivalent to $UCL(B,G\cup IT,G\cup IT)$, the target is hit because this
formula is the same as $UCL(B,G\cup IT)$.

The difference between $UCL(B,G\cup IT,F)$ and $UCL(B,G\cup IT,G\cup IT)$ is
the selection criteria: $F\models B\rightarrow B^{\prime}$ versus $G\cup
IT\models B\rightarrow B^{\prime}$ where $B^{\prime}$ is the body of a clause.
These conditions differ in general. Yet, they coincide under the current
assumption $UCL(B,G\cup IT)\models BCL(B,F)$.

###### Lemma 61

If $UCL(B,G\cup IT)\models BCL(B,F)$ then $F\models B\rightarrow B^{\prime}$
is equivalent to $G\cup IT\models B\rightarrow B^{\prime}$ for every set of
variables $B^{\prime}$.

Proof. By Lemma 50 and Lemma 52, $F$ entails $G\cup IT$. As a result, if
$G\cup IT\models B\rightarrow B^{\prime}$, then $F\models B\rightarrow
B^{\prime}$.

The rest of the proof obtains $G\cup IT\models B\rightarrow B^{\prime}$ from
$F\models B\rightarrow B^{\prime}$. Since $F\models B\rightarrow B^{\prime}$,
then $F\models B\rightarrow b$ holds for every $b\in B^{\prime}$. If $b\in B$
then $B\rightarrow b$ is a tautology and is therefore entailed by $BCL(B,F)$.
Otherwise, $b\not\in B$ and $F\models B\rightarrow b$ with the trivially true
$F\models B\equiv B$ define $B\rightarrow b\in BCL(B,F)$. Either way,
$B\rightarrow b$ is entailed by $BCL(B,F)$ for every $b\in B^{\prime}$. By
assumption, $UCL(B,G\cup IT)\models BCL(B,F)$, which implies $G\cup IT\models
B\rightarrow b$ since $UCL(B,G\cup IT)$ is defined as a subset of $G\cup IT$.
This holds for every $b\in B^{\prime}$, proving $G\cup IT\models B\rightarrow
B^{\prime}$.

The first part of the proof can now be completed.

###### Lemma 62

If $UCL(B,G\cup IT)\models BCL(B,F)$ then $SCL(B,F)\cup IT\models BCL(B,F)$.

Proof. The only difference between $UCL(B,G\cup IT)$ and $UCL(B,G\cup IT,G\cup
IT)$ is that the former does not contain tautologies. The latter does not as
well because it is a subset of $G\cup IT$, which does not by Lemma 45.

The set $UCL(B,G\cup IT,G\cup IT)$ contains some clauses $G\cup IT$ like
$UCL(B,G\cup IT,F)$ does, but differs from it in the selection criteria:
$G\cup IT\models B\rightarrow B^{\prime}$ instead of $F\models B\rightarrow
B^{\prime}$. The assumption $UCL(B,G\cup IT)\models BCL(B,F)$ proves that $F$
and $G\cup IT$ entail the same clauses $B\rightarrow B^{\prime}$ by Lemma 61.
Therefore, $UCL(B,G\cup IT,G\cup IT)$ is identical to $UCL(B,G\cup IT,F)$.

Lemma 60 proves that $UCL(B,G\cup IT,F)$ is equivalent to $SCL(B,F)\cup IT$.

Summarizing, the assumption $UCL(B,G\cup IT)\models BCL(B,F)$ implies that
$UCL(B,G\cup IT)$ is the same as $UCL(B,G\cup IT,F)$, which is the same as
$SCL(B,F)\cup IT$; this equality and the assumption $UCL(B,G\cup IT)\models
BCL(B,F)$ imply $SCL(B,F)\cup IT\models BCL(B,F)$.

The proof looks like a sequence of equivalences. As such, it would also prove
the opposite direction, saving the cost of a further proof. But this is a
false impression: $UCL(B,G\cup IT)$ is not always equivalent to $SCL(B,F)\cup
IT$, it is only when $UCL(B,G\cup IT)\models BCL(B,F)$ holds.

The converse direction has to be proved separately: $SCL(B,F)\cup IT\models
BCL(B,F)$ implies $UCL(B,G\cup IT)\models BCL(B,F)$.

The first step in this direction is that $UCL()$ maintains certain entailments
of the formula it is applied to.

###### Lemma 63

For every formulae $F$ and $G$, variable $x$ and sets of variables $B$ and
$B^{\prime}$ such that $F\models G$ and $F\models B\rightarrow B^{\prime}$, it
holds $G\models B^{\prime}\rightarrow x$ if and only if $UCL(B,G,F)\models
B^{\prime}\rightarrow x$.

Proof. Since $UCL(B,G,F)$ only comprises clauses of $G$ by definition, it is
entailed by $G$. This proves the first direction of the claim: if
$UCL(B,G,F)\models B^{\prime}\rightarrow x$ then $G\models
B^{\prime}\rightarrow x$.

The converse direction is proved by contradiction: $G\models
B^{\prime}\rightarrow x$ and $UCL(B,G,F)\not\models B^{\prime}\rightarrow x$
do not both hold at the same time. The latter is equivalent to the existence
of a model $M$ that satisfies $UCL(B,G,F)\cup B^{\prime}\cup\\{\neg x\\}$.

Let $M^{\prime}$ be the model that evaluates all variables of $BCN(B,F)$ like
$M$ and all others to false: if $F\models B\rightarrow z$ then $z$ has the
same value in $M$ and $M^{\prime}$; otherwise, $z$ is false in $M^{\prime}$.
This model $M^{\prime}$ is proved to satisfy every element of $G\cup
B^{\prime}\cup\\{\neg x\\}$, contradicting the assumption $G\models
B^{\prime}\rightarrow x$. The proof is done separately for the elements of
$G\backslash UCL(B,G,F)$, of $UCL(B,F,F)$, of $B^{\prime}$ and of $\\{\neg
x\\}$.

Let $B^{\prime\prime}\rightarrow y$ be a clause of $G$ but not of
$UCL(B,G,F)$. Since $UCL(B,G,F)$ contains all clauses of $G$ except those
whose body is not entailed by $B$, this is only possible if $F\not\models
B\rightarrow B^{\prime\prime}$. As a result, $F\not\models B\rightarrow b$ for
some $b\in B^{\prime\prime}$. By construction, $M^{\prime}$ evaluates $b$ to
false and therefore satisfies $B^{\prime\prime}\rightarrow y$.

The definition of $B^{\prime\prime}\rightarrow y\in UCL(B,G,F)$ is
$B^{\prime\prime}\rightarrow y\in G$ and $F\models B\rightarrow
B^{\prime\prime}$. The latter implies $F\models B\rightarrow b$ for every
$b\in B^{\prime\prime}$. Therefore, $M^{\prime}$ evaluates every $b\in
B^{\prime\prime}$ in the same way as $M$ does. Since $F\models G$ holds by
Lemma 50, $B^{\prime\prime}\rightarrow y\in G$ implies $F\models
B^{\prime\prime}\rightarrow y$. With $F\models B\rightarrow B^{\prime\prime}$,
it implies $F\models B\rightarrow y$. Therefore, $y$ is evaluated by
$M^{\prime}$ in the same way as $M$ does. This proves that all variables in
every $B^{\prime\prime}\rightarrow y\in UCL(B,G,F)$ is evaluated by
$M^{\prime}$ in the same way as $M$ does. Since $M$ satisfies $UCL(B,G,F)$,
also $M^{\prime}$ does.

Since $B^{\prime}\rightarrow b$ is a tautology for every $b\in B$, it is
entailed by $F$. Which also entails $B\rightarrow B^{\prime}$. By
transitivity, $F$ entails $B\rightarrow b$ for every $b\in B^{\prime}$. As a
result, $M^{\prime}$ evaluates all variables of $B^{\prime}$ in the same way
as $M$. Since $M$ satisfies $B^{\prime}$ by assumption, also $M^{\prime}$
does.

A consequence of $F\models B\rightarrow B^{\prime}$ and $G\models
B^{\prime}\rightarrow x$ is $F\models B\rightarrow x$ since $F\models G$. It
implies that $M^{\prime}$ evaluates $\neg x$ in the same way as $M$, which
satisfies it.

This proves that $M^{\prime}$ satisfies $G\backslash UCL(B,G,F)\cup
UCL(B,G,F)\cup B^{\prime}\cup\\{\neg b\\}$, which is the same as $G\cup
B^{\prime}\cup\\{\neg x\\}$. The satisfiabily of this set is the same as
$G\not\models B^{\prime}\rightarrow x$, which contradicts the assumption
$G\models B^{\prime}\rightarrow x$.

This lemma tells that $UCL(B,G,F)$ is the same as $G$ when checking entailment
of clauses whose body is entailed by $B$ according to $F$. It also applies to
the case where the two formulae $G$ and $F$ are the same.

###### Lemma 64

If $SCL(B,F)\cup IT\models BCL(B,F)$ then $UCL(B,G\cup IT)\models BCL(B,F)$.

Proof. Lemma 46 proves $G\models SCL(B,F)$. With the assumption $SCL(B,F)\cup
IT\models BCL(B,F)$, it implies $G\cup IT\models BCL(B,F)$.

Let $B^{\prime}\rightarrow x\in BCL(B,F)$. By definition, $F\models
B\rightarrow B^{\prime}$. This implies $F\models B\rightarrow b$ for every
$b\in B^{\prime}$. If $b\in B$ then $B\rightarrow b$ is a tautology and is
therefore entailed by $BCL(B,F)$. Otherwise, $b\not\in B$, $F\models
B\rightarrow b$ and the trivially true $F\models B\rightarrow B$ imply
$B\rightarrow b\in BCL(B,F)$. Either way, $B\rightarrow b$ is entailed by
$BCL(B,F)$. Since $G\cup IT$ entails this set, it also entails $B\rightarrow
b$ as well. This hold for all $b\in B^{\prime}$; therefore, $G\cup IT\models
B\rightarrow B^{\prime}$.

Lemma 63 applies to $UCL(B,G\cup IT,G\cup IT)$: since $G\cup IT\models G\cup
IT$, $G\cup IT\models B\rightarrow B^{\prime}$ and $G\cup IT\models
B^{\prime}\rightarrow x$, it follows $UCL(B,G\cup IT,G\cup IT)\models
B^{\prime}\rightarrow x$. This is the same as $UCL(B,G\cup IT)\models
B^{\prime}\rightarrow x$ since the only difference between the definitions of
$UCL(B,G\cup IT,G\cup IT)$ and $UCL(B,G\cup IT)$ is that the latter does not
contain tautologies, but the former does not as well since it is a subset of
$G\cup IT$, which does not by Lemma 45.

This lemma proves that $SCL(B,F)\cup IT\models BCL(B,F)$ implies $UCL(B,G\cup
IT)\models BCL(B,F)$. The converse implication is Lemma 62. The conclusion is
that these two conditions are the same.

###### Lemma 65

The conditions $SCL(B,F)\cup IT\models BCL(B,F)$ and $UCL(B,G\cup IT)\models
BCL(B,F)$ are equivalent.

Proof. Immediate consequence of Lemma 62 and Lemma 64.

###  4.12 Ubi minor major cessat

The previous section proves that the dominant operation of the algorithm
$SCL(B,F)\cup IT\models BCL(B,F)$ is equivalent to $UCL(B,G\cup IT)\models
BCL(B,F)$. While $SCL(B,F)$ is a set of consequences and can therefore be very
large, $UCL(B,G\cup IT)$ is a subset of $G\cup IT$ and is therefore bounded by
the size of the formula under construction $G$ and the candidate set $IT$. The
latter is in turn bounded because it is single-head: it has no more clauses
than the variables in $F$.

The problem remains on the other side of the implication: $BCL(B,F)$ contains
all clauses $B^{\prime}\rightarrow x$ entailed by $F$ such that $F\models
B\rightarrow B^{\prime}$. Many such clauses may be entailed even from a small
formula $F$.

The solution is to use $UCL(B,F)$ in place of $BCL(B,F)$. This is the set of
clauses of $F$ whose body is entailed by $B$ according to $F$. It is monotonic
with respect to entailment of the formula, as the following lemma proves.

###### Lemma 66

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

Proof. Every clause $B^{\prime}\rightarrow x$ of $UCL(B,F^{\prime})$ satisfies
$B^{\prime}\rightarrow x\in F^{\prime}$ and $F^{\prime}\models B\rightarrow
B^{\prime}$ by definition. The former implies $F^{\prime}\models
B^{\prime}\rightarrow x$. Since $F\models F^{\prime}$, these two entailments
carry over to the other formula: $F\models B^{\prime}\rightarrow x$ and
$F\models B\rightarrow B^{\prime}$. By Lemma 36, these two conditions imply
$UCL(B,F)\models B^{\prime}\rightarrow x$. This argument shows that every
clause of $UCL(B,F^{\prime})$ is entailed by $UCL(B,F)$.

Another result about $UCL()$ is that $RCN()$ is invariant with respect to
replacing $F$ with $UCL(B,F)$, as it is $BCN()$ as proved by Lemma 34.

###### Lemma 67

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

Proof. The first step of the proof is $F\models
B\rightarrow(BCN(B,F)\backslash\\{x\\})$. The definition of $y\in BCN(B,F)$ is
$F\models B\rightarrow y$. This is the case for every $y\in BCN(B,F)$;
therefore, $F\models B\rightarrow BCN(B,F)$ follows. Since
$BCN(B,F)\backslash\\{x\\}$ is a subset of $BCN(B,F)$, also $F\models
B\rightarrow(BCN(B,F)\backslash\\{x\\})$ holds.

This entailment is the precondition of Lemma 36, which proves that $F$ and
$UCL(B,F)$ entail the same clauses whose body is entailed by $B$. In this
case, $F\models B\rightarrow(BCN(B,F)\backslash\\{x\\})$ proves that
$F\models(BCN(B,F)\backslash\\{x\\})\rightarrow x$ is the same as
$UCL(B,F)\models(BCN(B,F)\backslash\\{x\\})\rightarrow x$. These two
entailments define $x\in RCN(B,F)$ and $x\in RCN(B,UCL(B,F))$. Since they are
the same, $RCN(B,F)$ and $RCN(B,UCL(B,F))$ coincide.

This lemma allows proving $UCL(B,F)$ can replace $BCL(B,F)$ in a certain
situation.

A semantical counterpart of Lemma 31 shows that $UCL(B,F)$ is equivalent to
the union of the two other considered sets of clauses.

###### Lemma 68

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

Proof. Lemma 31 proves $UCL(B,F)=F\cap(SCL(B,F)\cup BCL(B,F))$. As a subset of
$SCL(B,F)\cup BCL(B,F)$, the set $UCL(B,F)$ is entailed by it: $SCL(B,F)\cup
BCL(B,F)\models UCL(B,F)$.

The converse implication $UCL(B,F)\models SCL(B,F)\cup BCL(B,F)$ is proved by
showing that every clause $B^{\prime}\rightarrow x$ of $SCL(B,F)\cup BCL(B,F)$
is entailed by $UCL(B,F)$. The definition of $B^{\prime}\rightarrow x\in
SCL(B,F)\cup BCL(B,F)$ includes $F\models B^{\prime}\rightarrow x$ and either
$B^{\prime}<_{F}B$ or $B^{\prime}\equiv_{F}B$. The two alternatives are
equivalent to $B^{\prime}\leq_{F}B$, which is defined as $F\models
B\rightarrow B^{\prime}$. Lemma 36 proves that $F\models B\rightarrow
B^{\prime}$ and $F\models B^{\prime}\rightarrow x$ imply $UCL(B,F)\models
B^{\prime}\rightarrow x$.

Lemma 46 proves that $G$ entails $SCL(B,F)$. This fact cannot be pushed from
$G$ to $UCL(B,G)$ since $UCL(B,G)$ does not contain the clauses of $G$ whose
body is not entailed by $G$. Adding $IT$ and requiring $BCL(B,F)$ to be
entailed fills the gap.

###### Lemma 69

If $UCL(B,G\cup IT)\models BCL(B,F)$ then $UCL(B,G\cup IT)\models SCL(B,F)$.

Proof. The claim is proved by showing that every clause $B^{\prime}\rightarrow
x$ of $SCL(B,F)$ is entailed by $UCL(B,G\cup IT)$.

The definition of $B^{\prime}\rightarrow x\in SCL(B,F)$ includes
$B^{\prime}<_{F}B$, which includes $F\models B\rightarrow B^{\prime}$. This is
the same as $F\models B\rightarrow b$ for every $b\in B^{\prime}$. If $b\in B$
then $B\rightarrow b$ is a tautology and is therefore entailed by $BCL(B,F)$.
Otherwise, $b\not\in B$ and $F\models B\rightarrow b$ and the trivially true
$F\models B\equiv B$ define $B\rightarrow b\in BCL(B,F)$. Either way,
$BCL(B,F)$ entails $B\rightarrow b$. Since this is the case for every $b\in
B^{\prime}$, it proves $BCL(B,F)\models B\rightarrow B^{\prime}$. Since
$UCL(B,G\cup IT)$ entails $BCL(B,F)$ by assumption, it also entails its
consequence $B\rightarrow B^{\prime}$. Since $UCL(B,G\cup IT)$ is by
definition a subset of $G\cup IT$, monotonicity implies $G\cup IT\models
B\rightarrow B^{\prime}$.

Lemma 46 proves $G\models SCL(B,F)$. Therefore, $G\models
B^{\prime}\rightarrow x$. By monotonicity, $G\cup IT\models
B^{\prime}\rightarrow x$. Since $G\cup IT\models B\rightarrow B^{\prime}$ as
proved in the previous paragraph, $G\cup IT\models B^{\prime}\rightarrow x$
implies $UCL(B,G\cup IT)\models B^{\prime}\rightarrow x$ by Lemma 36.

If $UCL(B,G\cup IT)$ implies $BCL(B,F)$, it also implies $SCL(B,F)$. If it
implies the first, it implies both. Their union is $SCL(B,F)\cup BCL(B,F)$,
which is semantically the same as $UCL(B,F)$. This is proved by the next
lemma.

###### Lemma 70

The conditions $UCL(B,G\cup IT)\models BCL(B,F)$ and $UCL(B,G\cup IT)\equiv
UCL(B,F)$ are equivalent.

Proof. Lemma 50 states $F\models G\cup IT$. This is the precondition of Lemma
66, which proves $UCL(B,F)\models UCL(B,G\cup IT)$. This is half of the second
condition in the claim, $UCL(B,G\cup IT)\equiv UCL(B,F)$. It holds regardless
of the first.

The claim is therefore proved if the first condition $UCL(B,G\cup IT)\models
BCL(B,F)$ is the same as the other half of the second: $UCL(B,G\cup IT)\models
UCL(B,F)$.

Lemma 68 proves $UCL(B,F)\equiv SCL(B,F)\cup BCL(B,F)$; therefore, the claim
is that $UCL(B,G\cup IT)\models BCL(B,F)$ and $UCL(B,G\cup IT)\models
SCL(B,F)\cup BCL(B,F)$ are the same. The first entailment follows from the
second because its consequent is a subset of that of the second. The converse
is a consequence of Lemma 69: $UCL(B,G\cup IT)\models BCL(B,F)$ implies
$UCL(B,G\cup IT)\models SCL(B,F)$. Therefore, it implies $UCL(B,G\cup
IT)\models SCL(B,F)\cup BCL(B,F)$.

Lemma 65 proves that $SCL(B,F)\cup IT\models BCL(B,F)$ is the same as
$UCL(B,G\cup IT)\models BCL(B,F)$, which Lemma 70 proves the same as
$UCL(B,G\cup IT)\equiv UCL(B,F)$. The formulae in the equivalence are both
bounded in size by $F$ and $G\cup IT$; the latter is single-head by
construction, and is therefore polynomially bounded by the number of
variables.

Yet, equivalence is still to be checked. It is the same as mutual inference:
$UCL(B,G\cup IT)$ entails every clause of $UCL(B,F)$ and vice versa. Each
inference check is linear in time, making the total quadratic.

An alternative is to trade space for time. Equivalence is equality in some
cases. For example, if both $A$ and $B$ are deductively closed, they are
equivalent if and only if they coincide. Equivalence is equality on the
deductive closure of the two formulae.

Checking equality is easy, but the deductive closure may be very large.
Working on the sets of prime implicants is a more efficient alternative. In
the present case, a still better alternative is to use the minimal implicants
with heads in $H$. The formula under construction $G$ already entails
$SCL(B,F)$; the target of the current iteration is to entail $BCL(B,F)$ with
clauses that have heads in $H$. Only these clauses matter. The minimal such
clauses are $HCLOSE()$.

The final step of this section is to prove that equality is enough if checked
on $HCLOSE()$ when its first argument is $RCN(B,F)$ and the second is either
$UCL(B,G\cup IT)$ or $UCL(B,F)$. These formulae have something in common: the
premise of the following lemma.

###### Lemma 71

If $F\models B\rightarrow B^{\prime}$ holds for every clause
$B^{\prime}\rightarrow x\in F$, then $F\equiv HCLOSE(RCN(B,F),F)$.

Proof. The definition of $B^{\prime}\rightarrow x\in HCLOSE(H,F)$ includes
$F\models B^{\prime}\rightarrow x$: every clause of $HCLOSE(H,F)$ is entailed
by $F$. This also happens in the particular case $H=RCN(B,F)$, and proves
$F\models HCLOSE(RCN(B,F),F)$ holds even when the premise of the lemma does
not.

The premise is necessary to the converse implication
$HCLOSE(RCN(B,F),F)\models F$. Every clause $B^{\prime}\rightarrow x$ of $F$
is proved to be entailed by $HCLOSE(RCN(B,F),F)$.

The premise of the lemma is that $F\models B\rightarrow B^{\prime}$ holds for
every clause $B^{\prime}\rightarrow x\in F$. It implies $B^{\prime}\subseteq
BCN(B,F)$. If $x\in B^{\prime}$ then $B^{\prime}\rightarrow x$ is tautological
and is therefore entailed by $HCLOSE(RCN(B,F),F)$. Otherwise, $x\not\in
B^{\prime}$ strengthens $B^{\prime}\subseteq BCN(B,F)$ to $B^{\prime}\subseteq
BCN(B,F)\backslash\\{x\\}$. Since $F$ contains $B^{\prime}\rightarrow x$ it
also entails it: $F\models B^{\prime}\rightarrow x$. Monotonicity implies
$F\models(BCN(B,F)\backslash\\{x\\})\rightarrow x$. This is the definition of
$x\in RCN(B,F)$.

The definition of $B^{\prime}\rightarrow x\in HCLOSEALL(RCN(B,F),F)$ is met:
$x\in RCN(B,F)$, $x\not\in B^{\prime}$ and $F\models B^{\prime}\rightarrow x$.
Lemma 25 proves that $HCLOSE(RCN(B,F),F)$ contains the minimal clauses of
$HCLOSEALL(RCN(B,F),F)$. If $B^{\prime}\rightarrow x$ is minimal it is in
$HCLOSE(RCN(B,F),F)$; otherwise, one of its subclauses is in
$HCLOSE(RCN(B,F),F)$, and a subclause always entails its superclauses.

A particular case where the premise of this lemma holds is when the formula is
$UCL(B,F)$.

###### Lemma 72

It holds $UCL(B,F)\equiv HCLOSE(RCN(B,F),UCL(B,F))$.

Proof. By definition, $UCL(B,F)$ contains only clauses $B^{\prime}\rightarrow
x$ such that $F\models B\rightarrow B^{\prime}$. This entailment is the same
as $F\models B\rightarrow b$ for every $b\in B^{\prime}$. Lemma 33 tells that
$F\models B\rightarrow b$ is the same as $UCL(B,F)\models B\rightarrow b$.
This implies $UCL(B,F)\models B\rightarrow b$ for every $b\in B^{\prime}$,
which is the same as $UCL(B,F)\models B\rightarrow B^{\prime}$.

This condition $UCL(B,F)\models B\rightarrow B^{\prime}$ holds for every
$B^{\prime}\rightarrow x\in UCL(B,F)$. Lemma 71 proves $UCL(B,F)\equiv
HCLOSE(RCN(B,F),UCL(B,F))$.

Another step is the equality of the real consequences of $F$ and $G\cup IT$.

###### Lemma 73

If $UCL(B,G\cup IT)\equiv UCL(B,F)$ then $RCN(B,F)=RCN(B,G\cup IT)$.

Proof. Since $RCN()$ is defined semantically, it is unaffected by replacing a
formula with an equivalent one: $UCL(B,G\cup IT)\equiv UCL(B,F)$ implies
$RCN(B,UCL(B,G\cup IT))=RCN(B,UCL(B,F))$. The claim follows from Lemma 67,
which states $RCN(B,F)=RCN(B,UCL(B,F))$ and $RCN(B,G\cup IT)=RCN(B,UCL(B,G\cup
IT))$.

The latest version of the check $SCL(B,F)\cup IT\models BCL(B,F)$ was
$UCL(B,G\cup IT)\equiv UCL(B,F)$. This equivalence can be turned into an
equality.

###### Lemma 74

The condition $UCL(B,G\cup IT)\equiv UCL(B,F)$ is the same as
$HCLOSE(RCN(B,F),UCL(B,F))=HCLOSE(RCN(B,G\cup IT),UCL(B,G\cup IT))$.

Proof. Lemma 72 proves that $UCL(B,F)$ is equivalent to
$HCLOSE(RCN(B,F),UCL(B,F))$ and $UCL(B,G\cup IT)$ to $HCLOSE(RCN(B,G\cup
IT),UCL(B,G\cup IT))$. If $HCLOSE(RCN(B,F),UCL(B,F))$ is equal to
$HCLOSE(RCN(B,G\cup IT),UCL(B,G\cup IT))$ then $UCL(B,F)$ and $UCL(B,G\cup
IT)$ are equivalent to the same formula. Therefore, they are equivalent.

The other direction of the claim is now proved. Since $HCLOSE()$ is defined
semantically, it has the same value when applied to two identical sets and two
equivalent formulae. Since $RCN(B,F)=RCN(B,G\cup IT)$ as proved by Lemma 73
and $UCL(B,F)\equiv UCL(B,G\cup IT)$ by assumption, the claim
$HCLOSE(RCN(B,F),UCL(B,F))=HCLOSE(RCN(B,G\cup IT),UCL(B,G\cup IT))$ follows.

The chain of Lemma 65, Lemma 70 and Lemma 74 prove that the dominant operation
of the algorithm $SCL(B,F)\cup IT\models BCL(B,F)$ is equivalent to
$HCLOSE(RCN(B,F),UCL(B,F))=HCLOSE(RCN(B,G\cup IT),UCL(B,G\cup IT))$. The first
set can be determined from $F$ and $B$ alone, outside the loop over the
possible sets $IT$.

The algorithm that calculates $UCL()$ also produces $RCN()$. As a result,
$RCN(B,G\cup IT)$ is determined at no additional cost when $UCL(B,G\cup IT)$
is calculated.

A slight simplification for $HCLOSE(RCN(B,F),UCL(B,F))$ is that
$HCLOSE(HEADS(B,F),UCL(B,F))$ is already known as a part of the mechanism for
determining the bodies of the clauses of $IT$. Since $HEADS(B,F)\subseteq
RCN(B,F)$ by definition, the required set $HCLOSE(RCN(B,F),UCL(B,F))$ can be
calculated as $HCLOSE(HEADS(B,F),UCL(B,F))\cup HCLOSE(RCN(B,F)\backslash
HEADS(B,F),UCL(B,F))$.

###  4.13 Necessity is the mother of invention

The dominating operation $SCL(B,F)\cup IT\models BCL(B,F)$ is simplified as
much as possible to improve the algorithm efficiency. Yet, even in the form
$HCLOSE(RCN(B,F),UCL(B,F))=HCLOSE(RCN(B,G\cup IT),UCL(B,G\cup IT))$ it is
expensive as it requires computing a resolution closure, albeit bounded by the
heads.

The good news is that sometimes it is not necessary. For example, if
$RCN(B,F)\not=RCN(B,G\cup IT)$ then $G\cup IT$ fails at replicating $F$ since
they differ on their consequences of $B$; the candidate $IT$ can be discarded
without further analysis. The additional cost of this check is only that of
comparing two sets, since both $RCN(B,F)$ and $RCN(B,G\cup IT)$ are necessary
anyway.

Other necessary conditions exist.

They are all proved as: $SCL(B,F)\cup IT\models BCL(B,F)$ implies something.
By contraposition, not something implies not $SCL(B,F)\cup IT\models
BCL(B,F)$. If that something is easy to determine, it saves from the expensive
entailment test when false: $IT$ is discarded straight away.

Any of the conditions that are equivalent to $SCL(B,F)\cup IT\models BCL(B,F)$
can be used in its place: $UCL(B,G\cup IT)\models BCL(B,F)$, $UCL(B,G\cup
IT)\equiv UCL(B,F)$, and $HCLOSE(RCN(B,F),UCL(B,F))=HCLOSE(RCN(B,G\cup
IT),UCL(B,G\cup IT))$.

The trick can be repeated as many times as useful: if $SCL(B,F)\cup IT\models
BCL(B,F)$ implies condition one, condition two and condition three, they are
all checked; failure in any stops the iteration over $IT$ since it fails
$SCL(B,F)\cup IT\models BCL(B,F)$.

####  4.13.1 The first necessary condition

The first necessary condition to $SCL(B,F)\cup IT\models BCL(B,F)$ is that
every variable in the bodies of $HCLOSE(RCN(B,F),UCL(B,F))$ occurs in the body
of a clause of $G\cup IT$.

A formal proof is an overshooting. The condition $SCL(B,F)\cup IT\models
BCL(B,F)$ is the same as the equality of $HCLOSE(RCN(B,F),UCL(B,F))$ and
$HCLOSE(RCN(B,G\cup IT),UCL(B,G\cup IT))$. Equality implies that every
variable in a body of the former is in a body of the latter. Since the latter
can be obtained by resolving clauses of $UCL(B,G\cup IT)$ and resolution does
not create literals, that variable is in a body of $UCL(B,G\cup IT)$. Since
$UCL(B,G\cup IT)$ is defined as a subset of $G\cup IT$, that variable is also
in a body of $G\cup IT$.

In the other way around, if $G\cup IT$ contains no body with a variable that
is in a body of $HCLOSE(RC(B,F),UCL(B,F))$ then
$HCLOSE(RCN(B,F),UCL(B,F))=HCLOSE(RCN(B,G\cup IT),UCL(B,G\cup IT))$ is false.

This necessary condition can be seen as the version on bodies of the condition
over the heads. But the condition on the heads is strict: the heads of
$ITERATION(B,F)$ are exactly $HEADS(B,F)$. Instead, a specific body of
$HCLOSE(HEADS(B,F),UCL(B,F))$ may occur in $ITERATION(B,F)$ or not. The
example in nobody.py shows such a case: $F=\\{a\rightarrow b,b\rightarrow
a,c\rightarrow d,d\rightarrow c,ac\rightarrow e\\}$ and $B=\\{a,b\\}$; it
makes $a$ equivalent to $b$ and $c$ to $d$; while $ac\rightarrow e$ is in
$HCLOSE(HEADS(B,F),UCL(B,F))$, the iteration function
$ITERATION(B,F)=\\{bd\rightarrow e\\}$ is valid in spite of not containing a
body $ac$. The example twobodies.py instead shows a case when the same body
occurs multiple times: $F=\\{a\rightarrow b,a\rightarrow c\\}$ and
$B=\\{a\\}$. The only valid iteration function has $ITERATION(B,F)$ equal to
$F$ itself, which contains the body $a$ twice.

The reconstruct.py program exploits this condition by checking whether the
union of the bodies of $G\cup IT$ contains the union of the bodies of
$HCLOSE(RCN(B,F),UCL(B,F))$, failing $IT$ if it does not.

This condition involves $IT$: the bodies of $G\cup IT$ contain all variables
in the bodies of $HCLOSE(RCN(B,F),UCL(B,F))$. Therefore, it can only be
checked inside the loop over the possible sets $IT$. However, the bodies of
$IT$ are by construction bodies of $HCLOSE(HEADS(B,F),UCL(B,F))$. This
provides a further necessary condition: the bodies of $G$ and
$HCLOSE(HEADS(B,F),UCL(B,F))$ contain all variables in the bodies of
$HCLOSE(RCN(B,F),UCL(B,F))$. This other necessary condition involves $IT$ no
longer. Therefore, it can be checked before entering the loop over the
possible sets $IT$.

One outside the loop, one inside the loop. Both necessary conditions are based
on the bodies of $G\cup IT$ containing those of $HCLOSE(RCN(B,F),UCL(B,F))$;
they differ on employing the actual bodies of $IT$ (only given inside the
loop) or their upper bound $HCLOSE(HEADS(B,F),UCL(B,F))$ (known outside the
loop).

Given the length of these formulae, the following shortcuts are employed:
$H=HEADS(B,F)$, $R=RCN(B,F)$ and $U=UCL(B,F)$. If $BD(F)$ is the set of
variables in the bodies of a formula, the conditions are:

$\displaystyle BD(HCLOSE(R,U))$ $\displaystyle\subseteq$ $\displaystyle
BD(G)\cup BD(IT)$ $\displaystyle BD(HCLOSE(R,U))$ $\displaystyle\subseteq$
$\displaystyle BD(G)\cup BD(HCLOSE(H,U))$

They share some components. Since $H=HEADS(B,F)$ is a subset of $R=RCN(B,F)$,
the latter is the union of the former and their set difference:
$R=H\cup(R\backslash H)$.

This reformulation propagates to the head closure of these sets: by
definition, $HCLOSE(A\cup B,F)$ comprises the clauses $B^{\prime}\rightarrow
x$ that obey certain conditions including $x\in A\cup B$ and not involving
$A\cup B$ in any other way. As a result, $HCLOSE(A\cup B,F)=HCLOSE(A,F)\cup
HCLOSE(B,F)$.

In the present case, $HCLOSE(R,U)$ is equal to
$HCLOSE(H,U)\cup{}HCLOSE(R\backslash H,U)$. If two sets of clauses are the
same, the variables in their bodies are the same:
$BD(HCLOSE(R,U)={}BD(HCLOSE(H,U))\cup{}BD(HCLOSE(R\backslash H,U))$.

This equality allows reformulating the two necessary conditions as follows.

$\displaystyle BD(HCLOSE(H,U))\cup BD(HCLOSE(R\backslash H,U))$
$\displaystyle\subseteq$ $\displaystyle BD(G)\cup BD(IT)$ $\displaystyle
BD(HCLOSE(H,U))\cup BD(HCLOSE(R\backslash H,U))$ $\displaystyle\subseteq$
$\displaystyle BD(G)\cup BD(HCLOSE(H,U))$

In the second containment, $BD(HCLOSE(H,U))$ is in both sides. Since a set is
always contained in itself, it can be removed from the left-hand side.

$\displaystyle BD(HCLOSE(H,U))\cup BD(HCLOSE(R\backslash H,U))$
$\displaystyle\subseteq$ $\displaystyle BD(G)\cup BD(IT)$ $\displaystyle
BD(HCLOSE(R\backslash H,U))$ $\displaystyle\subseteq$ $\displaystyle BD(G)\cup
BD(HCLOSE(H,U))$

The reconstruct.py program checks these two conditions employing the following
two sets.

$\displaystyle IB$ $\displaystyle=$ $\displaystyle BD(HCLOSE(H,U))\backslash
BD(G)$ $\displaystyle HL$ $\displaystyle=$ $\displaystyle
BD(HCLOSE(R\backslash H,U))\backslash BD(G)\backslash IB$

The first set is called inbodies in the program; it comprises the variables
that are involved in implying a variable in $HEADS(B,F)$ and are not in a body
of $G$. The second is called headlessbodies; it comprises the variables that
are involved in implying a variable that is a head in $G$, but cannot do that
because they are neither in $G$ nor in $IB$.

The second set $HL$ is used to determine the second necessary condition, the
one that is independent of $IT$. Making its definition explicit in the
definition tells why.

$\displaystyle HL$ $\displaystyle=$ $\displaystyle BD(HCLOSE(R\backslash
H,U))\backslash BD(G)\backslash IB$ $\displaystyle=$ $\displaystyle
BD(HCLOSE(R\backslash H,U))\backslash
BD(G)\backslash(BD(HCLOSE(H,U))\backslash BD(G))$ $\displaystyle=$
$\displaystyle BD(HCLOSE(R\backslash H,U))\backslash BD(G)\backslash
BD(HCLOSE(H,U))$

The last step is a consequence of the equality between $A\backslash
B\backslash C$ and $A\backslash B\backslash(C\backslash B)$. Since
$A\backslash B$ does contain any element of $B$, subtracting $C$ or
subtracting $C$ without the elements of $B$ is the same.

This reformulation shows that the second necessary condition is the same as
$HL\subseteq\emptyset$. The only subset of an empty set is itself:
$HL=\emptyset$. Since $HL$ does not depend on $IT$, its emptiness can be
checked before entering the loop over the possible sets $IT$.

The first condition is also expressible in terms of $IB$ and $HL$. The first
step is to reformulate the union by placing the intersection in one of the two
sets only: $A\cup B$ is the same as $((A\backslash B)\cup(A\cap
B))\cup{}((B\backslash A)\cup(A\cap B))$; the duplication of $A\cap B$ is not
necessary, making this union the same as $(A\backslash B)\cup(A\cap
B)\cup(B\backslash A)$. This is the same as $A\cup(B\backslash A)$. The first
necessary conditions is reformulated using this property.

$\displaystyle BD(HCLOSE(H,U))\cup(BD(HCLOSE(R\backslash H,U))\backslash
BD(HCLOSE(H,U)))$ $\displaystyle\subseteq BD(G)\cup BD(IT)\hfill$

The union of two sets is contained in the union of $BD(G)$ and $BD(IT)$.
Stated differently, the variables in the two sets that are not in $BD(G)$ are
in $BD(IT)$.

$\displaystyle\begin{array}[]{l}(BD(HCLOSE(H,U))\backslash BD(G))\cup\\\
(BD(HCLOSE(R\backslash H,U))\backslash BD(HCLOSE(H,U))\backslash
BD(G))\end{array}$ $\displaystyle\subseteq BD(IT)$

The two sets in the union are exactly $IB$ and $HL$. The first necessary
condition becomes $IB\cup HL\subseteq BD(IT)$. Since it involves $IT$, it can
only be checked inside the loop. But the loop is not entered at all if $HL$ is
not empty. Therefore, it could be reformulated as $IB\subseteq BD(IT)$. The
program checks the condition including $HL$ to allow disabling the other
necessary condition $HL=\emptyset$ for testing.

Both necessary conditions involve $HEADS(B,F)$, but the program never
calculates it. Rather, it exploits Lemma 53 by replacing $HEADS(B,F)$ with
$RCN(B,F)\backslash\\{x\mid\exists B^{\prime}~{}.~{}B^{\prime}\rightarrow x\in
G\\}$. The lemma proves that either they coincide or the autoreconstruction
algorithm fails and $F$ is not single-head equivalent. The replacing set is
not always the same as the replaced set, but can take its place when checking
the two necessary conditions. This is proved by looking at the two cases
separately:

  * •

if $HEADS(B,F)$ and $RCN(B,F)\backslash\\{x\mid\exists
B^{\prime}~{}.~{}B^{\prime}\rightarrow x\in G\\}$ coincide the two conditions
are unchanged by replacing the former with the latter;

  * •

if $HEADS(B,F)$ and $RCN(B,F)\backslash\\{x\mid\exists
B^{\prime}~{}.~{}B^{\prime}\rightarrow x\in G\\}$ differ the two conditions
may change when replacing the former with the latter; this is not a problem
because these conditions are only necessary; if they are made true, the
program proceeds as if it did not check them, and fails as proved by Lemma 53;
if they are made false they make the program fail immediately. In both cases
the program fails sooner or later. This is correct behavior because $F$ is not
single-head equivalent as proved by Lemma 53.

####  4.13.2 The second necessary condition

The aim of the inner loop of the algorithm is to find a set $IT$ that imitates
a part of $F$. A necessary condition is to optimistically assume that
everything that could possibly be entailed by $IT$ is entailed: the set of its
heads $H$. Since $IT$ is used with $G$, these heads are also plugged into $G$
for further entailments, producing $RCN(B\cup H,G)$. The union $H\cup
RCN(B\cup H,G)$ bounds the variables that $B$ can imply in $G\cup IT$. If it
does not include all of $RCN(B,F)$ in spite of the optimistic assumption,
$G\cup IT$ does not imitate $F$.

This condition only involves the heads of $IT$, not all of it. By
construction, these heads are exactly $HEADS(B,F)$. They are the same for all
sets $IT$. As a result, the condition can be checked before entering the loop
over the possible candidate sets $IT$.

The complication is that $RCN()$ is not the set of variables that can be
entailed. That is $BCN()$. Rather, it is the set of real consequences, the
variables that are entailed not just because they are in $B$. This is why a
formal proof is required.

###### Lemma 75

If $H$ is the set of heads of the formula $E$, then $RCN(B,G\cup E)\subseteq
H\cup RCN(B\cup H,G)$ holds for every formula $G$ that contains no tautology.

Proof. Let $x$ be a variable of $RCN(B,G\cup E)$. By definition, $G\cup E$
entails $(BCN(B,G\cup E)\backslash\\{x\\})\rightarrow x$. Let
$B^{\prime}=BCN(B,G\cup E)\backslash\\{x\\}$ be the body of this clause. The
entailment turns into $G\cup E\models B^{\prime}\rightarrow x$, with $x\not\in
B^{\prime}$.

By Lemma 1, it holds $G\cup E\models B^{\prime}\rightarrow B^{\prime\prime}$
for some clause $B^{\prime\prime}\rightarrow x\in G\cup E$. If this clause is
in $E$ its head $x$ is in $H$ by the premise of the lemma and the claim is
proved.

Otherwise, $B^{\prime\prime}\rightarrow x$ is in $G$. In this case, $x$ is
proved to belong to $RCN(B\cup H,G)$.

Since $B^{\prime}$ is $BCN(B,G\cup E)\backslash\\{x\\}$, it is a subset of
$BCN(B,G\cup E)$. Therefore, all its variables are entailed by $G\cup E\cup
B$. Equivalently, $G\cup E\models B\rightarrow B^{\prime}$. With $G\cup
E\models B^{\prime}\rightarrow B^{\prime\prime}$, it implies $G\cup E\models
B\rightarrow B^{\prime\prime}$.

The head of every clause of $E$ is in $H$ since $H$ is the set of heads of
$E$. As a result, $H\models E$. Together with $G\cup E\models B\rightarrow
B^{\prime\prime}$, it implies $G\cup H\models B\rightarrow B^{\prime\prime}$.
This entailment can be rewritten as $G\models(B\cup H)\rightarrow
B^{\prime\prime}$: every variable of $B^{\prime\prime}$ is implied by $B\cup
H$ according to $G$. Therefore, $B^{\prime\prime}\subseteq BCN(B\cup H,G)$.

Since $G$ contains no tautology by assumption, and
$B^{\prime\prime}\rightarrow x$ is one of its clauses, it is not a tautology:
$x\not\in B^{\prime\prime}$. The containment $B^{\prime\prime}\subseteq
BCN(B\cup H,G)$ strengthens to $B^{\prime\prime}\subseteq BCN(B\cup
H,G)\backslash\\{x\\}$. Since $B^{\prime\prime}\rightarrow x$ is in $G$, it is
also entailed by it: $G\models B^{\prime\prime}\rightarrow x$. By
monotonicity, the body $B^{\prime\prime}$ of this clause can be replaced by
any of its supersets like $BCN(B\cup H,G)\backslash\\{x\\}$, leading to
$G\models(BCN(B\cup H,G)\backslash\\{x\\})\rightarrow x$, which defines $x\in
RCN(B\cup H,G)$.

A condition is necessary if it follows from $SCL(B,F)\cup IT\models BCL(B,F)$
or an equivalent formulation of it, like $UCL(B,F)\equiv UCL(B,G\cup IT)$.

###### Lemma 76

If $UCL(B,F)\equiv UCL(B,G\cup IT)$ then $RCN(B,F)\subseteq HEADS(B,F)\cup
RCN(B\cup HEADS(B,F),F)$.

Proof. Lemma 73 proves that $UCL(B,F)\equiv UCL(B,G\cup IT)$ implies
$RCN(B,F)=RCN(B,G\cup IT)$. Lemma 75 tells that the second formula of the
equality $RCN(B,G\cup IT)$ is a subset of $H\cup RCN(B\cup H,G)$ where $H$ is
the set of heads of $IT$. The heads of $IT$ are $HEADS(B,F)$. A consequence is
$RCN(B,F)\subseteq HEADS(B,F)\cup RCN(B\cup HEADS(B,F),G)$.

When using $H=RCN(B,F)\backslash\\{x\mid\exists
B^{\prime}.B^{\prime}\rightarrow x\in G\\}$ as the heads of $IT$, Lemma 53
applies: if $F$ is single-head equivalent, then $H$ coincides with
$HEADS(B,F)$ by Lemma 53. As a result, $RCN(B,F)\subseteq H\cup RCN(B\cup
HEADS(B,F),F)$ is another consequence of $F$ being single-head equivalent. If
it does not hold, $F$ is not single-head equivalent and the algorithm fails as
required.

The set $H\cup RCN(B\cup HEADS(B,F),G)$ is called maxit in the reconstruct.py
program because it is an upper bound to the set of consequences achievable by
adding whichever set of clauses $IT$ with heads $HEADS(B,F)$ to $G$. Yet, it
does not involve $IT$ itself. Therefore, it can be checked once for all before
entering the loop rather than once for each iteration.

####  4.13.3 The third necessary condition

Since $G\cup IT$ aims at imitating $F$ on the sets $B^{\prime}$ that are
equivalent to $B$, it must have the same consequences. A specific case is
already proved: $RCN(B,G\cup IT)=RCN(B,F)$ as proved by Lemma 73. This
condition extends from $B$ to every equivalent set: $RCN(B^{\prime},G\cup
IT)=RCN(B,F)$ for every $B^{\prime}\equiv_{F}B$. This is mostly proved by the
following lemma.

###### Lemma 77

If $B\equiv_{F}B^{\prime}$ then $RCN(B,F)=RCN(B^{\prime},F)$.

Proof. The definition of $B\equiv_{F}B^{\prime}$ is $F\models B\equiv
B^{\prime}$. This is equivalent to $F\cup B\equiv F\cup B^{\prime}$. The
definition $BCN(B,F)=\\{x\mid F\models B\rightarrow x\\}$ can be rewritten as
$BCN(B,F)=\\{x\mid F\cup B\models x\\}$. Since $F\cup B$ is equivalent to
$F\cup B^{\prime}$, this set is equal to $\\{x\mid F\cup B^{\prime}\models
x\\}$, or $BCN(B^{\prime},F)$. This proves $BCN(B,F)=BCN(B^{\prime},F)$.

As a result, $RCN(B,F)=\\{x\mid F\models(BCN(B,F)\backslash\\{x\\})\rightarrow
x\\}$ can be rewritten as $\\{x\mid
F\models(BCN(B^{\prime},F)\backslash\\{x\\})\rightarrow x\\}$, the definition
of $RCN(B^{\prime},F)$.

The goal is a necessary condition to the dominant operation of the loop, the
check $SCL(B,F) \cup IT\models BCL(B,F)$. Lemma 65 and Lemma 70 prove it
equivalent to $UCL(B,G\cup IT)\equiv UCL(B,F)$, which Lemma 73 proves to imply
$RCN(B,F)=RCN(B,G\cup IT)$. Transitivity with $RCN(B^{\prime},G\cup
IT)=RCN(B,G\cup IT)$ would prove the claim $RCN(B^{\prime},G\cup
IT)=RCN(B,F)$. Unfortunately, the premise $RCN(B^{\prime},G\cup
IT)=RCN(B,G\cup IT)$ is only proved by Lemma 77 if $B\equiv_{G\cup
IT}B^{\prime}$ holds, but the assumption is $B\equiv_{F}B^{\prime}$. The
following lemma provides this missing bit.

###### Lemma 78

If $UCL(B,G\cup IT)\equiv UCL(B,F)$ then $B^{\prime}\equiv_{F}B$ is equivalent
to $B^{\prime}\equiv_{G\cup IT}B$.

Proof. If $G\cup IT$ entails $B^{\prime}\equiv B$ then $F$ entails it as well
because Lemma 50 proves $F\models G\cup IT$.

The converse is now proved: if $F\models B^{\prime}\equiv B$ then $G\cup
IT\models B^{\prime}\equiv B$.

Lemma 36 applies to $F\models B\rightarrow B$ and $F\models B\rightarrow b$
for every $b\in B^{\prime}$, proving $UCL(B,F)\models B\rightarrow b$ for
every $b\in B^{\prime}$, which implies $UCL(B,F)\models B\rightarrow
B^{\prime}$. It also applies to $F\models B\rightarrow B^{\prime}$ and
$F\models B^{\prime}\rightarrow b$ for every $b\in B$, proving
$UCL(B,F)\models B^{\prime}\rightarrow b$, which implies $UCL(B,F)\models
B^{\prime}\rightarrow B$. The conclusion is $UCL(B,F)\models B\equiv
B^{\prime}$.

Since $UCL(B,F)$ is equivalent to $UCL(B,G\cup IT)$ by assumption, also
$UCL(B,G\cup IT)\models B^{\prime}\equiv B$ holds. Since $UCL(B,G\cup IT)$ is
by definition a subset of $G\cup IT$, the claim $G\cup IT\models
B^{\prime}\equiv B$ follows.

The third necessary condition can now be proved.

###### Lemma 79

If $UCL(B,G\cup IT)\equiv UCL(B,F)$, then $RCN(B^{\prime},G\cup IT)=RCN(B,F)$
holds for every $B^{\prime}$ such that $B^{\prime}\equiv_{F}B$.

Proof. Given the premise $UCL(B,G\cup IT)\equiv UCL(B,F)$, Lemma 73 proves
$RCN(B,F)=RCN(B,G\cup IT)$. Lemma 78 proves that $B^{\prime}\equiv_{F}B$
implies $B\equiv_{G\cup IT}B^{\prime}$. Lemma 77 applies: $RCN(B,G\cup
IT)=RCN(B^{\prime},G\cup IT)$. The claim $RCN(B,F)=RCN(B^{\prime},G\cup IT)$
follows by transitivity.

Lemma 65 and Lemma 70 prove that $SCL(B,F) \cup IT\models BCL(B,F)$ is
equivalent to $UCL(B,G\cup IT)\equiv UCL(B,F)$, which implies
$RCN(B^{\prime},G\cup IT)=RCN(B,F)$ for every $B^{\prime}$ such that
$B^{\prime}\equiv_{F}B$. This is a necessary condition. It is used like the
others: in reverse. If $RCN(B,F)\not=RCN(B^{\prime},G\cup IT)$ for some
$B^{\prime}$ that is equivalent to $B$, any further processing of $IT$ is
unnecessary since $SCL(B,F)\cup IT\models BCL(B,F)$ is bound to fail.

From the computational point of view, $RCN(B,F)$ is already known from the
very beginning. The second set $RCN(B^{\prime},G\cup IT)$ can be easily
determined given a body $B^{\prime}$ of a clause in $BCL(B,F)$. The problem is
the possibly large number of such sets $B^{\prime}$. Restricting to
$HCLOSE(HEADS(B,F),UCL(B,F))$ or even to
$MINBODIES(HCLOSE(HEADS(B,F),UCL(B,F)),UCL(B,F)\cap SCL(B,F))$ still leaves
this condition necessary: weaker but easier to check. The singlehead.py
program uses this restriction in the noteq loop.

###  4.14 Too many optimizations, too little time

Some further directions for improvement to the algorithm have not been
investigated enough to prove their correctness and are left unimplemented.

The first undeveloped optimization is turning the third necessary condition
into a sufficient condition. It looks like checking $RCN(B^{\prime},G\cup
IT)=RCN(B,F)$ for all $B^{\prime}\in HCLOSE(HEADS(B,F),UCL(B,F)\cap SCL(B,F))$
is not just necessary to $SCL(B,F)\cup IT\models BCL(B,F)$ but also
sufficient. If so, the following check
$HCLOSE(RCN(B,F),UCL(B,F))=HCLOSE(RCN(B,G\cup IT),UCL(B,G\cup IT))$ is
redundant.

The second undeveloped optimization is a simplification of the check
$HCLOSE(RCN(B,F),UCL(B,F))=HCLOSE(RCN(B,G\cup IT),UCL(B,G\cup IT))$. A subset
of $HCLOSE(RCN(B,F),UCL(B,F))$ is already known: $HCLOSE(HEADS(B,F),UCL(B,F))$
is computed to determine the possible sets $IT$ to test. Restricting the check
to $HCLOSE(HEADS(B,F),UCL(B,F))=HCLOSE(HEADS(B,F),UCL(B,G\cup IT))$ saves time
both because the first formula is already known and because the second is
easier to compute due to the smaller first argument.

This is not correct in general, as various examples in bnotheads.py show. One
of them is the following.

$\displaystyle F$ $\displaystyle=$ $\displaystyle\\{ab\equiv ef,a\equiv c\\}$
$\displaystyle=$ $\displaystyle\\{ab\rightarrow e,ab\rightarrow
f,ef\rightarrow a,ef\rightarrow b,a\rightarrow c,c\rightarrow a\\}$

$a$$b$$c$$f$$e$

Since $SCL(B,F)$ is $\\{a\rightarrow c,c\rightarrow a\\}$ when $B=\\{a,b\\}$,
the variable $a$ is not in $SFREE(B,F)$, and therefore not in $HEADS(B,F)$.
Therefore, $ef\rightarrow a$ is never in $IT$. Yet, its absence goes
undetected because it is not in $HCLOSE(HEADS(B,F),UCL(B,F))$ either.

The third necessary condition catches the anomaly: $a$ is in $RCN(B,F)$ but
not in $RCN(\\{e,f\\},G\cup IT)$ since no $IT$ contains a clause of head $a$.
This is however specific to this case, as the following counterexample still
from bnotheads.py shows.

$\displaystyle F$ $\displaystyle=$ $\displaystyle\\{ab\equiv ef,a\equiv
c,b\equiv d)$ $\displaystyle=$ $\displaystyle\\{ab\rightarrow e,ab\rightarrow
f,ef\rightarrow a,ef\rightarrow b,a\rightarrow c,c\rightarrow a,b\rightarrow
d,d\rightarrow b\\}$

$a$$b$$c$$f$$e$$d$

Again, $a\not\in HEADS(B,F)$ causes $ef\rightarrow a$ not to be in
$HCLOSE(HEADS(B,F),UCL(B,F))$. However, $b$, $c$ and $d$ are not in
$HEADS(B,F)$ either, making $ef\rightarrow b$, $ef\rightarrow c$,
$ef\rightarrow d$ not being in $HCLOSE(HEADS(B,F),UCL(B,F))$. As a result,
$\\{e,f\\}$ is not a body of $HCLOSE(HEADS(B,F),UCL(B,F))$. The equality
$RCN(\\{e,f\\},G\cup IT)=RCN(B,F)$ is not even checked.

An undetected inequality like this is due to some sets $B^{\prime}$ not being
recognized as equivalent to $B$. In turns, this seems to be only possible if
$B\cap HEADS(B,F)=\emptyset$, but this is yet to be proved. If proved, the
optimization can be employed if $B\cap HEADS(B,F)\not=\emptyset$, resorting to
the general condition $HCLOSE(RCN(B,F),UCL(B,F))=HCLOSE(RCN(B,G\cup
IT),UCL(B,G\cup IT))$ otherwise.

The third undeveloped optimization is that associating a body to a variable
$x\in HEADS(B,F)$ is easy if $x$ is not in any of the possible bodies of $IT$.
This condition is easy to check: $x\not\in\bigcup T$.

All clauses in $ITERATION(B,F)$ are in $BCL(B,F)$ by definition: they are
nontautological clauses $B^{\prime}\rightarrow x$ entailed by $F$ that meet
$B\equiv_{F}B^{\prime}$. When building a clause for the head $x$, all
acceptable bodies are equivalent to $B$ according to $F$, and are therefore
all equivalent to each other. Since they are equivalent, they are the same.
Any one will do. Even just $B$.

Why the requirement $x\not\in\bigcup T$, then? Because $B\equiv_{F}B^{\prime}$
is equivalence according to $F$, not to $G\cup IT$. Equivalence according to
$G\cup IT$ is still to be achieved. The following formula (in outloop.py)
clarifies this point.

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

The heads for $B=\\{a\\}$ are $HEADS(B,F)=\\{a,b,c,x\\}$. The task is to
produce a body for each of these variables. The simplified rule lets $B$ be
the body for all.

This is correct for $x$: the clause $a\rightarrow x$ is a valid choice for a
clause with head $x$. It is in the equivalent single-head formula
$F^{\prime}$, for example:

$F^{\prime}=\\{a\rightarrow x,a\rightarrow b,b\rightarrow c,c\rightarrow x\\}$

The same choice does not work for $b$ and $c$: no single-head formula
equivalent to $F$ contains both $a\rightarrow b$ and $a\rightarrow c$. For
example, the latter cannot replace $b\rightarrow c$ in $F^{\prime}$ even if
their bodies are equivalent because the equivalence $a\equiv_{F}b$ extends to
$F^{\prime}$ only as consequence of $b\rightarrow c$.

This mechanism does not work because it relies on body equivalences that are
not achieved yet. Saying that $B\rightarrow x$ is as good as
$B^{\prime}\rightarrow x$ because $B$ is equivalent to $B^{\prime}$ anyway is
incorrect because $B^{\prime}\rightarrow x$ may be necessary to ensure this
equivalence.

This is not the case for $x$. Visually, $x$ is outside any loop.

$a$$b$$c$$x$

Technically, if $x$ is not in $\bigcup T$ it cannot contribute to the
equivalence of $B$ with any other set $B^{\prime}$. Equivalence requires going
from a set to another and back. Instead, $x$ can only be entailed. It cannot
entail. Since $B^{\prime}\rightarrow x$ is unnecessary to $B^{\prime}\equiv
B$, removing it does invalidate this equivalence. Therefore, $B\rightarrow x$
still entails $B^{\prime}\rightarrow x$, constituting a valid replacement.

This optimization would use $H^{\prime}=H\cap\bigcup T$ in place of $H$ and
search for a set $IT$ that meets $HCLOSE(RCN(B,F)\cap\bigcup
T,UCL(B,F))={}HCLOSE(RCN(B,G\cup IT)\cap\bigcup T,UCL(B,G\cup IT))$ instead of
$HCLOSE(RCN(B,F),UCL(B,F))={}HCLOSE(RCN(B,G\cup IT),UCL(B,G\cup IT))$. On
success, a clause $B\rightarrow x$ for every $x\in H\backslash H^{\prime}$ is
added to $G$ along with $IT$.

Most of the other examples in this article and in the test directory of the
singlehead.py program would not benefit from this optimization. This is
probably a distortion due to the nature of the technical analysis of the
problem and its algorithms. What makes single-head equivalence difficult from
the theoretical and implementation point of view is establishing equivalence
of sets $B^{\prime}$ with $B$; this is why most examples revolve around this
case. Variables that are entailed but not in a loop are simple to deal with.
Examples that contain them are not significant.

Not significant to the technical analysis of the problem does not mean not
significant to the problem itself.

To the contrary, this optimization may dramatically increase performance. For
example, the algorithm is fast at telling that Formula 2 is not single-head
equivalent because it only needs to test the possible associations of three
heads $H=\\{x,a,b\\}$ with three bodies $\\{b,d\\}$, $\\{a,c\\}$ and
$\\{x\\}$. Adding easy clauses like $x\rightarrow y_{i}$ with $i=1,\ldots,n$
creates $n$ new heads, exponentially increasing the number of associations to
test. This is wasted time, since their bodies can for example be all
$\\{x\\}$.

$F=\\{x\rightarrow a,a\rightarrow d,x\rightarrow b,b\rightarrow
c,ac\rightarrow x,bd\rightarrow x\\}$ (2)

This formula is in the file disjointnotsingle.py, the variant with the two
additional clauses in insignificant.py.

The fourth unimplemented optimization would allow establishing that a formula
is not single-head equivalent without a single entailment test. It is based on
a counting argument, a calculation of the number of necessary clauses. The
following example illustrates its principle.

$a$$d$$b$$e$$c$$f$

A box stands for a set of variables that is equivalent to the others:
$\\{a,b,c\\}\equiv\\{a,d\\}\equiv\\{b,e\\}\equiv\\{c,f\\}$. The equivalence
between $\\{a,b,c\\}$ and $\\{a,d\\}$ is for example realized by
$abc\rightarrow d$, $ad\rightarrow b$ and $ad\rightarrow c$: each variable
that is in a set but not in the other is implied by the other. The file for
this formula is disjointemptynotsingle.py.

The bodies of the formula are the equivalent sets; therefore, they are all
equivalent to each other. The first precondition chosen by the program could
for example be $\\{a,b,c\\}$. Regardless, $SCL(B,F)$ is empty. The
singlehead.py program disproves the formula single-head equivalent testing
4096 combinations of heads and bodies.

This computation can be skipped altogether by just counting the number of
necessary clauses. Since $\\{a,d\\}$ implies the other equivalent sets and
only the equivalent sets imply something, $G\cup IT$ must contain some clauses
that make $\\{a,d\\}$ directly imply at least another equivalent set:
$\\{a,b,c\\}$, $\\{b,e\\}$ or $\\{c,f\\}$. Each contains two variables not in
$\\{a,d\\}$, requiring two clauses. For example, $ad\rightarrow b$ and
$ad\rightarrow c$ are required to imply $\\{b,c\\}$ from $\\{a,d\\}$. They are
irredundant as $a$ alone does not imply anything in $F$, nor does $d$.

The same applies to the other three equivalent sets: two clauses each. The
total is eight clauses. They are all different: the clauses for different
equivalent sets are different because the equivalent sets all differ from each
other; the two clauses for the same equivalent set are different because they
have different heads. The eight clauses are all different.

The variables are only six; a single-head formula contains at most six
clauses. The formula is not single-head equivalent because no equivalent
formula contains less than eight clauses.

This mechanism generalizes to all formulae that contain equivalent sets of
variables. For each of them $B^{\prime}$, the number of variables in the
minimal difference $B^{\prime\prime}\backslash B^{\prime}\backslash
SFREE(B,F)$ to another equivalent set $B^{\prime\prime}$ is counted. The
variables not in $SFREE(B,F)$ are discarded, as implicitly done on the example
where $SCL(B,F)=\emptyset$. The total is the minimal number of necessary
clauses. If it is larger than the number of heads, the formula is not single-
head equivalent.

When determining the equivalent sets of variables, only the minimal ones
count. For example, the sets that matter in $F=\\{a\rightarrow b,b\rightarrow
a,a\rightarrow c\\}$ are only $\\{a\\}$ and $\\{b\\}$, not $\\{a,c\\}$ and
$\\{b,c\\}$.

This condition is only necessary, as some formulae have less equivalent sets
than heads but are not single-head equivalent anyway. An example is the
formula $ab\equiv bc\equiv ca\equiv de\equiv ef\equiv fd$. Each set can imply
another with a single clause. For example, $\\{c,a\\}$ implies $\\{b,c\\}$
thanks to $ca\rightarrow b$ only.

$ca$$ab$$de$$ef$$bc$$fd$

The counting condition is satisfied. Yet, the six clauses it counts as
necessary only realize the two loops of equivalences. Other clauses are
necessary to link the two, outnumbering the heads.

The final undeveloped variant is not an optimization of the algorithm but a
way to make it produce a meaningful result even if the input formula is not
single-head equivalent. At each step, the set of heads of the candidate set
$IT$ is $RCN(B,F)$ minus the heads of the formula under construction $G$. If
the formula is single-head equivalent, the result is equal to $HEADS(B,F)$.
Otherwise, the autoreconstruction algorithm fails as proved by Lemma 53.

This mechanism presumes that a single-head formula equivalent to $F$ is the
only goal; if none exists, no output is necessary. This may not be the case. A
formula that contains just a pair of clauses with the same head is almost as
good as one containing none: forgetting requires only one true
nondeterministic choice, which only doubles the running time. Double is still
polynomial.

The goal extends from finding a single-head formula to a formula containing
few duplicated heads. It is achieved by adding a clause $B^{\prime}\rightarrow
x$ for each $x\in RCN(B,F)\backslash RCN(B,G\cup IT)$.

##  5 Polynomial or NP-complete?

The reconstruction algorithm requires a valid iteration function, which in
turn requires testing the possible association of some bodies to some heads.
These associations may be exponentially many. The algorithm takes exponential
time if so.

Is this specific to the reconstruction algorithm? Or is the problem itself
that requires exponential time to be solved?

While no proof of NP-hardness is found so far, at least the problem is not
harder than NP. The considered decision problem is: does the formula have an
equivalent formula that is single-head? Testing all equivalent formulae for
both equivalence and single-headness is not feasible even in nondeterministic
polynomial time since formulae may be arbitrarily large. Single-headness caps
that size, since it allows at most one clause for each head. A single-head
formula may at most contain a clause for each variable.

###### Theorem 2

Checking whether a formula is equivalent to a single-head formula is in NP.

Proof. Equivalence to a single-head formula can be established by a
nondeterministic variant of the reconstruction algorithm, where $IT$ is not
looped over but is uniquely determined by guessing a body for each variable in
$HEADS(B,F)$. Technically, the loop “for all $IT$…” is replaced by
“nondeterministically assign an element of $T$ to each element of $H$”. The
resulting algorithm is polynomial.

Proving membership to NP only takes a short paragraph. Proving NP-hardness is
a completely different story. The rest of this section gives clues about it.

A proof of NP-hardness is a reduction from some other NP-hard problem to that
of telling whether $F$ is single-head equivalent. Given an instance of the
problem that is known NP-hard, it requires building a formula that is single-
head equivalent or not depending on that instance. This is generally done by
some sort of formula template, a scheme that has some parts left partially
unspecified. The specific NP-hard problem instance fills these so that the
resulting concrete formula is either single-head or not depending on it.

While no such reduction is known, still something can be said about the
formula schemes that work and the ones that do not.

Lemma 22 tells that single-head equivalence requires two things: first,
$HEADS(B,F)$ and $HEADS(B^{\prime},F)$ are disjoint whenever
$B\not\equiv_{F}B^{\prime}$; second, $ITERATION(B,F)$ is single-head.

The first condition is polynomial. A reduction that only exploits it would
reduce a NP-hard problem to a polynomial one. Winning the million dollar price
at stake for it [Coo03] would be certainly appreciated, but seems unlikely.
Rather, it suggests that a NP-hard proof is not based on the disjointness of
heads.

The reduction, if any, is based on the other condition: the existence of a
valid iteration function such that $ITERATION(B,F)$ is single-head. This is
exactly where the autoreconstruction algorithm spends more time: testing all
associations of the bodies in $T$ to the heads in $H$. A reduction from the
propositional satisfiability of a formula $G$ to the single-head equivalence
of $F$ would probably hinge around a single, fixed set $B$:

  * •

$HEADS(B^{\prime},F)$ and $HEADS(B^{\prime\prime},F)$ are disjoint for all
$B^{\prime}\not\equiv_{F}B^{\prime\prime}$ regardless of $G$;

  * •

$SCL(B,F)$ is independent on $G$, or maybe only depends on the variables of
$G$;

  * •

$B$ is a fixed set of variables, maybe a singleton; maybe it is a set that
only depends on the variables of $G$;

  * •

$G$ is satisfiable if and only if a single-head subset of
$HCLOSE(HEADS(B,F),UCL(B,F))$ entails $BCL(B,F)$ with $SCL(B,F)$.

The core of the reduction is the last point: the satisfiability of $G$
corresponds to the existence of a single-head subset $IT$ of
$HCLOSE(HEADS(B,F),UCL(B,F))$ satisfying $SCL(B,F)\cup IT\models BCL(B,F)$,
where $B$ is fixed. The clauses of $F\cap SCL(B,F)$ may support this
construction; or maybe they are just not needed, and $F$ is entirely made of
clauses of $BCL(B,F)$. Whether $SCL(B,F)$ is necessary or not might further
restrict the range of possible reductions. The clauses of $SCL(B,F)$ and
$BCL(B,F)$ differ in an important way when it comes to ensuring $SCL(B,F)\cup
IT\models BCL(B,F)$, as explained in the next section.

###  5.1 What do clauses do?

While searching for a proof of NP-hardness for the single-head equivalence
problem, an observation emerged: clauses in $SCL(B,F)$ and in $ITERATION(B,F)$
differ in a fundamental point: which and how many clauses of $BCL(B,F)$ they
collaborate to imply.

All clauses of $BCL(B,F)$ have the form $B^{\prime}\rightarrow x$ with
$B^{\prime}\equiv_{F}B$. Apart the case where $B$ is only equivalent to
itself, this means that $B^{\prime}$ entails $B$ and all other sets equivalent
to $B$. This is not possible if $SCL(B,F)\cup ITERATION(B,F)$ does not contain
at least a clause that can be applied from $B^{\prime}$: a clause whose body
is contained in $B^{\prime}$. This clause makes $B^{\prime}$ entail another
equivalent set, which in turn entail another in the same way. This clause may
belong to $SCL(B,F)$ or to $BCL(B,F)$.

$B^{\prime\prime}\rightarrow x\in SCL(B,F)$

may have a body $B^{\prime\prime}$ that is a subset of multiple sets
$B^{\prime}$ that are equivalent to $B$; therefore,
$B^{\prime\prime}\rightarrow x$ may be a starting point of implication from
many differing $B^{\prime}$;

$B^{\prime\prime}\rightarrow x\in ITERATION(B,F)$

implies that $B^{\prime\prime}$ is exactly one of these sets that are
equivalent to $B$; therefore, $B^{\prime\prime}\rightarrow x$ may only be the
starting point of implications from $B^{\prime}=B^{\prime\prime}$ itself.

The hard task for $ITERATION(B,F)$ is to realize all equivalences
$B^{\prime}\equiv B$ entailed by $F$. As explained in the previous sections,
the clauses not involved in implying such equivalences are easy to find.
Equivalences are mutual entailments and are therefore broken down into
entailments like $B^{\prime}\rightarrow B^{\prime\prime}$ where both
$B^{\prime}$ and $B^{\prime\prime}$ are equivalent to $B$ according to $F$.
The difference between a clause of $SCL(B,F)$ and one of $ITERATION(B,F)$ is
that the first can be used to realize many implications $B^{\prime}\rightarrow
B^{\prime\prime}$, the second only the ones starting from its body.

The following example clarifies the difference: $F=\\{a\equiv b,ac\rightarrow
d,ad\rightarrow e,ae\rightarrow c\\}$ when $B=\\{a,c\\}$.

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

The clauses of strictly entailed bodies are $SCL(B,F)=\\{a\equiv b\\}$. The
bodies equivalent to $B$ are $\\{a,c\\}$, $\\{a,d\\}$, $\\{a,e\\}$,
$\\{b,c\\}$, $\\{b,d\\}$, and $\\{b,e\\}$. The clause $ad\rightarrow e\in
BCL(B,F)$ can only be used when $B^{\prime}=\\{a,d\\}$ is true. It only allows
the direct implication $ad\rightarrow ae$. On the other hand, the clause
$a\rightarrow b\in SCL(B,F)$ entails $ac\rightarrow bc$, $ad\rightarrow bd$
and $ae\rightarrow be$.

$a\rightarrow b$$a\rightarrow b$$a\rightarrow b$$ad$$bd$$ad\rightarrow
e$$ae$$ac$$bc$$be$

###  5.2 Counterexamples

Lemma 22 implies that $HEADS(B,F)$ and $HEADS(B^{\prime},F)$ are always
disjoint if $F$ does not entail $B\equiv B^{\prime}$ and is single-head
equivalent. This is however only a necessary condition, as sufficiency also
requires the existence of a valid iteration function such that
$ITERATION(B,F)$ is single-head.

Since $HEADS(B,F)\cap HEADS(B^{\prime},F)=\emptyset$ is easy to check for
fixed $B$ and $B^{\prime}$, a proof of NP-hardness cannot be based on it. It
should instead hinge around the other condition. For example, it produces
formulae that always have disjoint $HEADS(B,F)$, but have a single-head
$ITERATION(B,F)$ if the given formula is satisfiable.

Such a reduction may result from generalizing one of the example formulae that
have disjoint $HEADS(B,F)$ but $ITERATION(B,F)$ is not single-head.

  1. 1.

A set entails two equivalent sets; achieving equivalence requires them to
entail another equivalent set each, but this requires two clauses with the
same head.

Technically, $SCL(B,F)$ implies $A\rightarrow B$, $A\rightarrow C$ but no
other entailment among the minimal $F$-equivalent sets $A$, $B$, $C$ and $D$.
Some other entailments are required to make the four sets equivalent. For
example, to make $B$ equivalent to the other sets, it has to imply at least
one of them. Since the clauses of $SCL(B,F)$ do not suffice, some clauses from
$BCL(B,F)$ are needed. Such clauses have body $B$ because they are directly
applicable from $B$ (their body is a subset of $B$) and are not in $SCL(B,F)$
(their body is not a proper subset of $B$). At least one clause $B\rightarrow
x$ is necessary. For the same reason, $C\rightarrow y$ and $D\rightarrow z$
are also necessary, but cannot be entailed from single-head clauses.

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

This example is in the disjointnotsingle.py file. As required, $SCL(B,F)$
implies $A\rightarrow B$ and $A\rightarrow C$ and nothing else. Realizing all
equivalences among $A$, $B$, $C$ and $D$ requires completing the loops: while
$A$ already implies other equivalent sets, $B$, $C$ and $D$ do not. This can
only be done with clauses of $BCL(B,F)$. Since tautologies are useless and
heads in $SCL(B,F)$ are forbidden, the only possible clauses for $B$ are
$B\rightarrow b$ and $B\rightarrow x$; this respectively leaves $C\rightarrow
x$ or $C\rightarrow a$ for $C$. Either $a$ or $b$ is the head of one such
clause. This leaves only the other one to $D$, but neither $D\rightarrow a$
alone nor $D\rightarrow b$ alone is enough to make $D$ entail the other
equivalent sets. The problem can be attributed to the presence of $D$, since
all equivalences are otherwise completed by $B\rightarrow b$ and $C\rightarrow
a$.

The problem may show up even if $SCL(B,F)$ is empty. The counterexample is in
disjointemptynotsingle.py. It makes $ad$, $be$, $cf$ and $abc$ equivalent.
Each of them should imply another; since $SCL(B,F)$ is empty, this can only be
done by clauses having them as bodies. Since each body differs from the others
by two variables, the total is eight clauses. The variables are only six,
insufficient for eight single-head clauses.

$a$$d$$b$$e$$c$$f$

  2. 2.

The same variable is necessary for two entailments among equivalent sets. For
example, $F$ entails both $A\rightarrow B$ and $C\rightarrow D$, but $B$ and
$D$ contain the same variable. An example is $A=\\{a,b\\}$, $B=\\{c,d\\}$,
$C=\\{a,e\\}$ and $D=\\{c,f\\}$ with the formula in the file
disjointemptynotsingle.py.

..............................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................$a$$a$$c$$b$$d$$e$$c$$f$

Starting from $\\{a,b\\}$, the $SCL(B,F)$ part of $F$ already entails $d$,
which is part of the equivalent set $\\{c,d\\}$. This calls for $ab\rightarrow
c$. The same applies to $\\{a,e\\}$ and $ae\rightarrow c$, which has the same
head.

The variables $a$ and $c$ and shown twice to emphasize the structure of the
closed chain $A$, $B$, $C$ and $D$. Without the repetition the formula looks
like the following figure. The two clauses with head $a$ can be replaced by
$c\rightarrow a$.

$d$$b$$c$$e$$f$$a$

  3. 3.

The formula requires connecting too many equivalent sets. All examples shown
so far show some “local” issues: a path of equivalent sets that cannot be
completed to form a loop. Other counterexamples allow each set to entail
another, but the resulting graph of equivalent sets of variables is
disconnected, like the formula in disconnected.py:

$F=\\{abc\equiv def,def\equiv ghi,ghi\equiv jk,jk\equiv mn,mn\equiv
abc,a\rightarrow d,e\rightarrow g,i\rightarrow c,j\rightarrow m,q\rightarrow
n\\}$

The binary clauses in $SCL(B,F)$ push $ITERATION(B,F)$ toward entailing
$abc\rightarrow def$, $def\rightarrow ghi$ and $ghi\rightarrow abc$, closing
the loop short of including $jm$ and $qn$.

Looking at every single part of the formula in isolation it looks single-head
equivalent, since each equivalent set can entail another. The problem is
producing a single loop that reaches all of them. This shows that single-head
equivalence is not a local property that can be checked by looking only at the
individual equivalent sets of variables.

##  6 Python implementation

The reconstruct.py Python program implements the algorithm described in
Sections 3 and 4. It is available at
https://github.com/paololiberatore/reconstruct.

It takes either a sequence of clauses or a file name as commandline options.
Formulae like ab->cd and df=gh are translated into clauses. Examples
invocations are:

    reconstruct.py -f ’ab->cd’ ’df=gh’
    reconstruct.py -t tests/chains.py

After turning ab->cd into $ab\rightarrow c$ and $ab\rightarrow d$ and turning
df=gh into $df\rightarrow g$, $hg\rightarrow f$, $df\rightarrow h$ and
$hg\rightarrow d$, it removes the tautologies from them, if any.

The reconstruction algorithm described in Section 3 with the iteration
function in Section 4 is implemented in the reconstruct(f) function. The loops
over the bodies of the formula and over the candidate set of clauses for the
iteration function are in this function. This is because the optimized method
for the latter uses a number of sets accumulated by the former: the set of
clauses under construction, their heads, their bodies and the clauses of the
original formula used so far. Only the calculation of $RCN()$, $UCL()$,
$HCLOSE()$ and the search for the minimal bodies are split into separate
functions: rcnucl(b, f), hclose(heads, usable) and minbodies(f). The first is
copied verbatim from the implementation of the incomplete algorithm described
in a previous article [Lib20c].

The function rcnucl(b,f) is first called on each body of the formula, and the
results stored. These are used to check for example $A\leq_{F}B$. This
condition is indeed the same as $F\models B\rightarrow A$, which is the same
as $BCN(A,F)\subseteq BCN(B,F)$, in turn equivalent to as $A\cup
RCN(A,F)\subseteq B\cup RCN(B,F)$.

For each precondition $B$, the candidate values for $ITERATION(B,F)$ are
produced by first calculating the required heads $HEADS(B,F)$ and attaching
the allowed bodies to them in all possible ways. All property of valid
iteration functions hold by construction except $G\cup ITERATION(B,F)\models
BCL(B,F)$, which is checked as $HCLOSE(RCN(B,F),UCL(B,F))=HCLOSE(RCN(B,G\cup
IT),UCL(B,G\cup IT))$ using hclose(heads, usable) and rcnucl(b, f).

The algorithm is complete, but slower than the incomplete algorithm presented
in the previous article [Lib20c]. The number of candidate sets for
$ITERATION(B,F)$ may exponentially increase with the number of variables. This
happens when a set of variables $B$ is equivalent to many minimal equivalent
sets. Such equivalences are due to loops of clauses. They are the reason why
the previous algorithm is incomplete, and they make the present one
exponential in time.

##  7 Conclusions

The algorithm for turning a formula in single-head form if possible is correct
and complete, but may take exponential time. It complements the previous
algorithm, which is polynomial but incomplete [Lib20c], rather than overcoming
it. Which of them is the best depends on the goal.

If the goal is to reduce the size of forgetting rather than computing it
quickly, completeness wins over efficiency. The formulae that are not turned
into single-head form by the previous algorithm are by the present one.
Forgetting from them produces polynomially-sized formulae. Running time is
sacrificed on the altar of size reduction.

If the goal is to forget quickly, spending exponential time on preprocessing
is self-harming. Forgetting may take polynomial time on the single-head
formula, but producing it took exponential time. Better spend less time
preparing the formula, and rather jump straight to forgetting.

The present algorithm may still be of use in the second case. What it does is
to reconstruct the formula by groups of clauses of equivalent bodies. If a
group takes too long, the reconstruction can be cut short by just producing
the clauses with these bodies in the original formula. This part of the output
formula may not be single-head, but the rest will. Since the efficiency of
forgetting depends on the number of duplicated heads, this is still an
improvement.

The two algorithms can be applied in turn. The old computes a formula
$SHMIN(F)$ that is always single-head but may not be equivalent to the
original. Only if it is not the second, slower algorithm is run. It may take
advantage of $SHMIN(F)$. When searching for the clauses with a certain set of
heads, the ones from $SHMIN(F)$ may be tested first.

Given that the only source of exponentiality in time are cycles of clauses, it
makes sense to simplify them as much as possible. A way to do it is to merge
equivalent sets of variables. As an example, if the formula under construction
entails the equivalence of $A$ and $B$, only one of them is really necessary.
For example, every occurrence of $B$ can be replaced by $A$. This is a
simplification because it negates the need to test both
$(A\cup\\{y\\})\rightarrow x$ and $(B\cup\\{y\\})\rightarrow x$ as possible
clauses for the head $x$. A followup article [Lib20d] further analyzes this
trick.

A specific formula that turned out important during the analysis of the
algorithm is $F=\\{x\rightarrow a,a\rightarrow d,x\rightarrow b,b\rightarrow
c,{}ac\rightarrow x,bd\rightarrow x\\}$, in the disjointnotsingle.py test file
of the singlehead.py program.

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

It is not single-head because the four sets $A$, $B$, $C$ and $D$ are
equivalent, but only three heads are available: $a$, $b$ and $x$. The other
two variables are already the heads of $a\rightarrow d$ and $b\rightarrow c$.

A formula may also not be single-head equivalent for other reasons, but
examples for these cases are much simpler than this. They range from two to
three binary clauses. They are quite immediate. The relative size of this one,
with six clauses including two ternary ones, witnesses the complexity of this
case.

Given that the first algorithm is polynomial but incomplete and the second is
complete but not polynomial, a natural question is whether a complete and
polynomial algorithm exists. If so, the problem of recognizing whether a
formula is single-head equivalent would be tractable. This problem is in the
complexity class NP, but whether it is NP-complete or not is an open question.

Another open question is the applicability of the algorithms outside the Horn
fragment of propositional logic.

In the general propositional case, resolving all occurrences of a variable
forgets the variable. This is the same as viewing a clause like $\neg a\vee
b\vee c$ as an implication $a\neg b\rightarrow c$. If no other occurrence of
$c$ is positive, it is forgotten by replacing every negative occurrence of it
with $a\neg b$. The size increase is only linear in the single-head case. The
question is whether the algorithms for turning a formula in single-head form
extends to the general propositional case.

The problem complicates when forgetting multiple variables, since the
replacement may multiply the number of positive occurrences of other
variables, like $a$ in this case. An alternative is to apply the replacing
algorithm only to the definite Horn clauses of the formula. In the example, a
clause like $\neg c\vee d\vee e$ would be left alone, and $c$ only replaced by
definite Horn clauses like $\neg c\vee\neg d\vee e$, equivalent to
$dc\rightarrow e$. The remaining occurrences of $c$ are then forgotten by
resolving them out. If the formula contains few non-Horn clauses, this
procedure may be relatively efficient.

This second mechanism would probably apply to every logic that includes the
definite Horn fragment. Information like “this, this and this imply that” is
common, so definite Horn clauses are likely to be present in large number.
Turning them into single-head formula would allow to efficiently forget them
before turning to the others.

## References

  * [AEW12] G. Antoniou, T. Eiter, and K. Wang.  Forgetting for defeasible logic.  In Proceedings of the eighteenth conference on Logic for Programming, Artificial Intelligence, and Reasoning (LPAR-18), volume 7180 of Lecture Notes in Computer Science, pages 77–91. Springer, 2012.
  * [BK94] A.J. Bonner and M. Kifer.  An overview of transaction logic.  Theoretical Computer Science, 133(2):205–265, 1994.
  * [Boo54] G. Boole.  Investigation of The Laws of Thought, On Which Are Founded the Mathematical Theories of Logic and Probabilities.  Walton and Maberly, 1854.
  * [BV06] R. Bělohlávek and V. Vychodil.  Fuzzy horn logic i.  Archive for Mathematical Logic, 45(1):3–51, 2006.
  * [Coo03] Stephen Cook.  The importance of the P versus NP question.  Journal of the ACM, 50(1):27–29, 2003.
  * [Del17] J.P. Delgrande.  A knowledge level account of forgetting.  Journal of Artificial Intelligence Research, 60:1165–1213, 2017\.
  * [DW15] J.P. Delgrande and K. Wang.  A syntax-independent approach to forgetting in disjunctive logic programs.  In Proceedings of the Twenty-Ninth Conference on Artificial Intelligence (AAAI 2015), pages 1482–1488. AAAI Press, 2015.
  * [EF07] E. Erdem and P. Ferraris.  Forgetting actions in domain descriptions.  In Proceedings of the Twenty-Second AAAI Conference on Artificial Intelligence (AAAI 2007), pages 409–414. AAAI Press, 2007.
  * [EIS+06] T. Eiter, G. Ianni, R. Schindlauer, H. Tompits, and K. Wang.  Forgetting in managing rules and ontologies.  In 2006 IEEE / WIC / ACM International Conference on Web Intelligence (WI 2006), 18-22 December 2006, Hong Kong, China, pages 411–419. IEEE Computer Society Press, 2006.
  * [EKI19] T. Eiter and G. Kern-Isberner.  A brief survey on forgetting from a knowledge representation and perspective.  KI — Kuenstliche Intelligenz, 33(1):9–33, 2019.
  * [EL00] T. Eiter and T. Lukasiewicz.  Default reasoning from conditional knowledge bases: Complexity and tractable cases.  Artificial Intelligence, 124(2):169–241, 2000.
  * [FAS+20] R. Feng, E. Acar, S. Schlobach, Y. Wang, and W. Liu.  On sufficient and necessary conditions in bounded ctl: A forgetting approach.  In Proceedings of the Seventeenth International Conference on Principles of Knowledge Representation and Reasoning, (KR 2020), pages 361–370, 2020.
  * [FHMV95] R. Fagin, J.Y. Halpern, Y. Moses, and M. Vardi.  Reasoning about knowledge.  The MIT Press, 1995.
  * [GKL16] R. Gonçalves, M. Knorr, and J. Leite.  The ultimate guide to forgetting in answer set programming.  In Proceedings of the Fifteenth International Conference on Principles of Knowledge Representation and Reasoning (KR 2016), pages 135–144. AAAI Press, 2016.
  * [GKLW17] R. Gonçalves, M. Knorr, J. Leite, and S. Woltran.  When you must forget: Beyond strong persistence when forgetting in answer set programming.  Theory and Practice of Logic Programming, 17(5-6):837–854, 2017\.
  * [Got92] G. Gottlob.  Complexity results for nonmonotonic logics.  Journal of Logic and Computation, 2(3):397–425, 1992.
  * [KRH13] M. Krötzsch, S. Rudolph, and P. Hitzler.  Complexities of horn description logics.  ACM Transactions on Computational Logic, 14(1):1–36, 2013.
  * [KWW09] B. Konev, D. Walther, and F. Wolter.  Forgetting and uniform interpolation in extensions of the description logic EL.  In Proceedings of the 22nd International Workshop on Description Logics (DL 2009), volume 9, 2009.
  * [Lib20a] P. Liberatore.  Common equivalence and size after forgetting.  Computing Research Repository (CoRR), abs/2006.11152, 2020.
  * [Lib20b] P. Liberatore.  The ghosts of forgotten things: A study on size after forgetting.  Computing Research Repository (CoRR), abs/2005.04123, 2020.
  * [Lib20c] P. Liberatore.  One head is better than two: a polynomial restriction for propositional definite horn forgetting.  Computing Research Repository (CoRR), abs/2009.07497, 2020.
  * [Lib20d] P. Liberatore.  Reconstructing a single-head formula to facilitate logical forgetting.  Unpublished, 2020.
  * [LLM03] J. Lang, P. Liberatore, and P. Marquis.  Propositional independence — formula-variable independence and forgetting.  Journal of Artificial Intelligence Research, 18:391–443, 2003.
  * [LM10] J. Lang and P. Marquis.  Reasoning under inconsistency: A forgetting-based approach.  Artificial Intelligence, 174(12-13):799–823, 2010.
  * [LR94] F. Lin and R. Reiter.  Forget it!  In Proceedings of the AAAI Fall Symposium on Relevance, pages 154–159, 1994.
  * [Mak87] J.A. Makowsky.  Why horn formulas matter in computer science: Initial structures and generic examples.  Journal of Computer and System Sciences, 34(2-3):266–292, 1987\.
  * [Moi07] Y. Moinard.  Forgetting literals with varying propositional symbols.  Journal of Logic and Computation, 17(5):955–982, 2007.
  * [NCL07] A. Nayak, Y. Chen, and F. Lin.  Forgetting and update - an exploration.  In Dagstuhl Seminar Proceedings, 2007.
  * [RHPT14] D. Rajaratnam, Levesque. H.J., M. Pagnucco, and M. Thielscher.  Forgetting in action.  In Proceedings of the Fourteenth International Conference on Principles of Knowledge Representation and Reasoning (KR 2014). AAAI Press, 2014.
  * [vDHLM09] H. van Ditmarsh, A. Herzig, J. Lang, and P. Marquis.  Introspective forgetting.  Synthese, 169:809–827, 2009.
  * [WSS05] K. Wang, A. Sattar, and K. Su.  A theory of forgetting in logic programming.  In Proceedings of the Twentieth National Conference on Artificial Intelligence and the Seventeenth Innovative Applications of Artificial Intelligence, pages 682–688. AAAI Press/The MIT Press, 2005.
  * [WZZZ14] Y. Wang, Y. Zhang, Y. Zhou, and M. Zhang.  Knowledge forgetting in answer set programming.  Journal of Artificial Intelligence Research, 50, 05 2014.
  * [ZP12] Z. Zhuang and M. Pagnucco.  Model based horn contraction.  In Proceedings of the Thirteenth International Conference on Principles of Knowledge Representation and Reasoning (KR 2012), pages 169–178. AAAI Press/The MIT Press, 2012.
  * [ZZ11] Y. Zhou and Y. Zhang.  Bounded forgetting.  In Proceedings of the Twenty-Fifth AAAI Conference on Artificial Intelligence (AAAI 2011). AAAI Press, 2011.