\documentclass[12pt]{article}
\usepackage[latin1]{inputenc}
\usepackage[OT1]{fontenc}
\usepackage{fullpage}
\usepackage{graphicx}
\usepackage{url}
\usepackage{amssymb,times,stmaryrd}
\usepackage{proof}
\usepackage[all]{xypic,xy}
\usepackage{natbib}

\newtheorem{theorem}{Theorem}[section]
\newtheorem{example}{Example}[section]
\newtheorem{proposition}[theorem]{Proposition}
\newtheorem{corollary}[theorem]{Corollary}
\newtheorem{lemma}[theorem]{Lemma}
\newenvironment{proof}{{\bf Proof. }}{\vskip0.3em}
\newtheorem{definition}[theorem]{Definition}
\newtheorem{assumption}[theorem]{Assumption}
\newtheorem{exercise}[theorem]{Exercise}
\newtheorem{problem}[theorem]{Problem}
\newtheorem{solution}[theorem]{Solution}
\newtheorem{note}[theorem]{Note}
\newtheorem{remark}[theorem]{Remark}
\newtheorem{question}[theorem]{Question}
\def\qedsign{$\Box$}
\def\qed{\ifmmode\qedsign\else{\unskip\nobreak\hfil%
\penalty50\hskip1em\null\nobreak\hfil\qedsign%
\parfillskip=0pt\finalhyphendemerits=0\endgraf}\fi}

\newcommand\Eval[1]{\left\llbracket{#1}\right\rrbracket}
\newcommand\Dom{\mathrm{dom}\;}
\newcommand\pow{\mathbb{P}}
\newcommand\nat{\mathbb{N}}
\newcommand\Z{\mathbb{Z}}
\newcommand\csu{\mathrm{csu}}
\newcommand\sel{\mathrm{sel}\;}
\newcommand\cname[1]{\ulcorner {#1} \urcorner}
\newcommand\limp{\Rightarrow}
\newcommand\qarg{\relax} %{(*)}

\title{The Theory Behind {\tt h1}}
\author{Jean Goubault-Larrecq\\
  \begin{tabular}{c}
    LSV/CNRS UMR 8643 \& INRIA Futurs projet SECSI \&
    ENS Cachan\\
    61 avenue du président-Wilson, F-94235 Cachan Cedex \\
    {\small\tt goubault@lsv.ens-cachan.fr} \\
    Phone: +33-1 47 40 75 68 \quad Fax: +33-1 47 40 75 21
  \end{tabular}
}

\begin{document}
\maketitle

\begin{abstract}
  The {\tt h1} prover is based on refinements of resolution.  We explain which
  one exactly.  One can say that {\tt h1} rests on ordered resolution with
  selection, however it is more practical to say that {\tt h1} is based on
  resolution with free selection.  By the way, we give a completeness proof
  for the latter on Horn clauses.
  
  We also describe what other rules {\tt h1} relies on: splittingless
  splitting, definition introduction, least model pruning, linear subsumption,
  fully defined predicates.  {\tt h1} also applies safe approximations, that
  preserve completeness while not being sound in general.  This way, {\tt h1}
  allows one to discover counter-models to given clause sets.  We also explain
  the approximations that {\tt h1} makes, and why they preserve completeness.
\end{abstract}

\tableofcontents

\section{Introduction}
\label{sec:intro}



\section{Tree Automata, Clauses}
\label{sec:theory}

Fix a signature $\Sigma$ of function symbols, each coming with a fixed arity, and
let $\mathcal E$ be an equational theory, inducing a congruence $\approx_{\mathcal E}$ on
all terms built on $\Sigma$.  While {\tt h1} originally does not deal with
equational theories, completeness still holds modulo $\mathcal E$.  This will come
in handy when we justify the way {\tt h1} deals with equational theories.


\subsection{Monadic Horn Clauses}
\label{sec:prelim:horn}

Let us fix once and for all a countably infinite set of unary predicate
symbols $\mathcal P$.  An {\em atom\/} is an object of the form $P (t)$, where $P$
is a predicate symbol in $\mathcal P$, and $t$ is a term on $\Sigma$.  We restrict
to unary predicate symbols, since this does not entail any loss of generality,
and we shall anyway only use unary predicate symbols in the sequel.

\begin{definition}[Definite Clause, Fact, Goal, Horn Clause]
  \label{defn:defclause}
  A {\em definite clause\/} is an implication of the form
  \begin{equation}
    \label{eq:definite}
    P (t) \Leftarrow P_1 (t_1), \ldots, P_n (t_n)
  \end{equation}
  where $P (t)$, $P_1 (t_1)$, \ldots, $P_n (t_n)$ is an unordered set of
  atoms.  If $n=0$, this is called a {\em fact}, and is often written just $P
  (t)$.  A {\em goal clause\/} is an implication of the form
  \begin{equation}
    \label{eq:goal}
    \bot \Leftarrow P_1 (t_1), \ldots, P_n (t_n)
  \end{equation}
  where $\bot$ is meant to denote false.  A {\em Horn clause\/} is a definite
  or a goal clause.
\end{definition}
%  We shall simply say clause instead of Horn clause, since we shall only
 %  consider Horn clauses in this paper.
We shall also write $P (t)$ instead of $P (t) \Leftarrow$ when $n=0$, and
$\bot$ instead of $\bot \Leftarrow$.

While we are only interested in Horn clauses in this paper, it is also useful
to consider (general) clauses, which are finite disjunctions of literals.  A
{\em literal\/} is either a positive literal $+ P (t)$, or a negative literal
$- P (t)$, where $P (t)$ is an atom.  We write such disjunctions $±_1 P_1
(t_1) \lor ±_2 P_2 (t_2) \lor \ldots \lor ±_k P_k (t_k)$, and $\Box$ if
$k=0$.  A Horn clause is then exactly a clause containing at most one positive
literal, and a definite clause contains exactly one positive literal.


\subsection{Semantics of Clauses}
\label{sec:prelim:sem}


\begin{definition}[Structure, Environment]
  \label{defn:tarski}
  A {\em structure\/} $I$ is a tuple consisting of a non-empty set $D$ (the
  {\em domain\/}), together with subsets $I_P$ of $D$, one for each predicate
  $P$, and functions $I_f : D^n \to D$ for each function $f \in \Sigma$, of
  arity $n$.
  
  Given any {\em environment\/} $\rho$ mapping variables to elements of $D$,
  the {\em value\/} $I \Eval t \rho$ of a term $t$ is defined by $I \Eval x
  \rho = \rho (x)$ for every variable $x$, $I \Eval {f (t_1, \ldots, t_n)}
  \rho = I_f (I \Eval {t_1} \rho, \ldots, I \Eval {t_n} \rho)$.  Then we let
  $I, \rho \models P (t)$, and say that $P (t)$ {\em holds\/} in $I, \rho$, if
  and only $I \Eval t \rho \in I_P$.

  A clause $C$ holds under $I, \rho$ (and we write $I, \rho \models C$) if and
  only if $I, \rho \models P (t)$ for some literal $+ P (t)$ in $C$, or $I,
  \rho \not\models P (t)$ for some literal $- P (t)$ in $C$.
\end{definition}
In the special case of Horn clauses, this can be recast as follows. By
convention, let $I, \rho \not\models \bot$. We let $I, \rho \models C$, where
$C$ is a Horn clause $A \Leftarrow A_1, \ldots, A_n$, if and only if $I, \rho
\not\models A_i$ for some $i$, $1\leq i\leq n$, or $I, \rho \models A$.

\begin{definition}[Model, $\mathcal E$-Structure, $\mathcal E$-Model]
  \label{defn:model}
  The structure $I$ is a {\em model\/} of the clause $C$ if and only if $I,
  \rho \models C$ for every environment $\rho$; we then write $I \models C$.
  $I$ is a model of a set $S$ of clauses if and only if $I \models C$ for
  every clause $C$ in $S$; we write $I \models S$ for this.
  
  The structure $I$ is an {\em $\mathcal E$-structure\/} if and only if, whenever
  $s$ and $t$ are two terms that are equal modulo $\mathcal E$, then $I \Eval s
  \rho = I \Eval t \rho$ for every environment $\mathcal E$.  An $\mathcal
  E$-structure that is a model of $C$, resp.\ $S$, is called an {\em $\mathcal
    E$-model\/} of $C$, resp.\ $S$.
  
  We then say that a clause $C$, resp.\ a clause set $S$, is {\em $\mathcal
    E$-satisfiable\/} if and only if it has an $\mathcal E$-model.
\end{definition}

A term, an atom, a literal, a clause is {\em ground\/} if and only if it
contains no free variable.  A {\em substitution\/} $\sigma$ is any map from
variables to terms.  We write $[x_1:=t_1, \ldots, x_n:=t_n]$ the substitution
mapping $x_i$ to $t_i$, $1\leq i\leq n$, and any other variable to itself. The {\em
  domain\/} $\Dom \sigma$ of $\sigma$ is $\{x | x\sigma \neq x\}$.  We also write $t \sigma$ the result
of applying the substitution $\sigma$ to the term $t$: $x \sigma = \sigma (x)$, $f (t_1, \ldots,
t_n) \sigma = f (t_1 \sigma, \ldots, t_n \sigma)$.  An {\em instance\/} of $t$ is any term $t \sigma$,
for some substitution $\sigma$. An {\em $\mathcal E$-instance\/} of $t$ is any term
that is equal modulo $\mathcal E$ to some instance of $t$.

\begin{definition}[Herbrand Semantics]
  \label{defn:Herbrand}
  The {\em Herbrand universe\/} $H_{\mathcal E}$ is the set of all $\mathcal
  E$-equivalence classes of ground terms.  A {\em Herbrand structure\/} is any
  structure $I$ whose domain is $H_{\mathcal E}$, and such that $I_f$ maps any
  $n$-tuple of ground terms $t_1$, \ldots, $t_n$ modulo $\mathcal E$, to the term
  $f (t_1, \ldots, t_n)$, again modulo $\mathcal E$, where $f$ has arity $n$.
\end{definition}
We assume here, without loss of generality, that $\Sigma$ contains at least one
constant, i.e., one function symbol of arity $0$, so that $H_{\mathcal E}$ is
not empty.  This is required for Herbrand structures to be structures at all.
It is easy to see that this is well-defined, that $I \Eval t \rho = t \rho$, where
$\rho$ is read as a substitution on the right-hand side, and that any Herbrand
interpretation $I$ is an $\mathcal E$-structure.

By standard arguments, a clause set $S$ is $\mathcal E$-satisfiable if and
only if it has a Herbrand model, i.e., provided there is a Herbrand model $I$
such that $I \models E$.

Notice that any Herbrand structure $I$ can be alternatively characterized as a
set of ground atoms that is stable under $\mathcal E$: namely the ground atoms
$P (t)$ such that $I \models P (t)$ (the environment part is irrelevant here, hence
omitted).  In this setting, Herbrand structures can be ordered by inclusion.
Then, any $\mathcal E$-satisfiable Horn clause set has a {\em least\/}
Herbrand model.  (This is the first place where dealing with {\em Horn\/}
clauses matters.)  In particular, any set of definite clauses has a least
Herbrand model; indeed, it has a Herbrand model, which contains every ground
atom.

An alternative characterization of least Herbrand models, which should be
familiar to Prolog experts, is as follows.  Fix a Horn clause set $S$. Let
$\mathcal F$ be the set of all ground atoms, union $\bot$, and let $\bot \sigma$ be
defined as $\bot$, by convention.  We consider $\bot$ as ground, and extend
$\approx_{\mathcal E}$ so that $t \approx_{\mathcal E} \bot$ if and only if $t = \bot$.  Define
the operator $T_S$ from $\pow ({\mathcal F})$ to $\pow ({\mathcal F})$ by
\begin{eqnarray*}
  T_S (I) & = & \{A' | A \Leftarrow A_1, \ldots, A_n \in S, \\
  && \phantom{\{} A' \approx_{\mathcal E} A \sigma \mbox{ ground}, A_1 \sigma \in I, \ldots, A_n \sigma \in I\}
\end{eqnarray*}
Since $T_S$ is monotonic with respect to inclusion, it has a least fixpoint.
In fact, this least fixpoint is $\bigcup_{n \in \nat} T_S^n (\emptyset)$, and
is just the least Herbrand model of $S$ in case it does not contain $\bot$.
If it contains $\bot$, then $S$ is $\mathcal E$-unsatisfiable.


\subsection{Languages, Recognizability}
\label{sec:prelim:accept}

We shall use sets of Horn clauses in the sequel to define various forms of
automata.  For all these notions, the notions of {\em recognizability}, and of
{\em language\/} recognized at some state will be the same.  Therefore we
choose to introduce these notions here.

\begin{definition}[Language, State, Recognizability]
  \label{defn:lang}
  Given an $\mathcal E$-satisfiable set of Horn clauses $S$, and a predicate
  symbol $P$, the {\em language\/} $L_P (S)$ of $S$ at {\em state\/} $P$ is
  the set of all $\mathcal E$-equivalence classes of ground terms $t$ such that $P
  (t)$ is in the least Herbrand model of $S$.  The elements of $L_P (S)$ are
  called the ($\mathcal E$-equivalence classes of) terms {\em recognized\/} at $P$
  in $S$.
\end{definition}

By abuse of language, we say that $P$ is {\em empty\/} in $S$ if and only if
$L_P (S)$ is empty, and similarly for other properties. We have the following
easy lemmas.  The first one characterizes recognizability semantically.
\begin{lemma}
  \label{lemma:recog}
  Given an $\mathcal E$-satisfiable set $S$ of Horn clauses, the ground term $t$
  is recognized at $P$ in $S$ if and only if $S$ plus the clause $\bot
  \Leftarrow P (t)$ is $\mathcal E$-unsatisfiable.
\end{lemma}
\begin{proof}
  If $t \in L_P (S)$, then by definition $P (t)$ is in the least Herbrand
  model of $S$, so it is in every Herbrand model of $S$; it follows that $S$
  plus $\bot \Leftarrow P (t)$ is $\mathcal E$-unsatisfiable.  Conversely, if $S$
  plus $\bot \Leftarrow P (t)$ is $\mathcal E$-unsatisfiable, then every model of
  $S$ must fail to satisfy $\bot \Leftarrow P (t)$, so must contain $P (t)$;
  therefore $t \in L_P (S)$.  \qed
\end{proof}

The second lemma characterizes emptiness.
\begin{lemma}
  \label{lemma:emptiness}
  Given an $\mathcal E$-satisfiable set $S$ of Horn clauses, $P$ is empty in $S$
  if and only if $S$ plus the so-called {\em query clause\/} $\bot \Leftarrow
  P (x)$ is $\mathcal E$-satisfiable.
\end{lemma}
\begin{proof}
  If $P$ is empty, then the least Herbrand model of $S$ does not contain
  any ground atom of the form $P (t)$, hence makes $\bot \Leftarrow P(x)$
  true.
  
  Conversely, if $S$ plus $\bot \Leftarrow P (x)$ is $\mathcal E$-satisfiable,
  then its least Herbrand model does not contain any ground atom of the form
  $P (t)$.  Since every model of $S$ plus $\bot \Leftarrow P(x)$ is also a
  model of $S$, the least Herbrand model of $S$ is included in that of $S$
  plus $\bot \Leftarrow P(x)$, hence does not contain any ground atom of the
  form $P (t)$ either; so $P$ is empty in $S$.  \qed
\end{proof}

The third lemma characterizes {\em intersection-emptiness}, that is, given
finitely many predicate symbols $P_1$, \ldots, $P_n$, whether $L_{P_1} (S)
\cap \ldots \cap L_{P_n} (S)$ is empty.  (We say for short that the
intersection of $P_1$, \ldots, $P_n$ is empty in this case.)
\begin{lemma}
  \label{lemma:inter:emptiness}
  Given an $\mathcal E$-satisfiable set $S$ of Horn clauses, the intersection of
  $P_1$, \ldots, $P_n$ is empty in $S$ if and only if $S$ plus the so-called
  {\em final intersection clause\/} $\bot \Leftarrow P_1 (x), \ldots, P_n (x)$
  is $\mathcal E$-satisfiable.
\end{lemma}
\begin{proof}
  The proof is similar.
  
  If the intersection of $P_1$, \ldots, $P_n$ is empty, then the least
  Herbrand model of $S$ cannot contain all atoms $P_i (t)$, $1\leq i\leq n$,
  for any ground term $t$.  So it makes $\bot \Leftarrow P_1(x), \ldots,
  P_n(x)$ true.
  
  Conversely, if $S$ plus $\bot \Leftarrow P_1 (x), \ldots, P_n (x)$ is $\mathcal
  E$-satisfiable, then its least Herbrand model does not contain all atoms
  $P_i (t)$, $1\leq i\leq n$, for any ground term $t$.  Since every model of
  $S$ plus $\bot \Leftarrow P_1(x), \ldots, P_n(x)$ is also a model of $S$,
  the least Herbrand model of $S$ is included in that of $S$ plus $\bot
  \Leftarrow P_1(x), \ldots, P_n(x)$, hence cannot contain all atoms $P_i
  (t)$, $1\leq i\leq n$, for any ground term $t$.  So the intersection of
  $P_1$, \ldots, $P_n$ is empty in $S$.  \qed
\end{proof}




\subsection{Resolution, Subsumption, Splitting}
\label{sec:prelim:res}


We shall consider yet other characterizations, coming from automated
deduction.
\begin{definition}[$\mathcal E$-Unifier, Complete Sets of $\mathcal E$-Unifiers]
  \label{defn:unifier}
  A {\em $\mathcal E$-unifier\/} $\sigma$ of two terms or atoms $s$ and $t$ is any
  substitution such that $s \sigma \approx_{\mathcal E} t \sigma$.
  
  The substitution $\sigma$ is {\em $\mathcal E$-more general\/} than $\sigma'$ if
  and only if there is a third substitution $\theta$ such that $\sigma'
  \approx_{\mathcal E} \sigma \theta$, by which we mean $x \sigma' \approx_{\mathcal
    E} x \sigma \theta$ for every variable $x$.
  
  A {\em complete set of $\mathcal E$-unifiers\/} of $s$ and $t$ is any set of
  $\mathcal E$-unifiers of $s$ and $t$ such that any $\mathcal E$-unifier of $s$ and
  $t$ is less general than some element of the set.
\end{definition}
Any list of pairs of terms or atoms $(s_i, t_i)$, $1\leq i\leq n$ has a complete set
of $\mathcal E$-unifiers $\csu_{\mathcal E} (s_1 \doteq t_1, \ldots, s_n \doteq t_n)$.  At
the least, the set of all $\mathcal E$-unifiers is such a complete set.
Unfortunately, such a set need not be finite or even computable.  For a survey
of which theories have finite and computable complete sets of $\mathcal
E$-unifiers, see \citet{LRI:UnifSurvey}.  We shall only use the fact that
such a complete set of $\mathcal E$-unifiers is always computable in
polynomial time, and consists of at most one, most general unifier in case
$\mathcal E$ is the empty theory.

%This
%is certainly the case for all theories considered here based on AC
%\citep{Stickel:ACUnif,Fages:ACUnif,AdvACUnification}.

The rule of {\em binary resolution\/} is:
\[
\begin{prooftree}
  C \lor +A \quad C' \lor -A'
  \justifies
  C \sigma \lor C' \sigma
  \using \sigma \in \csu_{\mathcal E} (A_1 \doteq B)
\end{prooftree}
\]
where we understand $C \lor +A$ in the premise as meaning additionally that
$+A$ is not in $C$, and similarly for the other premise.  This specializes to
the following rule in the framework of Horn clauses:
\[
\begin{prooftree}
  A \Leftarrow A_1, \ldots, A_m \quad
  B \Leftarrow B_1, \ldots, B_n
  \justifies
  A \sigma \Leftarrow B_1 \sigma, \ldots, B_n \sigma, A_2 \sigma, \ldots, A_m
  \sigma
  \using \sigma \in \csu_{\mathcal E} (A_1 \doteq B)
\end{prooftree}
\]
This assumes that the two premises (the {\em resolved clauses\/}) have
disjoint sets of free variables.  This can be achieved by prior renaming.  The
conclusion is called the {\em resolvent}, and $A_1$ and $B$ are the {\em
  resolved atoms}.  We also say that we resolve {\em upon\/} $A_1$ and $B$.

Binary resolution is complete for Horn clauses, i.e., $\bot$ is derivable from a
clause set $S$ if and only if $S$ is $\mathcal E$-unsatisfiable.  In the
non-Horn case, we would also need an additional factoring rule, which is not
needed here.

Binary resolution has a number of complete restrictions.  One is the case
where $n$ is restricted to be $0$, that is, one of the resolved clauses is
constrained to be a fact.  This is called (positive) {\em unit resolution}.
This is a special case of the so-called {\em positive hyperresolution\/} rule,
which is complete for general, not just Horn clauses \citep{ChangLee}.
Similarly, {\em negative hyperresolution\/} is also complete, and specializes
to {\em input resolution\/} on Horn clause sets.  This is the binary
resolution rule above, restricted to the case where $A = \bot$; {\em ordered
  negative hyperresolution\/} in addition restricts $A_1$ to be maximal with
respect to some stable, admissible ordering (see below).

It is important to note that there is a more synthetic way of writing the unit
resolution rule, which is equivalent from the standpoint of derivability of
the empty clause $\bot$:
\begin{equation}
  \label{eq:unit:macro}
  \begin{prooftree}
    P_1 (u_1) \quad \ldots \quad P_n (u_n)
    \justifies
    P (t \sigma)
    \using P (t) \Leftarrow P_1 (t_1), \ldots, P_n (t_n)
  \end{prooftree}
\end{equation}
where $\sigma \in \csu_{\mathcal E} (u_1 \doteq t_1, \ldots, u_n \doteq t_n)$. See e.g.,
\citet{ChangLee} where semantic resolution and therefore also hyperresolution
and unit resolution are presented in this way.

While the basic strategy that {\tt h1} uses can be explained as ordered
resolution with selection, it is in fact more convenient to explain it as
resolution with {\em free selection}.  While ordered resolution with selection
is always complete, resolution with free selection is only complete in the
case of Horn clauses \citep[Corollary~6.7.5]{deNivelle:PhD}.

\begin{definition}[Selection Function]
  \label{defn:sel}
  Let $\sel$ be a {\em selection function}, mapping every Horn clause $A \Leftarrow
  A_1, \ldots, A_m$ to a possibly empty subset of its {\em body} $A_1, \ldots, A_m$.  We
  require that $\sel (C)$ be non-empty when $A = \bot$ and $m\neq 0$.
  
  If $A_i$ is in $\sel (C)$, then we say that $A_i$ is {\em selected\/} in
  $C$.  By abuse of language, when $A \neq \bot$, we say that the head $A$ is
  selected in $C$ if and only if $\sel (C)$ is empty.
\end{definition}
In particular, we cannot select both the head and some atoms in the body:
either $\sel (C)$ is empty and the head is selected, or $\sel (C)$ is not
empty and the selected atoms are those of $\sel (C)$, which are by definition
in the body of $C$.  Since $\sel (C)$ is not empty when $A = \bot$ and $m\neq 0$,
at least one atom is selected in $C$, unless $C$ is the empty clause $\bot$.

We shall often distinguish the selected atoms in clauses by underlining them.
For example, letting $C$ be $A \Leftarrow \underline {A_1}, A_2, \underline {A_3}, A_4,
A_5$ means that $\sel (C) = \{A_1, A_3\}$; letting $C$ be $\underline A
\Leftarrow A_1, A_2, A_3$ means that $\sel (C) = \emptyset$ and $A \neq \bot$. The only
exception to this rule is when we do not underline any atom, in which case we
do not mean that no literal is selected (which would be absurd), rather that
the set of selected literals is left unspecified.  This is the case, notably,
in the conclusion of the rule of resolution with free selection (below).

\begin{definition}[Resolution with Free Selection]
  \label{defn:selresol}
  The rule of {\em resolution with free selection\/} is:
  \[
  \begin{prooftree}
    A \Leftarrow \underline {A_1}, \ldots, \underline {A_m}, A_{m+1}, \ldots, A_n
    \qquad
    \underline {B_1} \Leftarrow body_1 \quad \ldots \quad \underline {B_m} \Leftarrow body_m
    \justifies
    A \sigma \Leftarrow body_1 \sigma, \ldots, body_m \sigma, A_{m+1} \sigma, \ldots, A_n \sigma
  \end{prooftree}
  \]
  where $\sigma \in \csu_{\mathcal E} (A_1 \doteq B_1, \ldots, A_m \doteq B_m)$, and all premises
  are assumed to be renamed in advance so as to share no free variable;
  here, $body_i$ abbreviates a list of atoms.
  
  The upper left clause is called the {\em main premise\/}, the other clauses
  on top of the bar are the {\em side premises\/}, and the clause below is the
  {\em conclusion\/}, a.k.a., the {\em resolvent}.
\end{definition}

Extending resolution with free selection to the non-Horn case requires some
care.  In particular, requiring that $\sel$ must select at least one literal
from each clause and cannot select both a positive and a negative literal is
not enough, as the following counter-example, due to
\citet[Example~6.3.8]{deNivelle:PhD}, shows:
\begin{eqnarray*}
  \underline{-p} \lor \underline{-q} &
  \underline{-q} \lor \underline{-r} &
  \underline{-r} \lor \underline{-p}
  \\ && \\
  +q \lor \underline{+p} & +r \lor \underline{+q} & +p \lor \underline{+r}
\end{eqnarray*}
Only the three upper clauses can be used as main premises (assuming the
obvious generalization of Definition~\ref{defn:selresol}). So, from these
clauses, we can only derive:
\[
\begin{prooftree}
  \underline{-p} \lor \underline{-q} \  +q \lor \underline{+p} \  +r \lor
  \underline{+q}
  \justifies
  +r \lor +q
\end{prooftree}
\quad
\begin{prooftree}
  \underline{-q} \lor \underline{-r} \  +r \lor \underline{+q} \  +p \lor
  \underline{+r}
  \justifies
  +p \lor +r
\end{prooftree}
\quad
\begin{prooftree}
  \underline{-r} \lor \underline{-p} \  +p \lor \underline{+r} \  +q \lor
  \underline{+p}
  \justifies
  +q \lor +p
\end{prooftree}
\]
And, if we select $+q$ from the first conclusion, $+r$ from the second, $+p$
from the third, we retrieve clauses that were already present in the initial
set of clauses, showing that the empty clause cannot be derived this way.
However, the initial set of clauses is unsatisfiable. This can be shown by
selecting different atoms in clauses:
\[
\begin{prooftree}
  \underline{-r} \lor \underline{-p}
  \[
  \underline{-p} \lor \underline{-q} \quad \underline{+p} \lor +r \quad +r \lor
  \underline{+q}
  \justifies
  +r
  \]
  \[
  \underline{-q} \lor \underline{-r} \quad \underline{+q} \lor +p \quad +p \lor
  \underline{+r}
  \justifies
  +p
  \]
  \justifies
  \bot
\end{prooftree}
\]

Resolution with free selection is {\em sound\/}: if $\bot$ can be derived by
repeated applications of this rule from a given set $S$ of clauses, then $S$
is unsatisfiable.  This is clear, as a resolvent is always a logical
consequence of its premises.
\begin{proposition}[Completeness]
  \label{prop:selresol:complete}
  Resolution with free selection is complete for Horn clauses.  That is, given
  any $\mathcal E$-unsatisfiable set $S_0$ of Horn clauses, there is a
  derivation of the empty clause $\bot$ from $S_0$, whatever the selection
  function $\sel$ is.
\end{proposition}
\begin{proof}
  We give a proof based on semantic trees \citep{KH:semtree}.  This proof
  appears novel: the only known proof to date, due to \citet{deNivelle:PhD},
  rests on syntactic arguments.  We choose to use a semantic proof, because it
  will be easier to show that linear subsumption, splittingless splitting, and
  various other rules retain completeness later on, by altering the current
  proof only slightly.
  
  First, by Herbrand's Theorem, there is a finite unsatisfiable set $\{C^0_i
  \theta_i | 1\leq i \leq p\}$ of ground $\mathcal E$-instances of clauses $C^0_i$ of
  $S_0$.  In particular, the set of all $\mathcal E$-equivalence classes of
  ground atoms occurring in it is finite, let us say $\{A^0_1, \ldots, A^0_n\}$.  We
  shall reason on semantic trees based on $A^0_1$, \ldots, $A^0_n$, which we now
  define.
  
  A {\em semantic tree\/} (implicitly, on $A^0_1$, \ldots, $A^0_n$) is a binary
  tree that represents all possible Boolean interpretations of $A^0_1$, \ldots,
  $A^0_n$.  The root has two sons, corresponding to the two choices $A^0_1$
  false, $A^0_1$ true.  Each son has two sons, corresponding to the two
  choices $A^0_2$ false, $A^0_2$ true, and so on.  See
  Figure~\ref{fig:semtree} for an illustration, where $A^0_1 = p$, $A^0_2 =
  q$, $A^0_3 = r$.

  \begin{figure}[htbp]
    \centering
    \includegraphics{semtree.eps}    
    \caption{A semantic tree}
    \label{fig:semtree}
  \end{figure}
  
  Formally, a {\em partial interpretation\/} is a finite list $±_1 A^0_1, ±_2
  A^0_2, \ldots, ±_k A^0_k$, $0\leq k\leq n$.  If $A^0_i$ occurs with the $+$ sign, we
  say that $A^0_i$ is {\em true\/} in this partial interpretation; it is {\em
    false\/} if it occurs with the $-$ sign. Otherwise, $A^0_i$ is {\em
    undefined\/} in the partial interpretation.
  
  The {\em semantic tree\/} is the tree whose nodes $N$ are the partial
  interpretations.  The partial interpretation $±_1 A^0_1, ±_2 A^0_2, \ldots, ±_k
  A^0_k$ has two sons, its {\em left son\/} $±_1 A^0_1, \allowbreak ±_2 A^0_2,
  \allowbreak \ldots, \allowbreak ±_k A^0_k, \allowbreak -A^0_{k+1}$ and its {\em
    right son\/} $±_1 A^0_1, \allowbreak ±_2 A^0_2, \allowbreak \ldots, \allowbreak
  ±_k A^0_k, \allowbreak +A^0_{k+1}$.  (This, provided that $A^0_{k+1}$
  exists, i.e., provided $k < n$; otherwise, $±_1 A^0_1,\allowbreak ±_2
  A^0_2,\allowbreak \ldots,\allowbreak ±_k A^0_k$ has no son.)  We say that the
  partial interpretation $±_1 A^0_1, ±_2 A^0_2, \ldots, ±_k A^0_k$, as a node, is a
  {\em choice node\/} on $A^0_{k+1}$.  The root $\epsilon$ of the tree is the empty
  partial interpretation.
  
  The maximal branches of the semantic tree are in natural bijection with
  Herbrand structures.  If $I$ is a Herbrand structure, we obtain a maximal
  branch by going through the nodes $\epsilon$, then $±_1 A^0_1$, then $±_1 A^0_1,
  ±_2 A^0_2$, ..., where $±_i$ is $+$ if $A^0_i \in I$, $-$ otherwise.
  Conversely, on every maximal branch, each atom $A^0_i$ occurs with a unique
  sign $±_i$ in every partial interpretation of length at least $i$; we then
  get a Herbrand structure containing exactly the $A^0_i$s such that $±_i$ is
  the $+$ sign.
  
  A ground clause $A \Leftarrow A_1, \ldots, A_k$ is {\em false\/} at node $N$ if and only
  if each $A_j$, $1\leq j\leq k$, is true in the partial interpretation $N$, and $A$
  is false in $N$.  (We assume here that $\bot$ is false in any partial
  interpretation.)  Look at Figure~\ref{fig:semtree} for an example.  The
  clause $p \Leftarrow q$ is false at node 5 (i.e., the partial interpretation $-p,
  +q$).  Letting $S_0$ be the clause set $+r$; $q \Leftarrow r$; $p \Leftarrow q$; $\bot \Leftarrow p, q,
  r$, then every branch meets a node that makes some clause from $S_0$ false.
  This holds for any unsatisfiable ground clause set.  The minimal (highest)
  nodes $N$ that make some clause from $S_0$ false are called {\em failure
    nodes\/}; these are the nodes that are targets of arrows on
  Figure~\ref{fig:semtree}.
  
  A {\em closed semantic tree\/} for a given clause set $S$ is any triple $(T,
  C_\bullet, \theta_\bullet)$, where:
  \begin{itemize}
  \item $T$ is the subtree of the semantic tree whose leaves are exactly the
    failure nodes.  (See Figure~\ref{fig:closedsemtree}.)
  \item $C_\bullet$ is a family of clauses $C_N$ from $S$, one for each failure node
    $N$;
  \item $\theta_\bullet$ is a family of substitutions $\theta_N$, one for each failure node $N$.
  \end{itemize}
  We require that $C_N \theta_N$ is a ground clause consisting of atoms taken from
  $A^0_1$, \ldots, $A^0_n$ modulo $\mathcal E$, and that $C_N \theta_N$ is false at $N$
  for each failure node $N$.

  \begin{figure}[htbp]
    \centering
    \includegraphics{closedsemtree.eps}
    \caption{A closed semantic tree}
    \label{fig:closedsemtree}
  \end{figure}
  
  We claim that if $S_0$ is $\mathcal E$-unsatisfiable, then it has a closed
  semantic tree.  As we have said above there is a finite set $\{C^0_i \theta_i | 1\leq
  i \leq p\}$ of ground $\mathcal E$-instances of clauses $C^0_i$ of $S$, using
  only $A^0_1$, \ldots, $A^0_n$ as atoms, which is unsatisfiable.  This means that
  on each branch of the semantic tree, at least one of $C^0_i \theta_i$ must be
  false.  So there is a failure node along each branch.  Chop the semantic
  tree at these failure nodes: the tree $T$ that we get this way has the
  property that its leaves are exactly the failure nodes.  Now pick one pair
  $(C^0_i, \theta_i)$ such that $C^0_i \theta_i$ is false at $N$, for each failure node
  $N$, and call it $(C_N, \theta_N)$: we get a closed semantic tree for $S$.
  
  The rest of the proof now goes as follows.  If $S_0$ has a closed semantic
  tree whose root $\epsilon$ is a failure node, then clearly $S_0$ must contain the
  empty clause, and we are finished.  Otherwise, given a closed semantic tree
  for $S_0$, we shall apply the rule of resolution with free selection to
  specific clauses in $S_0$ to get a new clause set $S_1$, in such a way that
  $S_1$ has a smaller closed semantic tree than $S_0$, for a given ordering
  that we shall define later.  (To be precise, this will an ordering on pairs
  consisting of a clause set and a closed semantic tree for it.)  Provided
  this ordering is well-founded, this procedure will eventually stop on a
  clause set $S_i$ that has a closed semantic tree whose root is a failure
  node, and which therefore must contain the empty clause.

  So, we have to find a way to pick the right clauses to resolve upon first.
  Then, we shall show that applying resolution with free selection produces
  smaller and smaller closed semantic trees.

  \paragraph{Picking the right clauses.}
  
  Let $S$ be any clause set not containing the empty clause and $(T, C_\bullet,
  \theta_\bullet)$ a closed semantic tree for $S$.  Consider the set $S'$ of clauses $C_N
  \theta_N$, when $N$ ranges over the failure nodes of $T$.  $C_N \theta_N$ is a ground
  clause.  By convention, let us say that an atom is {\em selected\/} in $C_N
  \theta_N$ if and only if it is obtained from a selected atom in $C_N$ by
  instantiating it using $\theta_N$.
  
  Build a propositional interpretation $I$ on $A^0_1$, \ldots, $A^0_n$ as follows.
  We equate $I$ with the set of true atoms in $I$, and define $I$ as the
  smallest set of atoms such that, for every ground clause $\underline p \Leftarrow
  p_1, \ldots, p_k$ in $S'$ with head selected, if $p_1, \ldots, p_k \in I$ then $p \in I$.

  \begin{figure}[htbp]
    \centering
    \includegraphics{selsemtree.eps}
    \caption{The closed semantic tree, displaying selected literals}
    \label{fig:selsemtree}
  \end{figure}
  
  Look at Figure~\ref{fig:selsemtree} for an example.  The clauses in $S'$
  whose head is selected are $\underline r$ and $\underline p \Leftarrow q$.  Therefore
  $I = \{r\}$.  We say that $r$ is true in $I$, and $p$ and $q$ are false in
  $I$.
  
  $I$ can now be read as a branch in the semantic tree, hence there is a
  prefix of it which is a branch $B$ in the closed semantic tree $T$.  (On the
  example, this is the branch coming down from $1$ to $9$: $p$ false, $q$
  false, $r$ true.)  Look at the failure node $N$ that ends branch $B$.  (In
  the example, node 9.)  We claim that we may apply resolution with free
  selection, with $C_N$ as main premise.  (On the example, $q \Leftarrow \underline r$
  can indeed be resolved with $\underline r$, yielding $q$.)
  
  Write $C_N \theta_N$ as $p \Leftarrow p_1, \ldots, p_k$.  $C_N \theta_N$ is false in $I$, so $p$ is
  false in $I$, and $p_1$, \ldots, $p_k$ are true in $I$.  In particular, $p$
  cannot be selected, otherwise by the definition of $I$, $p$ would be true in
  $I$.  So some non-empty subset of $p_1$, \ldots, $p_k$ is selected, say $p_1, \ldots,
  p_j$.  In other words, $C_N \theta_N$ is $p \Leftarrow \underline p_1, \ldots, \underline p_j,
  p_{j+1}, \ldots, p_k$.  Since $p_1$, \ldots, $p_j$ are true in $I$, there are failure
  nodes $N_1$, \ldots, $N_j$ in $T$ such that, for each $i$, $1\leq i\leq j$, $C_{N_i}
  \theta_{N_i}$ is a clause whose head is selected and is equal to $p_i$, say
  $\underline p_i \Leftarrow H_i$, where $H_i$ is some collection of unselected ground
  atoms.  In particular, the head of $C_{N_i}$ is selected.  Furthermore, all
  the atoms in $H_i$ are true in $I$.
  
  It is then clear that we may resolve the main premise $C_N \theta_N = p \Leftarrow
  \underline p_1, \ldots, \underline p_j, p_{j+1}, \ldots, p_k$ with the side premises
  $C_{N_i} \theta_{N_i} = \underline p_i \Leftarrow H_i$, yielding $p \Leftarrow H_1, \ldots, H_j,
  p_{j+1}, \ldots, p_k$.  But this is at the ground level, and we need to lift this
  to the first-order level.  This is not hard, but requires some heavy
  notation.
  
  Since $C_N \theta_N = p \Leftarrow \underline p_1, \ldots, \underline p_j, p_{j+1}, \ldots, p_k$,
  write $A_{i1}, \ldots, A_{ik_i}$ the set of all atoms $A_{ii'}$ in the body of
  $C_N$ such that $A_{ii'} \theta_N \approx_{\mathcal E} p_i$.  Clearly $k_i\geq 1$; in
  general $k_i$ may fail to be exactly $1$, since $\theta_N$ may unify several
  atoms in the body and therefore yield the same $p_i$.  If $1\leq i\leq j$,
  moreover, at least one of $A_{i1}, \ldots, A_{ik_i}$ is selected; say that
  $A_{i1}, \ldots, A_{ij_i}$ ($1\leq j_i\leq k_i$) are the selected ones.  So $C_N$ is of
  the form
  \begin{eqnarray}
    \label{eq:CN}
    A & \Leftarrow & (\underline A_{11}, \ldots, \underline A_{1j_1}, A_{1(j_1+1)}, \ldots,
    A_{1k_1}), \ldots, (\underline A_{j1}, \ldots, \underline A_{jj_j}, A_{j(j_j+1)}, \ldots,
    A_{jk_j}), \\\nonumber
    && (A_{(j+1)1}, \ldots, A_{(j+1)k_{j+1}}), \ldots, (A_{k1}, \ldots, A_{kk_k})
  \end{eqnarray}
  Similarly, $C_{N_i}$ is of the form $A'_i \Leftarrow body_i$, with $A'_i \theta_{N_i}
  \approx_{\mathcal E} p_i$ and $body_i \theta_{N_i} \approx_{\mathcal E} H_i$.  Since $A_{ii'}
  \theta_N \approx_{\mathcal E} p_i \approx_{\mathcal E} A'_i \theta_{N_i}$ for every $i$, $i'$, and
  since by assumption $C_N$, $C_{N_1}$, \ldots, $C_{N_j}$ are assumed to be renamed
  apart, the disjoint union $\sigma' = \theta_N \uplus \theta_{N_1} \uplus \ldots \uplus \theta_{N_j}$ is a
  well-defined substitution that unifies $A_{ii'}$ with $A'_i$ for every $i$,
  $i'$, $1\leq i\leq j$, $1\leq i'\leq j_i$ modulo $\mathcal E$.  So there is $\sigma \in
  \csu_{\mathcal E} (A_{11} \doteq A'_1, \ldots, A_{1j_1} \doteq A'_1, \ldots, A_{j1} \doteq A'_j, \ldots,
  A_{jj_j} \doteq A'_j)$ such that $\sigma' \approx_{\mathcal E} \sigma \vartheta$ for some substitution
  $\vartheta$, by definition of complete sets of unifiers.  We can therefore produce
  the clause
  \begin{eqnarray}
    \label{eq:free:conc}
    A \sigma & \Leftarrow & body_1 \sigma, \ldots, body_j \sigma, (A_{(j+1)1} \sigma, \ldots, A_{(j+1)k_{j+1}} \sigma), \ldots,
    (A_{k1} \sigma, \ldots, A_{kk_k} \sigma)
  \end{eqnarray}
  by resolving the main premise $C_N$ (\ref{eq:CN}) against $j_1$ copies of
  $C_{N_1}$, \ldots, $j_j$ copies of $C_{N_j}$ as side premises.

  \paragraph{Termination.}
  
  Let $C$ be clause (\ref{eq:free:conc}) obtained by resolution with free
  selection from $C_N$, $C_{N_1}$, \ldots, $C_{N_j}$.  Using the substitution $\vartheta$
  such that $\sigma' \approx_{\mathcal E} \sigma \vartheta$,
  %(beware of the typographical difference between $\vartheta$ and $\theta$),
  we get that $C \vartheta$ is exactly the clause
  \begin{eqnarray*}
    p & \Leftarrow & H_1, \ldots, H_j, p_{j+1}, \ldots, p_k
  \end{eqnarray*}
  since $A \sigma \vartheta \approx_{\mathcal E} A \sigma' \approx_{\mathcal E} A \theta_N \approx_{\mathcal E} p$,
  $body_i \sigma \vartheta \approx_{\mathcal E} body_i \sigma' \approx_{\mathcal E} body_i \theta_{N_i}
  \approx_{\mathcal E} H_i$, and $A_{ii'} \sigma \vartheta = A_{ii'} \sigma' \approx_{\mathcal E} A_{ii'}
  \theta_{N_i} \approx_{\mathcal E} p_i$.  This is exactly the resolvent of $C_N \theta_N$
  against $C_{N_1} \theta_{N_1}$, \ldots, $C_{N_j} \theta_{N_j}$ on the ground level.
  
  \begin{figure}[htbp]
    \centering
    \includegraphics{selsemtree2.eps}
    \caption{Resolving may shrink the complete semantic tree}
    \label{fig:semsemtree2}
  \end{figure}
  
  Look at the example.  Resolving $\underline r$ with $q \Leftarrow \underline r$
  yields the clause $q$.  Now, since there is only one literal in $q$, it must
  be selected.  Adding $\underline q$ to the set of clauses makes failure
  nodes out of nodes 4 and 6.  See Figure~\ref{fig:selsemtree2}.  In this
  case, the closed semantic tree shrinks.  Repeat the construction: the
  interpretation $I$ makes $q$ (because of $\underline q$ at node 4), $p$
  (because of $\underline p \Leftarrow q$ at node 5, and since $q$ is true), and $r$
  true (because of $\underline r$ at node 14).  So now the failure node $N$
  where we shall find the main premise is node 15: the main premise is $\bot \Leftarrow
  \underline p, \underline q, r$.  The side premises are now $\underline p \Leftarrow
  q$ from node 5 and $\underline q$ from node 4, yielding the resolvent $\bot \Leftarrow
  q, r$.  Notice that the underlined $q$ disappeared from $\bot \Leftarrow \underline p,
  \underline q, r$ by resolving it with clause $\underline q$, but one fresh
  $q$ reappeared in the resolvent because of resolution with $\underline p \Leftarrow
  q$.  Now, adding the resolvent $\bot \Leftarrow q, r$ does {\em not\/} make the complete
  semantic tree shrink any longer: see Figure~\ref{fig:selsemtree3}.

  \begin{figure}[htbp]
    \centering
    \includegraphics{selsemtree3.eps}
    \caption{Resolving may also fail to shrink the complete semantic tree}
    \label{fig:selsemtree3}
  \end{figure}

  Remember that, at failure node $N$, $p$ is false and $p_1$, \ldots, $p_k$ are
  true.  Also, all the atoms of $H_1$, \ldots, $H_j$ are true in $I$.  Since $N$,
  as a partial interpretation, is a prefix of $I$, any atom that is true in
  $I$ is either 

\qed
\end{proof}
%!!!

A useful simplification rule is {\em subsumption}. In general, a clause $C$
{\em subsumes\/} the clause $D$ iff $C \sigma \subseteq D$ for some substitution $\sigma$ (read
the inclusion mod $\mathcal E$).  Deleting subsumed clauses from clause sets
may cause incompleteness in subtle ways.  The standard way to delete subsumed
clauses safely is to erase newly created clauses that are subsumed by old
clauses, and old clauses that are {\em strictly\/} subsumed by new clauses;
see \citet{BG:HAR} for details, in the non-equational case.

We don't want to care with such subtleties if they can be avoided.  Instead,
we shall observe that we can always delete {\em linearly subsumed\/} clauses
(whether new or old).
\begin{definition}[Linear Subsumption]
  \label{defn:lin:subs}
  We say that $C$ {\em linearly subsumes\/} $D$ if and only if $C \sigma
  \subseteq D$ for some substitution $\sigma$ that unifies no pair of literals
  of $C$.
\end{definition}
In other words, if and only if there is a one-to-one mapping from literals
$L_i$ of $C$ to literals $L'_i$ of $D$, such that $L_i \sigma = \L'_i$ for all
$i$.
%  (It is also slightly simpler, computationally speaking, to test for linear subsumption than for the usual
%form, although the linear subsumption test is also NP-complete.)
For example, the clause $\bot \Leftarrow P (x), P (y)$ linearly subsumes the
clauses $\bot \Leftarrow P (a), P (y)$ (with $\sigma$ mapping $x$ to $a$), $Q
(z) \Leftarrow P (a), P (y)$, and $Q (z) \Leftarrow P (x), P (y)$; it also
subsumes $\bot \Leftarrow P (x)$ and $\bot \Leftarrow P (a)$, but not
linearly; conversely, $\bot \Leftarrow P (x)$ linearly subsumes $\bot
\Leftarrow P (x), P (y)$.  In the rest of this paper, we shall only be
interested in removing clauses that are renaming variants of each variant---so
each linearly subsumes the other.

A final rule that we shall use liberally is {\em splitting}.  To be fair, we
shall be interesting in an encoding of splitting that we shall call {\em
  splittingless splitting}, and which seemingly first appears in print in
\citet{Voronkov:IJCAR}.  To explain the latter, it is clearer to explain the
former first.

Splitting is used when some clause in the current clause set is a disjunction
$C \lor C'$, where $C$ and $C'$ share no free variable.  Then the clause set
$S \cup \{C \lor C'\}$ is $\mathcal E$-unsatisfiable if and only if both clause
sets $S \cup \{C\}$ and $S \cup \{C'\}$ are $\mathcal E$-unsatisfiable.  Each
resulting clause set is called a {\em branch}.  (Resolution with splitting is
then indeed a form of tableaux.)  For example, consider the following set of
clauses:
\begin{eqnarray*}
  (a) \quad P (f (x, y)) \Leftarrow P_1 (x), P_2 (y) &
  (b) \quad Q_1 (x) \Leftarrow P (f (x, y)), Q_2 (y) &
  \\
  (c) \quad P_2 (g (g (y))) \Leftarrow P_2 (y) &
  (d) \quad P_2 (g (a)) &
  \\
  (e) \quad Q_2 (g (g (g (y)))) \Leftarrow Q_2 (y) &
  (f) \quad Q_2 (g (g (a))) &
  \\
  (g) \quad \bot \Leftarrow Q_1 (g (a)) &
  (h) \quad P_1 (g (x)) &
\end{eqnarray*}
When the two clauses $(a)$ and $(b)$ are resolved on $P (f (x,
y))$, we generate the clause $Q_1 (x) \Leftarrow P_1 (x), P_2 (y), Q_2 (y)$,
which is a splittable disjunction.  The current branch then splits in two
branches, on which reasoning proceeds independently:
\[
\begin{array}{c|c}
  \multicolumn{2}{c}{(i) \quad Q_1 (x) \Leftarrow P_1 (x), P_2 (y), Q_2 (y)
    \quad \mbox{by }(a), (b)} \\
  (j) \quad Q_1 (x) \Leftarrow P_1 (x) & (k) \quad \bot \Leftarrow P_2 (y),
  Q_2 (y) \\
  (l) \quad \bot \Leftarrow P_1 (g (a)) \quad \mbox{by }(j), (g) &
  (m) \quad \bot \Leftarrow P_2 (y), Q_2 (g (g (y)) \quad \mbox{by }(k), (c)
  \\
  \bot \quad \mbox{by }(l), (h) &
  (n) \quad \bot \Leftarrow P_2 (g (y)), Q_2 (y) \quad \mbox{by }(m), (e) \\
  & (o) \quad \bot \Leftarrow P_2 (y), Q_2 (g (y)) \quad \mbox{by }(n), (c)
  \\
  & (p) \quad \bot \Leftarrow Q_2 (g (g (a)) \quad \mbox{by }(o), (d) \\
  & (q) \quad \bot \quad \mbox{by }(p), (f)
\end{array}
\]
Splittingless splitting is originally a trick to simulate splitting in
resolution-like theorem provers, avoiding the copying of clause sets
\citep{Voronkov:IJCAR}.  This will be used as a theoretical tool in the rest
of this paper.  While splitting rests on the equivalence of $\forall x, y \cdot C (x) \lor
C' (y)$ and $(\forall x \cdot C (x)) \lor (\forall y \cdot C' (y))$ (assuming $x$ denotes the free
variables of $C (x)$, and $y$ those of $C' (y)$), the idea of splittingless
splitting stems from the equivalence between the former and $\exists q \cdot (\forall x \cdot q
\limp C (x)) \land (\forall y \cdot ¬ q \limp C' (y))$, where $q$ is a second-order
propositional variable.  A bit more formally, the splittingless splitting rule
generates the two clauses $C \lor -q$ and $C' \lor +q$, where $q$ is fresh, from a
splittable clause $C \lor C'$ (i.e., $C$ and $C'$ share no free variable).

Splittingless splitting should be defined in such a way that it preserves
completeness, and that $q$ symbols are generated as parsimoniously as possible
(the latter will be useful in showing decidability results).  Here is a way.
We first define formally what it means to create fresh predicate symbols.  The
idea is that $\mathcal P$ is a finite set of symbols containing all predicate
symboles that we shall be interested in, and $\mathcal Q$ is a set of fresh
predicate symbols.
\begin{definition}[$\mathcal P$-Clause, $\mathcal Q$, $\cname C$]
  \label{defn:PQ}
  Fix a set $\mathcal P$ of predicate symbols.  A {\em $\mathcal P$-clause\/} is any
  clause whose predicate symbols are all from $\mathcal P$.
  
  Let $\mathcal Q$ be some set of zero-ary predicate symbols disjoint from $\mathcal
  P$, in one-to-one correspondence with the set of $\mathcal P$-clauses modulo
  renaming: for each $\mathcal P$-clause $C$, let $\cname C$ be a symbol in $\mathcal
  Q$, so that $\cname C = \cname {C'}$ iff there is a renaming $\varrho$ such
  that $C = C' \varrho$.
\end{definition}
This construction is always possible: e.g., take $\mathcal Q$ the quotient of the
set of $\mathcal P$-clauses modulo the equivalence relation generated by renaming.

\begin{definition}[Splittingless Splitting]
  \label{defn:split}
  The rule of {\em splittingless splitting\/} is:
  \[
  \begin{prooftree}
    C \lor C'
    \justifies
    C \lor -\cname {C'} \qarg \quad
    +\cname {C'} \qarg \lor C'
  \end{prooftree}
  \]
  where $C$ and $C'$ are two non-empty subclauses sharing no variable, where
  $C'$ is restricted to be a $\mathcal P$-clause, and $C$ is required to contain
  at least an atom $P (t)$ with $P \in {\mathcal P}$.
  
  The effect of the rule is to {\em replace\/} $C \lor C'$ by the two clauses
  $C \lor -\cname {C'} \qarg$ and $+\cname {C'} \qarg \lor C'$ in conclusion.
\end{definition}
%  Here $*$ is any fixed ground
%term, typically a fresh constant.  Usually $*$ will always be the same fixed
%constant, but by using different such constants we shall achieve a similar
%effect as using not just one but several sets $\mathcal Q$ of nullary predicate
%symbols; this will come in handy in Proposition~\ref{prop:oracle:complete} for
%example.
%  We shall usually leave the ground term $*$ implicit.  When we want
%to make the term $*$ explicit, we shall say that the above rule is
%splittingless splitting {\em based on $*$}.

\begin{remark}
  Note to the cognoscenti: the restriction that $C'$ is a $\mathcal P$-clause can
  be lifted, at the price of some complication. We shall not need the more
  liberal, but more complicated version.
\end{remark}

We may use ordered resolution with selection in combination with any strategy
for removing linearly subsumed clauses and for applying splittingless
splitting.  In particular, we may remove subsumed clauses and do splittingless
splitting eagerly (as soon as can be); we may also decide to apply
splittingless splitting in selected cases only. Any such strategy is sound and
complete, provided $\succ$ is a stable and compatible ordering. In practice,
we shall also assume that $\succ$ is {\em admissible\/}:
\begin{definition}[Admissible]
  \label{defn:admissible}
  A strict ordering $\succ$ is {\em admissible\/} if and only if it is stable,
  compatible with $\mathcal E$, and $P (t) \succ q$ for every $P \in {\mathcal P}$ and
  $q \in {\mathcal Q}$.
\end{definition}
Admissibility prevents the conclusions of the splittingless splitting rule to
be resolved on $\cname {C'} \qarg$ to get the premise again, leading to an
endless loop.

The clause set $(a)$--$(h)$ above generates the following clauses, when using
resolution and eager splittingless splitting:
\begin{eqnarray*}
  & (i) \quad Q_1 (x) \Leftarrow P_1 (x), P_2 (y), Q_2 (y)
  & \mbox{by }(a), (b) \\
  & (j') \quad Q_1 (x) \Leftarrow P_1 (x), q\qarg & \\
  & (k') \quad q\qarg \Leftarrow P_2 (y), Q_2 (y) & \\
  & (m') \quad q\qarg \Leftarrow P_2 (y), Q_2 (g (g (y))) & \mbox{by }(k'),
  (c) \\
  & (n') \quad q\qarg \Leftarrow P_2 (g (y)), Q_2 (y) & \mbox{by }(m'), (e) \\
  & (o') \quad q\qarg \Leftarrow P_2 (y), Q_2 (g (y)) & \mbox{by }(n'), (c) \\
  & (p') \quad q\qarg \Leftarrow Q_2 (g (g (a))) & \mbox{by }(o'), (d) \\
  & (q') \quad q\qarg & \mbox{by }(p'), (f) \\
  & (j'') \quad Q_1 (x) \Leftarrow P_1 (x) & \mbox{by }(q'), (j') \\
  & (l') \quad \bot \Leftarrow P_1 (g (a)) & \mbox{by }(j''), (g) \\
  & \bot & \mbox{by }(l'), (h)
\end{eqnarray*}
where $q = \cname{\bot \Leftarrow P_2 (y), Q_2 (y)}$.  Note that steps $(k')$--$(q')$
simulate exactly the right branch $(k)$--$(q)$ of the tableau presented above,
and the steps following $(j'')$ simulate the left branch---as claimed in
\citet{Voronkov:IJCAR}.

Instead of using either form of splitting, we might have used {\em
  condensing\/} \citep{Joyner:dec}. Consider any clause $C$ such that, for
some substitution $\sigma$, $C \sigma$ is a proper subclause of $C$ modulo $\mathcal E$;
in other words, $C$ can be written $C \sigma \lor D$ for some non-empty clause $D$
disjoint from $C \sigma$, modulo $\mathcal E$.  Then the condensing rule consists
in replacing $C$ by its {\em condensation\/} $C \sigma$.  (We deviate slightly from
\citet{Joyner:dec}, who defines condensations of $C$ as the condensations of a
condensation of \ldots{} of a condensation of $C$ that does not condense any
longer.)  For example, letting $C$ be the clause $-P (x) \lor -P (y)$ (a
splittable clause).  Take $\sigma = [x:=y]$. Then $C \sigma$ is $-P (y)$, a subclause of
$C$.  In general, any clause $C$ can be written modulo $\mathcal E$ as a
disjunction $C_1 \lor \ldots \lor C_n$, where $n$ is maximal such that the subclauses
$C_i$ and $C_j$ share no free variable when $i\neq j$.  Call this decomposition
the {\em decomposition of $C$ in blocks $C_1$, \ldots, $C_n$}. Assume that $C_i$
subsumes $C_j$ for some $i\neq j$, say $C_j = C_i \sigma \lor D$, where the domain of $\sigma$
is contained in the free variables of $C_i$: then the clause $C$ where $C_i$
has been removed, namely $C_1 \lor \ldots \lor C_{i-1} \lor C_{i+1} \lor \ldots \lor C_n$, is a
condensation $C \sigma$ of $C$. Condensing is both less efficient in practice and
more difficult to reason about than splitting or splittingless splitting,
hence we won't use it.
%  We shall still need
%condensing in specific cases, to ensure that (after condensing) no $C_i$ is a
%renaming of $C_j$ for any $i\neq j$ in any decomposition in blocks $C_1$,
%\ldots, $C_n$ of any clause.

We prove the soundness and completeness of ordered resolution with selection
combined with any strategy of subsumption and splittingless splitting, and
condensing, in Appendix~\ref{app:complete}---in fact even in the non-Horn
case.  Let the reader not be mistaken: formally speaking, this result {\em
  is\/} new; we relegate it to an appendix because, while the completeness
result is central to this paper, the completeness proof is not.  Further, the
completeness result will hardly be a surprise to automated deduction
specialists; but a proof had to be given.  Note that, while this proof is
based on improvements of the ancient semantic tree technique \citep{ChangLee},
it nevertheless improves on the standard Bachmair-Ganzinger style forcing
argument \citep{BG:HAR}, which requires an ordering $\succ$ that is in addition
total on ground formulas, and well-founded.  On the other hand, we only
consider clausal forms, contrarily to \citet{BG:HAR}, because this is all we
need.



%\subsection{Splitting, and Resolution Tableaux}
%\label{sec:prelim:split}

%A final rule that will be crucial in finding decision procedures is {\em
%  splitting}.  Intuitively, splitting allows one to replace a clause of the
%form, say, $\bot \Leftarrow P (x), Q (y)$, where $x$ and $y$ are distinct
%variables, by the disjunction of the clauses $\bot \Leftarrow P (x)$ and $\bot
%\Leftarrow Q (y)$.  In the sequel, when $C_1, \ldots, C_k$ are Horn clauses
%such that at most one of them is definite, say $C_i = A^i \Leftarrow A^i_1,
%\ldots, A^i_{n_i}$ and $A_2 = \ldots = A_k = \bot$, we write $C_1 \lor \ldots
%\lor C_k$ the Horn clause $A_1 \Leftarrow A^1_1, \ldots, A^1_{n_1}, \ldots,
%A^k_1, \ldots, A^k_{n_k}$.

%Formally speaking, splitting is a tableau rule.  A {\em tableau\/} is just a
%finite set of clause sets, called the {\em branches\/} of the tableau.
%Resolution steps (to be precise, steps of ordered resolution, or input
%resolution, depending on the precise refinement we shall use) are applied to
%each branch independently of the other branches. The initial tableau for the
%clause set $S$ contains just the branch $S$.  Splitting applies when some
%branch of the tableau $S_1, \ldots, S_n$, say $S_1$, contains a clause $C_1
%\lor \ldots \lor C_k$, where the subclauses $C_i$ share no free variable, and
%$k\geq 2$.  Let $S'_1$ be $S_1$ minus this clause.  Then splitting produces
%the new tableau $S'_1 \cup \{C_1\}$, \ldots, $S'_1 \cup \{C_k\}$, $S_2$,
%\ldots, $S_n$, where the branch $S_1$ has been split in $k$ subbranches.

%The combination of ordered resolution,
%% with (positive, resp.\ negative) selection,
%splitting and subsumption is complete, even when subsumption and splitting are
%applied eagerly; i.e., when resolution is only applied on branches where no
%clause subsumes any other, and no clause can be split further.  Completeness
%means here that $S$ is $\mathcal E$-unsatisfiable if and only if the combination
%eventually produces a tableau, all of whose branches contain the empty clause.

%Indeed, given any tableau with branches $S_1, \ldots, S_n$, assume that the
%set of clauses $S_1$ contains a splittable clause, i.e., $S_1$ is of the form
%$S'_1 \cup \{C_1 \lor \ldots \lor C_k\}$.  Splitting produces a tableau with
%branches $S'_1 \cup \{C_1\}$, \ldots, $S'_1 \cup \{C_k\}$, $S_2$, \ldots,
%$S_n$.  The new branches $S'_1 \cup \{C_i\}$, $1\leq i\leq k$, have closed
%semantic trees that are not larger than that of $S_1$, and proceeding produces
%tableaux with smaller and smaller branches.  (Formally, termination of
%splitting follows from using a multiset ordering on the multisets of sizes of
%branches.) Subsumption on each branch also clearly terminates.  Then
%resolution on the resulting branches can be made to decrease the size of
%closed semantic trees for each branch.  It follows that resolution (resp.\ 
%ordered, or any refinement complete by semantic trees) with subsumption and
%splitting applied eagerly will produce a tableau with all branches containing
%$\bot$ after finitely many steps, starting from any $\mathcal E$-unsatisfiable set
%$S$ of clauses.

%See \citet{BG:HAR} for further information about splitting, for different
%completeness proofs, and for an extremely general framework of resolution,
%refinements of resolution, and simplification rules.

% for splitting: BG:HAR, 10.2 (p.66)
% renaming: 8.1, p.44

%In this paper, we shall always take the following ordering.  Split the
%function symbols in $\Sigma$ in so-called {\em free\/} function symbols $f$,
%$g$, $h$, \ldots, and {\em AC\/} symbols $+_1$, \ldots, $+_p$.  The equational
%theory AC is associativity and commutativity of each operator $+_i$, $1\leq
%i\leq p$.  Then we let $P (s) > Q (t)$ if and only $s$ is a strict superterm
%of $t$, where the strict superterm relation is the smallest such that $f
%(\ldots, t, \ldots)$ is a strict superterm of $t$ for every free function
%symbol $f$, and $s$ is a strict superterm of $t$ if $s \approx_{\AC} t
%+_i u$ for some term $u$ and some $i$, $1\leq i\leq p$.

%On the other hand, we shall use the following positive selection function.  In
%$A \Leftarrow A_1, \ldots, A_n$, if some $+_i$ symbol occurs in the clause and
%$A \neq \bot$, then we select $A$; otherwise, no literal is selected.

% clauses; H1 clauses; alternating tree automata; non-deterministic TA;
% deterministic TA.

% complementation is Prolog negation.  Can be computed on tree automata.

% also, word automata (because of linauto).


\bibliographystyle{apalike}
\bibliography{h1}

\end{document}
