# Cut-elimination and the decidability of reachability in alternating pushdown systems

Gilles Dowek, Ying Jiang

► To cite this version:

Gilles Dowek, Ying Jiang. Cut-elimination and the decidability of reachability in alternating pushdown systems. 2015. hal-01101835

HAL Id: hal-01101835

https://inria.hal.science/hal-01101835

Preprint submitted on 30 Jan 2015

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>
# Cut-elimination and the decidability of reachability in alternating pushdown systems

Gilles Dowek¹ and Ying Jiang²

1 Inria, 23 avenue d'Italie, CS 81321, 75214 Paris Cedex 13, France, gilles.dowek@inria.fr.

2 State Key Laboratory of Computer Science, Institute of Software, Chinese Academy of Sciences, 100190 Beijing, China, jy@ios.ac.cn.

## Abstract

We propose a new approach to formalize alternating pushdown systems as natural-deduction style inference systems. In this approach, the decidability of reachability can be proved as a simple consequence of a cut-elimination theorem for the corresponding inference system. Then, we show how this result can be used to extend an alternating pushdown system into a complete system where, for every configuration A, either A or $\neg A$ is provable. The key idea is that cut-elimination permits to build a system where a proposition of the form $\neg A$ has a co-inductive (hence possibly infinite) proof if and only if it has an inductive (hence finite) proof.

## 1 Introduction

Several methods can be used to prove that a problem is decidable. One of them is to reduce this problem to provability in some inference system and prove that provability in this system is decidable. Another is to reduce this problem to reachability in some transition system and prove that reachability is decidable in this transition system.

For instance deciding if a number $n$ is even can be reduced to deciding if the proposition $even(S^n(0))$ is provable in the inference system defined by the rules

$$ \begin{array}{c} even(0) \\ even(x) \\ \hline odd(S(x)) \\ odd(x) \\ \hline even(S(x)) \end{array} $$

It can also be reduced to decide if the final configuration $f$ is reachable from the configuration $\langle even, S^n(0) \rangle$ in the pushdown system

$$ \begin{align*} \langle even, 0 \rangle &\leftrightarrow f \\ \langle even, Sw \rangle &\leftrightarrow \langle odd, w \rangle \\ \langle odd, Sw \rangle &\leftrightarrow \langle even, w \rangle \end{align*} $$

Although at a first glance, inference and transition systems look alike as they both define a set of things—propositions, states, configurations—and rules—deduction rules, transition rules—to go step by step from one thing to another, the details look quite different. In particular, the methods used to prove the decidability of provability in an inference system—quantifier-elimination, finite model property, cut-elimination, etc.—and those used to prove the decidability of reachability in a transition system—finite state automata, etc.—are not easy to relate.
This work is a first step towards establishing a connection between proof-theoretical methods and automata-theoretical methods to prove decidability results. In particular, we show that the run of an automaton can be seen as a cut-free proof and the proof that the set of reachable configurations in a transition system can be recognized by a finite-state automaton as a cut-elimination theorem.

We focus on alternating pushdown systems. The decidability of reachability in alternating pushdown systems [1] is a seminal result in automata theory. Many other results, such as the decidability of LTL, CTL, and the alternation-free modal μ-calculus over pushdown systems, are corollaries. We prove a cut-elimination theorem for a class of inference systems and show that the decidability of reachability in alternating pushdown systems is a consequence of this cut-elimination theorem. Although this proof shares many ideas with the original one, in particular both rest on the construction of an alternating multi-automaton, the relation of this automaton construction to cut-elimination seems to be new and the method used here could be adapted to other decidability problems.

This work can also be seen as an extension of the methods developed in [6, 7] where decidable proof systems are introduced to formalize validity in finite models, but the methods developed here to deal with infinity are radically different from those developed for the finite case.

In the remainder of the paper, we first prove a cut-elimination theorem for a class of inference systems and show that the decidability of reachability in alternating pushdown systems is a consequence of this cut-elimination theorem (Section 2). We then relate the notion of negation as failure and of complementation of an automaton, and prove how this decidability result permits to design a complete inference system where, for each closed proposition, either A or ¬A is provable (Sections 3 and 4). The key idea is that cut-elimination permits to build a system where a proposition of the form ¬A has a co-inductive (hence possibly infinite) proof if and only if it has an inductive (hence finite) proof.

## 2 Decidability

In this section, we define a class of inference systems, called alternating pushdown systems and prove the decidability of provability in these systems.

**► Definition 1 (State, word, configuration).** Consider a language $\mathcal{L}$ in monadic predicate logic, containing a finite number of predicate symbols, called states, a finite number of function symbols, called stack symbols, and a constant $\varepsilon$, called the empty word.

A closed term in $\mathcal{L}$ has the form $\gamma_1(\gamma_2...(\gamma_n(\varepsilon)))$ where $\gamma_1, ..., \gamma_n$ are stack symbols. Such a term is called a word and is often written $w = \gamma_1\gamma_2...\gamma_n$. An open term has the form $\gamma_1(\gamma_2...(\gamma_n(x)))$ for some variable $x$. It is often written $\gamma_1\gamma_2...\gamma_n x$ or $wx$ for $w = \gamma_1\gamma_2...\gamma_n$.

A closed atomic proposition, called a configuration, has the form $P(w)$ where $P$ is a state and $w$ a word. An open atomic proposition has the form $P wx$ where $P$ is a state, $w$ a word, and $x$ a variable.

**► Definition 2 (Alternating pushdown system).** Given a language $\mathcal{L}$, an alternating pushdown system is defined by a finite set of inference rules, called transition rules, of the form

$$ \frac{P_1(v_1 x) \dots P_n(v_n x)}{Q wx} $$

where $P_1, \dots, P_n, Q$ are predicate symbols, $v_1, \dots, v_n, w$ are words and $n$ may be zero, or of the form

$$ \overline{Q(\varepsilon)} $$
A rule of the first form may also be written as

$$ \langle Q, wx \rangle \hookrightarrow \{ \langle P_1, v_1 x \rangle, \dots, \langle P_n, v_n x \rangle \} $$

or simply

$$ \langle Q, w \rangle \hookrightarrow \{ \langle P_1, v_1 \rangle, \dots, \langle P_n, v_n \rangle \} $$

and a rule of the second form may also be written as

$$ \langle Q, \varepsilon \rangle \hookrightarrow \emptyset $$

**► Definition 3 (Proof).** A proof in an inference system $\mathcal{I}$ is a finite tree labeled by configurations such that for each node $N$, there exists an inference rule

$$ \frac{A_1 \dots A_n}{B} $$

in $\mathcal{I}$, and a substitution $\sigma$ such that the node $N$ is labeled with $\sigma B$ and its children are labeled with $\sigma A_1, \dots, \sigma A_n$.

A proof is a *proof of a configuration A* if its root is labeled by A.

A configuration A is said to be *provable*, written $A \in \text{pre}^*(\emptyset)$, if it has a proof.

**► Example 4.** Consider the language containing a constant $\varepsilon$, two monadic function symbols $a$ and $b$, and monadic predicate symbols $P$, $Q$, $R$, $S$, and $T$. In the inference system

$$ \begin{array}{ccccccc} \frac{Q(x)}{P(ax)} & \mathbf{i1} & \frac{T(x)}{P(bx)} & \mathbf{i2} & \frac{T(x)}{R(ax)} & \mathbf{i3} & \overline{R(bx)} & \mathbf{i4} \\ \frac{P(x)}{Q(x)} & \mathbf{n1} & \overline{T(x)} & \mathbf{n2} & & & & \\ \frac{P(ax)}{S(x)} & \mathbf{e1} & & & & & & \end{array} $$

the configuration $S(ab)$ has the following proof

$$ \begin{array}{ccccccc} \overline{\frac{T(\varepsilon)}{P(b)}} & \mathbf{n2} & \overline{\frac{R(b)}{P(ab)}} & \mathbf{i4} & \overline{\frac{T(b)}{R(ab)}} & \mathbf{i3} & \mathbf{n2} \\ \overline{\frac{Q(b)}{P(ab)}} & \mathbf{i1} & \mathbf{n1} & & \mathbf{n1} & & \mathbf{n1} \\ \frac{Q(ab)}{P(ab)} & \mathbf{i1} & \mathbf{e1} & & & & & \end{array} $$

This proof can also be written $\{S(ab)\} \hookrightarrow \{P(ab)\} \hookrightarrow \{Q(ab)\} \hookrightarrow \{P(ab), R(ab)\} \hookrightarrow \{Q(b), R(ab)\} \hookrightarrow \{Q(b), T(b)\} \hookrightarrow \{Q(b)\} \hookrightarrow \{P(b), R(b)\} \hookrightarrow \{P(b)\} \hookrightarrow \{T(\varepsilon)\} \hookrightarrow \emptyset$.

**► Definition 5 (Introduction rule, elimination rule, neutral rule).** An *introduction rule* is a rule of the form

$$ \frac{P_1(x) \dots P_n(x)}{Q(\gamma x)} $$

where $\gamma$ is a stack symbol, $n$ may be zero, or of the form

$\overline{Q(\varepsilon)}$
An elimination rule is a rule of the form

$$ \frac{P_1(\gamma x) P_2(x) \dots P_n(x)}{Q(x)} $$

where $\gamma$ is a stack symbol and $n$ is at least one.

A neutral rule is a rule of the form

$$ \frac{P_1(x) \dots P_n(x)}{Q(x)} $$

where $n$ may be zero.

**► Definition 6 (Alternating multi-automaton).** An alternating pushdown system of which all rules are introduction rules is called an alternating multi-automaton. If the configuration $P(w)$ is provable in an alternating multi-automaton, we say also that the word $w$ is recognized in $P$.

The introduction rule

$$ \frac{P_1(x) \dots P_n(x)}{Q(\gamma x)} $$

may be written as

$$ \langle Q, \gamma x \rangle \leftrightarrow \{ \langle P_1, x \rangle, \dots, \langle P_n, x \rangle \} $$

or simply

$$ \langle Q, \gamma \rangle \leftrightarrow \{ \langle P_1, \varepsilon \rangle, \dots, \langle P_n, \varepsilon \rangle \} $$

It is also sometime written as

$$ Q \leftrightarrow \gamma \{ P_1, \dots, P_n \} $$

**► Lemma 7 (Decidability).** *Provability is decidable in an alternating multi-automaton.*

**Proof.** Bottom-up proof-search terminates as the size of configurations decreases at each step. ◀

If decidability is obvious for alternating multi-automata, it is less obvious for general alternating pushdown systems, as bottom-up proof-search, that is eager application of the transition rules, does not always terminate, even if we include a redundancy check à la Kleene [10]. For instance, consider an alternating pushdown system containing the elimination rule

$$ \frac{P(ax)}{P(x)} $$

applying this rule bottom-up to the configuration $P(a)$ yields $P(aa), P(aaa), P(aaaa), \dots$

To prove the decidability of provability in arbitrary alternating pushdown systems, we shall prove a cut-elimination theorem and a subformula property that permit to avoid considering configurations such as $P(aa), P(aaa), \dots$, which are not subformulae of $P(a)$.

We start with a simple lemma, that permits to restrict to particular alternating pushdown systems called *small step alternating pushdown systems*.

**► Definition 8 (Small step alternating pushdown system).** A small step alternating pushdown system is an alternating pushdown system of which each rule is either an introduction rule, an elimination rule or a neutral rule.

**► Lemma 9.** For each alternating pushdown system $I_0$, there exists a small step alternating pushdown system $I$ that is a conservative extension of $I_0$.
**Proof.** Assume the system $\mathcal{I}_0$ contains a rule $r$ that is neither an introduction rule, nor an elimination rule, nor a neutral rule.

For all propositions of the form $P(\gamma_1...\gamma_n x)$ occurring as a premise or a conclusion of this rule, we introduce $n$ predicate symbols $P^{\gamma_1}$, $P^{\gamma_1\gamma_2}$, ..., $P^{\gamma_1...\gamma_n}$, $n$ introduction rules

$$ \frac{P^{\gamma_1...\gamma_i \gamma_{i+1}}(x)}{P^{\gamma_1...\gamma_i}(\gamma_{i+1}x)} $$

and $n$ elimination rules

$$ \frac{P^{\gamma_1...\gamma_i}(\gamma_{i+1}x)}{P^{\gamma_1...\gamma_i \gamma_{i+1}}(x)} $$

and we replace the rule $r$ by the neutral rule $r'$ obtained by replacing the proposition $P(\gamma_1...\gamma_n x)$ by $P^{\gamma_1...\gamma_n}(x)$.

Obviously, this system is an extension of $\mathcal{I}_0$, as the rule $r$ is derivable from the rule $r'$ and the added introduction and elimination rules. And this extension is conservative as, by replacing the configuration $P^{\gamma_1...\gamma_i}(w)$ by $P(\gamma_1...\gamma_i w)$, we obtain a proof in the original system. ◀

**Definition 10 (Cut).** A cut is a proof of the form

$$ \frac{\frac{\pi_1}{P_1(w)} \quad \dots \quad \frac{\pi_m}{P_m(w)} \quad \dots \quad \frac{\rho_2}{Q_2(w)} \quad \dots \quad \frac{\rho_n}{Q_n(w)}}{Q_1(\gamma w)} \text{ intro } R(w) \quad \dots \quad \text{ elim } R(w) $$

$$ \frac{\frac{\pi_1^1}{P_1^1(w)} \quad \dots \quad \frac{\pi_{m_1}^1}{P_{m_1}^1(w)} \quad \dots \quad \frac{\pi_1^n}{P_1^n(w)} \quad \dots \quad \frac{\pi_{m_n}^n}{P_{m_n}^n(w)}}{Q_1(\gamma w)} \text{ intro } \dots \quad \text{ neutral } R(\gamma w) \quad \dots \quad \text{ elim } R(\gamma w) $$

or

$$ \frac{\overline{Q_1(\varepsilon)} \text{ intro } \dots \overline{Q_n(\varepsilon)} \text{ intro} \quad \dots \quad \overline{R(\varepsilon)} \text{ neutral}}{R(\varepsilon)} $$

A proof *contains a cut* if one of its subproofs is a cut. A proof is *cut-free* if it contains no cut. A small step alternating pushdown system *has the cut-elimination property* if every provable configuration has a cut-free proof.

Not all small step alternating pushdown systems have the cut-elimination property. For instance, in the system defined in Example 4, the configuration $S(ab)$ has a proof but no cut-free proof. Thus, instead of proving that every small step alternating pushdown system has the cut-elimination property, we shall prove that every small step alternating pushdown system has an extension with derivable rules, and this extended system has the cut-elimination property.

**Definition 11 (Saturation).** Consider a small step alternating pushdown system.

■ If the system contains an introduction rule

$$ \frac{P_1(x) \dots P_m(x)}{Q_1(\gamma x)} \text{ intro} $$

and an elimination rule

$$ \frac{Q_1(\gamma x) Q_2(x) \dots Q_n(x)}{R(x)} \text{ elim} $$
then we add to it the neutral rule

$$ \frac{P_1(x) \dots P_m(x) Q_2(x) \dots Q_n(x)}{R(x)} \text{ neutral} $$

■ If the system contains introduction rules

$$ \frac{P_1^1(x) \dots P_{m_1}^1(x)}{Q_1(\gamma x)} \text{ intro} $$

...

$$ \frac{P_1^n(x) \dots P_{m_n}^n(x)}{Q_n(\gamma x)} \text{ intro} $$

and a neutral rule

$$ \frac{Q_1(x) \dots Q_n(x)}{R(x)} \text{ neutral} $$

then we add to it the introduction rule

$$ \frac{P_1^1(x) \dots P_{m_1}^1(x) \dots P_1^n(x) \dots P_{m_n}^n(x)}{R(\gamma x)} \text{ intro} $$

In particular, if the system contains a neutral rule

$$ \overline{R(x)} \text{ neutral} $$

then we add to it the introduction rule

$$ \overline{R(\gamma x)} \text{ intro} $$

for all $\gamma$.

■ If the system contains introduction rules

$$ \overline{Q_1(\varepsilon)} \text{ intro} $$

...

$$ \overline{Q_n(\varepsilon)} \text{ intro} $$

and a neutral rule

$$ \frac{Q_1(x) \dots Q_n(x)}{R(x)} \text{ neutral} $$

then we add to it the introduction rule

$$ \overline{R(\varepsilon)} \text{ intro} $$

In particular, if the system contains a neutral rule

$$ \overline{R(x)} \text{ neutral} $$

then we add to it the introduction rule

$$ \overline{R(\varepsilon)} \text{ intro} $$
As there is only a finite number of possible rules, this process terminates.

**► Example 12.** Saturating the system defined in Example 4 adds the following rules

$$ \begin{array}{lclcl} \frac{Q(x)}{S(x)} & \mathbf{n3} & \overline{T(\varepsilon)} & \mathbf{i5} & \overline{T(ax)} & \mathbf{i6} \\ \frac{Q(x) T(x)}{Q(ax)} & \mathbf{i7} & \frac{Q(x) T(x)}{S(ax)} & \mathbf{i8} & \frac{}{} & \mathbf{i9} \\ \frac{T(x)}{Q(bx)} & \mathbf{i10} & \frac{T(x)}{S(bx)} & \mathbf{i11} & \frac{}{} & \mathbf{i9} \end{array} $$

where the rule **n3** is obtained from **i1** and **e1**, the rule **i5** from **n2**, the rule **i6** from **n2**, the rule **i7** from **i1**, **i3**, and **n1**, the rule **i8** from **i7** and **n3**, the rule **i9** from **n2**, the rule **i10** from **i2**, **i4**, and **n1**, and the rule **i11** from **i10** and **n3**.

Then, no more rules can be added.

**► Lemma 13.** If *I* is a small step system, and *I*<sub>s</sub> is its saturation, then *I* and *I*<sub>s</sub> prove the same configurations.

**Proof.** All the rules added in *I*<sub>s</sub> are derivable in *I*.

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

Now, we are ready to prove that a saturated system has the cut-elimination property.

**► Lemma 14 (Cut-elimination).** If a configuration *A* has a proof *π* in a saturated system, it has a cut-free proof.

**Proof.** Assume the proof *π* contains a cut. If this cut has the form

$$ \frac{\frac{\pi_1}{P_1(w)} \quad \frac{\pi_m}{P_m(w)} \quad \dots \quad \frac{\rho_2}{Q_2(w)} \quad \dots \quad \frac{\rho_n}{Q_n(w)}}{R(w)} \text{ intro } \frac{\pi_1}{P_1(w)} \quad \frac{\pi_m}{P_m(w)} \quad \dots \quad \frac{\rho_2}{Q_2(w)} \quad \dots \quad \frac{\rho_n}{Q_n(w)}}{R(w)} \text{ elim} $$

we replace it by the proof

$$ \frac{\frac{\pi_1}{P_1(w)} \quad \frac{\pi_m}{P_m(w)} \quad \dots \quad \frac{\rho_2}{Q_2(w)} \quad \dots \quad \frac{\rho_n}{Q_n(w)}}{R(w)} \text{ neutral} $$

If it has the form

$$ \frac{\frac{\pi_1^1}{P_1^1(w)} \quad \frac{\pi_{m_1}^1}{P_{m_1}^1(w)} \quad \dots \quad \frac{\pi_1^n}{P_1^n(w)} \quad \dots \quad \frac{\pi_{m_n}^n}{P_{m_n}^n(w)}}{Q_1(\gamma w)} \text{ intro } \frac{\dots \quad \dots \quad \dots \quad \dots}{R(\gamma w)} \text{ intro} $$

we replace it by the proof

$$ \frac{\frac{\pi_1^1}{P_1^1(w)} \quad \frac{\pi_{m_1}^1}{P_{m_1}^1(w)} \quad \dots \quad \frac{\pi_1^n}{P_1^n(w)} \quad \dots \quad \frac{\pi_{m_n}^n}{P_{m_n}^n(w)}}{R(\gamma w)} \text{ intro} $$

If it has the form

$$ \frac{\overline{Q_1(\varepsilon)} \text{ intro} \quad \dots \quad \overline{Q_n(\varepsilon)} \text{ intro}}{R(\varepsilon)} \text{ neutral} $$

we replace it by the proof

$$ \overline{R(\varepsilon)} \text{ intro} $$
This process terminates as the ordered pair formed with the number of elimination rules and the number of neutral rules decreases at each step of the reduction for the lexicographic order on $N^2$.

► **Example 15.** In the system of Example 12, the proof

$$ \begin{array}{c} \begin{array}{c} \overline{T(\varepsilon)} \ n2 \\ \overline{P(b)} \ i2 \end{array} \\ \begin{array}{c} \overline{R(b)} \ i4 \\ \overline{P(ab)} \ i1 \end{array} \end{array} \begin{array}{c} n1 \\ n1 \end{array} \begin{array}{c} \overline{T(b)} \ n2 \\ \overline{R(ab)} \ i3 \end{array} \begin{array}{c} n1 \\ n1 \end{array} \begin{array}{c} \overline{Q(ab)} \ i1 \\ \overline{P(ab)} \ e1 \end{array} \end{array} $$

reduces to

$$ \begin{array}{c} \begin{array}{c} \overline{T(\varepsilon)} \ i5 \\ \overline{P(b)} \ i2 \end{array} \\ \begin{array}{c} \overline{R(b)} \ i4 \\ \overline{P(ab)} \ i1 \end{array} \end{array} \begin{array}{c} n1 \\ n1 \end{array} \begin{array}{c} \overline{T(b)} \ n2 \\ \overline{R(ab)} \ i3 \end{array} \begin{array}{c} n1 \\ n1 \end{array} \begin{array}{c} \overline{Q(ab)} \ i1 \\ \overline{P(ab)} \ e1 \end{array} \end{array} $$

then to

$$ \begin{array}{c} \begin{array}{c} \overline{T(\varepsilon)} \ i5 \\ \overline{P(b)} \ i2 \end{array} \\ \begin{array}{c} \overline{R(b)} \ i4 \\ \overline{P(ab)} \ i1 \end{array} \end{array} \begin{array}{c} n1 \\ n1 \end{array} \begin{array}{c} \overline{T(b)} \ i9 \\ \overline{R(ab)} \ i3 \end{array} \begin{array}{c} n1 \\ n1 \end{array} \begin{array}{c} \overline{Q(ab)} \ i1 \\ \overline{P(ab)} \ e1 \end{array} \end{array} $$

then to

$$ \begin{array}{c} \begin{array}{c} \overline{T(\varepsilon)} \ i5 \\ \overline{P(b)} \ i2 \end{array} \\ \begin{array}{c} \overline{R(b)} \ i4 \\ \overline{P(ab)} \ i1 \end{array} \end{array} \begin{array}{c} n1 \\ n1 \end{array} \begin{array}{c} \overline{T(b)} \ i9 \\ \overline{R(ab)} \ i3 \end{array} \begin{array}{c} n1 \\ n1 \end{array} \begin{array}{c} \overline{Q(ab)} \ n3 \\ \overline{S(ab)} \ n3 \end{array} \end{array} $$

then to

$$ \begin{array}{c} \begin{array}{c} \overline{T(\varepsilon)} \ i5 \\ \overline{Q(b)} \ i10 \\ \overline{P(ab)} \ i1 \end{array} \\ \begin{array}{c} \overline{T(b)} \ i9 \\ \overline{R(ab)} \ i3 \end{array} \end{array} \begin{array}{c} n1 \\ n1 \end{array} \begin{array}{c} \overline{Q(ab)} \ n3 \\ \overline{S(ab)} \ n3 \end{array} \end{array} $$
then to

$$ \frac{\overline{T(\varepsilon)}^{i5} \quad \overline{i10}^{i9} \quad \overline{T(b)}^{i9} \quad \overline{i7}^{i5}}{\overline{Q(b)}^{i10} \quad \overline{Q(ab)}^{i9} \quad \overline{S(ab)}^{i7}} $$

and finally to

$$ \frac{\overline{T(\varepsilon)}^{i5} \quad \overline{i10}^{i9} \quad \overline{T(b)}^{i9} \quad \overline{i8}^{i5}}{\overline{Q(b)}^{i10} \quad \overline{S(ab)}^{i8}} $$

**► Lemma 16.** A cut-free proof contains introduction rules only.

**Proof.** By induction over proof structure. The proof has the form

$$ \frac{\pi_1}{A_1} \quad \dots \quad \pi_n}{B} $$

By induction hypothesis, the proofs $\pi_1, \dots, \pi_n$ contain introduction rules only. As the proof is cut-free, the last rule is neither an elimination rule, nor a neutral rule. Thus, it is an introduction rule. ◀

Notice the difference with Natural Deduction [12], where only the last rule of a cut-free proof can be proved to be an introduction rule, while here all the rules are introduction rules.

**► Theorem 17.** *Provability in an alternating pushdown system is decidable.*

**Proof.** Assume $\mathcal{I}_0$ is an alternating pushdown system, $\mathcal{I}$ the small step corresponding system, $\mathcal{I}_s$ its saturation, and $\mathcal{I}'$ the alternating multi-automaton obtained by dropping all the elimination rules and all the neutral rules from $\mathcal{I}_s$. Then, $\mathcal{I}_0, \mathcal{I}, \mathcal{I}_s$, and $\mathcal{I}'$ prove the same configurations expressed in the language of $\mathcal{I}_0$ and provability in the alternating multi-automaton $\mathcal{I}'$ is decidable. ◀

Note that this decidability proof follows the line of [1], in the sense that, for a given alternating pushdown system, it builds an alternating multi-automaton recognizing the same configurations. The originality of our approach is that, in our setting, alternating multi-automata are just particular alternating pushdown systems, while, these concepts are usually defined independently. This way, we can avoid building this alternating multi-automaton from scratch. Rather, we progressively transform the alternating pushdown system under consideration into an alternating multi-automaton recognizing the same configurations.

Note also the similarity between this method and the Knuth-Bendix method [11], which does not prove that all rewrite systems are confluent, but instead that, in some cases, it is possible to extend a rewrite system with derivable rules to make it confluent [5].

This idea of building an automaton via a saturation process is also related to Resolution based decidability proofs [8] [9] and specially [4] (Theorem 7.6.3), where terminating saturation of Horn clauses by Resolution is used to build an automaton. Yet, the relation to cut-elimination is not stressed there. In contrast, the relation between saturation by Resolution and cut-elimination has been investigated in [2].

In Section 3 and Section 4, we will prove, as a corollary of Theorem 17, that any alternating pushdown system can be extended to a complete system, where for every configuration $A$, either $A$ or $\neg A$ is provable.
### 3 Complementation and co-inductive proofs

In this section we recall some well-known facts about inductive and co-inductive proofs and apply them to alternating pushdown systems.

**Definition 18.** An inference system $\mathcal{I}$ defines a function $F_{\mathcal{I}}$ mapping a set of configurations $X$ to the set of configurations that can be deduced in one step with the rules of $\mathcal{I}$ from the configurations of $X$:

$$F_{\mathcal{I}}(X) = \{ \sigma B \in \mathcal{P} \mid \exists A_1 \dots A_n \text{ such that} \\ \qquad \sigma A_1 \in X, \dots, \sigma A_n \in X, \text{ and } \frac{A_1 \dots A_n}{B} \in \mathcal{I} \}$$

where $\mathcal{P}$ is the set of all configurations.

It is well-known that the function $F_{\mathcal{I}}$ is continuous, that is, for all increasing sequences $X_0, X_1, \dots$ of sets of configurations, $F_{\mathcal{I}}(\bigcup_n X_n) = \bigcup_n F_{\mathcal{I}}(X_n)$. Thus, this function $F_{\mathcal{I}}$ has a least fixed point

$$D = \bigcup_n F_{\mathcal{I}}^n(\emptyset)$$

and a configuration $A$ is an element of $D$ if and only if it has a proof in the sense of Definition 3.

**Definition 19 (Conjugate function).** Consider an inference system $\mathcal{I}$ and the associated function $F_{\mathcal{I}}$. The conjugate $G_{\mathcal{I}}$ of the function $F_{\mathcal{I}}$ is defined by

$$G_{\mathcal{I}}(X) = \mathcal{P} \setminus F_{\mathcal{I}}(\mathcal{P} \setminus X)$$

**Lemma 20.** Let $\mathcal{I}$ be an inference system. The function $G_{\mathcal{I}}$ is co-continuous, that is, for all decreasing sequences $X_0, X_1, \dots$ of sets of configurations, one has $G_{\mathcal{I}}(\bigcap_n X_n) = \bigcap_n G_{\mathcal{I}}(X_n)$ and the complement of the set $D$, of Definition 18, is the greatest fixed point of this function:

$$\mathcal{P} \setminus D = \bigcap_n G_{\mathcal{I}}^n(\mathcal{P})$$

**Proof.** It is easy to check, using the definition of $G_{\mathcal{I}}$ and the continuity of $F_{\mathcal{I}}$, that $G_{\mathcal{I}}$ is co-continuous. Then, by induction on $n$, we prove that $G_{\mathcal{I}}^n(\mathcal{P}) = \mathcal{P} \setminus F_{\mathcal{I}}^n(\emptyset)$ and with $\mathcal{P} \setminus \bigcup_n F_{\mathcal{I}}^n(\emptyset) = \bigcap_n (\mathcal{P} \setminus F_{\mathcal{I}}^n(\emptyset))$, we conclude that $\mathcal{P} \setminus D = \bigcap_n G_{\mathcal{I}}^n(\mathcal{P})$. ◀

In the case of alternating pushdown systems, the function $G_{\mathcal{I}}$ can be defined with an inference system $\tilde{\mathcal{I}}$, the complementation of $\mathcal{I}$ defined below.

**Lemma 21.** For each small step alternating pushdown system $\mathcal{I}$, we can build an equivalent inference system $\tilde{\mathcal{I}}$ and a set $C$ such that

- the conclusions of the rules of $\tilde{\mathcal{I}}$ are in $C$,

- for every configuration $A$ there exists a unique proposition $B$ in $C$ such that $A$ is an instance of $B$.

**Proof.** We take for $C$ the set containing all the atomic propositions of the form $P(\varepsilon)$ and $P(\gamma x)$. Then, we replace each neutral rules and elimination rules with the conclusion $P(x)$ by an instance with the conclusion $P(\varepsilon)$ and for each stack symbol $\gamma$, an instance with the conclusion $P(\gamma x)$. ◀

**Definition 22 (Complementation).** Let $\mathcal{I}$ be a small step alternating pushdown system, $\tilde{\mathcal{I}}$ the system built at Lemma 21, and $C$ be a finite set of atomic propositions such that
- the conclusions of the rules of $\tilde{\mathcal{I}}$ are in the set $\mathcal{C}$,

- for every configuration $A$, there exists a unique proposition $B$ in $\mathcal{C}$ such that $A$ is an instance of $B$.

Then, we define the system $\overline{\mathcal{I}}$, the complementation of $\mathcal{I}$, as follows: for each $B$ in $\mathcal{C}$, if the system $\tilde{\mathcal{I}}$ contains $n$ rules $r_1^B, \dots, r_n^B$ with the conclusion $B$, where $n$ may be zero

$$ \frac{A_1^1 \dots A_{m_1}^1}{B} $$

...

$$ \frac{A_1^n \dots A_{m_n}^n}{B} $$

then the system $\overline{\mathcal{I}}$ contains the $m_1 \dots m_n$ rules

$$ \frac{A_{j_1}^1 \dots A_{j_n}^n}{B} $$

**Example 23.** Consider the language containing a constant $\varepsilon$, a monadic function symbol $a$, and monadic predicate symbols $P, Q, R, S$. Consider the small step inference system $\mathcal{R}$

$$ \frac{Q(x) \quad R(x)}{P(x)} \quad \mathbf{n1} \quad \frac{S(x)}{P(x)} \quad \mathbf{n2} \quad \frac{P(ax)}{Q(x)} \quad \mathbf{e1} \quad \overline{R(ax)} \quad \mathbf{i1} $$

we transform this system into the equivalent inference system $\tilde{\mathcal{R}}$

$$ \frac{Q(\varepsilon) \quad R(\varepsilon)}{P(\varepsilon)} \quad \frac{Q(ax) \quad R(ax)}{P(ax)} \quad \frac{S(\varepsilon)}{P(\varepsilon)} \quad \frac{S(ax)}{P(ax)} $$

$$ \frac{P(a)}{Q(\varepsilon)} \quad \frac{P(aax)}{Q(ax)} \quad \overline{R(ax)} $$

Then, the system $\overline{\mathcal{R}}$ is defined by the rules

$$ \frac{Q(\varepsilon) \quad S(\varepsilon)}{P(\varepsilon)} \quad \frac{R(\varepsilon) \quad S(\varepsilon)}{P(\varepsilon)} \quad \frac{Q(ax) \quad S(ax)}{P(ax)} $$

$$ \frac{R(ax) \quad S(ax)}{P(ax)} \quad \frac{P(a)}{Q(\varepsilon)} \quad \frac{P(aax)}{Q(ax)} $$

$$ \overline{R(\varepsilon)} \quad \overline{S(\varepsilon)} \quad \overline{S(ax)} $$

**Lemma 24.** The function $F_{\overline{\mathcal{I}}}$ is the function $G_{\tilde{\mathcal{I}}}$, that is, a configuration is provable in $\overline{\mathcal{I}}$ in one step from the set of configurations $\mathcal{P} \setminus X$, if and only if it is not provable in one step in $\tilde{\mathcal{I}}$ from the set of configurations $X$.

**Proof.** Consider a configuration $B$. There exists a unique proposition $C$ in $\mathcal{C}$ such that $B = \sigma C$.

Given a set of configurations $X$, assume $B$ is provable in one step from $\mathcal{P} \setminus X$ with a rule of $\overline{\mathcal{I}}$, then the premises $\sigma A_{j_i}^i$ are in $\mathcal{P} \setminus X$. Thus none of these configurations is in $X$, thus $B$ is not provable in one step from $X$ with a rule of $\tilde{\mathcal{I}}$.

Conversely, assume $B$ is not provable in one step in $\tilde{\mathcal{I}}$ from the configurations of $X$, then for each inference rule with the conclusion $C$, $r_i^C$ of $\tilde{\mathcal{I}}$, there exists a premise $A_{j_i}^i$ such that $\sigma A_{j_i}^i$ is not an element of $X$. Thus, all the configurations $\sigma A_{j_i}^i$ are in $\mathcal{P} \setminus X$ and hence $B$ is provable in one step from $\mathcal{P} \setminus X$ with a rule of $\overline{\mathcal{I}}$. ◀
**► Definition 25 (Co-inductive proof).** A co-inductive proof in an inference system $\mathcal{J}$ is a finite or infinite tree labeled by configurations such that for each node $N$, there exists an inference rule

$$ \frac{A_1 \dots A_n}{B} $$

in $\mathcal{J}$, and a substitution $\sigma$ such that the node $N$ is labeled with $\sigma B$ and its children are labeled with $\sigma A_1, \dots, \sigma A_n$. A co-inductive proof is a co-inductive proof of a configuration $A$ if its root is labeled by $A$. A configuration $A$ is said to be co-inductively provable if it has a co-inductive proof.

It is well-known that a configuration $A$ is an element of the greatest fixed point of the co-continuous function $F_{\mathcal{J}}$ if and only if it has a co-inductive proof in the system $\mathcal{J}$ [13].

**► Theorem 26.** Let $\mathcal{I}$ be a small step alternating pushdown system. A configuration has a co-inductive proof in $\mathcal{I}$ if and only if it has no proof in $\mathcal{I}$.

**Proof.** A configuration $A$ has a co-inductive proof in $\mathcal{I}$ if and only if it is an element of the greatest fixed point of the co-continuous function $F_{\mathcal{I}}$, if and only if it is an element of the greatest fixed point of the co-continuous function $G_{\mathcal{I}}$ (by Lemma 24), if and only if it is not an element of the least fixed point of the function $F_{\mathcal{I}}$ (by Lemma 20), if and only if it has no proof in $\mathcal{I}$ if and only if it has no proof in $\mathcal{I}$ (by Lemma 21). ◀

**► Example 27.** The configuration $P(a)$ is not provable in the system $\mathcal{R}$ defined in Example 23, and it has a co-inductive proof in the system $\mathcal{R}$:

$$ \frac{\frac{\frac{P(\mathcal{I})}{Q(\mathcal{I})} \quad \frac{S(\mathcal{I})}{Q(\mathcal{I})}}{P(\mathcal{I}) \quad S(\mathcal{I})}}{P(\mathcal{I})} $$

Theorem 26 can be used to introduce negation as failure [3] in alternating pushdown systems. Instead of defining another system $\mathcal{I}$, we just extend the system $\mathcal{I}$ into a system $\mathcal{I}_-$, with the rules

$$ \frac{\neg A_{j_1}^1 \dots \neg A_{j_n}^n}{\neg B} $$

However, this requires to consider co-inductive proofs for closed propositions of the form $\neg A$ and usual inductive proofs for closed propositions of the form $A$, as illustrated in Example 27.

# 4 From co-inductive proofs to inductive proofs

To avoid considering co-inductive proofs for closed propositions of the form $\neg A$, as we did in Section 3, we can first transform a small step alternating pushdown system $\mathcal{I}$ into a saturated alternating pushdown system $\mathcal{I}_s$ and then into an alternating multi-automaton $\mathcal{I}'$
and then transform $\mathcal{I}'$ into $\mathcal{I}'_-$

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

Then, in the rules of system $\mathcal{I}'_-$, the premises are always smaller than the conclusion. Thus, a co-inductive proof in $\mathcal{I}'_-$ is always finite. This leads to the following theorem.

**Theorem 28.** *The proposition $\neg A$ has a (finite) proof in $\mathcal{I}'_-$ if and only if it has a co-inductive proof in $\mathcal{I}_-$.*

**Proof.** The proposition $\neg A$ has a (finite) proof in $\mathcal{I}'_-$ if and only if it has a co-inductive proof in $\mathcal{I}'_-$ if and only if $A$ has no proof in $\mathcal{I}'$ if and only if $A$ has no proof in $\mathcal{I}$ if and only if $\neg A$ has a co-inductive proof in $\mathcal{I}_-$.

**Example 29.** As the system $\mathcal{R}$, defined in Example 23, is saturated, a configuration $A$ is provable in $\mathcal{R}$ if and only if it is provable in the system $\mathcal{R}'$ containing only the introduction rule.

$$ \overline{R(ax)} $$

The system $\mathcal{R}'_-$ contains this introduction rule and the rules

$$ \neg P(\varepsilon) $$

$$ \neg P(ax) $$

$$ \neg Q(\varepsilon) $$

$$ \neg Q(ax) $$

$$ \neg R(\varepsilon) $$

$$ \neg S(\varepsilon) $$

$$ \neg S(ax) $$

and the proposition $\neg P(a)$ has the finite proof

$$ \overline{\neg P(a)} $$

From Theorem 28, if a proposition $\neg A$ has a finite proof in $\mathcal{I}'_-$, it has a co-inductive proof in $\mathcal{I}_-$. In the sequel, we give a more complex, but more informative proof, where from a finite proof of $\neg A$ in $\mathcal{I}'_-$ we reconstruct a co-inductive proof in $\mathcal{I}_-$. Such a co-inductive proof in the complementation of the original system $\mathcal{I}$ is more informative than the proof in $\mathcal{I}'_-$ because it contains an explicit counter-example to $A$: for instance the proof

$$ \begin{array}{ccc} \begin{array}{c} \vdots \\ \overline{\neg P(aaa)} \\ \overline{\neg Q(aa)} \end{array} & & \overline{\neg S(aa)} \\ \hline \begin{array}{c} \overline{\neg P(aa)} \\ \overline{\neg Q(a)} \end{array} & \overline{\neg P(a)} & \\ \hline \end{array} $$

explains that $P(a)$ is false because $Q(a)$ and $S(a)$ are false, $Q(a)$ is false because $P(aa)$ is false, etc.
**► Lemma 30.** Consider a natural number $n \ge 1$, $n$ families of sets $\langle H_1^1, \dots, H_{k_1}^1 \rangle$, ..., $\langle H_1^n, \dots, H_{k_n}^n \rangle$ and a set $S$, such that each of the $k_1 \dots k_n$ sets of the form $H_{j_1}^1 \cup \dots \cup H_{j_n}^n$ contains an element of $S$. Then, there exists an index $l$, $1 \le l \le n$, such that each of the sets $H_1^l, \dots, H_{k_l}^l$ contains an element of $S$.

**Proof.** By induction on $n$.

If $n=1$, then each of the sets $H_1^1, \dots, H_{k_1}^1$ contains an element of $S$.

Then, assume the property holds for $n$ and consider $\langle H_1^1, \dots, H_{k_1}^1 \rangle$, ..., $\langle H_1^n, \dots, H_{k_n}^n \rangle$, $\langle H_1^{n+1}, \dots, H_{k_{n+1}}^{n+1} \rangle$ such that each of the $k_1 \dots k_n k_{n+1}$ sets of the form $H_{j_1}^1 \cup \dots \cup H_{j_n}^n \cup H_{j_{n+1}}^{n+1}$ contains an element of $S$. We have,

- each of the $k_1 \dots k_n$ sets of the form $(H_{j_1}^1 \cup \dots \cup H_{j_n}^n) \cup H_1^{n+1}$ contains an element of $S$,

- ...

- each of the $k_1 \dots k_n$ sets of the form $(H_{j_1}^1 \cup \dots \cup H_{j_n}^n) \cup H_{k_{n+1}}^{n+1}$ contains an element of $S$.

- either each of the $k_1 \dots k_n$ sets of the form $H_{j_1}^1 \cup \dots \cup H_{j_n}^n$ contains an element of $S$ or $H_1^{n+1}$ contains an element of $S$,

- ...

- either each of the $k_1 \dots k_n$ sets of the form $H_{j_1}^1 \cup \dots \cup H_{j_n}^n$ contains an element of $S$ or $H_{k_{n+1}}^{n+1}$ contains an element of $S$.

Hence,

- either each of the $k_1 \dots k_n$ sets of the form $H_{j_1}^1 \cup \dots \cup H_{j_n}^n$ contains an element of $S$,

- or $H_1^{n+1}$ contains an element of $S$, ..., and $H_{k_{n+1}}^{n+1}$ contains an element of $S$.

Thus, either, by induction hypothesis, there exists an index $l \le n$ such that each of the $H_1^l$, ..., $H_{k_l}^l$ contains an element of $S$, or each of the sets $H_1^{n+1}, \dots, H_{k_{n+1}}^{n+1}$ contains an element of $S$. Therefore, there exists an index $l \le n+1$ such that each of the sets $H_1^l, \dots, H_{k_l}^l$ contains an element of $S$.

**► Lemma 31.** Let $\mathcal{I}$ be a small step alternating pushdown system. For each rule of $\mathcal{I}'$ of the form

$$ \frac{\neg B_1 \dots \neg B_q}{\neg A} $$

there exists a rule of $\mathcal{I}'$

$$ \frac{\neg C_1 \dots \neg C_p}{\neg A} $$

such that the $\neg C_1, \dots, \neg C_p$ are provable in $\mathcal{I}'$ from the hypotheses $\neg B_1, \dots, \neg B_q$.

**Proof.** The rules in $\mathcal{I}'$ whose conclusion is a negation have the form

$$ \frac{\neg S_1(x) \dots \neg S_q(x)}{\neg P(ax)} $$

and

$$ \overline{\neg P(\varepsilon)} $$

Consider first a rule of the form

$$ \frac{\neg S_1(x) \dots \neg S_q(x)}{\neg P(ax)} $$

By the construction of $\mathcal{I}'$, it is sufficient to prove that each rule of $\tilde{\mathcal{I}}$ with the conclusion $P(ax)$ has a premise whose negation is provable in $\mathcal{I}'$ from the hypotheses $\neg S_1(x), \dots, \neg S_q(x)$.
Consider an introduction rule in $\tilde{\mathcal{I}}$

This rule is also a rule of $\mathcal{I}$, $\mathcal{I}_s$ and $\mathcal{I}'$, thus, by construction of $\mathcal{I}'_-$, one of the $S_i(x)$ is a $Q_j(x)$, thus $\neg Q_j(x)$ is provable in $\mathcal{I}'_-$ from $\neg S_1(x)$, ..., $\neg S_q(x)$.

Consider a rule of $\tilde{\mathcal{I}}$

instance of a neutral rule of $\mathcal{I}$

$$ \frac{Q_1(ax) \dots Q_n(ax)}{P(ax)} $$

$$ \frac{Q_1(x) \dots Q_n(x)}{P(x)} $$

As there is a rule $\mathcal{I}'_-$, with the conclusion $\neg P(ax)$, the number $n$ of premises is at least 1. Consider the $k_1$ introduction rules of $\mathcal{I}_s$ with the conclusion $Q_1(ax)$ and respective sets of premises $H_1^1$, ..., $H_{k_1}^1$, ..., the $k_n$ introduction rules of $\mathcal{I}_s$ with the conclusion $Q_n(ax)$ and respective sets of premises $H_1^n$, ..., $H_{k_n}^n$. As the system $\mathcal{I}_s$ is saturated it contains $k_1 \dots k_n$ introduction rules with the conclusion $P(ax)$ and sets of premises of the form $H_{j_1}^1 \cup \dots \cup H_{j_n}^n$. All these rules are rules of $\mathcal{I}'$ thus, by the construction of $\mathcal{I}'_-$, each of these $k_1 \dots k_n$ sets contains an element of $\{S_1(x), \dots, S_q(x)\}$. By Lemma 30, there exists an index $l$ such that each $H_j^l$ contains an element of $\{S_1(x), \dots, S_q(x)\}$. Thus, by construction, the system $\mathcal{I}'_-$ contains a rule deducing the proposition $\neg Q_l(ax)$ from premises in $\{\neg S_1(x), \dots, \neg S_q(x)\}$ and thus $\neg Q_l(ax)$ is provable in $\mathcal{I}'_-$ from $\neg S_1(x), \dots, \neg S_q(x)$.

Consider a rule of $\tilde{\mathcal{I}}$

$$ \frac{Q_1(bax) Q_2(ax) \dots Q_n(ax)}{P(ax)} $$

instance of an elimination rule of $\mathcal{I}$

$$ \frac{Q_1(bx) Q_2(x) \dots Q_n(x)}{P(x)} $$

Consider the $k$ introduction rules of $\mathcal{I}_s$ with the conclusion $Q_1(bx)$ and respective sets of premises $H_1$, ..., $H_k$. As the system $\mathcal{I}_s$ is saturated it contains $k$ neutral rules with the conclusion $P(x)$ and sets of premises of the form $H_j \cup \{Q_2(x), \dots, Q_n(x)\}$. Consider the instances of these neutral rules with the conclusion $P(ax)$ and premises $(ax/x)H_j \cup \{Q_2(ax), \dots, Q_n(ax)\}$. By the previous case, each of these $k$ sets contains an element whose negation is provable in $\mathcal{I}'_-$ from $\neg S_1(x), \dots, \neg S_q(x)$. Thus, either one of the $\neg Q_i(ax)$ is provable in $\mathcal{I}'_-$ from $\neg S_1(x), \dots, \neg S_q(x)$, or each of the sets $(ax/x)H_1, \dots, (ax/x)H_k$ contains an element whose negation is provable in $\mathcal{I}'_-$ from $\neg S_1(x), \dots, \neg S_q(x)$ in which case $\neg Q_1(bax)$ is provable in $\mathcal{I}'_-$ from $\neg S_1(x), \dots, \neg S_q(x)$.

The proof is similar for rules of the form

$$ \neg P(\varepsilon) $$

By the construction of $\mathcal{I}'_-$, it is sufficient to prove that each rule of $\tilde{\mathcal{I}}$ with the conclusion $P(\varepsilon)$ has a premise whose negation is provable in $\mathcal{I}'_-$.

As $\mathcal{I}'_-$ contains the rule

$$ \neg P(\varepsilon) $$

there is no rule in $\mathcal{I}'$ with the conclusion $P(\varepsilon)$. Thus, there is no introduction rule, in $\mathcal{I}_s$, in $\mathcal{I}$, hence in $\tilde{\mathcal{I}}$, with the conclusion $P(\varepsilon)$.
Consider a rule of $\tilde{\mathcal{I}}$

$$ \frac{Q_1(\varepsilon) \dots Q_n(\varepsilon)}{P(\varepsilon)} $$

instance of a neutral rule of $\mathcal{I}$

$$ \frac{Q_1(x) \dots Q_n(x)}{P(x)} $$

As there is a rule $\mathcal{I}'$, with the conclusion $\neg P(\varepsilon)$, the number $n$ of premises is at least 1. As the system $\mathcal{I}_s$ is saturated and contains no introduction rule with the conclusion $P(\varepsilon)$, there exists an index $i$ such that there is no introduction rule in $\mathcal{I}_s$ of the form

$$ \overline{Q_i(\varepsilon)} $$

Hence, there is no such introduction rule in $\mathcal{I}'$. Thus, the system $\mathcal{I}'$, contains the rule

$$ \overline{\neg Q_i(\varepsilon)} $$

and the proposition $\neg Q_i(\varepsilon)$ is provable in $\mathcal{I}'$.

Consider a rule of $\tilde{\mathcal{I}}$

$$ \frac{Q_1(b) Q_2(\varepsilon) \dots Q_n(\varepsilon)}{P(\varepsilon)} $$

instance of an elimination rule of $\mathcal{I}$

$$ \frac{Q_1(bx) Q_2(x) \dots Q_n(x)}{P(x)} $$

Consider the $k$ introduction rules of $\mathcal{I}_s$ with the conclusion $Q_1(bx)$ and respective sets of premises $H_1, \dots, H_k$. As the system $\mathcal{I}_s$ is saturated it contains $k$ neutral rules with the conclusion $P(x)$ and sets of premises of the form $H_j \cup \{Q_2(x), \dots, Q_n(x)\}$. Consider the instances of these neutral rules with the conclusion $P(\varepsilon)$ and premises $(\varepsilon/x)H_j \cup \{Q_2(\varepsilon), \dots, Q_n(\varepsilon)\}$. By the previous case, each of these $k$ sets contains an element whose negation is provable in $\mathcal{I}'$. Thus either one of the $\neg Q_i(\varepsilon)$ is provable in $\mathcal{I}'$ or each of the sets $(\varepsilon/x)H_1, \dots, (\varepsilon/x)H_k$ contains an element whose negation is provable in $\mathcal{I}'$ in which case $\neg Q_1(b)$ is provable in $\mathcal{I}'$.

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

**► Example 32.** In the system described in Example 23 and Example 27, consider the rule of $\mathcal{R}'$

$$ \overline{\neg P(ax)} $$

Both rules of $\tilde{\mathcal{R}}$

$$ \frac{Q(ax) \quad R(ax)}{P(ax)} $$

and

$$ \frac{S(ax)}{P(ax)} $$

have a premise whose negation is provable in $\mathcal{R}'$: $Q(ax)$ for the first and $S(ax)$ for the second. Thus the rule of $\mathcal{R}'$

$$ \frac{\neg Q(ax) \quad \neg S(ax)}{\neg P(ax)} $$

deduces $\neg P(ax)$ from premises $\neg Q(ax)$ and $\neg S(ax)$ that are both provable in $\mathcal{R}'$.
In the same way, the system $\mathcal{R}'_{\neg}$ contains the rule

$$ \neg Q(ax) $$

and the rule of $\mathcal{R}_{\neg}$

$$ \frac{\neg P(aax)}{\neg Q(ax)} $$

deduces $\neg Q(ax)$ from the premise $\neg P(aax)$ that is provable in $\mathcal{R}'_{\neg}$.

Finally, the system $\mathcal{R}'_{\neg}$ contains the rule

$$ \neg S(ax) $$

and the rule of $\mathcal{R}_{\neg}$

$$ \neg S(ax) $$

deduces $\neg S(ax)$ from no premises.

**Lemma 33.** If the proposition $\neg A$ is provable in $\mathcal{I}'_{\neg}$, then there exists a rule in $\mathcal{I}_{\neg}$, deducing $\neg A$ from premises that are all provable in $\mathcal{I}'_{\neg}$.

**Proof.** If the last rule of the proof of $\neg A$ has the form

$$ \frac{\neg S_1(x) \dots \neg S_q(x)}{\neg P(ax)} $$

then $A = P(aw)$, and the propositions $\neg S_1(w), \dots, \neg S_q(w)$ have proofs in $\mathcal{I}'_{\neg}$. By Lemma 31, there exists a rule in $\mathcal{I}_{\neg}$ deducing $\neg P(ax)$ from premises that are all provable in $\mathcal{I}'_{\neg}$ from $\neg S_1(x), \dots, \neg S_q(x)$. Thus this rule deduces $\neg P(aw)$ from premises that are provable in $\mathcal{I}'_{\neg}$ from $\neg S_1(w), \dots, \neg S_q(w)$. As these propositions are provable in $\mathcal{I}'_{\neg}$, so are the premises.

If the last rule of the proof of $\neg A$ has the form

$$ \neg P(\varepsilon) $$

then $A = P(\varepsilon)$. By Lemma 31, there exists a rule in $\mathcal{I}_{\neg}$ deducing $\neg P(\varepsilon)$ from premises that are all provable in $\mathcal{I}'_{\neg}$. ◀

**Theorem 34.** If a proposition $\neg A$ has a proof in the system $\mathcal{I}'_{\neg}$, then it has a co-inductive proof in the system $\mathcal{I}_{\neg}$.

**Proof.** By Lemma 33, the proposition $\neg A$ can be proved with a rule of $\mathcal{I}_{\neg}$ whose premises are provable in $\mathcal{I}'_{\neg}$. We co-inductively build a proof of these premises. ◀

**Example 35.** In the system of Example 23, consider the proof in $\mathcal{R}'_{\neg}$

$$ \neg P(a) $$

This proof can be transformed into the proof in $\mathcal{R}_{\neg}$

$$ \frac{\neg Q(a) \quad \neg S(a)}{\neg P(a)} $$
and the proofs in $R'_{\neg}$

$$ \neg Q(a) $$

and

$$ \neg S(a) $$

Applying the same procedure to these premises yields the proof in $R_{\neg}$

$$ \frac{\frac{\neg P(aa)}{\neg Q(a)} \quad \neg S(a)}{\neg P(a)} $$

and the proof in $R'_{\neg}$

$$ \neg P(aa) $$

And iterating this process yields the co-inductive proof in $R_{\neg}$

$$ \frac{\frac{\neg P(aaa)}{\neg Q(aa)} \quad \neg S(aa)}{\frac{\neg P(aa)}{\neg Q(a)} \quad \neg S(a)} \quad \neg P(a) $$

## Conclusion

We have proposed a new approach to formalize alternating pushdown systems as natural-deduction style inference systems, and to prove the decidability of reachability based on a cut-elimination theorem.

This result permits to extend an alternating pushdown system into a complete system where, for every configuration A, either $A$ or $\neg A$ is provable. The key idea is that, in the complementation of an alternating multi-automaton, a proposition of the form $\neg A$ has a co-inductive (hence possibly infinite) proof if and only if it has an inductive (hence finite) proof. Moreover, if $A$ is not provable, we transform a finite proof of $\neg A$ into a possibly infinite counter-example, via a transformation of the proof of $\neg A$ in the complementation of the alternating multi-automaton into a co-inductive proof of the same proposition in the complementation of the original system.

This work is a first step towards establishing a connection between proof-theoretical methods and automata-theoretical methods to prove decidability results. Future work includes extension of this method to more expressive systems and the design of a general framework where decidability results, coming both from automata theory and from proof theory, can be proved.

From the implementation perspective, these connections also suggest connections between model-checking and proof-search.

## Acknowledgement

The authors want to thank Ahmed Bouajjani for enlightening discussions. This work is supported by the ANR-NSFC project LOCALI (NSFC 61161130530 and ANR 11 IS02 002 01) and the Chinese National Basic Research Program (973) Grant No. 2014CB340302.
References

1 A. Bouajjani, J. Esparza, and O. Maler, Reachability analysis of pushdown automata: Application to model-checking A. W. Mazurkiewicz, J. Winkowski (Eds.) *Concurrency theory*, Lecture Notes in Computer Science, 1243, 1997, 135-150.

2 G. Burel, Cut Admissibility by Saturation, G. Dowek (ed.) *Rewriting and Typed Lambda Calculi*, Lecture Notes in Computer Science 8560, 2014, pp. 124-138.

3 K. Clark. Negation as failure. H. Gallaire and J. Minker, (eds.), *Logic and Databases*, Plenum Press, 1978.

4 H. Comon, M. Dauchet, R. Gilleron, C. Löding, F. Jacquemard, D. Lugiez, S. Tison, and M. Tommasi, *Tree Automata Techniques and Applications*, http://www.grappa.univ-lille3.fr/tata, 2007

5 N. Dershowitz and C. Kirchner, Abstract canonical presentations, *Theoretical Computer Science*, 357, 2006, 53-69.

6 G. Dowek and Y. Jiang, A logical approach to CTL. Manuscript, 2013.

7 G. Dowek and Y. Jiang, Axiomatizing truth in a finite model. Manuscript, 2013.

8 T. Frühwirth, E. Shapiro, M. Vardi, E. Yardeni, Logic Programs as Types for Logic Programs, *Logic in Computer Science*, 1991, pp. 300–309.

9 J. Goubault-Larrecq, Deciding $H_1$ by Resolution, *Information Processing Letters*, 95(3), 2005, pp. 401–408.

10 S.C. Kleene, *Introduction to Metamathematics*, North Holland, 1952.

11 D.E. Knuth and P.B. Bendix, Simple word problems in universal algebras, J. Leech (Ed.), *Computational Problems in Abstract Algebras*, Pergamon Press, 1970, 263–297.

12 D. Prawitz, Natural Deduction, Almqvist & Wiksell, Stockholm, 1965.

13 D. Sangiorgi, *Introduction to Bisimulation and Coinduction*, Cambridge University Press, 2011.