Linking focusing and resolution with selection

Guillaume Burel

► To cite this version:

Guillaume Burel. Linking focusing and resolution with selection. 43rd International Symposium on Mathematical Foundations of Computer Science(MFCS), Aug 2018, Liverpool, United Kingdom. pp.9:1-9:14, 10.4230/LIPIcs.MFCS.2018.9 . hal-01670476v3

HAL Id: hal-01670476

https://inria.hal.science/hal-01670476v3

Submitted on 27 Apr 2018

**HAL** is a multi-disciplinary open access
archive for the deposit and dissemination of sci-
entific research documents, whether they are pub-
lished or not. The documents may come from
teaching and research institutions in France or
abroad, or from public or private research centers.

L'archive ouverte pluridisciplinaire HAL, est
destinée au dépôt et à la diffusion de documents
scientifiques de niveau recherche, publiés ou non,
émanant des établissements d'enseignement et de
recherche français ou étrangers, des laboratoires
publics ou privés.

<figure><img src="image_1.png" /></figure>

Distributed under a Creative Commons Attribution 4.0 International License
# Linking Focusing and Resolution with Selection

Guillaume Burel

ENSIIE and Samovar, Télécom SudParis and CNRS, Université Paris-Saclay, Évry, France

Inria and LSV, CNRS and ENS Paris-Saclay, Université Paris-Saclay, Cachan, France

guillaume.burel@ensiie.fr

## Abstract

Focusing and selection are techniques that shrink the proof search space for respectively sequent calculi and resolution. To bring out a link between them, we generalize them both: we introduce a sequent calculus where each *occurrence* of an atom can have a positive or a negative polarity; and a resolution method where each literal, whatever its sign, can be selected in input clauses. We prove the equivalence between cut-free proofs in this sequent calculus and derivations of the empty clause in that resolution method. Such a generalization is not semi-complete in general, which allows us to consider complete instances that correspond to theories of any logical strength. We present three complete instances: first, our framework allows us to show that ordinary focusing corresponds to hyperresolution and semantic resolution; the second instance is deduction modulo theory and the related framework called superdeduction; and a new setting, not captured by any existing framework, extends deduction modulo theory with rewriting rules having several left-hand sides, which restricts even more the proof search space.

**2012 ACM Subject Classification** Theory of computation → Proof theory Theory of computation → Automated reasoning

**Keywords and phrases** logic in computer science, automated deduction, proof theory, sequent calculus, refinements of resolution, deduction modulo theory, polarization

Related Version https://hal.inria.fr/hal-01670476

## 1 Introduction

In addition to clever implementation techniques and data structures, a key point that explains the success of state-of-the-art automated theorem provers is the use of calculi that dramatically reduce proof search space. In the last decades, the independent developments of two families of techniques can be highlighted. First, in the kind of methods based on resolution, proof search space can be shrunk using ordering and selection techniques. The intuition is to restrict the application of the resolution rule to only some literals in a clause. If equality is considered, this leads to the superposition calculus [2] which is the base calculus of the currently most efficient automated provers for first-order classical logic. Second, in sequent calculi, Andreoli [1] introduced a technique called focusing to reduce non-determinism in the application of sequent-calculus rules. It works by first applying all invertible rules (those whose conclusion is logically equivalent to their premises) and second by chaining the application of non-invertible rules. Originally developed for linear logic, focusing has been extended to intuitionistic and classical first-order logic [28]. Focusing is mostly used in fields where sequent calculi, and related inverse and tableaux methods, are the most accurate proving method. For instance, there exists tools for first-order linear logic [13], for intuitionistic logic [29] and for modal logic [30]. Focusing is also the key ingredient in Miller's ProofCert project aiming at building a universal framework for proof certification [16].

Despite their apparent lack of relation, we show in this paper that selection in refinements of the resolution calculus and focusing in sequent calculus are in fact strongly related, so that ordinary focusing in classical first-order logic corresponds actually to hyperresolution,
23:2 Linking Focusing and Resolution with Selection

where all negative literals are selected in a clause and are resolved at once. This connection is obtained by relaxing both techniques: concerning resolution, we allow any literal of the input clauses to be selected, whatever its sign; for the focusing part, we allow polarization not only of connectives, but also of all occurrences of literals. The main theorem of this paper, Theorem 3, shows that the sets of clauses whose insatisfiability can be proved by the resolution method with arbitrary input selection are exactly the sequents that have a cut-free proof in the generalized focusing setting.

This generalization allows us to cover a wider spectrum of proof systems. In particular, this permits to consider systems that search for proofs modulo some theory. Indeed, in real world applications, proof obligations are often verified within one or several theories. This explains the interest in and the success of Satisfiability Modulo Theory tools in recent years. Embedding a theory in our framework amounts to giving an axiomatic presentation of it where some literals are selected.

By relaxing the conditions for selecting literals, our framework is not always refutationally complete. However, this should not be considered as a drawback, but as an essential point to be able to represent efficiently all kinds of theories. Indeed, let us consider a proof search method $\mathbb{P}(\mathcal{T})$ parameterized by a theory $\mathcal{T}$. Ideally, $\mathbb{P}(\mathcal{T})$ should be as efficient as a generic proof search metho if it is fed with a formula that is not related to the theory $\mathcal{T}$. In particular, if it tries to refute the true formula $\top$, it should terminate, and with the answer “NO”. Let us say that $\mathbb{P}(\mathcal{T})$ is relatively consistent if it is the case. As we pointed out with Dowek [9], we cannot have a generic proof of the completeness of a relatively consistent method $\mathbb{P}(\mathcal{T})$ that would work for all $\mathcal{T}$. Indeed, such a proof would imply the consistency of the theory $\mathcal{T}$, and, according to Gödel, this cannot be performed in $\mathcal{T}$ itself. So either the completeness of the proof system is proved once and for all, but it cannot represent theories that are logically at least as strong as that proof of completeness; or it is not complete in general but it can be proved to be complete for particular theories of some arbitrary logical strength. What is interesting therefore is to give proofs of completeness of $\mathbb{P}(\mathcal{T})$ for particular theories $\mathcal{T}$.

Therefore, we give three instances of our framework, where we can have proofs of completeness. First, as stated above, we link ordinary focusing with hyperresolution, and, in the ground case, with semantic resolution. Second, we show that Deduction Modulo Theory [21] is also a particular instance of this framework, knowing that there exists numerous proof techniques to prove the completeness of Deduction Modulo a particular theory, for instance [25, 22, 19, 8]. Third, we show how completeness in our framework can be reduced to completeness of several instances of Deduction Modulo Theory. To give an intuition about this last part, and to illustrate how much the proof search space can be constrained without losing completeness, let us consider for example the theory defining the powerset:

$$ \forall X, \forall Y, (X \in \mathcal{P}(Y)) \Leftrightarrow (\forall Z, (Z \in X) \Rightarrow (Z \in Y)) $$

This theory can be put in clausal normal form, using $d$ as a Skolem symbol, and we select (by underlining them) some literals in these clauses<fnref n="1" />:

$$ \neg X \in \mathcal{P}(Y) \Upsilon \neg Z \in X \Upsilon Z \in Y \qquad (1) $$

$$ X \in \mathcal{P}(Y) \Upsilon d(X, Y) \in X \qquad (2) $$

$$ X \in \mathcal{P}(Y) \Upsilon \neg d(X, Y) \in Y \qquad (3) $$

<footnote n="1">¹ We use the associative-commutative-idempotent symbol $\Upsilon$ in clauses to distinguish it from the symbol $\vee$ that is used in formulas.</footnote>
Using focusing in general, and in our framework in particular, the decomposition of connectives is so restricted that, given an axiom, a proof derivation decomposing this axiom would necessarily have certain shapes. Thus, the axiom can be replaced by new inference rules, called synthetic rules, that are used instead of the derivation of those shapes. See end of Section 2, page 6, for more details. In our framework, this would lead to the following three synthetic rules, that can be used in place of the axioms (the explanation how these rules are obtained is given in Section 5.3):

$$ (1) \vdash \frac{\Delta, u \in \mathcal{P}(v), t \in u, t \in v \vdash}{\Delta, u \in \mathcal{P}(v), t \in u \vdash} $$

$$ (2) \vdash \frac{\Delta, \neg u \in \mathcal{P}(v), d(u, v) \in v \vdash}{\Delta, \neg u \in \mathcal{P}(v), d(u, v) \in v \vdash} $$

$$ (3) \vdash \frac{\Delta, \neg u \in \mathcal{P}(v), d(u, v) \in u \vdash}{\Delta, \neg u \in \mathcal{P}(v) \vdash} $$

The only proof of transitivity of the membership in the powerset is then

$$ (2) \vdash \frac{a \in \mathcal{P}(b), b \in \mathcal{P}(c), \neg a \in \mathcal{P}(c), d(a, c) \in a, d(a, c) \in b, d(a, c) \in c \vdash}{a \in \mathcal{P}(b), b \in \mathcal{P}(c), \neg a \in \mathcal{P}(c), d(a, c) \in a, d(a, c) \in b \vdash} $$

$$ (1) \vdash \frac{a \in \mathcal{P}(b), b \in \mathcal{P}(c), \neg a \in \mathcal{P}(c), d(a, c) \in a, d(a, c) \in b \vdash}{a \in \mathcal{P}(b), b \in \mathcal{P}(c), \neg a \in \mathcal{P}(c), d(a, c) \in a \vdash} $$

$$ (1) \vdash \frac{a \in \mathcal{P}(b), b \in \mathcal{P}(c), \neg a \in \mathcal{P}(c), d(a, c) \in a \vdash}{a \in \mathcal{P}(b), b \in \mathcal{P}(c), \neg a \in \mathcal{P}(c) \vdash} $$

$$ (3) \vdash \frac{a \in \mathcal{P}(b), b \in \mathcal{P}(c), \neg a \in \mathcal{P}(c) \vdash}{a \in \mathcal{P}(b), b \in \mathcal{P}(c), \neg a \in \mathcal{P}(c) \vdash} $$

$$ \wedge \vdash \frac{a \in \mathcal{P}(b) \wedge b \in \mathcal{P}(c) \wedge \neg a \in \mathcal{P}(c) \vdash}{a \in \mathcal{P}(b) \wedge b \in \mathcal{P}(c) \wedge \neg a \in \mathcal{P}(c) \vdash} $$

$$ \exists \vdash \frac{\exists A. \exists B. \exists C. A \in \mathcal{P}(B) \wedge B \in \mathcal{P}(C) \wedge \neg A \in \mathcal{P}(C) \vdash}{\exists A. \exists B. \exists C. A \in \mathcal{P}(B) \wedge B \in \mathcal{P}(C) \wedge \neg A \in \mathcal{P}(C) \vdash} $$

where the active formulas in a sequent are underwaved, and double lines indicate potentially several applications of an inference rule.

On the resolution side, clauses (1) to (3) lead to the following ground derived rules (see also Section 5.3):

$$ (1) \frac{u \in \mathcal{P}(v) \Upsilon C \quad t \in u \Upsilon D}{t \in v \Upsilon C \Upsilon D} $$

$$ (2) \frac{\neg u \in \mathcal{P}(v) \Upsilon C}{d(u, v) \in u \Upsilon C} $$

$$ (3) \frac{\neg u \in \mathcal{P}(v) \Upsilon C \quad d(u, v) \in v \Upsilon D}{C \Upsilon D} $$

Once again, there is only one proof of transitivity, i.e. starting from the set of clauses $\{a \in \mathcal{P}(b); b \in \mathcal{P}(c); \neg a \in \mathcal{P}(c)\}$:

$$ (1) \frac{a \in \mathcal{P}(b)}{b \in \mathcal{P}(c)} \frac{(2) \frac{\neg a \in \mathcal{P}(c)}{d(a, c) \in a}}{d(a, c) \in b} $$

and we cannot even infer other clauses than those. We let the reader compare with what happens if we used clauses (1) to (3) in resolution, even using the ordered resolution with selection refinement.

**Related work.** Chaudhuri et al. [14] show that hyperresolution for Horn clauses can be explained as an instance of a sequent calculus for intuitionistic linear logic with focusing where atoms are given a negative polarity.

Farooque et al. [24] developed a sequent calculus, based on focusing, that is able to simulate DPLL($\mathcal{T}$), the most common calculus used in SMT provers. The main difference with our framework is that in [24], the theory is considered as a black box which is called as an oracle. Here, the theory is considered as a first-class citizen.

Within the ProofCert project, resolution proofs can be checked by a kernel built upon a sequent calculus with focusing [16]. Based on this, the tool Checkers [15] is able to
23:4 Linking Focusing and Resolution with Selection

verify proofs coming from automated theorem provers based on resolution such as E-prover.
Different from here, they translate resolution derivations using cuts to get smaller proofs.

Hermant [26] proves the correspondance between the cut-free fragment of a sequent
calculus and a resolution method, in the setting of Deduction Modulo Theory. Since
Deduction Modulo Theory is subsumed by our framework, Theorem 3 is a generalization of
Hermant's work. Proving it is simpler in our setting because focusing restrains the shape of
possible sequent calculus proofs, whereas Hermant had to prove technical lemmas to give
proofs a canonical shape.

**Notations and conventions.** We use standard definitions for terms, predicates, formulas (with connectives $⊥$, $⊤$, $¬$, $∧$, $∨$ and quantifiers $∀$, $∃$), sequents and substitutions. A literal is an atom or its negation. A clause is a set of literals. We will identify a literal with the unit clause containing it. Unless stated otherwise, letters $P, Q, R, P', P_1, ...$ denote atoms, $L, K, L', L_1, ...$ denote literals, $A, B, A', A_1, ...$ denote formulas, $C, D, C', C_1, ...$ denote clauses, $Γ, Δ$ denote set of clauses or set of formulas (depending on the context). $A^⊥$ denotes the negation normal form of $¬A$.

2 Focusing with Polarized Occurrences of Atoms

Focusing was introduced by Andreoli [1] to restrict the non-determinism in some sequent calculus for linear logic. It relies on the alternation of two phases: During the asynchronous phase (sequents with $\Uparrow$), all invertible rules are applied on the formulas of the sequent. Recall that a rule is said invertible if its conclusion implies the conjunction of its premises. During the synchronous phase (sequents with $\Downarrow$), a particular formula is selected —the focus is on it— and all possible non-invertible rules are successively applied on it. This idea has been extended to intuitionistic and classical first-order logic [28]. In these, connectives may have invertible and non-invertible versions of their sequent calculus rules. Therefore, one considers in that case two versions of a connective, one called positive when the right introduction rule is non-invertible, and one called negative when it is invertible. Some connectives, i.e. $∃$ in classical logic, only have a positive version, and dually, others, such as $∀$ in classical logic, only have a negative version. Given a usual formula, one can decide which version of a connective one wants to use at a particular occurrence, which is called a polarization of the formula.<fnref n="2" /> Note that the polarity of a connective does not affect its semantics, it only alters the shape of the sequent calculus proofs. Similarly, one can decide the polarity of each literal. If a literal with negative polarity $L$ is focused on in a branch, then this branch must necessarily be closed, with $L^⊥$ in the same context. (See rule $\overline{L \vdash}$ in Figure 1.) In the ordinary presentation of focusing, this polarity is chosen globally for all occurrences of each atom, and the polarity of $¬P$ is defined as the inverse of that of $P$. In our setting, the polarity is attached to the position of the literal in the formula. In particular, if a substitution is applied to the formula, the polarities of the resulting literals do not change. The polarity of a formula is defined as the polarity of its top connective. Besides, note that to switch the polarity of a formula, e.g. to impose a change of phase, one can prefix it by so-called delays: $\delta^−A$ is negative whatever the polarity of $A$. Delays can be defined for instance by $\delta^−A = ∀x. A$ where $x$ is not free in $A$, so we do not need them in the syntax and the rules.

<footnote n="2">² Let us note that this notion of polarity is a standard denomination when dealing with focusing, and should not be confused with the more usual but unrelated notion defined by the parity of the negation-depth of a position in a formula.</footnote>
<figure><img src="image_2.png" /><figcaption>■ **Figure 1** The sequent calculus LKF<sup>⊥</sup></figcaption></figure>

Liang and Miller [28] introduce the sequent calculus LKF, and prove it to be complete for classical first-order logic. In Figure 1, we present the calculus LKF<sup>⊥</sup>, which is almost the same with the following differences:

■ All formulas are put on the left-hand side of the sequent, instead of the right-hand side. Therefore, one does not try to prove a disjunction of formulas, but one tries to refute a conjunction of formulas. This is the same thanks to the dual nature of classical first-order logic, and this helps to be closer to the resolution derivations. Note that, consequently, the focus is on negative formulas, and invertible rules are applied on positive formulas.

■ The polarity of atoms is not chosen globally, but each *occurrence* of a literal can have a positive or a negative polarity. In particular, we can have two literals *L* and *L*<sup>⊥</sup> which are both negative, or both positive. We denote by *L* the fact that the literal *L* has a negative polarity. To be able to close branches on which we have two positive opposed literals, we add a rule $\hat{\leftrightarrow}$.

We denote by $\Gamma \Uparrow \Delta \vdash$ (with $\Gamma$ or $\Delta$, possibly empty, containing polarized formulas) the fact that there exists a proof of the sequent $\Gamma \Uparrow \Delta \vdash$ in LKF<sup>⊥</sup>, that is, a derivation starting from this sequent and whose branches are all closed (by $\hat{\leftrightarrow}$, $\hat{\Uparrow}$ or $\Uparrow \bot \leftrightarrow$). Thanks to focusing, such a proof has the following shape :

■ Since one starts in an asynchronous (↑) phase, invertible rules are successively applied to the positive formulas of $\Delta$, until one obtains negative formulas or literals that are put on the left of ↑ using **Store**.

■ When no formula appears on the right of ↑, then either the branch is closed by $\hat{\leftrightarrow}$; or the focus is put on a negative formula using **Focus**.

■ In the latter case, one is now in synchronous (↓) phase where non-invertible rules are successively applied to the formula upon which the focus is, until either the branch is closed using $\hat{\leftrightarrow}$ or $\Uparrow \bot \leftrightarrow$; or one obtains a positive formula and the synchronous phase ends using **Release**.

■ In the latter case, one starts again in the asynchronous phase.

Focusing therefore strongly constrains the shape of possible proofs, and therefore reduces the proof search space. The $\hat{\leftrightarrow}$ in particular imposes to close branches immediately when the focus is on a negative literal, and thus rules out many derivations.

Note that proofs can be closed when the polarities of an atom and its negation are both positive (rule $\hat{\leftrightarrow}$), or when one is positive and the other negative (rule $\hat{\Uparrow}$), but not when
23:6 Linking Focusing and Resolution with Selection

they are both negative. Therefore, this restricts how formulas that contains literals with
negative polarities can interact one with the others, and this is the main point of LKF⊥ to
reduce the proof search space.

Restricting proof search using focusing leads to what are called synthetic rules (see for
instance [14, pp.148–150] where they are called derived rules). The idea is to replace some
formula A in the context of the sequent by new inference rules. Instead of proving the sequent
A, Δ ↠ in LKF⊥, one proves Δ ↠ in (LKF⊥+ the synthetic rules obtained from A). Indeed,
a proof focusing on A can only have certain shapes, and thus instead of having A in the
context, it can be replaced by new rules synthesizing those shapes. For instance, the formula
P ∨ (Q ∧+ R) in a context Γ can only lead to the following derivations when the focus is
put on it:

<figure><img src="image_3.png" /></figure>

In the left derivation, $P^{\perp}$ must be in $\Gamma$ to be able to close the left branch, so $\Gamma$ is in fact of the
form $\underline{P} \vee^{-} (Q \wedge^{+} \underline{R})$, $\Delta, P^{\perp}$. In the right one, $\Gamma$ must be of the form $\underline{P} \vee^{-} (Q \wedge^{+} \underline{R})$, $\Delta, P^{\perp}, R^{\perp}$.
Instead of searching for a proof with $\underline{P} \vee^{-} (Q \wedge^{+} \underline{R})$ in the context, the following two synthetic
rules can therefore be used:

<figure><img src="image_4.png" /></figure>

Provability is the same because each application of a synthetic rule can be replaced by applying Focus on $\underline{P} \vee^{-} (Q \wedge^{+} \underline{R})$ and following the derivation leading the synthetic rule, and vice versa. This is used for instance in provers based on the inverse method and focusing [29].

The sequent calculus LKF⊥ is not complete in general. One of the simplest examples of incompleteness is the sequent $\underline{P} \vee^{-} Q, \neg \underline{P} \vee^{-} Q, \neg Q \Uparrow \vdash$ which has no proof although $P \vee Q, \neg P \vee Q, \neg Q$ is not satisfiable.

3 Resolution with Input Selection

Two approaches can be used to reduce the proof search space of the resolution calculus: first,
one can restrict on which pairs of clauses the resolution rule can be applied; this leads for
instance to the set-of-support strategy [34], in which clauses are split into two sets, called the
theory and the set of support; at least one of the clauses involved in a resolution step must
be in the set of support. Second, one can restrict which literals in the clauses can be resolved
upon; those literals are said to be selected in the clause. Resolution with free selection is
complete for Horn clauses, but incomplete in general. Selecting a subset of the negative
literals (if no literal is selected, then any literal of the clause can be used in resolution) is
however complete, and combining this with an ordering restriction on clauses with no selected
literals leads to Ordered Resolution with Selection, which was introduced by Bachmair and
Ganzinger [2] (see also [3]) as a complete refinement of resolution.

Resolution with Input Selection combines these two approaches. It is parameterized by a selection function $S$ that associate to each input clause a subset of its literals. If the selection function selects at least one literal, only those can be used in Resolution. Otherwise, any of them can be used. Note that for generated clauses, we impose that $S(C) = \emptyset$. We also allow to have the same input clause several times with different selections. (That is, we
Resolution $\frac{L \gamma C \qquad L' \perp \gamma D}{\sigma(C \gamma D)}$

■ $S(L \gamma C) = \emptyset$

■ $S(L' \perp \gamma D) = \emptyset$

■ $\sigma$ is the most general unifier of $L = ? L'$

Factoring $\frac{L \gamma L' \gamma C}{\sigma(L \gamma C)}$

■ $S(L \gamma L' \gamma C) = \emptyset$

■ $\sigma$ is the most general unifier of $L = ? L'$

Resolution with Selection $\frac{\underline{K_1} \gamma \dots \gamma \underline{K_n} \gamma C \qquad K_1' \perp \gamma D_1 \qquad \dots \qquad K_n' \perp \gamma D_n}{\sigma(C \gamma D_1 \gamma \dots \gamma D_n)}$

■ $S(\underline{K_1} \gamma \dots \gamma \underline{K_n} \gamma C) = \{K_1; \dots; K_n\}$

■ $S(K'_i \perp \gamma D_i) = \emptyset$

■ $\sigma$ is the mgu of the simultaneous unification problem $K_1 = ? K'_1, \dots, K_n = ? K'_n$

<caption>Figure 2 Resolution with Input Selection</caption>

222

223

224

225

226

227

228

229

230

231

232

233

234

actually work with couples composed of a clause and its selected literals.) The inference rules of Resolution with Input Selection are presented in Fig. 2. Literals that are selected in a clause are underlined. We will see that they indeed correspond to the literals that have a negative polarization in LKF$^{\perp}$. As usual, variables are renamed in the clauses to avoid that premises of the inference rules share variables. We have two flavors of the resolution rule: the usual binary resolution, that is applied on two premises that do not select any literal; and Resolution with Selection that is applied on a clause in which $n$ literals are selected and $n$ clauses is which no literal is selected. Consequently, clauses with a non-empty selection cannot be resolved one with the others. By considering them as the theory part, and the clauses with an empty selection as the set of support, it is easy to see that Resolution with Input Selection is a generalization of the set-of-support strategy. Notwithstanding, note that neither Resolution with Input Selection is a generalization of Ordered Resolution with Selection nor the converse.

235

236

237

► **Definition 1 (Resolution derivation).** We write $\Gamma \rightsquigarrow C$ if $C$ can be derived from some clauses in $\Gamma$ using the inference rules Resolution with Selection, Resolution, or Factoring presented in Figure 2. We write $\Gamma \rightsquigarrow^* C$ if

238

■ $C \in \Gamma$ or if

239

■ there exists $D$ such that $\Gamma \rightsquigarrow D$ and $\Gamma, D \rightsquigarrow^* C$.

240

241

242

243

244

As usual in resolution methods, the goal is to produce the empty clause $\Box$ starting from a set of clauses $\Gamma$ to show, since all rules are sound, that $\Gamma$ is unsatisfiable. Here again, the calculus is not complete in general: from the set of clauses $\underline{P} \gamma Q, \neg \underline{P} \gamma Q, \neg Q$, no inference rule can be applied: to apply Resolution with Selection, we would need a clause where $P$, or $\neg P$, is not selected, and Resolution needs two clauses without selection.

245

246

## 4 LKF$^{\perp}$ is a Conservative Extension of Resolution with Input Selection

247

248

To link LKF$^{\perp}$ with Resolution with Input Selection, we need to indicate how clauses are related to polarized formulas.

249

250

251

252

► **Definition 2.** Given a clause $C = \underline{L_1} \gamma \dots \gamma \underline{L_n} \gamma K_1 \gamma \dots \gamma K_m$ whose free variables are $x_1, \dots, x_l$ and such that $S(C) = \{L_1; \dots; L_n\}$, we define the associated formula $\lceil C \rceil = \forall x_1, \dots, x_l. \underline{L_1} \vee^- \dots \vee^- \underline{L_n} \vee^- \delta^-(K_1 \vee^+ \dots \vee^+ K_m)$. $\lceil C \rceil$ is said to be in clausal form. By extension, $\lceil \Gamma \rceil$ is the set of the formulas associated to the clauses of the set $\Gamma$.
The main theorem of this article relates LKF⊥ with Resolution with Input Selection:

**Theorem 3.** Let $\Gamma$ be a set of clauses. We have $\Gamma \models \Gamma \vdash$ iff $\Gamma \leadsto *$. □

The proof is given in the appendix. To prove the right-to-left direction, we prove that all inference rules of Resolution with Input Selection are admissible in LKF⊥, in the sense that if $\Gamma \leadsto C$ then LKF⊥ proofs of $\Gamma \models \Gamma \vdash$ can be turned into proofs of $\Gamma \models \Gamma \vdash$. Note that they are admissible, but they are not derivable. In particular, the size of the proof in LKF⊥ can be much larger than the resolution derivation, as expected in a cut-free sequent calculus. Using cuts would lead to a closer correspondence between resolution derivations and sequent-calculus proofs, as in [16]. However, we chose to stay in the cut-free fragment to prove that, even in the incomplete case, resolution coincides with cut-free proofs, as in [26].

# 5 Complete Instances

## 5.1 Ordinary Focusing and Semantic Hyperresolution

As said earlier, in standard LKF, not all occurrences of literals can have an arbitrary polarity. Instead, each atom $P$ is given globally a polarity, and $P^\perp$ has the opposite polarity.

Let us first look at the simple case where atoms are given a positive polarity. We recall the completeness proof of LKF:

**Theorem 4 (Corollary of [28, Theorem 17]).** If the literals with a positive polarity are exactly the atoms, LKF⊥ is (sound and) complete.

If we look at the corresponding resolution calculus, Resolution with Selection for this particular instance becomes:

$$ \text{R.w.S.} \frac{\neg P_1 \Upsilon \dots \Upsilon \neg P_n \Upsilon C \qquad P'_1 \Upsilon D_1 \dots P'_n \Upsilon D_n}{\sigma(C \Upsilon D_1 \Upsilon \dots \Upsilon D_n)} $$

where $C$ and $D_i$ for all $i$ contain only positive literals, and $\sigma$ is the most general unifier of $P_1 =? P'_1, \dots, P_n =? P'_n$. Note that the clause $\sigma(C \Upsilon D_1 \Upsilon \dots \Upsilon D_n)$ contains only positive literals, so no literal would be selected in it even if it was an input clause. Besides, Resolution cannot be applied, since there exists no clause $\neg P \Upsilon C$ with $S(\neg P \Upsilon C) = \emptyset$.

This corresponding resolution calculus is therefore exactly hyperresolution of [31]: premises of an inference contains all only positive literals, except one clause whose all negative literals are resolved at once. Theorem 3 therefore links ordinary focusing with hyperresolution. Consequently, Theorem 4 implies the completeness of hyperresolution.

Chaudhuri et al. [14, Theorem 16] prove a similar result by establishing a correspondence between hyperresolution derivations and proofs in a focused sequent calculus for intuitionistic linear logic, but only considering Horn clauses. In their setting, choosing a negative polarity for atoms leads to SLD resolution, which is the reasoning mechanism of Prolog.

Let us now look at the general case, where atoms are given an arbitrary polarity. Let us stick to the ground case. We first recall a refinement of resolution called Semantic hyperresolution [33][12, Sect. 1.3.5.3]. Let $I$ be an arbitrary Herbrand interpretation, i.e. a model whose domain is the set of terms interpreted as themselves. Note that $I$ is not assumed to be a model of the input set of clauses (which is fortunate, since one is trying to show that it is unsatisfiable). Given a clause $C$, the idea of semantic hyperresolution is to resolve all literals of $C$ that are valid in $I$ at once, with clauses whose literals are all not valid in $I$. This gives the rule:
294

$$ \text{SHR} \frac{K_1 \gamma \dots \gamma K_n \gamma C \quad K_1^{\perp} \gamma D_1 \quad \dots \quad K_n^{\perp} \gamma D_n}{C \gamma D_1 \gamma \dots \gamma D_n} $$

295

296

where for all $i$, $I \models K_i$ (and thus $I \not\models K_i^{\perp}$), $I \not\models C$ and $I \not\models D_i$. Note that $I \not\models C \gamma D_1 \gamma \dots \gamma D_n$.

297

298

299

300

301

Semantic hyperresolution for a Herbrand interpretation $I$ can be seen as an instance of Resolution with Input Selection by using the following polarization of atoms: a literal $L$ has a negative polarity iff $I \models L$. In that case, SHR corresponds exactly to Resolution with Selection, and Resolution cannot be applied since we cannot have clauses $P \gamma C$ and $\neg P \gamma D$ where both $P$ and $\neg P$ are not valid in $I$.

302

303

304

305

306

This particular instance of polarization is in fact the ordinary version of focusing. Indeed, once a global polarity is assigned to each atom, the set of literals whose polarity is negative defines an Herbrand interpretation, and we saw reciprocally how to design a global polarization from the Herbrand interpretation. Theorem 3 therefore links ordinary focusing in the ground case with semantic hyperresolution. They are both complete, thanks to this theorem:

307

308

**► Theorem 5 (Corollary of [28, Theorem 17]).** *Given a global polarization of atoms, where the polarity of $P^{\perp}$ is the opposite of that of $P$, LKF$^{\perp}$ is (sound and) complete.*

309

## 5.2 Deduction Modulo Theory

310

311

312

313

314

315

316

317

318

319

320

321

322

323

Deduction Modulo Theory [21] is a framework that consists in applying the inference rules of an existing proof system modulo some congruence over formulas. This congruence represents the theory, and it is in general defined by means of rewriting rules. To be expressive enough, these rules are defined not only at the term level, but also for formulas. To get simpler presentations of theories, we distinguish between rewrite rules that can be applied at positive and at negative positions by giving them a polarity$^3$, where by negative position we mean under an odd number of $\neg$. We therefore have positive rules $P \to^+ A$ and negative rules $P \to^- A$ where $P$ is an atom and $A$ an arbitrary formula whose free variables appears in $P$. Given a rule $P \to^+ A$, the rewrite relation $B_1 \stackrel{\pm}{\to} B_2$ is defined as usual by saying that there exists a position $p$ and a substitution $\sigma$ such that the subformula of $B_1$ at position $p$ is $\sigma P$ and $B_2$ equals $B_1$ where the subformula at position $p$ is replaced by $\sigma A$. $\stackrel{\dasharrow}{\to}$ is defined similarly. In Polarized Sequent Calculus Modulo theory [18], the inference rules of the sequent calculus are applied modulo such a polarized rewriting system, as in for instance $\text{in } \leftarrow \frac{\Gamma \vdash A, \Delta \quad \Gamma \vdash B, \Delta}{\Gamma \vdash C, \Delta} C \stackrel{\pm}{\to} *A \wedge B$. Note that the implicit semantics of a negative rule $P \to^- A$ is therefore $\forall x$. ($P \Rightarrow A$), whereas the semantics of $P \to^+ A$ is $\forall x$. ($A \Rightarrow P$), where $\bar{x}$ are the free variables of $P$.

324

325

326

327

328

329

330

331

332

333

With Kirchner [10], we proved the equivalence of Polarized Sequent Calculus Modulo theory to a sequent calculus where polarized rewriting rules are applied only on literals, using explicit rules. This calculus, Polarized Unfolding Sequent Calculus, is almost the calculus PUSC$^{\perp}$ presented in Figure 3. The only difference is that all formulas are put on the left of the sequent in PUSC$^{\perp}$. We denote by $\Gamma \vdash_R$ the fact that $\Gamma \vdash$ can be proved in PUSC$^{\perp}$ using the polarized rewriting system $\mathcal{R}$. Note that the rule for the universal quantifier $\forall \leftarrow$ as well as the unfolding rules $\uparrow \leftarrow$ and $\uparrow \leftarrow$ contain an implicit contraction rule, as in the sequent calculus G4 of Kleene, in order to ensure that all rules of PUSC$^{\perp}$ are invertible.

We can translate polarized rewriting rules as formulas with selection, and see PUSC$^{\perp}$ as an instance of LKF$^{\perp}$. We first consider how to translate formulas of the right-hand side of

<footnote>$^3$ This polarity must not be confused with the other notions of polarity mentioned in the paper.</footnote>
23:10 Linking Focusing and Resolution with Selection

<figure><img src="image_5.png" /><figcaption>■ **Figure 3** The sequent calculus PUSC$^{⊥}$</figcaption></figure>

<figure><img src="image_6.png" /><figcaption>■ **Figure 4** Inference rules of Polarized Resolution Modulo theory</figcaption></figure>

polarized rewriting rules. We polarize them by choosing positive connectives for $\vee$ and $\wedge$ and, to unchain the introduction of the universal quantifier, we introduce delays. (Let us recall that a delay $\delta^+$ allows to force a formula to be positive, and it can be encoded using an existential quantifier.) This gives the translation:

<figure><img src="image_7.png" /></figure>

► **Definition 6.** Given a negative rewriting rule $P \to^- A$ where the free variables of $P$ are $x_1, \dots, x_n$, its translation as a formula with selection is $\llbracket P \to^- A \rrbracket = \forall x_1 \dots \forall x_n. \neg P \vee^- \delta^+ |A|$.

Given a positive rewriting rule $P \to^+ A$ where the free variables of $P$ are $x_1, \dots, x_n$, its translation as a formula with selection is $\llbracket P \to^+ A \rrbracket = \forall x_1 \dots \forall x_n. \underline{P} \vee^- \delta^+ |A^\perp|$.

The translation $\llbracket \mathcal{R} \rrbracket$ of a polarized rewriting system $\mathcal{R}$ is the multiset of the translation of its rules.

► **Definition 7.** Let $N_1, \dots, N_n$ be a multiset of formulas whose top connective is $\forall$ or $\perp$ or that are literals, and let $P_1, \dots, P_m$ be a multiset of non-literal formulas whose top connective is neither $\forall$ nor $\perp$, then the translation of the PUSC$^{⊥}$ sequent $N_1, \dots, N_n, P_1, \dots, P_m$ Modulo the rewriting system $\mathcal{R}$ is the LKF$^{⊥}$ sequent $\llbracket \mathcal{R} \rrbracket, |N_1|, \dots, |N_n| \Uparrow |P_1|, \dots, |P_m| \searrow$.

► **Theorem 8.** $N_1, \dots, N_n, P_1, \dots, P_m \vdash_{\mathcal{R}}$ in PUSC$^{⊥}$ iff $\llbracket \mathcal{R} \rrbracket, |N_1|, \dots, |N_n| \Uparrow |P_1|, \dots, |P_m| \vdash$ in LKF$^{⊥}$.

The proof is given in the appendix.

Let us now consider the subcase where the rewriting rules are clausal, according to the terminology of [20], e.g. they are of the form $P \to^- C$ or $P \to^+ \neg C$ for some formula $C$ in clausal normal form. In that case, the resolution method based on Deduction Modulo Theory [21] can be refined into what is called Polarized Resolution Modulo theory [20], whose rules are given in Fig. 4. (A refinement of) Polarized Resolution Modulo theory is actually implemented in the automated theorem prover iProverModulo [6].

By noting that the translation of the rule $Q \to^- D$ is $\llbracket Q \to^- D \rrbracket = \forall x_1 \dots \forall x_n. \neg Q \vee^-$, whereas $\lceil \neg Q \gamma D \rceil = \forall x_1 \dots \forall x_n. \neg Q \vee^- \delta^- |D|$, we can relate the rule $Q \to^- D$ with the clause with selection $\neg Q \gamma D$, which is called a one-way clause by [20]. Indeed,
23:12 Linking Focusing and Resolution with Selection

395 The question that remains is how we can prove the completeness of such a selection. We can
396 in fact consider only subselections.

397 ▶ **Definition 10 (Singleton subselection).** Given a selection function $S$, the selection function
398 $S_1$ is a singleton subselection of $S$ if

399 $\underline{S_1}(C) \subseteq S(C)$ for all $C$

400 $\underline{\text{if }} S(C) \neq \emptyset$ then $\text{card}(S_1(C)) = 1$

▶ **Example 11.** A singleton subselection of Example 9 can be

$$
\neg X \in \mathcal{P}(Y) \Upsilon \neg Z \in \underline{X} \Upsilon Z \in Y \qquad \underline{X} \in \mathcal{P}(Y) \Upsilon d(X, Y) \in X \qquad \underline{X} \in \mathcal{P}(Y) \Upsilon \neg d(X, Y) \in Y
$$

401 ▶ **Theorem 12.** *Resolution with input selection *S* is complete iff for all singleton subselections
402 *S*₁ of *S*, *Resolution with input selection S*₁ *is complete*.

403 Since singleton subselections can be linked with rewriting systems in Deduction Modulo
404 Theory according to last subsection, we can reduce the problem of completeness in our
405 framework to several problems of completeness in Deduction Modulo Theory.

406 Conclusion and Further Work

407 We generalized focusing and resolution with selection, proved that they correspond, and
408 showed how known calculi are instances of this framework, namely ordinary focusing, hy-
409 perresolution, Deduction Modulo Theory and Superdeduction. We also showed how to
410 reduce completeness of this framework to several completeness proofs in Deduction Modulo
411 Theory. We can therefore reuse the various techniques for proving completeness in Deduction
412 Modulo Theory [25, 22, 19, 8] in our framework. As Deduction Modulo Theory already
413 gives significant results in industrial applications when the theory is a variant of set theory
414 (more precisely, set theory of the B method) [11], we can expect our framework to lead to
415 even better outcomes. The notable results presented here raise the following new areas of
416 investigations.

417 First, we need to study how to apply selection also in the generated clauses. This should
418 allow us to cover the cases of Ordered Resolution with Selection and of Semantic Resolution
419 in the first-order case. Dually, in the sequent calculus part, this would correspond to the
420 possibility to dynamically add selection in formulas of subderivations. This could probably
421 be linked with the work of Deplagne [17] where rewrite rules corresponding to induction
422 hypotheses are dynamically added in the rewriting system of a sequent calculus for Deduction
423 Modulo Theory. Note that we already have one direction, namely from Resolution with
424 Input Selection to LKF⊥, since Lemmas 17, 19, and 20 do not assume anything on the
425 generated clauses; except, for Factoring, that it selects only instances of literals that were
426 already selected. The converse direction would require a meta-theorem of completeness, since
427 obviously it is not complete for all possible dynamic choices of selection.

428 Since focusing is defined not only for classical first-order logic but also for linear, intu-
429 itionistic, modal logics, the work in this paper could serve as a starting point to study how
430 to get automated proof search methods for these logics with a selection mechanism.

431 Another worthwhile point is how equality should be handled in our framework. In partic-
432 ular, it would be interesting to see how paramodulation calculi, in particular superposition,
433 can be embedded into a sequent calculus.

434 Finally, it would be worth investigating whether completeness proofs based on model
435 construction, such as semantic completeness proofs of tableaux (related to sequent calculus),
436 and completeness proof of superposition [2], can be related in our framework.
437

References

438

439

1 Jean-Marc Andreoli. Logic programming with focusing proofs in linear logic. *Journal of Logic and Computation*, 2(3):297-347, 1992.

440

441

2 L. Bachmair and H. Ganzinger. Rewrite-based equational theorem proving with selection and simplification. *Journal of Logic and Computation*, 4(3):1-31, 1994.

442

443

444

3 Leo Bachmair and Harald Ganzinger. Resolution theorem proving. In John Alan Robinson and Andrei Voronkov, editors, *Handbook of Automated Reasoning*, pages 19–99. Elsevier and MIT Press, 2001.

445

446

447

4 Richard Bonichon and Olivier Hermant. A semantic completeness proof for TaMed. In Miki Hermann and Andrei Voronkov, editors, *LPAR*, volume 4246 of LNCS, pages 167–181. Springer, 2006.

448

449

5 Paul Brauner, Clément Houtmann, and Claude Kirchner. Principle of superdeduction. In Luke Ong, editor, *LICS*, pages 41–50, jul 2007.

450

451

6 Guillaume Burel. Experimenting with deduction modulo. In Viorica Sofronie-Stokkermans and Nikolaj Bjørner, editors, *CADE*, volume 6803 of LNCS, pages 162–176. Springer, 2011.

452

7 Guillaume Burel. From axioms to rewriting rules. Available on author's web page, 2013.

453

454

8 Guillaume Burel. Cut admissibility by saturation. In Gilles Dowek, editor, *RTA-TLCA*, volume 8560 of LNCS, pages 124–138. Springer, 2014.

455

456

457

9 Guillaume Burel and Gilles Dowek. How can we prove that a proof search method is not an instance of another? In *LFMTP*, ACM International Conference Proceeding Series, pages 84–87. ACM, 2009.

458

459

10 Guillaume Burel and Claude Kirchner. Regaining cut admissibility in deduction modulo using abstract completion. *Information and Computation*, 208(2):140–164, 2010.

460

461

462

463

464

11 Guillaume Bury, David Delahaye, Damien Doligez, Pierre Halmagrand, and Olivier Hermant. Automated deduction in the B set theory using typed proof search and deduction modulo. In Ansgar Fehnker, Annabelle McIver, Geoff Sutcliffe, and Andrei Voronkov, editors, *LPAR*, volume 35 of *EPiC Series in Computing*, pages 42–58. EasyChair, 2015. URL: http://www.easychair.org/publications/volume/LPAR-20.

465

466

12 Samuel R. Buss, editor. *Handbook of proof theory*. Studies in logic and the foundations of mathematics. Elsevier, Amsterdam, 1998.

467

468

469

13 Kaustuv Chaudhuri and Frank Pfenning. A focusing inverse method theorem prover for first-order linear logic. In Robert Nieuwenhuis, editor, *CADE*, volume 3632 of LNCS, pages 69–83. Springer, 2005.

470

471

472

14 Kaustuv Chaudhuri, Frank Pfenning, and Greg Price. A logical characterization of forward and backward chaining in the inverse method. *Journal of Automated Reasoning*, 40(2-3):133–177, 2008.

473

474

15 Zakaria Chihani, Tomer Libal, and Giselle Reis. The proof certifier checkers. In *TABLEAUX*, volume 9323 of LNCS, pages 201–210, Wroclaw, Poland, 2015. Springer.

475

476

477

16 Zakaria Chihani, Dale Miller, and Fabien Renaud. Foundational proof certificates in first-order logic. In Maria Paola Bonacina, editor, *CADE*, volume 7898 of LNCS, pages 162–177. Springer, 2013.

478

479

480

17 Eric Deplagne and Claude Kirchner. Induction as deduction modulo. Rapport de recherche, LORIA, Nov 2004. URL: http://www.loria.fr/publications/2004/A04-R-468/A04-R-468.ps.

481

482

18 Gilles Dowek. What is a theory? In Helmut Alt and Afonso Ferreira, editors, *STACS*, volume 2285 of LNCS, pages 50–64. Springer, 2002.

483

484

19 Gilles Dowek. Truth values algebras and proof normalization. In Thorsten Altenkirch and Conor McBride, editors, *TYPES*, volume 4502 of LNCS, pages 110–124. Springer, 2006.

485

486

20 Gilles Dowek. Polarized resolution modulo. In Cristian S. Calude and Vladimiro Sassone, editors, *IFIP TCS*, volume 323 of *IFIP AICT*, pages 182–196. Springer, 2010.
23:14 Linking Focusing and Resolution with Selection

487

21 Gilles Dowek, Thérèse Hardin, and Claude Kirchner. Theorem proving modulo. *Journal of Automated Reasoning*, 31(1):33-72, 2003.

488

489

22 Gilles Dowek and Benjamin Werner. Proof normalization modulo. *The Journal of Symbolic Logic*, 68(4):1289-1316, 2003.

490

491

23 Gilles Dowek and Benjamin Werner. Arithmetic as a theory modulo. In Jürgen Giesl, editor, *RTA*, volume 3467 of LNCS, pages 423-437. Springer, 2005.

492

493

24 Mahfuza Farooque, Stéphane Graham-Lengrand, and Assia Mahboubi. A bisimulation between DPLL(T) and a proof-search strategy for the focused sequent calculus. In Alberto Momigliano, Brigitte Pientka, and Randy Pollack, editors, *LFMTP*, pages 3-14. ACM, 2013.

494

495

496

497

25 Olivier Hermant. *Méthodes Sémantiques en Déduction Modulo*. PhD thesis, École Poly-technique, 2005.

498

499

26 Olivier Hermant. Resolution is cut-free. *Journal of Automated Reasoning*, 44(3):245-276, 2009.

500

501

27 Clément Houtmann. Axiom directed focusing. In Stephano Berardi, Ferruccio Damiani, and Ugo de'Liguoro, editors, *Types for Proofs and Programs*, volume 5497 of LNCS, pages 169-185. Springer, 2008.

502

503

504

28 Chuck Liang and Dale Miller. Focusing and polarization in linear, intuitionistic, and classical logics. *Theoretical Computer Science*, 410(46):4747-4768, 2009. Abstract Interpretation and Logic Programming: In honor of professor Giorgio Levi.

505

506

507

29 Sean McLaughlin and Frank Pfenning. Imogen: Focusing the polarized inverse method for intuitionistic propositional logic. In Iliano Cervesato, Helmut Veith, and Andrei Voronkov, editors, *LPAR*, volume 5330 of *Lecture Notes in Computer Science*, pages 174-181. Springer, 2008.

508

509

510

511

30 Dale Miller and Marco Volpe. Focused labeled proof systems for modal logic. In Martin Davis, Ansgar Fehnker, Annabelle McIver, and Andrei Voronkov, editors, *LPAR*, volume 9450 of LNCS, pages 266-280. Springer, 2015.

512

513

514

31 J. A. Robinson. Automatic deduction with hyper-resolution. *International Journal of Computer Mathematics*, 1:227-234, 1965.

515

516

32 Peter Schroeder-Heister. Cut elimination for logics with definitional reflection. In *Non-classical Logics and Information Processing*, volume 619 of LNCS, pages 146-171. Springer, 1990.

517

518

519

33 James R. Slagle. Automatic theorem proving with renamable and semantic resolution. *J. ACM*, 14(4):687-697, 1967.

520

521

34 Larry Wos, George A. Robinson, and Daniel F. Carson. Efficiency and completeness of the set of support strategy in theorem proving. *J. ACM*, 12(4):536-541, 1965.

522
# A Appendix

The two directions of the proof of Theorem 3 are given in the next sections.

## A.1 From Focused Proofs to Resolution Derivations

We need a few lemmas to prove the first direction.

**Lemma 13.** For all sets of clauses $\Gamma$, for all clauses $C_1, \dots, C_n$ and $D$ such that $S(C_i) = \emptyset$ for all $i$ and $S(D) = \emptyset$, if $\Gamma, C_1, \dots, C_n \rightsquigarrow \Box$ and $\Gamma, D \rightsquigarrow \Box$, then $\Gamma, C_1 \cup D, \dots, C_n \cup D \rightsquigarrow \Box$ where $S(C_i \cup D) = \emptyset$ for all $i$.

**Proof.** By induction on the derivation length of $\Gamma, C_1, \dots, C_n \rightsquigarrow \Box$, generalizing on $\Gamma$.

The base case is when $\Box \in \Gamma$. Then, trivially $\Gamma, C_1 \cup D, \dots, C_n \cup D \rightsquigarrow \Box$.

For the inductive case, suppose that there exists $C_{n+1}$ such that $\Gamma, C_1, \dots, C_n \rightsquigarrow C_{n+1}$ and $\Gamma, C_1, \dots, C_n, C_{n+1} \rightsquigarrow \Box$.

There are two cases:

- $C_{n+1}$ is derived using other clauses than one of the $C_i$. We therefore have $\Gamma, C_1 \cup D, \dots, C_n \cup D \rightsquigarrow C_{n+1}$.

We can apply the induction hypothesis on $\Gamma, C_1, \dots, C_n, C_{n+1} \rightsquigarrow \Box$, which can be viewed as $\Gamma, C_{n+1}, C_1, \dots, C_n \rightsquigarrow \Box$, since by weakening we have $\Gamma, C_{n+1}, D \rightsquigarrow \Box$. We obtain $\Gamma, C_{n+1}, C_1 \cup D, \dots, C_n \cup D \rightsquigarrow \Box$. By definition of $\rightsquigarrow^*$ we therefore have $\Gamma, C_1 \cup D, \dots, C_n \cup D \rightsquigarrow \Box$.

- At least one of the parents of $C_{n+1}$ is some $C_i$. Since no literal is selected in the $C_i$, they can only be side clauses of Resolution with Selection, or any clause in Resolution or Factoring. We can therefore derive $C_{n+1} \cup D$ from $\Gamma, C_1 \cup D, \dots, C_n \cup D$ with the same inference rule that produced $C_{n+1}$. We can apply the induction hypothesis on $\Gamma, C_1, \dots, C_n, C_{n+1} \rightsquigarrow \Box$ which gives us $\Gamma, C_1 \cup D, \dots, C_n \cup D, C_{n+1} \cup D \rightsquigarrow \Box$. Hence $\Gamma, C_1 \cup D, \dots, C_n \cup D \rightsquigarrow \Box$.

**Corollary 14.** For all sets of clauses $\Gamma$, for all clauses $C_1, \dots, C_n$ such that $S(C_i) = \emptyset$ for all $i$. If $\Gamma, C_i \rightsquigarrow \Box$ for all $i$ then $\Gamma, C_1 \cup \dots \cup C_n \rightsquigarrow \Box$ where $S(C_1 \cup \dots \cup C_n) = \emptyset$.

**Lemma 15.** For all sets of clauses $\Gamma$, for all substitutions $\theta$, for all clauses $C$ such that $S(\theta C) = \emptyset$, if $\Gamma, \theta C \rightsquigarrow \Box$ then $\Gamma, C \rightsquigarrow \Box$ where $S(C) = \emptyset$.

**Proof.** By induction on the derivation length of $\Gamma, \theta C \rightsquigarrow \Box$. As in the previous proof, the only interesting case is when the clause $\theta C$ is used in the first step $\Gamma, \theta C \rightsquigarrow D$ of the derivation. If the first step $\Gamma, \theta C \rightsquigarrow D$ is Factoring, then $D = \sigma \theta C$ where $\sigma$ is the most general unifier of two literals in $\theta C$. We can apply the induction hypothesis using $\sigma \theta$ instead of $\sigma$.

Otherwise, if the first step is Resolution with Selection or Resolution. Let $\theta C$ be $L \cup \theta C'$ where $L$ is the literal of $\theta C$ used in that step. Let $C$ be $L_1 \cup \dots \cup L_n \cup C'$ where the $L_i$ are exactly the literals of $C$ such that $\theta L_i = L$. The step produces therefore a clause $D = \sigma(\theta C' \cup D')$ where $\sigma$ is the most general unifier of a unification problem $L =? L'$, Prob. Let $\omega = \text{mgu}(L_1, \dots, L_n)$, then $\theta = \theta'\omega$. First, from $C$ one can derive $\omega L_1 \cup \omega C'$ by repetitively applying Factoring to $C$. We have $\sigma L = \sigma L'$, hence $\sigma \theta' \omega L_1 = \sigma L'$. Since we rename variables in the premises of the resolution rules, we can assume that $\theta'$ does not affect
if $\Gamma, \lceil \underline{K_1} \rceil \dots \lceil \underline{K_n} \rceil C \rceil, \dots, \lceil K'_i \rceil \gamma D_i \rceil, \dots, \lceil \sigma(C \gamma D_1 \gamma \dots \gamma D_n) \rceil \Uparrow \vdash$ then $\Gamma, \lceil \underline{K_1} \rceil \dots \lceil \underline{K_n} \rceil C \rceil, \dots, \lceil K'_i \rceil \gamma D_i \rceil, \dots, \Uparrow \vdash$.

**Proof.** By induction on the proof

$\Gamma, \lceil \underline{K_1} \rceil \dots \lceil \underline{K_n} \rceil C \rceil, \dots, \lceil K'_i \rceil \gamma D_i \rceil, \dots, \lceil \sigma(C \gamma D_1 \gamma \dots \gamma D_n) \rceil \Uparrow \vdash$. We follow the same idea as in the proofs of the two precedent lemmas. If the proof does not begin by focusing on $\lceil \sigma(C \gamma D_1 \gamma \dots \gamma D_n) \rceil \rceil$, this is a simple application of the induction hypothesis. Otherwise, let $\Gamma'$ be

$\Gamma, \lceil \underline{K_1} \rceil \dots \lceil \underline{K_n} \rceil C \rceil, \dots, \lceil K'_i \rceil \gamma D_i \rceil, \dots$ and $\Gamma''$ be

$\Gamma', \lceil \sigma(C \gamma D_1 \gamma \dots \gamma D_n) \rceil \rceil$. Focusing leads us either to sequents $\Gamma'' \Downarrow \theta I_j \vdash$, with $\theta I_j \perp$ in $\Gamma$, or to sequents $\Gamma''$, $\theta J_k \Uparrow \vdash$ upon which one can apply the induction hypothesis. Let us remark that for each literal $L$ of $C$ or $D_i$, $\theta \sigma L$ is either one of $\theta I_j$ or one of $\theta J_k$. Therefore, we know how to close proofs of $\Gamma' \Uparrow \theta \sigma L \vdash$ for each, either by induction hypothesis or using $\theta I_j \perp$ in $\Gamma$.

To build the proof of $\Gamma' \Uparrow \vdash$, we first focus on $\lceil K'_1 \rceil \gamma D_1 \rceil$, instantiating the variables using the substitution $\theta \sigma$. As explain above, we know how to close the branches coming from $D_1$, it remains the branch $\Gamma', \theta \sigma K'_1 \Uparrow \vdash$.

We do the same, focusing on $\lceil K'_2 \rceil \gamma D_2 \rceil$ then ... then $\lceil K'_n \rceil \gamma D_n \rceil$ and the remaining branch is $\Gamma', \theta \sigma K'_1 \perp, \dots, \theta \sigma K'_n \Uparrow \vdash$.

We can close the proof by focusing on $\lceil \underline{K_1} \rceil \dots \lceil \underline{K_n} \rceil C \rceil$. Branches coming from $C$ can be closed as before, and the other branches are closed by

$\Uparrow \vdash \frac{\Gamma', \theta \sigma K'_1 \perp, \dots, \theta \sigma K'_n \perp \Downarrow \theta \sigma K_i \Uparrow \vdash}{\Gamma', \theta \sigma K'_1 \perp, \dots, \theta \sigma K'_n \perp \Downarrow \theta \sigma K_i \Uparrow \vdash}$ since $\theta \sigma K'_i = \theta \sigma K_i$ for all $i$.

**Theorem 21.** For all set of clauses $\Gamma$, if $\Gamma \rightsquigarrow^* \square$, then $\Gamma \Uparrow \vdash$.

**Proof.** By induction on the length of the derivation $\Gamma \rightsquigarrow^* \square$. If $\square$ is in $\Gamma$, then we focus on $\lceil \square \rceil = \perp$ and apply $\Downarrow \Uparrow \vdash$. If the first step is Factoring, we apply Lemma 17. If it is Resolution, we apply Lemma 19. If it is Resolution with Selection, we apply Lemma 20.

### A.3 Proofs of Section 5

**Proof of Theorem 8.** Proofs in both calculi correspond almost exactly. $\Uparrow \vdash$, $\wedge \vdash$, $\vee \vdash$ and $\exists \vdash$ in PUSC$\perp$ correspond exactly to $\Uparrow \Uparrow \vdash$, $\Uparrow \wedge \vdash$, $\Uparrow \vee \vdash$ and $\Uparrow \exists \vdash$ in LKF$\perp$, except that if the top connective of the subformulas in the premise(s) is $\forall$ or $\perp$, or if they are literals, they have to be put on the left hand side of $\Uparrow$ using Store. The translation of $\perp \vdash$ corresponds to $\Downarrow \Uparrow \vdash$, except that the latter can only be applied when there is no formula with positive polarity:

$\Uparrow \vdash \frac{\perp \vdash \quad \lceil \underline{N_1}, \dots, \perp, \dots, \underline{N_n} \rceil}{\perp \vdash \quad \lceil \underline{N_1}, \dots, \perp, \dots, \underline{N_n} \rceil}$ becomes $\text{Focus} \frac{\lceil \underline{\mathcal{R}} \rceil, |N_1|, \dots, \perp, \dots, |N_n| \Downarrow \perp \vdash}{\lceil \underline{\mathcal{R}} \rceil, |N_1|, \dots, \perp, \dots, |N_n| \Uparrow \vdash}$.

Similarly, $\forall \vdash$ corresponds to $\Downarrow \forall \vdash$, with the same proviso that there are no formulas with positive polarity:

$\forall \vdash \frac{\underline{N_1}, \dots, \underline{N_n}, \forall x. A, \{t/x\}A \Uparrow \vdash}{\underline{N_1}, \dots, \underline{N_n}, \forall x. A \Uparrow \vdash}$ becomes

$\text{Release} \frac{\lceil \underline{\mathcal{R}} \rceil, |N_1|, \dots, |N_n|, \forall x. \delta^- |A| \Uparrow |\{t/x\}A| \Uparrow \vdash}{\lceil \underline{\mathcal{R}} \rceil, |N_1|, \dots, |N_n|, \forall x. \delta^- |A| \Downarrow \delta^- |\{t/x\}A| \Uparrow \vdash}$
$\text{Focus} \frac{\lceil \underline{\mathcal{R}} \rceil, |N_1|, \dots, |N_n|, \forall x. \delta^- |A| \Downarrow \forall x. \delta^- |A| \Uparrow \vdash}{\lceil \underline{\mathcal{R}} \rceil, |N_1|, \dots, |N_n|, \forall x. \delta^- |A| \Uparrow \vdash}$

with an extra Store step if the top connective of $\{t/x\}A$ is $\forall$ or $\perp$ or if it is a literal.

For the unfolding rules, if $P$ rewrites positively to $A$, then there exists a rule $Q \to^+ B$ and a substitution $\theta$ such that $P = \theta Q$ and $A = \theta B$. This rule corresponds to a formula $\lceil Q \to^+ B \rceil = \forall x. Q \vee \delta^+ |B^\perp|$. Always with the proviso that there is no formula with positive polarity, let $\Gamma = \lceil \underline{\mathcal{R}'} \rceil, \forall x. Q \vee \delta^+ |B^\perp|, |N_1|, \dots, |N_n|, \neg P$, then $\Uparrow \Uparrow \vdash$ therefore corresponds
$$ \stackrel{\leftrightarrow}{\Gamma} \vdash \frac{\Gamma \Downarrow \underline{P} \vdash \Gamma}{\Gamma \Downarrow \underline{\Gamma} \vdash \Gamma} \quad \text{Release} \quad \frac{\Gamma \Uparrow |A^{\perp}| \vdash \Gamma}{\Gamma \Downarrow \delta^{+} |A^{\perp}| \vdash \Gamma} $$

$$ \stackrel{\leftrightarrow}{\Gamma} \vdash \frac{\Gamma \Downarrow \theta Q \vee \neg \delta^{+} |\theta B^{\perp}| \vdash \Gamma}{\Gamma \Downarrow \forall x. \underline{\Gamma} \vee \neg \delta^{+} |B^{\perp}| \vdash \Gamma} $$

with an extra Store step if the top connective of $|A^{\perp}|$ is $\forall$ or $\perp$, or if it is a literal. Reciprocally, given a sequent $\llbracket \mathcal{R}' \rrbracket, \forall x. Q \vee \neg \delta^{+} |B^{\perp}|, \Gamma \Uparrow \vdash$, if we apply a Focus on $\forall x. Q \vee \neg \delta^{+} |B^{\perp}|$, the derivation is necessarily of the same shape as above, so that there must be a literal $\neg \theta Q$ in $\Gamma$. The derivation therefore corresponds to an unfolding of $\neg \theta Q$ into $|\theta B^{\perp}|$.

The case of a negative rewriting is dual.

There remains to be proved that, in PUSC$^{\perp}$, the rules $\perp \vdash$, $\forall \vdash$ and $\Uparrow \vdash$ can be delayed until the other rules are no longer applicable. This can be done by showing that these rules permute with the other ones. Note that this fact can be related with the strategy used in Tamed [4], a tableaux method based on Deduction Modulo Theory, where rules for universal quantifiers and for rewriting are applied when no other rules can be. ◀

**Proof sketch of Theorem 12.** Showing that LKF$^{\perp}$ is complete amounts to proving that the cut rule

$$ \stackrel{\leftrightarrow}{\Gamma}, A \Uparrow \vdash \frac{\Gamma, A^{\perp} \Uparrow \vdash \Gamma}{\Gamma \Uparrow \vdash} $$

is admissible.

Using the same techniques as in [10], we can try to eliminate cuts using structural cut elimination à la Pfenning. The only problematic case is when we cut around a literal that is used in focused instance in both branches:

$$ \stackrel{\leftrightarrow}{\Gamma}, A \Downarrow \underline{\Gamma'}, A \Downarrow \underline{\Gamma''}, A^{\perp} \Downarrow \underline{\Gamma} \vdash \frac{\Gamma, A \Downarrow E[A^{\perp}] \vdash \Gamma}{\Gamma, A^{\perp} \Downarrow \Gamma} \quad \text{Focus} \quad \frac{\Gamma, A^{\perp} \Downarrow F[A] \vdash \Gamma}{\Gamma, A^{\perp} \Uparrow \Gamma} \quad \text{Focus} \quad \frac{\Gamma, A^{\perp} \Uparrow F[A] \vdash \Gamma}{\Gamma, A^{\perp} \Uparrow \Gamma} $$

But, since LKF$^{\perp}$ is complete for all singleton subselection, it is complete if one selects only $A^{\perp}$ in $E[A^{\perp}]$ and only $A$ in $F[A]$. Consequently, we know how to eliminate the cut above. ◀

## B Other complete instances

### B.1 Superdeduction

We can go a step further than what is done concerning Deduction Modulo Theory and benefit from focusing to decompose the right-hand side formula after an unfolding has occurred. This leads to what [5] called Superdeduction. [27] studied the links between Superdeduction and focusing, but not with the idea that the rules themselves should be considered as polarized formulas. To link Superdeduction with LKF$^{\perp}$, we just need to change the translation of rewriting rules in order to ensure that the right-hand side is decomposed as much as possible. This is done by suppressing the positive delay $\delta^{+}$ and trying to stay in synchronous (i.e. focused) phase by using negative connectives, until we reach a $\exists$ quantifier, after which we try
to stay in the asynchronous phase. Note, however, that literals are always given a positive
polarization. We introduce the negative translation of a formula:

$$
\begin{align*}
& [L] = L \quad \text{when } L \text{ is } \top, \bot \text{ or a literal} \\
& [A \land B] = [A] \land \neg [B] \qquad [A \lor B] = [A] \lor \neg [B] \\
& [\exists x. A] = \exists x. |A| \qquad [\forall x. A] = \forall x. [A]
\end{align*}
$$

716 and the translation of rewrite rules becomes:

$$
717 \quad \|P \to^{-} A\| = \overline{\forall x. \neg P \lor^{-} A} [A]
$$

$$
\begin{align*}
\llap{718\quad} \|P \to^+ A\| &= \overline{\forall x. \neg P \lor^- A} [A^\perp] \\
\llap{719\quad} \|P \to^- A\| &= \overline{\forall x. P \lor^\perp A} [A]
\end{align*}
$$

720 The synthetic rules given by the translation of rewriting rules correspond exactly to the
721 superrules of Superdeduction.

722 Note that the same kind of encodings can be used to show that Definitional reflection, as
723 defined by [32], can be seen as an instance of LKF⊥.