11institutetext: PUC-Rio/UERJ/CNPq 22institutetext: UCL/UFRN
<EMAIL_ADDRESS><EMAIL_ADDRESS>
# On an ecumenical natural deduction with stoup \- Part I: The propositional
case

Luiz Carlos Pereira Pereira is supported by CAPES (PRINT and COFECUB) and
CNPq.11 Elaine Pimentel 22

##  1 Introduction

Natural deduction systems, as proposed by Gentzen [Gen69] and further studied
by Prawitz [Pra65], is one of the most well known proof-theoretical
frameworks. Part of its success is based on the fact that natural deduction
rules present a simple characterization of logical constants, especially in
the case of intuitionistic logic. However, there has been a lot of criticism
on extensions of the intuitionistic set of rules in order to deal with
classical logic. Indeed, most of such extensions add, to the usual
introduction and elimination rules, extra rules governing negation. As a
consequence, several meta-logical properties, the most prominent one being
harmony, are lost.111A logical connective is called harmonious in a certain
proof system if there exists a certain balance between the rules defining it.
For example, in natural deduction based systems, harmony is ensured when
introduction/elimination rules do not contain insufficient/excessive amounts
of information [CDD21].

In [Pra15], Dag Prawitz proposed a natural deduction ecumenical system, where
classical logic and intuitionistic logic are codified in the same system. In
this system, the classical logician and the intuitionistic logician would
share the universal quantifier, conjunction, negation and the constant for the
absurd ($\forall,\wedge,\neg,\bot$), but they would each have their own
existential quantifier, disjunction and implication, with different meanings
($\exists_{j},\vee_{j},\to_{j}$, where $j\in\\{i,c\\}$ for the intuitionistic
and classical versions, respectively). Prawitz’ main idea is that these
different meanings are given by a semantical framework that can be accepted by
both parties.

In his ecumenical system, Prawitz recovers the harmony of rules, but the rules
for the classical operators do not satisfy separability [Mur20]. In fact, the
classical rules are not pure, in the sense that negation is used in the
definition of the introduction and elimination rules for the classical
operators.

For example, the rules for $\vee_{c}$ are defined as

$[\neg A,\neg B]$ $\Pi$ $\bot$ $\vee_{c}$-int $A\vee_{c}B$ $A\vee_{c}B$ $\neg
A$ $\neg B$ $\vee_{c}$-elim $\bot$

The situation is not different in the case of the definition of left and right
rules for these classical operators in a sequent calculus codification, as
presented in [PPdP21]. The rules for $\vee_{c}$, for example, are defined as

$\Gamma,\neg A,\neg B\Rightarrow\bot$ $\vee_{c}$-R $\Gamma\Rightarrow
A\vee_{c}B$ $\Gamma\Rightarrow\neg A$ $\Delta\Rightarrow\neg B$ $\vee_{c}$-L
$A\vee_{c}B,\Gamma,\Delta\Rightarrow\bot$

There are many ways of proposing pure, harmonic natural deduction systems for
(propositional) classical logic. Indeed, Murzi [Mur20] proposes a new set of
rules for classical logical operators based on absurdity as a punctuation
mark, and higher-level rules [Sch14]. D’Agostino [DAg05], on the other hand,
brings a totally sifferent approach, presenting a theory of classical natural
deduction that makes a distinction between operational rules, governing the
use of logical operators, and structural rules dealing with the metaphysical
assumptions governing the (classical) notions of truth and falsity, namely the
principle of bivalence and the principle of non-contradiction.

A complete different approach is presented in [GG05], where Michael and
Murdoch Gabbay present the natural deduction version of Dov Gabbay’s Restart
rule

$BA$

with the side-condition that, below every occurrence of $Restart$ from $A$ to
$B$, there is (at least) one occurrence of $A$. The intended meaning is that
$B$ is a new start to a line of reasoning concluding $A$. For example, in the
derivation of the Peirce’s Law

$[(A\to B)\to A)]$ $[A]$ $Restart^{\star}$ $B$ $\to$-int $A\to B$ $\to$-elim
$A^{\dagger}$ $\to$-int $((A\to B)\to A)\to_{c}A)$

the restart at ⋆ is justified at $\dagger$.

Similar to the Gabbays, Restall’s $Alt$ rule [Res21]

$BA\Pi$

has the following interpretation: Having a proof of $A$, one can set $A$ aside
and consider some alternative conclusion, $B$, while $A$ is added to the
collection of alternatives current at this point of the proof. Hence, the
proof of Peirce’s Law would have the form

$[(A\to B)\to A)]$ $[A]$ $Alt,\downarrow A$ $B$ $\to$-int $A\to B$
$\to$-elim,$\uparrow A$ $A$ $\to$-int $((A\to B)\to A)\to_{c}A)$

In this paper, we propose a different approach adapting, to the natural
deduction framework, Girard’s mechanism of stoup [Gir91]. This will allow the
definition of a pure harmonic natural deduction system $\mathcal{LE}_{p}$ for
the propositional fragment of Prawitz’ ecumenical logic, where $Restart$ and
$Alt$ appear as special cases of the use of stoup.222It should be noted that
this idea appears somewhat hidden in [Res21] for the propositional classical
case, where Restall uses sequent style
$X\mathrel{\small{\mbox{$>\\!\\!\\!-$}}}A;Y$ (the ‘score’), where $X$
represent the undischarged assumptions, $A$ the current conclusion, and $Y$
the alternatives.

##  2 Ecumenical natural deduction system

The language ${\mathcal{L}}$ used for ecumenical systems is described as
follows. We will use a subscript $c$ for the classical meaning and $i$ for the
intuitionistic, dropping such subscripts when formulae/connectives can have
either meaning.

Classical and intuitionistic n-ary predicate symbols ($p_{c},p_{i},\ldots$)
co-exist in ${\mathcal{L}}$ but have different meanings. The neutral logical
connectives $\\{\bot,\neg,\wedge,\forall\\}$ are common for classical and
intuitionistic fragments, while $\\{\rightarrow_{i},\vee_{i},\exists_{i}\\}$
and $\\{\rightarrow_{c},\vee_{c},\exists_{c}\\}$ are restricted to
intuitionistic and classical interpretations, respectively. In order to avoid
clashes of variables we make use of a denumerable set $a,b,\ldots$ of special
variables called parameters, which do not appear quantified.

In Fig. 1 we present $\mathcal{NE}$ Prawitz’ original natural deduction first-
order ecumenical system. In the rules for quantifiers, the notation $A(a/x)$
stands for the substitution of $a$ for every (visible) instance of $x$ in $A$.
In the rules $\exists_{i}\mbox{-elim},\forall\mbox{-int}$, $a$ is a fresh
parameter, i.e., it does not occur free in any assumption that $A,B$ depends
on (apart from the assumption eliminated by $\exists_{i}$-elim).

Intuitionistic rules

$\begin{array}[]{lc@{\quad}l}B\lx@proof@logical@and
A\rightarrow_{i}BA&A\rightarrow_{i}BB\Pi[A]&C\lx@proof@logical@and
A\vee_{i}BC\Pi_{1}[A]C\Pi_{2}[B]\\\\[5.0pt]
A_{1}\vee_{i}A_{2}A_{j}&B\lx@proof@logical@and\exists_{i}x.AB\Pi[A(a/x)]&\exists_{i}x.AA(a/x)\end{array}$

Classic rules

$\begin{array}[]{lc@{\quad}l}\bot\lx@proof@logical@and A\rightarrow_{c}BA\neg
B&A\rightarrow_{c}B\bot\Pi[A,\neg B]&\bot\lx@proof@logical@and A\vee_{c}B\neg
A\neg B\\\\[5.0pt] A\vee_{c}B\bot\Pi[\neg A,\neg
B]&\bot\lx@proof<EMAIL_ADDRESS>x.\neg
A&\exists_{c}x.A\bot\Pi[\forall x.\neg A]\\\\[5.0pt] \bot\lx@proof@logical@and
p_{c}\neg p_{i}&p_{c}\bot\Pi[\neg p_{i}]\end{array}$

Neutral rules

$\begin{array}[]{lc@{\qquad}lc@{\qquad}lc@{\qquad}l}A_{j}A_{1}\wedge
A_{2}&&A\wedge BA\quad B&&\bot\lx@proof@logical@and A\neg A&&\neg
A\bot\Pi[A]\\\\[5.0pt] A\bot&&A(a/x)\forall x.A&&\forall x.AA(a/x)\end{array}$

Figure 1: Ecumenical natural deduction system $\mathcal{NE}$. In rules
$\forall\mbox{-int}$ and $\exists_{i}\mbox{-elim}$, the parameter $a$ is
fresh.

The propositional fragment of the natural deduction Ecumenical system proposed
by Prawitz (here called $\mathcal{NE}_{p}$) has been proved normalizing, sound
and complete with respect to intuitionistic logic’s Kripke semantics in
[PR17].

The rules for intuitionistic implication are the traditional ones, while the
rules for classical implication make sure that $A\to_{c}B$ is treated as $\neg
A\lor_{c}B$, its classical rendering. The surprising facts are that (i) one
can have a single constant for absurdity $\bot$ (instead of two, one
intuitionistic and one classical, taking that absurd as the unit of
disjunction, of which we have two variants) and (ii) that the intuitionistic
and classical negations coincide. If negation was simply implication into
false (as it is the case for intuitionistic negation) one might expect two
negations, one intuitionistic and one classical.

##  3 Sequent Calculus with stoup

$\mathsf{LC}$ [Gir91] is a sequent system for classical logic that separates
the rules for positive and negative formulas, being a precursor of the notion
of focusing in sequent systems [And92]. The polarity of a formula in
$\mathsf{LC}$ is determined by its outermost connective and the polarity of
its subformulas. For example, atoms and unities are always positive and, if
$P,Q$ are positive formulas, then $P\wedge Q$ is also positive. The table of
polarities can be checked in [Gir91], page 10.

In $\mathsf{LC}$, sequents have the form $\Rightarrow\Delta;\Sigma$, where
$\Delta,\Sigma$ are multisets of formulas, with $\Sigma$, called the stoup,
containing at most one formula. The main idea is that the stoup controls the
rule applications, in the sense that a positive active formula in the
conclusion of a rule is always placed there, while active negative formulas
are handled in the classical context. Characteristic examples are the rules
for the conjunction of positive/negative formulas

$\Rightarrow\Gamma,\Delta;P\wedge
Q\lx@proof@logical@and\Rightarrow\Gamma;P\Rightarrow\Delta;Q\qquad\Rightarrow\Gamma,M\wedge
N;\Sigma\lx@proof@logical@and\Rightarrow\Gamma,N;\Sigma\Rightarrow\Gamma,M;\Sigma$

Observe that they also have a multiplicative/additive flavor.

The idea of focusing is also present in $\mathsf{LC}$, with the dereliction
and store rules

$\Rightarrow\Gamma,P;\cdot\Rightarrow\Gamma;P\qquad\qquad\Rightarrow\Gamma;N\Rightarrow\Gamma,N;\cdot{}$

While in $der$ positive formulas can be chosen to be focused on, in $store$
negative formulas are stored in the classical context, in a bottom-up reading
of rules. This enables for a two-phase proof construction, where the focused
formula $P$ is systematically decomposed until reaching a leaf or a negative
sub-formula $N$. In this last case, focusing is lost and $N$ is stored,
allowing for the beginning of a new focused phase.

Finally, due to polarities, $\mathsf{LC}$ has two admissible cut rules

$\Rightarrow\Gamma,\Delta;\Sigma\lx@proof@logical@and\Rightarrow\Gamma;P\Rightarrow\neg
P,\Delta;\Sigma\qquad\qquad\Rightarrow\Gamma,\Delta;\Sigma\lx@proof@logical@and\Rightarrow\Gamma,N;\cdot\Rightarrow\neg
N,\Delta;\Sigma$

In $\mathsf{LC}$, the sequent $\Rightarrow\Delta;\Sigma$ has an intuitionistic
interpretation: $\neg\Delta\Rightarrow\bot$ if $\Sigma$ is empty and
$\neg\Delta\Rightarrow A$ if $\Sigma=A$. That is, the context $\Delta$ makes
the classical information persistent, via an implicit double negation
elimination. This implies that sequents with empty stoup have also a classical
interpretation, using e.g. Gödel’s double negation translation. Sequents with
non-empty stoup do not have a classical interpretation, as discussed in
[Gir91].

Hence one could say that sequents with stoup have a certain ecumenical flavor:
formulas with intuitionistic behavior are identified as being positive, while
formulas with classical behavior are identified as being negative.

In this work, we will carry out a similar idea under the spectrum of Prawitz’
ecumenical natural deduction system. While it has some similarities with
Girard’s original proposal, our system will not consider polarities, and all
the conclusion formulas of introduction/elimination rules will be placed in
the stoup.

##  4 Natural Deduction with stoup \- the propositional system
$\mathcal{LE}_{p}$

We will now incorporate the notion of stoups to natural deduction in the case
of propositional logic, showing its natural connection to the ecumenical
setting.

Let the expression $\Delta;\Sigma$ denote an stoup with a context (abreviated
as stp-c), an extension of natural deduction formulas, where $\Sigma$ is the
stoup and $\Delta$ is its accompanying context (called alternatives in
[Res21]). As for the case of $\mathsf{LC}$, the stoup will carry the
intuitionistic (positive) and neutral information, while the context
accumulates the classical information related to it.

In the following, we will construct ecumenical introduction and elimination
rules over the stoup in a step-by-step manner, justifying all our choices.

###  4.1 Intuitionistic operators

#### Implication.

The following result, proved in [PPdP21] for the sequent calculus ecumenical
system, states that logical consequence in $\mathcal{NE}$ is interpreted
intuitionistically.

###### Theorem 4.1

Let $\Gamma$ be a set of ecumenical formulas. Then $B$ is provable from
$\Gamma$ in ecumenical logic iff $\bigwedge\Gamma\rightarrow_{i}B$ is provable
in $\mathcal{NE}$.

Hence the rule

$A\rightarrow_{i}BB\Pi[A]$

induces the rule with stoup

$\Delta;A\rightarrow_{i}B\Delta;B\Pi\lx@proof@logical@and[\cdot;A]\Gamma$

where the stoup is preserved in discarded assumptions. Note that all the
information $\Gamma$ about contexts should be remembered.

For the implication elimination rule, observe that different stoups carry
different contexts, so we will have the multiplicative version of the rule,
combining the classical information

$\Delta_{1};A\to_{i}B$ $\Delta_{2};A$ $\to_{i}$-elim $\Delta_{1},\Delta_{2};B$

#### Disjunction.

The rule for introduction is

$\Delta;A_{i}$ $\vee_{i}$-int $\Delta;A_{1}\vee_{i}A_{2}$

while the elimination rule combines the all the context information

$\Gamma_{1}$ $\Pi_{1}$ $\Delta_{1};A\vee_{i}B$ $[\cdot;A]$ $\Gamma_{2}$
$\Pi_{2}$ $\Delta_{2};C$ $[\cdot;B]$ $\Gamma_{3}$ $\Pi_{3}$ $\Delta_{3};C$
$\vee_{i}$-elim $\Delta_{1},\Delta_{2},\Delta_{3};C$

###  4.2 Classical operators

#### Implication.

Observe that the negated assumptions in $\mathcal{NE}$ will correspond to the
classical counterpart of the stoup, so the consequent of the implication will
be stored in this context. The introduction rule

$A\rightarrow_{c}B\bot\Pi[A,\neg B]$

then becomes

$[\cdot;A]$ $\Gamma$ $\Pi$ $\Delta,B;\cdot$ $\to_{c}$-int $\Delta;A\to_{c}B$

For the elimination rule, also the negated formula in the premise become
classical, this time with empty stoup.

$\Delta_{1};A\to_{c}B$ $\Gamma_{2}$ $\Pi_{2}$ $\Delta_{2};A$ $[\cdot;B]$
$\Gamma_{3}$ $\Pi_{3}$ $\Delta_{3};\cdot$ $\to_{c}$-elim
$\Delta_{1},\Delta_{2},\Delta_{3};\cdot$

#### Disjunction.

The same idea applies to disjunction, where negated assumptions become part of
the classical context, while positive assumptions are kept as stoups

$\Delta,A,B;\cdot$ $\vee_{c}$-int $\Delta;A\vee_{c}B$

$\Delta_{1};A\vee_{c}B$ $[\cdot;A]$ $\Gamma_{2}$ $\Pi_{2}$ $\Delta_{2};\cdot$
$[\cdot;B]$ $\Gamma_{3}$ $\Pi_{3}$ $\Delta_{3};\cdot$ $\vee_{c}$-elim
$\Delta_{1},\Delta_{2},\Delta_{3};\cdot$

###  4.3 Neutral operators

#### Negation.

Since negation can be defined in classical/intuitionistic logic as “implies
bottom”, the rules for $\neg$ can be derived from the ones for implication
with an empty stoup.

$[\cdot;A]$ $\Gamma$ $\Pi$ $\Delta;\cdot$ $\neg$-int $\Delta;\neg A$

$\Delta_{1};A$ $\Delta_{2};\neg A$ $\neg$-elim $\Delta_{1},\Delta_{2};\cdot$

#### Conjunction.

Since our ecumenical system is essentially intuitionistic (in the terms of
Proposition 4.1), all active formulas are placed in the stoup. Hence we will
adopt the multiplicative version of Girard’s rule for positive conjuncts.

$\Delta_{1};A$ $\Delta_{2};B$ $\wedge$-int $\Delta_{1},\Delta_{2};A\wedge B$

$\Delta;A_{1}\wedge A_{2}$ $\wedge$-elimj $\Delta;A_{j}$

###  4.4 Hypothesis formation and dereliction

The hypothesis formation is the usual one and, as in $\mathsf{LC}$,
dereliction is needed for guaranteeing the completeness of the system, since
ecumenical active formulas are always placed in the stoup.

Hypothesis formation

$\cdot;A$

Dereliction

$\Delta;A$ der $\Delta,A;\cdot$

###  4.5 Structural rules

Finally, on choosing the multiplicative version of rules, we need structural
rules acting in the classical context, so to transform multisets into sets. As
usual in intuitionistic systems, weakening is also allowed in the stoup.

Weakening

$\Delta;\cdot$ $W_{i}$ $\Delta;A$ $\Delta;C$ $W_{c}$ $\Delta,A;C$

Contraction

$\Delta,A,A;C$ $C_{c}$ $\Delta,A;C$

Derivations are then inductively defined in the usual way.

###### Definition 1

We say that the stp-c $\Delta;\Sigma$ is derivable from a set $\Gamma$ of stp-
cs in $\mathcal{LE}_{p}$ (denoted by
$\Gamma\vdash_{\mathcal{LE}_{p}}\Delta;\Sigma$) if and only if there is a
derivation of $\Delta;\Sigma$ from $\Gamma$. A formula $A$ is a theorem of
$\mathcal{LE}_{p}$ if and only if $\vdash_{\mathcal{LE}_{p}}\cdot;A$.

As usual, we also may add indices in derivations, for relating a discharged
assumption with a specific rule application.

##  5 Examples

We present below the proofs of some classical tautologies in
$\mathcal{LE}_{p}$.

  1. 1.

Peirce’s Law

$[\cdot;((A\to_{c}B)\to_{c}A)]^{3}$ $[\cdot;A]^{1}$ der $A;\cdot$ $W_{c}$
$A,B;\cdot$ 1  $\to_{c}$-int $A;(A\to_{c}B)$ $[\cdot;A]^{2}$ der $A;\cdot$ 2
$\to_{c}$-elim $A,A;\cdot$ $C_{c}$ $A;\cdot$ 3  $\to_{c}$-int
$\cdot;(((A\to_{c}B)\to_{c}A)\to_{c}A)$

Observe that the only difference of the proof above w.r.t. $Alt$ or $Restart$
systems lies in the use of structural rules in the classical context.

More interestingly, note that any sequent of the form
$(((A\to_{j}B)\to_{k}A)\to_{c}A)$ with $j,k\in\\{i,c\\}$ is provable in
$\mathcal{LE}_{p}$. That is, provability is maintained if the outermost
implication is classical.

  2. 2.

Excluded-middle

$[\cdot;A]^{1}$ der $A;\cdot$ 1  $\neg$-int $A;\neg A$ der $A,\neg A;\cdot$
$\vee_{c}$-int $\cdot;(A\vee_{c}\neg A)$

Of course, $\cdot;A\vee_{i}\neg A$ is not a theorem in $\mathcal{LE}_{p}$.

  3. 3.

Dummett’s linearity axiom

$[\cdot;A]^{1}$ der $A;\cdot$ $W_{c}$ $A,B;\cdot$ $1$ $\to_{c}$-int
$A;(A\to_{c}B)$ der $A,(A\to_{c}B);\cdot$ $\to_{c}$-int
$(A\to_{c}B);(B\to_{c}A)$ der $(A\to_{c}B),(B\to_{c}A));\cdot$ $\vee_{c}$-int
$\cdot;((A\to_{c}B)\vee_{c}(B\to_{c}A))$

This is also an interesting case, where any sequent of the form
$((A\to_{j}B)\vee_{c}(B\to_{k}A))$ with $j,k\in\\{i,c\\}$ is provable in
$\mathcal{LE}_{p}$. That is, provability is maintained if the outermost
conjunction is classical.

##  6 Systems equivalence

In the following, we will show that $\mathcal{LE}_{p}$ is correct and complete
w.r.t. $\mathcal{NE}_{p}$. We will use the following extra notation:

  * -

Given a multiset $\Delta$ of formulas, we denote by $\neg\Delta$ the multiset
formed by the negation of each formula in $\Delta$.

  * -

If $\Gamma$ is a set of formulas, we denote by
$\Gamma\vdash_{\mathcal{NE}_{p}}A$ the fact that the formula $A$ depends on
the set $\Gamma$ of assumptions in $\mathcal{NE}_{p}$.

  * -

If $\Gamma=\bigcup\\{\cdot;A_{i}\\}_{0\leq i\leq n}$ is a multiset of stoup
with empty contexts in $\mathcal{LE}_{p}$, we will abuse the notation and also
represent by $\Gamma$ the underlying set of formulas in these stp-c, that is,
$\Gamma=\bigcup\\{A_{i}\\}_{0\leq i\leq n}$ in $\mathcal{NE}_{p}$.

###### Theorem 6.1

Let $\Gamma=\bigcup\\{\cdot;A_{i}\\}_{0\leq i\leq n}$ be a set of hypothesis.
Then $\Gamma\vdash_{\mathcal{LE}_{p}}\Delta;\Sigma$ iff
$\Gamma,\neg\Delta\vdash_{\mathcal{NE}_{p}}\Sigma$. In case $\Sigma$ is empty,
we have $\Gamma,\neg\Delta\vdash_{\mathcal{NE}_{p}}\bot$.

###### Proof

By induction on the length of derivations in $\mathcal{LE}_{p}$ and
$\mathcal{NE}_{p}$. The only interesting cases are the ones involving
classical connectives and structural rules.

  * •

Case $\vee_{c}$-int. Suppose that we have the following derivation in
$\mathcal{LE}_{p}$:

$\Gamma$ $\Pi$ $\Delta,A,B;\cdot$ $\vee_{c}$-int $\Delta;A\vee_{c}B$

By the inductive hypothesis, $\Gamma,\neg A,\neg
B,\neg\Delta\vdash_{\mathcal{NE}_{p}}\bot$. We can then take the desired
derivation to be:

$\Gamma\quad\neg\Delta\quad[\neg A]^{n}\quad[\neg B]^{m}$ $\Pi^{\prime}$
$\bot$ $n,m$ $\vee_{c}$-int $A\vee_{c}B$

On the other hand, suppose that
$\Gamma,\neg\Delta\vdash_{\mathcal{NE}_{p}}A\vee_{c}B$ with proof

$\Gamma\quad\neg\Delta\quad[\neg A]\quad[\neg B]$ $\Pi$ $\bot$ $\vee_{c}$-int
$A\vee_{c}B$

By the inductive hypothesis, we have
$\Gamma\vdash_{\mathcal{LE}_{p}}\Delta,A,B;\cdot$. We can then take the
desired derivation to be:

$\Gamma$ $\Pi$ $\Delta,A,B;\cdot$ $\vee_{c}$-int $\Delta;A\vee_{c}B$

  * •

Case $\vee_{c}$-elim. Suppose that
$\Gamma_{1},\Gamma_{2},\Gamma_{3}\vdash_{\mathcal{LE}_{p}}\Delta_{1},\Delta_{2},\Delta_{3};\cdot$
with proof

$\Gamma_{1}$ $\Pi_{1}$ $\Delta_{1};A\vee_{c}B$ $\Gamma_{2}$ $[\cdot;A]$
$\Pi_{2}$ $\Delta_{2};\cdot$ $\Gamma_{3}$ $[\cdot;B]$ $\Pi_{3}$
$\Delta_{3};\cdot$ $\vee_{c}$-elim $\Delta_{1},\Delta_{2},\Delta_{3};\cdot$

By the inductive hypothesis we have:
$\Gamma_{1},\neg\Delta_{1}\vdash_{\mathcal{NE}_{p}}A\vee_{c}B$,
$\Gamma_{2},\neg\Delta_{2},A\vdash_{\mathcal{NE}_{p}}\bot$ and
$\Gamma_{3},\neg\Delta_{3},B\vdash_{\mathcal{NE}_{p}}\bot$. We can the obtain
the desired derivation as follows:

$\Gamma_{1}$ $\neg\Delta_{1}$ $\Pi_{1}^{\prime}$ $A\vee_{c}B$ $\Gamma_{2}$
$\neg\Delta_{2}$ $[A]^{n}$ $\Pi_{2}^{\prime}$ $\bot$ $n$ $\neg$-int $\neg A$
$\Gamma_{3}$ $\neg\Delta_{3}$ $[B]^{m}$ $\Pi_{3}^{\prime}$ $\bot$ $m$
$\neg$-int $\neg B$ $\vee_{c}$-elim $\bot$

On the other hand, suppose that
$\Gamma_{1},\Gamma_{2},\Gamma_{3},\neg[\Delta_{1}],\neg[\Delta_{2}],\neg[\Delta_{3}]\vdash_{\mathcal{NE}_{p}}\bot$
with the following derivation:

$\Gamma_{1}$ $\neg\Delta_{1}$ $\Pi_{1}$ $A\vee_{c}B$ $\Gamma_{2}$
$\neg\Delta_{2}$ $\Pi_{2}$ $\neg A$ $\Gamma_{3}$ $\neg\Delta_{3}$ $\Pi_{3}$
$\neg B$ $\vee_{c}$-elim $\bot$

By the inductive hypothesis:
$\Gamma_{1},\vdash_{\mathcal{LE}_{p}}\Delta_{1};A\vee_{c}B$,
$\Gamma_{2},\vdash_{\mathcal{LE}_{p}}\Delta_{2};\neg A$ and
$\Gamma_{3}\vdash_{\mathcal{LE}_{p}}\Delta_{3};\neg B$. We can then construct
our desired derivation as:

$\Gamma_{1}$ $\Pi_{1}^{\prime}$ $\Delta_{1};A\vee_{c}B$ $\Gamma_{2}$
$\Pi_{2}^{\prime}$ $\Delta_{2};\neg A$ $[\cdot;A]$ $\neg$-int
$\Delta_{2};\cdot$ $\Gamma_{3}$ $\Pi_{3}^{\prime}$ $\Delta_{3};\neg B$
$[\cdot;B]$ $\neg$-int $\Delta_{2};\cdot$ $\vee_{c}$-elim
$\Delta_{1},\Delta_{2},\Delta_{3};\cdot$

  * •

Case $\rightarrow_{c}$-int. Suppose that
$\Gamma\vdash_{\mathcal{LE}_{p}}\Delta;A\rightarrow_{c}B$ with a derivation
as:

$\Gamma$ $[\cdot;A]$ $\Pi$ $\Delta,B;\cdot$ $\to_{c}$-int $\Delta;A\to_{c}B$

By the inductive hypothesis, we have $\Gamma,A,\neg
B,\neg\Delta\vdash_{\mathcal{NE}_{p}}\bot$. We can then construct our desired
derivation in $\mathcal{NE}_{p}$ as:

$\Gamma$ $[A]$ $[\neg B]$ $\neg\Delta$ $\Pi^{\prime}$ $\bot$
$\rightarrow_{c}$-int $A\rightarrow_{c}B$

In the other direction, suppose that
$\Gamma,\neg\Delta\vdash_{\mathcal{NE}_{p}}A\rightarrow_{c}B$ with a
derivation as:

$\Gamma$ $\neg\Delta$ $[A]$ $[\neg B]$ $\Pi$ $\bot$ $\rightarrow_{c}$-int
$A\rightarrow_{c}B$

By the inductive hypothesis, we have
$\Gamma\cup\\{\cdot;A\\}\vdash_{\mathcal{LE}_{p}}\Delta,B;\cdot$. Thus, we can
obtain the desired derivation in $\mathcal{LE}_{p}$ as:

$\Gamma$ $[\cdot;A]$ $\Pi^{\prime}$ $\Delta,B;\cdot$ $\vee_{c}$-elim
$\Delta;A\rightarrow_{c}B$

  * •

Case $\rightarrow_{c}$-elim. Suppose that
$\Gamma_{1},\Gamma_{2},\Gamma_{3}\vdash_{\mathcal{LE}_{p}}\Delta_{1},\Delta_{2},\Delta_{3};\cdot$
with a derivation as:

$\Gamma_{1}$ $\Pi_{1}$ $\Delta_{1};A\to_{c}B$ $\Gamma_{2}$ $\Pi_{2}$
$\Delta_{2};A$ $\Gamma_{3}$ $[\cdot;B]$ $\Pi_{3}$ $\Delta_{3};\cdot$
$\to_{c}$-elim $\Delta_{1},\Delta_{2},\Delta_{3};\cdot$

By inductive hypothesis, we have
$\Gamma_{1},\neg\Delta_{1}\vdash_{\mathcal{NE}_{p}}A\to_{c}B$,
$\Gamma_{2},\neg\Delta_{2}\vdash_{\mathcal{NE}_{p}}A$ and
$\Gamma_{3},\neg\Delta_{3},B\vdash_{\mathcal{NE}_{p}}\bot$. Then, we can
obtain the desired derivation in $\mathcal{NE}_{p}$ as:

$\Gamma_{1}$ $\neg\Delta_{1}$ $\Pi_{1}^{\prime}$ $A\to_{c}B$ $\Gamma_{2}$
$\neg\Delta_{2}$ $\Pi_{2}^{\prime}$ $A$ $\Gamma_{3}$ $\neg\Delta_{3}\quad[B]$
$\Pi_{3}^{\prime}$ $\bot$ $\neg$-int $\neg B$ $\to_{c}$-elim $\bot$

In the other direction, suppose that
$\Gamma_{1},\Gamma_{2},\Gamma_{3},\neg\Delta_{1},\neg\Delta_{2},\neg\Delta_{3}\vdash_{\mathcal{NE}_{p}}\bot$
with a derivation as:

$\Gamma_{1}$ $\neg\Delta_{1}$ $\Pi_{1}$ $A\rightarrow_{c}B$ $\Gamma_{2}$
$\neg\Delta_{2}$ $\Pi_{2}$ $A$ $\Gamma_{3}$ $\neg\Delta_{3}$ $\Pi_{3}$ $\neg
B$ $\rightarrow_{c}$-elim $\bot$

By the inductive hypothesis, we have that
$\Gamma_{1}\vdash_{\mathcal{LE}_{p}}\Delta_{1};A\rightarrow_{c}B$,
$\Gamma_{2}\vdash_{\mathcal{LE}_{p}}\Delta_{2};A$ and
$\Gamma_{3}\vdash_{\mathcal{LE}_{p}}\Delta_{3};\neg B$. We can then obtain the
desired derivation in $\mathcal{LE}_{p}$ as:

$\Gamma_{1}$ $\Pi_{1}^{\prime}$ $\Delta_{1};A\rightarrow_{c}B$ $\Gamma_{2}$
$\Pi_{2}^{\prime}$ $\Delta_{2};A$ $\Gamma_{3}$ $\Pi_{3}^{\prime}$
$\Delta_{3};\neg B$ $[\cdot;B]$ $\neg$-int $\Delta_{2};\cdot$ $\vee_{c}$-elim
$\Delta_{1},\Delta_{2},\Delta_{3};\cdot$

  * •

Case der. Consider the derivation

$\Gamma$ $\Pi$ $\Delta;A$ der $\Delta,A;\cdot$

By the inductive hypothesis, we have
$\Gamma,\neg\Delta\vdash_{\mathcal{NE}_{p}}A$. We can then obtain the desired
derivation in $\mathcal{NE}_{p}$ as:

$\Gamma$ $\neg\Delta$ $\Pi^{\prime}$ $A$ $[\neg A]$ $\neg$-int $\bot$

The cases of the other structural rules are trivial.

##  7 Normalization

We will now describe how normalization works in the natural deduction with
stoup setting. The idea follows the usual one for natural deduction systems:
show how to compose derivations, so to eliminate detours. The presence of
stoups, however, adds an extra case analysis, since the composition may occur
in the stoup or in the classical context. Both processes will be carefully
described in what follows.

###  7.1 Composition

Before we define reductions and prove the normalization theorem for
$\mathcal{LE}_{p}$, we must guarantee that the process of composition of
derivations is preserved in $\mathcal{LE}_{p}$. As quickly mentioned in Sec.
3, sequent systems with stoup usually allow for two types of cut: a cut where
the left cut-formula is in the stoup and a cut where the left cut-formula is
in the classical region. These two types of cut will correspond to two modes
of composition: a composition that occurs in the stoup and a composition that
occurs in the classical context. We will detail these two forms of
compositions below.

  1. 1.

Composition in the stoup.

###### Theorem 7.1

Let $\Pi_{1}$ be a derivation of
$\Gamma_{1}\vdash_{\mathcal{LE}_{p}}\Delta_{1};A$ and $\Pi_{2}$ be a
derivation of
$\Gamma_{2}\cup\\{\cdot;A\\}\vdash_{\mathcal{LE}_{p}}\Delta_{2};B$. Then, the
result of replacing the assumption $\cdot;A$ in $\Pi_{2}$ by the derivation
$\Pi_{1}$ is a derivation $\Pi$ of
$\Gamma_{1},\Gamma_{2}\vdash_{\mathcal{LE}_{p}}\Delta_{1},\Delta_{2};B$.

###### Proof

By induction on the length of $\Pi_{2}$. We will examine two cases, the other
cases being treated in a similar way.

    1. (a)

The last rule applied in $\Pi_{2}$ is $\vee_{c}$-elim:

$\Gamma_{2}^{1}$ $\cdot;A$ $\Pi_{2}^{1}$ $\Delta_{2}^{1};C\vee_{c}D$
$[\cdot;C]$ $\cdot;A$ $\Gamma_{2}^{2}$ $\Pi_{2}^{2}$ $\Delta_{2}^{2};\cdot$
$[\cdot;D]$ $\cdot;A$ $\Gamma_{2}^{3}$ $\Pi_{2}^{3}$ $\Delta_{2}^{3};\cdot$
$\vee_{c}$-elim $\Delta_{2};\cdot$

where $\Delta_{2}^{i}$ indicates a partition of $\Delta_{2}$, the same with
$\Gamma_{2}$. By the induction hypothesis we obtain the following derivations:

$\Gamma_{1}$ $\Gamma_{2}^{1}$ $\Pi_{1}^{*}$
$\Delta_{1},\Delta_{2}^{1};(C\vee_{c}D)$

and

$\Gamma_{1}$ $[\cdot;C]$ $\Gamma_{2}^{2}$ $\Pi_{2}^{*}$
$\Delta_{1},\Delta_{2}^{2};\cdot$

and

$\Gamma_{1}$ $[\cdot;D]$ $\Gamma_{2}^{3}$ $\Pi_{3}^{*}$
$\Delta_{1},\Delta_{2}^{3};\cdot$

The resulting derivation $\Pi$ is:

$\Gamma_{1}$ $\Gamma_{2}^{1}$ $\Pi_{1}^{*}$
$\Delta_{1},\Delta_{2}^{1};(C\vee_{c}D)$ $\Gamma_{1}$ $[\cdot;C]$
$\Gamma_{2}^{2}$ $\Pi_{2}^{*}$ $\Delta_{1},\Delta_{2}^{2};\cdot$ $\Gamma_{1}$
$[\cdot;D]$ $\Gamma_{2}^{3}$ $\Pi_{3}^{*}$ $\Delta_{1},\Delta_{2}^{3};\cdot$
$\vee_{c}$-elim $\Delta_{1},\Delta_{1},\Delta_{1},\Delta_{2};\cdot$ $C_{c}$
$\Delta_{1},\Delta_{2};\cdot$

Where the double line indicates several applications of $C_{c}$.

    2. (b)

The last rule applied in $\Pi_{2}$ is dereliction:

$\Gamma_{2}$ $\cdot;A$ $\Pi_{2}$ $\Delta_{2};B$ der $\Delta_{2},B;\cdot$

By the induction hypothesis we obtain the following derivation:

$\Gamma_{1}$ $\Gamma_{2}$ $\Pi^{*}$ $\Delta_{1},\Delta_{2};B$

The resulting derivation $\Pi$ is then:

$\Gamma_{1}$ $\Gamma_{2}$ $\Pi^{*}$ $\Delta_{1},\Delta_{2};B$ der
$\Delta_{1},\Delta_{2},B;\cdot$

  2. 2.

Composition in the context.

###### Theorem 7.2

Let $\Pi_{1}$ be a derivation of
$\Gamma_{1}\vdash_{\mathcal{LE}_{p}}\Delta_{1};C$, where $A\in\Delta_{1}$, and
$\Pi_{2}$ be a derivation of
$\Gamma_{2}\cup\\{\cdot;A\\}\vdash_{\mathcal{LE}_{p}}\Delta_{2};B$. Then, the
result of replacing the assumption $\cdot;A$ in $\Pi_{2}$ by the derivation
$\Pi_{1}$ is a derivation $\Pi$ of
$\Gamma_{1},\Gamma_{2}\vdash_{\mathcal{LE}_{p}}\Delta_{1}^{*},\Delta_{2},B;C$,
where $\Delta_{1}^{*}$ is obtained from $\Delta_{1}$ by means of the
elimination of the occurrences of $A$.

###### Proof

The proof is by straightforward induction on the length of $\Pi_{1}$. The only
exception is dereliction, which uses Theorem 7.1.

Let the last rule applied in $\Pi_{1}$ be dereliction:

$\Gamma_{1}$ $\Pi_{1}$ $\Delta_{1};A$ der $\Delta_{1},A;\cdot$

By the induction hypothesis we can obtain a derivation $\Pi^{\prime}$ of
$\Gamma_{1},\Gamma_{2}\vdash_{\mathcal{LE}_{p}}\Delta_{1}^{*},\Delta_{2},B;A$.
By Theorem 2 we can obtain a derivation $\Pi^{\prime\prime}$ of
$\Gamma_{1},\Gamma_{2}\vdash_{\mathcal{LE}_{p}}\Delta_{1}^{*},\Delta_{2},\Delta_{2},B;B$.
We can now take the derivation $\Pi$ to be:

$\Gamma_{1}$ $\Gamma_{2}$ $\Pi^{\prime\prime}$
$\Delta_{1}^{*},\Delta_{2},\Delta_{2},B;B$ $der$
$\Delta_{1}^{*},\Delta_{2},\Delta_{2},B,B;\cdot$ $C_{c}$
$\Delta_{1}^{*},\Delta_{2},B;\cdot$

In what follows, we shall use the following notation to indicate composition
in the stoup and composition in the classical context.

  * •

Composition in the stoup:

$\Gamma_{1}$ $\Pi_{1}$ $\Delta_{1};[\frac{A}{\cdot;A}]$ $\Gamma_{2}$ $\Pi_{2}$
$\Delta_{1},\Delta_{2};B$

  * •

Composition in the classical context:

$\Gamma_{1}$ $\Pi_{1}$ $\Delta_{1},[\frac{A}{\cdot;A}];B$ $\Gamma_{2}$
$\Pi_{2}$ $\Delta_{1},\Delta_{2};B$

  * •

A more concise notation for composition in general:
$\Pi_{1}/[\frac{A}{\cdot;A}]/\Pi_{2}$.

###  7.2 Reductions

Derivations in $\mathcal{LE}_{p}$ may contain detours. These detours are of
two types: we may introduce a formula by an application of an introduction
rule to immediately use it as major premiss of an application of an
elimination rule; or we may introduce a formula by an application of an
introduction rule and use it as major premiss of an application of an
elimination rule after several applications of $\vee_{i}$-elim. The reductions
defined in this section are intended, as usual, to eliminate detours that may
occur in a derivation.

###### Definition 2

A segment in a derivation $\Pi$ is a sequence $A_{1},...,A_{n}$ of consecutive
formulas in a thread in $\Pi$ such that:

  * •

$A_{1}$ is not in the stoup of the consequence of an application of
$\vee_{i}$-elim or of an application of $C_{c}$;

  * •

$A_{j}$, for $j<n$, is in the stoup of the minor premiss of an application of
$\vee_{i}$-elim or of an application of $C_{c}$; and

  * •

$A_{n}$ is not in the stoup of the minor premiss of an application of
$\vee_{i}$-elim or of an application of $C_{c}$.

We note the presence of contraction in the last definition. The idea is that
contractions move down on reductions, just like in a sequent calculus’ cut-
elimination process.

###### Definition 3

A segment that begins with with the consequence of an application of an
introduction rule or $W_{i}$ and ends with an application of an elimination
rule is called a maximal segment. A maximal segment of length $1$ is called a
maximum formula.

###### Definition 4

Let $\Pi$ be a derivation in $\mathcal{LE}_{p}$. The degree of $\Pi$,
$d[\Pi]$, is defined as $\max\\{d[A]:$ A is the end-formula of maximal segment
in $\Pi\\}$, where $d[A]$ is the weight of the formula $A$, defined
inductively by

$\begin{array}[]{lcl}d[\bot]=d[p]&=&0\quad p\mbox{ atomic.}\\\ d[A\circ
B]&=&d[A]+d[B]+1\mbox{ for }\circ\in\\{\to_{i,c},\vee_{i,c},\wedge\\}\\\
d[\neg A]&=&d[A]+1.\end{array}$

###### Definition 5

A derivation $\Pi$ is called normal if and only if $d[\Pi]=0$.

We will present next all the reduction steps in $\mathcal{LE}_{p}$ that will
be used in the elimination of maximal segments.

  1. 1.

$\wedge$-reduction:

The derivation

$\Gamma_{1}$ $\Delta_{1};A_{1}$ $\Gamma_{2}$ $\Delta_{2};A_{2}$ $\wedge$-int
$\Delta_{1},\Delta_{2};(A_{1}\wedge A_{2})$ $\wedge_{j}$-elim
$\Delta_{1},\Delta_{2};A_{j}$

Reduces to

$\Gamma_{j}$ $\Delta_{j};A_{j}$ $W_{c}$ $\Delta_{1},\Delta_{2};A_{j}$

  2. 2.

$\to_{i}$-reduction:

The derivation

$\Gamma_{1}$ $\Pi_{1}$ $\Delta_{1};A$ $[\cdot;A]$ $\Gamma_{2}$ $\Pi_{2}$
$\Delta_{2};B$ $\rightarrow_{i}$-int $\Delta_{2};(A\to_{i}B)$
$\rightarrow_{i}$-elim $\Delta_{1},\Delta_{2};B$

Reduces to:

$\Gamma_{1}$ $\Pi_{1}$ $\Delta_{1};[\frac{A}{\cdot;A}]$ $\Gamma_{2}$ $\Pi_{2}$
$\Delta_{1},\Delta_{2};B$

Observe that the case for negation is analogous.

  3. 3.

$\vee_{i}$-reduction:

The derivation

$\Gamma_{1}$ $\Pi_{1}$ $\Delta_{1};A_{j}$ $\vee_{i}$-int
$\Delta_{1};(A_{1}\vee_{i}A_{2})$ $\Gamma_{2}$ $[\cdot;A_{1}]$ $\Pi_{2}$
$\Delta_{2};B$ $\Gamma_{3}$ $[\cdot;A_{2}]$ $\Pi_{3}$ $\Delta_{3};B$
$\vee_{i}$-elim $\Delta_{1},\Delta_{2},\Delta_{3};B$

Reduces to:

$\Gamma_{1}$ $\Pi_{1}$ $\Delta_{1};[\frac{A_{j}}{\cdot;A_{j}}]$ $\Gamma_{j}$
$\Pi_{j}$ $\Delta_{1},\Delta_{j};B$ $W_{c}$
$\Delta_{1},\Delta_{2},\Delta_{3};B$

  4. 4.

$\to_{c}$-reduction:

The derivation

$[\cdot;A]$ $\Gamma_{1}$ $\Pi_{1}$ $\Delta_{2},B;\cdot$ $\rightarrow_{c}$-int
$\Delta_{2};(A\to_{c}B)$ $\Gamma_{2}$ $\Pi_{2}$ $\Delta_{2};A$ $[\cdot;B]$
$\Gamma_{3}$ $\Pi_{3}$ $\Delta_{3};\cdot$ $\to_{c}$-elim
$\Delta_{1},\Delta_{2},\Delta_{3};\cdot$

Reduces to:

$\Gamma_{2}$ $\Pi_{2}$ $\Delta_{2};[\frac{A}{\cdot;A}]$ $\Gamma_{1}$ $\Pi_{1}$
$\Delta_{1},\Delta_{2},[\frac{B}{\cdot;B}];\cdot$ $\Gamma_{3}$ $\Pi_{3}$
$\Delta_{1},\Delta_{2}^{*},\Delta_{3};\cdot$ $W_{c}$
$\Delta_{1},\Delta_{2},\Delta_{3};\cdot$

  5. 5.

$\vee_{c}$-reduction:

The derivation

$\Gamma_{1}$ $\Pi_{1}$ $\Delta_{1},A,B;\cdot$ $\vee_{c}$-int
$\Delta_{1};(A\vee_{c}B)$ $\Gamma_{2}$ $[\cdot;A]$ $\Pi_{2}$
$\Delta_{2};\cdot$ $\Gamma_{3}$ $[\cdot;B]$ $\Pi_{3}$ $\Delta_{3};\cdot$
$\vee_{c}$-elim $\Delta_{1},\Delta_{2},\Delta_{3};\cdot$

Reduces to:

$\Gamma_{1}$ $\Pi_{1}$ $\Delta_{1},[\frac{A}{\cdot;A}],B;\cdot$ $\Gamma_{2}$
$\Pi_{2}$ $\Delta_{1}^{*},\Delta_{2},[\frac{B}{\cdot;B}];\cdot$ $\Gamma_{3}$
$\Pi_{3}$ $\Delta_{1}^{*},\Delta_{2}^{*},\Delta_{3};\cdot$ $W_{c}$
$\Delta_{1},\Delta_{2},\Delta_{3};\cdot$

  6. 6.

Permutative reductions:

    1. (a)

The derivation

$\Gamma_{1}$ $\Pi_{1}$ $\Delta_{1};(A\vee_{i}B)$ $[\cdot;A]$ $\Gamma_{2}$
$\Pi_{2}$ $\Delta_{2};C$ $[\cdot;B]$ $\Gamma_{3}$ $\Pi_{3}$ $\Delta_{3};C$
$\Delta_{1},\Delta_{2},\Delta_{3};C$ $\Sigma_{1}$ $\Theta_{1};\Lambda_{1}$
$\ldots$ $\Sigma_{m}$ $\Theta_{m};\Lambda_{m}$
$\Delta_{1},\Delta_{2},\Delta_{3},\Theta_{1},\ldots,\Theta_{m};\Lambda$

where $C$ is the major premiss of an elimination rule with minor premisses
$\Theta_{1};\Lambda_{1}\ldots\Theta_{m};\Lambda_{m}$ (if any), reduces to

$\Delta_{1},\Delta_{2},\Delta_{3},\Theta_{1},\ldots,\Theta_{m};\Lambda\Delta_{1},\Delta_{2},\Delta_{3},\Theta_{1},\ldots,\Theta_{m},\Theta_{1},\ldots,\Theta_{m};\Lambda\lx@proof@logical@and\Delta_{1};A\vee_{i}B\vspace{0.1cm}\Pi_{1}\vspace{0.1cm}\Gamma_{1}\Delta_{2},\Theta_{1},\ldots,\Theta_{m};\Lambda\lx@proof@logical@and\Delta_{2};C\vspace{0.1cm}\Pi_{2}\lx@proof@logical@and\vspace{0.1cm}[\cdot;A]\vspace{0.1cm}\Gamma_{2}\Theta_{1};\Lambda_{1}\vspace{0.1cm}\Sigma_{1}\ldots\Theta_{m};\Lambda_{m}\vspace{0.1cm}\Sigma_{m}\Delta_{3},\Theta_{1},\ldots,\Theta_{m};\Lambda\lx@proof@logical@and\Delta_{3};C\vspace{0.1cm}\Pi_{3}\lx@proof@logical@and\vspace{0.1cm}[\cdot;B]\vspace{0.1cm}\Gamma_{3}\Theta_{1};\Lambda_{1}\vspace{0.1cm}\Sigma_{1}\ldots\Theta_{m};\Lambda_{m}\vspace{0.1cm}\Sigma_{m}$

    2. (b)

The derivation

$\Gamma_{1}$ $\Pi_{1}$ $\Delta_{1},A,A;C$ $C_{c}$ $\Delta_{1},A;C$
$\Sigma_{1}$ $\Theta_{1};\Lambda_{1}$ $\ldots$ $\Sigma_{m}$
$\Theta_{m};\Lambda_{m}$
$\Delta_{1},\Delta_{2},\Delta_{3},\Theta_{1},\ldots,\Theta_{m};\Lambda$

where $C$ is the major premiss of an elimination rule with minor premisses
$\Theta_{1};\Lambda_{1}\ldots\Theta_{m};\Lambda_{m}$ (if any), reduces to

$\Gamma_{1}$ $\Pi_{1}$ $\Delta,A,A:C$ $\Sigma_{1}$ $\Theta_{1};\Lambda_{1}$
$\ldots$ $\Sigma_{m}$ $\Theta_{m};\Lambda_{m}$
$\Delta,A,A,\Theta_{1},\ldots,\Theta_{m};\Lambda$ $C_{c}$
$\Delta,A,\Theta_{1},\ldots,\Theta_{m},A;\Lambda$

###  7.3 Normalization

We shall use Pottinger’s critical derivation strategy [Pot76] to prove the
normalization theorem for $\mathcal{LE}_{p}$. But before the proof of
normalization, we need some definitions and preparatory lemmas that relate
reductions and composition to the degree of derivations. The proof of the next
lemma is obvious.

###### Lemma 1

Let $\Pi$ be $\Pi_{1}/[\frac{A}{\cdot;A}]/\Pi_{2}$, the composition of
derivations $\Pi_{1}$ with $\Pi_{2}$ at junction point $A$. Then,
$d[\Pi]=max\\{d[\Pi_{1}],d[\Pi_{2}],d[A]\\}$

###### Lemma 2

If $\Pi$ reduces to $\Pi^{\prime}$, then $d[\Pi]\leq d[\Pi^{\prime}]$.

###### Proof

Directly from the form of the reductions and Lemma 1.

###### Definition 6

A derivation $\Pi$ is critical iff:

  * •

$\Pi$ ends with an elimination rule $\alpha$;

  * •

The major premiss $A$ of $\alpha$ is the end of maximal segment;

  * •

$d[\Pi]$ = $d[A]$; and

  * •

For every proper subderivation $\Pi^{\prime}$ of $\Pi$, $d[\Pi^{\prime}]$ $<$
$d[\Pi]$.

###### Lemma 3

(Critical Lemma): Let $\Pi$ be a critical derivation of
$\Gamma\vdash_{\mathcal{LE}_{p}}\Delta;\Sigma$ in $\mathcal{LE}_{p}$. Then,
$\Pi$ reduces to a derivation $\Pi^{\prime}$ of
$\Gamma^{\prime}\vdash_{\mathcal{LE}_{p}}\Delta;\Sigma$ with
$\Gamma^{\prime}\subseteq\Gamma$, such that $d[\Pi^{\prime}]$ $<$ $d[\Pi]$.

###### Proof

By induction on the length of $\Pi$.

  * •

Case 1: The major premiss of the last rule applied in $\Pi$ is a maximum
formula. The result follows directly from the form of the reductions and Lemma
2.

  * •

Case 2: The major premiss of the last rule applied in $\Pi$ is the end formula
of maximum segment of length $>$1\. There are two sub-cases to be examined:

    1. 1.

$\Pi$ is:

$\Gamma_{1}$ $\Pi_{1}$ $\Delta_{1};(A\vee_{i}B)$ $[\cdot;A]$ $\Gamma_{2}$
$\Pi_{2}$ $\Delta_{2};C$ $[\cdot;B]$ $\Gamma_{3}$ $\Pi_{3}$ $\Delta_{3};C$
$\Delta_{1},\Delta_{2},\Delta_{3};C$ $\Sigma_{1}$ $\Theta_{1};\Lambda_{1}$
$\ldots$ $\Sigma_{m}$ $\Theta_{m};\Lambda_{m}$
$\Delta_{1},\Delta_{2},\Delta_{3},\Theta_{1},\ldots,\Theta_{m};\Lambda$

By a permutative reduction, $\Pi$ reduces to the following derivation
$\Pi^{*}$:

$\Delta_{1},\Delta_{2},\Delta_{3},\Theta_{1},\ldots,\Theta_{m};\Lambda\Delta_{1},\Delta_{2},\Delta_{3},\Theta_{1},\ldots,\Theta_{m},\Theta_{1},\ldots,\Theta_{m};\Lambda\lx@proof@logical@and\Delta_{1};A\vee_{i}B\vspace{0.1cm}\Pi_{1}\vspace{0.1cm}\Gamma_{1}\Delta_{2},\Theta_{1},\ldots,\Theta_{m};\Lambda\lx@proof@logical@and\Delta_{2};C\vspace{0.1cm}\Pi_{2}\lx@proof@logical@and\vspace{0.1cm}[\cdot;A]\vspace{0.1cm}\Gamma_{2}\Theta_{1};\Lambda_{1}\vspace{0.1cm}\Sigma_{1}\ldots\Theta_{m};\Lambda_{m}\vspace{0.1cm}\Sigma_{m}\Delta_{3},\Theta_{1},\ldots,\Theta_{m};\Lambda\lx@proof@logical@and\Delta_{3};C\vspace{0.1cm}\Pi_{3}\lx@proof@logical@and\vspace{0.1cm}[\cdot;B]\vspace{0.1cm}\Gamma_{3}\Theta_{1};\Lambda_{1}\vspace{0.1cm}\Sigma_{1}\ldots\Theta_{m};\Lambda_{m}\vspace{0.1cm}\Sigma_{m}$

By Lemma 2, $d[\Pi^{*}]\leq d[\Pi]$. If $d[\Pi^{*}]<d[\Pi]$, then we take
$\Pi^{\prime}=\Pi^{*}$. If $d[\Pi^{*}]=d[\Pi]$, then at least one of the
derivations of the minor premisses has degree = $d[\Pi]$. For the sake of the
argument, let’s assume that both have degree = $d[\Pi]$. By the induction
hypothesis, the derivation

$[\cdot;A]$ $\Gamma_{2}$ $\Pi_{2}$ $\Delta_{2};C$ $\Sigma_{1}$
$\Theta_{1};\Lambda_{1}$ $\ldots$ $\Sigma_{m}$ $\Theta_{m};\Lambda_{m}$
$\Delta_{2},\Theta_{1},\ldots,\Theta_{m};\Lambda$

reduces to a derivation $\Pi_{2}^{\prime}$ of
$\Delta_{2},\Theta_{1},\ldots,\Theta_{m};\Lambda$ such that
$d[\Pi_{2}^{\prime}]$ $<$ $d[\Pi_{2}]$, and the derivation

$[\cdot;B]$ $\Gamma_{3}$ $\Pi_{3}$ $\Delta_{3};C$ $\Sigma_{1}$
$\Theta_{1};\Lambda_{1}$ $\ldots$ $\Sigma_{m}$ $\Theta_{m};\Lambda_{m}$
$\Delta_{3},\Theta_{1},\ldots,\Theta_{m};\Lambda$

Reduces to a derivation $\Pi_{3}^{\prime}$ of
$\Delta_{3},\Theta_{1},\ldots,\Theta_{m};\Lambda$ such that
$d[\Pi_{3}^{\prime}]$ $<$ $d[\Pi_{3}]$.

Let $\Pi^{\prime}$ be:

$\Gamma_{1}$ $\Pi_{1}$ $\Delta_{1};(A\vee_{i}B)$ $\Pi_{2}^{\prime}$
$\Delta_{2},\Theta_{1},\ldots,\Theta_{m};\Lambda$ $\Pi_{3}^{\prime}$
$\Delta_{3},\Theta_{1},\ldots,\Theta_{m};\Lambda$
$\Delta_{1},\Delta_{2},\Delta_{3},\Theta_{1},\ldots,\Theta_{m};\Lambda$

We can easily see that $\Pi$ reduces to $\Pi^{\prime}$ and that
$d[\Pi^{\prime}]$ $<$ $d[\Pi]$.

    2. 2.

$\Pi$ is

$\Pi_{1}$ $\Delta_{1},A,A:C$ $C_{c}$ $\Delta_{1},A:C$ $\Sigma_{1}$
$\Theta_{1};\Lambda_{1}$ $\ldots$ $\Sigma_{m}$ $\Theta_{m};\Lambda_{m}$
$\Delta_{1},\Delta_{2},\Delta_{3},\Theta_{1},\ldots,\Theta_{m};\Lambda$

By a permutative reduction, $\Pi$ reduces to the following derivation
$\Pi^{*}$:

$\Pi_{1}$ $\Delta,A,A:C$ $\Sigma_{1}$ $\Theta_{1};\Lambda_{1}$ $\ldots$
$\Sigma_{m}$ $\Theta_{m};\Lambda_{m}$
$\Delta,A,A,\Theta_{1},\ldots,\Theta_{m};\Lambda$ $C_{c}$
$\Delta,A,\Theta_{1},\ldots,\Theta_{m},A;\Lambda$

As in the previous case, by Lemma 2, $d[\Pi^{*}]\leq d[\Pi]$. If
$d[\Pi^{*}]<d[\Pi]$, then we take $\Pi^{\prime}=\Pi^{*}$. If
$d[\Pi^{*}]=d[\Pi]$, then by the induction hypothesis, the derivation

$\Pi_{1}$ $\Delta,A,A:C$ $\Sigma_{1}$ $\Theta_{1};\Lambda_{1}$ $\ldots$
$\Sigma_{m}$ $\Theta_{m};\Lambda_{m}$
$\Delta,A,A,\Theta_{1},\ldots,\Theta_{m};\Lambda$

reduces to a derivation $\Pi^{**}$ of
$\Gamma^{*}\subseteq\Gamma\vdash_{\mathcal{LE}_{p}}\Delta,A,A,\Theta_{1},\ldots,\Theta_{m};\Lambda$
such that $d[\Pi^{**}]<d[\Pi]$. We can then take the desired derivation
$\Pi^{\prime}$ as

$\Pi^{**}$ $\Delta,A,A,\Theta_{1},\ldots,\Theta_{m};\Lambda$
$\Delta,A,\Theta_{1},\ldots,\Theta_{m};\Lambda$

###### Lemma 4

Let $\Pi$ be a derivation of $\Gamma\vdash_{\mathcal{LE}_{p}}\Delta;\Sigma$
with $d[\Pi]>0$. Then, $\Pi$ reduces to a derivation $\Pi^{\prime}$ of
$\Gamma^{\prime}\vdash_{\mathcal{LE}_{p}}\Delta;\Sigma$ with
$\Gamma^{\prime}\subseteq\Gamma$, such that $d[\Pi^{\prime}]$ $<$ $d[\Pi]$.

###### Proof

By induction on the length of $\Pi$.

  * •

Case 1: $\Pi$ ends with an application of an introduction rule.
This case follows directly from the induction hypothesis.

  * •

Case 2: $\Pi$ ends with an application of an elimination rule. The general
form of $\Pi$ is:

$\Pi_{1}$ $\Pi_{2}$ $\Pi_{3}$ $\Delta;\Lambda$

By the induction hypothesis, $\Pi_{k}$ reduces to a derivation
$\Pi_{k}^{\prime}$ such that $d[\Pi_{k}^{\prime}]$ $<$ $d[\Pi_{k}]$ ($1\leq
k\leq 3$).
Let $\Pi^{*}$ be:

$\Pi_{1}^{\prime}$ $\Pi_{2}^{\prime}$ $\Pi_{3}^{\prime}$ $\Delta;\Lambda$

By Lemma 2, $d[\Pi^{*}]$ $\leq$ $d[\Pi]$. If $d[\Pi^{*}]$ $<$ $d[\Pi]$, we
take $\Pi^{*}=\Pi^{\prime}$. If $d[\Pi^{*}]=d[\Pi]$, the $\Pi^{*}$ is a
critical derivation and the result follows from Lemma 3.

###### Theorem 7.3

(Normalization Theorem for $\mathcal{LE}_{p}$) Let $\Pi$ be a derivation of
$\Gamma\vdash_{\mathcal{LE}_{p}}\Delta;\Sigma$ in $\mathcal{LE}_{p}$. Then,
$\Pi$ reduces to a normal derivation $\Pi^{\prime}$ of
$\Gamma^{\prime}\vdash_{\mathcal{LE}_{p}}\Delta;\Sigma$ where
$\Gamma^{\prime}\subseteq\Gamma$.

###### Proof

Directly from Lemma 4 by induction on $d[\Pi]$.

##  8 Concluding remarks and future work

There are lots of things to be done in the domain of ecumenical systems and
more specifically in connection with pure ecumenical systems. We conclude this
paper by mentioning two possible lines of work we are pursuing.

###  8.1 Pure First-order ecumenical systems

We can easily show that, in Prawitz’ ecumenical system, if the main operator
of a formula $A$ is classical, if $\Gamma,\neg A\vdash\bot$, then
$\Gamma\vdash A$. For example, assume a derivation $\Pi$ as follows:

$\Gamma$ $\neg(B\vee_{c}C)$ $\Pi$ $\bot$

Then, we can construct the following derivation of $\Gamma\vdash(B\vee_{c}C)$:

$\Gamma$ $[(B\vee_{c}C)]^{1}$ $[\neg B]^{2}$ $[\neg C]^{3}$ $\bot$ 1
$[\neg(B\vee_{c}C)]$ $\Pi$ $\bot$ $2,3$ $(B\vee_{c}C)$

The same result holds for the classical existential quantifier. From the
derivation

$\Gamma$ $\neg\exists_{c}xB(x)$ $\Pi$ $\bot$

We can easily obtain the derivation:

$\Gamma$ $[\exists_{c}x(Bx)]^{1}$ $[\forall x\neg B(x)]^{2}$ $\bot$ 1
$[\neg\exists_{c}c(B(x)]$ $\Pi$ $\bot$ 2  $\exists_{c}xB(x)$

From these results it follows that the classical implication $\to_{c}$
satisfies modus ponens for classical succedents:

###### Theorem 8.1

Let the main operator of the formula $B$ be classical. Then we can prove in
Prawitz’ system that $\\{(A\to_{c}B),A\\}\vdash B$.

In the propositional system with the stoup, we can obtain the same results for
the classical propositional operators. For example, given a derivation of

$\cdot;\neg(B\vee_{c}C)$ $\Gamma$ $\Pi$ $\Delta;\cdot$

We can obtain a derivation of

$\Gamma$ $\Pi$ $\Delta;(B\vee_{c}C)$

But in the first-order case, a pure rule for the classical existential
quantifier in the stoup format requires an extra attention. Consider the
following pure rules with stoup for the classical existential quantifier:

$\Delta_{1},A(t);\cdot$ $\Delta;\exists_{c}xA(x)$
$\Delta_{1};\exists_{c}xA(x)$ $\cdot;A(a)$ $\Pi$ $\Delta_{2};\cdot$
$\Delta_{1};\Delta_{2};\cdot$

It is easy to show that the first order system with stoup obtained by means of
the addition of the intuitionistic rules for $\exists_{i}$, $\forall$ and
these rules for $\exists_{c}$ is not complete with respect to Prawitz’ first-
order ecumenical natural deduction. The important relation $\neg\forall x\neg
A(x)\vdash\exists_{c}xA(x)$ between $\forall$ and $\exists_{c}$ is not
derivable in this first-order system with stoup. As a future work, we propose
to investigate the first-order system obtained by the addition of the rules
mentioned above plus a new structural rule, the store rule:

$\Delta,A;\cdot$ store $\Delta;A$

with the side condition that the main operator of $A$ is classical.

###  8.2 A different approach to purity

A different and interesting approach to pure systems worth exploring is based
on some ideas proposed by Julien Murzi in [Mur20]. Murzi proposes a pure
single-conclusion Natural Deduction system that satisfies the basic
inferentialist requirements of harmony and separability. Murzi’s proposal
combines (in a very interesting way!) Peter Schroeder-Heister’s idea of
higher-level rules with Neil Tennant’s idea that the sign $\bot$ for the
absurd should be conceived as a punctuation mark. Using Murzi’s idea we can
formulate a new pure ecumenical natural deduction system for classical and
intuitionistic logic.

(1) The impure rule for $\vee_{c}$-Int becomes

$[\frac{A}{\bot}]^{j}$ $[\frac{B}{\bot}]^{k}$ $\underbrace{}$ $\vdots$ $\bot$
$j,k$ $(A\vee_{c}B)$

(2) $\vee_{c}$-Elim.

$(A\vee_{c}B)$ $[A]^{j}$ $\vdots$ $\bot$ $[B]^{k}$ $\vdots$ $\bot$ $j,k$
$\bot$

(3) The impure rule for $\to_{c}$-Int becomes

$[A]^{j}$ $[\frac{B}{\bot}]^{k}$ $\underbrace{}$ $\vdots$ $\bot$ $j,k$
$(A\to_{c}B)$

(4) $\to_{c}$-Elim.

$(A\to_{c}B)$ $A$ $[B]^{k}$ $\vdots$ $\bot$ $k$ $\bot$

It is easy to show that the impure rules can be obtained from the new pure
rules. In the case of $\vee_{c}$, for example, given a derivation $\Pi$ of
$\bot$ from $\neg A$ and $\neg B$, we can construct the following derivation:

$[\frac{A}{\bot}]^{j}$ $[\neg A]$ $[\frac{B}{\bot}]^{k}$ $[\neg B]$ $\Pi$
$\bot$ $j,k$ $(A\vee_{c}B)$

In order to prove the other direction, it is convenient to add a new general
rule that allows us to conclude rules. In the formulation of the rule we will
use (as Murzi does) the expression $\Delta/A$ as an alternative to the rule
$\frac{\Delta}{A}$.

$[A]^{j}$ $\Pi$ $B$ $j$ $(A/B)$

Suppose now that we have a derivation

$\frac{A}{\bot}$ $\frac{B}{\bot}$ $\Pi$ $\bot$

We can then construct the following derivation:

$[A]^{1}$ $[\neg A]^{3}$ $\bot$ 1  $[(A/\bot)]$ $[B]^{2}$ $[\neg B]^{4}$
$\bot$ 2  $[(B/\bot)]$ $\Pi$ $\bot$ $3,4$ $(A\vee_{c}B)$

An example: Peirce’s law:

$((A\to_{c}B)\to_{c}A)^{2}$ $[A]^{1}$ $[\frac{A}{\bot}]^{3}$ $\bot$ 1
$(A\to_{c}B)$ $[\frac{A}{\bot}]^{3}$ $\bot$ $2,3$
$(((A\to_{c}B)\to_{c}A)\to_{c}A)$

## References

  * [DAg05] Marcello D’Agostino.  Classical Natural Deduction.  In Sergei N. Artëmov, Howard Barringer, Artur S. d’Avila Garcez, Luís C. Lamb and John Woods. We Will Show Them! Essays in Honour of Dov Gabbay, Volume One, pages 429–468, College Publications, 2005.
  * [And92] Jean-Marc Andreoli.  Logic programming with focusing proofs in linear logic.  J. Log. Comput., 2(3):297–347, 1992.
  * [CDD21] Alejandro Díaz-Caro and Gilles Dowek.  A new connective in natural deduction, and its application to quantum computing.  In A. Cerone and P. C. Ölveczky, editors, Theoretical Aspects of Computing - ICTAC 2021 - 18th International Colloquium, Virtual Event, Nur-Sultan, Kazakhstan, September 8-10, 2021, Proceedings, volume 12819 of Lecture Notes in Computer Science, pages 175–193. Springer, 2021\.
  * [Gen69] Gerhard Gentzen.  The Collected Papers of Gerhard Gentzen.  Amsterdam: North-Holland Pub. Co., 1969.
  * [GG05] Michael Gabbay and Murdoch Gabbay.  Some formal considerations on Gabbay’s restart rule in natural deduction and goal-directed reasoning.  In Sergei N. Artëmov, Howard Barringer, Artur S. d’Avila Garcez, Luís C. Lamb, and John Woods, editors, We Will Show Them! Essays in Honour of Dov Gabbay, Volume One, pages 701–730. College Publications, 2005.
  * [Gir91] Jean-Yves Girard.  A new constructive logic: Classical logic.  Math. Struct. Comput. Sci., 1(3):255–296, 1991.
  * [Mur20] Julien Murzi.  Classical harmony and separability.  Erkenntnis, 85:391 – 415, 2020.
  * [PR17] Luiz Carlos Pereira and Ricardo Oscar Rodriguez.  Normalization, soundness and completeness for the propositional fragment of Prawitz’ ecumenical system.  Revista Portuguesa de Filosofia, 73(3-3):1153–1168, 2017.
  * [PPdP21] Elaine Pimentel, Luiz Carlos Pereira, and Valeria de Paiva.  An ecumenical notion of entailment.  Synthese, 198(22-S):5391–5413, 2021.
  * [Pot76] Garrel Pottinger  A New Way of Normalizing Intuitionist Propositional Logic.  Studia Logica, volume 35(4):387-408, 1976.
  * [Pra65] Dag Prawitz.  Natural Deduction, volume 3 of Stockholm Studies in Philosophy.  Almqvist and Wiksell, 1965.
  * [Pra15] Dag Prawitz.  Classical versus intuitionistic logic.  In Bruno Lopes Edward Hermann Haeusler, Wagner de Campos Sanz, editor, Why is this a Proof?, Festschrift for Luiz Carlos Pereira, volume 27, pages 15–32. College Publications, 2015.
  * [Res21] Greg Restall.  Speech acts & the quest for a natural account of classical proof.  Available at https://consequently.org/writing/, 2021.
  * [Sch14] Peter Schroeder-Heister.  The calculus of higher-level rules, propositional quantification, and the foundational approach to proof-theoretic harmony.  Studia Logica, 102(6):1185–1216, 2014.


# Comparative Study of Machine Learning Test Case Prioritization for
Continuous Integration Testing

Dusica Marijan  Simula Research Laboratory, Norway<EMAIL_ADDRESS>
###### Abstract

There is a growing body of research indicating the potential of machine
learning to tackle complex software testing challenges. One such challenge
pertains to continuous integration testing, which is highly time-constrained,
and generates a large amount of data coming from iterative code commits and
test runs. In such a setting, we can use plentiful test data for training
machine learning predictors to identify test cases able to speed up the
detection of regression bugs introduced during code integration. However,
different machine learning models can have different fault prediction
performance depending on the context and the parameters of continuous
integration testing, for example variable time budget available for continuous
integration cycles, or the size of test execution history used for learning to
prioritize failing test cases. Existing studies on test case prioritization
rarely study both of these factors, which are essential for the continuous
integration practice. In this study we perform a comprehensive comparison of
the fault prediction performance of machine learning approaches that have
shown the best performance on test case prioritization tasks in the
literature. We evaluate the accuracy of the classifiers in predicting fault-
detecting tests for different values of the continuous integration time budget
and with different length of test history used for training the classifiers.
In evaluation, we use real-world industrial datasets from a continuous
integration practice. The results show that different machine learning models
have different performance for different size of test history used for model
training and for different time budget available for test case execution. Our
results imply that machine learning approaches for test prioritization in
continuous integration testing should be carefully configured to achieve
optimal performance.

###### keywords:

Machine learning, neural networks, support vector regression, gradient
boosting, learning to rank, continuous integration, software testing,
regression testing, test prioritization, test selection, test optimization

††journal: arXiv

##  1 Introduction

Continuous integration (CI) is an agile software development practice where
software is realeased frequently following frequent code changes. Each change
needs to be verified before a new change can be made and a new version of the
code released. This process runs in CI cycles, also called builds or commits.
Software testing is an integral step running iteratively and successively as
part of continuous code integration. Each code integration is followed by an
integration testing iteration, which is typically extensive, to prevent
breaking a build. CI testing requires short turnaround between starting test
execution and detecting faulty regressions, to enable fast feedback. This
entails a short time budget allocated to integration testing, which denotes
the amount of time available for testing the code changes introduced in the
latest commit. Short time budget requires testing in CI to be time-efficient
[1, 2, 3, 4, 5, 6]. As a response to this challenge, researchers have proposed
various test selection, minimization, and prioritization [7, 8, 9, 10, 11, 12,
13] approaches. In this work we specifically focus on Test Prioritization
(TP). TP consists in ordering test cases that are more effective in detecting
faults to execute sooner. In this way, we ensure that the most important test
cases are executed in a short time budget. However, in dynamic CI environments
with frequent code changes, a time budget can vary across different CI cycles.
Therefore, an efficient TP approach needs to adapt to varying time constraints
across CI cycles.

Furthermore, given that testing runs frequently in CI generating a large
volume of test information, researchers have proposed history-based TP
approaches. These approaches use historical test execution information to
speed up the detection of regression faults introduced by developers. [14]
suggests that history-based TP is an effective approach for rapid release
software, while [15] reports that using historical test failure information is
a good indicator for test prioritization. However, history-based TP has its
challenges. One common challenge is to decide how old historical information
to use in TP. On the one hand, using too old history may capture old
(irrelevant) failures which have been fixed and thus are not indicative of new
failures. On the other hand, using too recent history may omit some relevant
failures. To deal with this challenge, [16] introduced the notion of time
windows, to capture how recently tests were executed and failures exposed,
which is further used for test selection in pre-submit and post-submit
testing.

Now we illustrate one example of CI testing, describing daily practices and
challenges of our industrial collaborator in the domain of testing
configurable communication software in CI, shown in Figure 1

Following a standard practice, code changes committed by developers are
regression tested before they can be deployed to production. Several hundreds
of changes made on a daily basis trigger the execution of several thousands of
test cases. Change impact analysis is run to select the test cases impacted by
the change. However, all impacted test cases cannot not fit the available time
budget, and moreover, not all impacted test cases are equally useful in
detecting faults. If test engineers were to manually select a subtest of tests
produced by change impact analysis which they believe have the highest chance
of detecting faults, such a process would be highly time-ineffeicient. Thus,
test engineers have applied automated regression TP, as an established
approach to improve the effectiveness of regression testing in CI.
Specifically, given code changes and test execution history, the applied
regression TP approach [17] computes an ordered set of test cases that are
impacted by the code changes, and that are of the highest historical fault
detection ability. With this approach, test engineers can detect up to 30%
more regression faults compared to manual test selection guided by tester’s
expertize, for the same time budget. However, this approach is not well suited
for processing a large set of historical test execution data. Following a
recent research direction of using machine learning (ML) for software testing,
the goal of test engineers has been to develop a ML approach for TP that will
be both time-efficient and have a high fault-detection efficiency as more test
data becomes available.

Figure 1: An iteration of CI testing consists of a code commit, build, and
test phase, before code deployment. Change impact analysis and regression test
prioritization are used to speed up testing. Regression test prioritization
can use test history to learn to prioritize test cases and ML to scale test
prioritization process to the size of large test history.

While developing a ML-based test prioritization approach addressing the needs
of our industrial partner, we observed that different ML models can have
different fault-detection performance depending on the CI testing context.
This was especially the case when we used ML models in CI cycles with
different time budget (budget for testing) and when we used different size of
test execution history for ML model learning. Therefore, we systematically
studied how do these two parameters affect the fault-prediction performance of
ML-based test prioritization models.

In this paper we report the experimental results of the systematic comparison
of four best-performing ML approaches reported in the literature on the task
of test case fault-prediction: support-vector machines (SVM), artificial
neural networks (ANN), gradient boosting decision trees (GBDT), and LambdaRank
using NN. In addition, we compare the performance of ML-based approaches
against two heuristic approaches: history-based TP approach $ROCKET$ [17] and
$Random$ test selection. We run the experiments on three industrial data sets
from the CI practice: Cisco, ABB, Google.

In summary, our work makes the following contributions:

  * 1.

Systematic analysis of how the size of test history affects fault-prediction
effectiveness of learning-based test case prioritization.

  * 2.

Systematic evaluation of the effectiveness of ML based test case
prioritization approaches relative to variable time budget across CI cycles.

  * 3.

Systematic comparison of the best-performing ML-based test case prioritization
approaches reported in literature, evaluated on three industrial datasets.

The paper is structured as follows. In Section 2, we review related work. In
Section 3, we describe learning based test case prioritization and present the
four ML-based test prioritization approaches evaluated in this study. Section
4 describes the experimental evaluation, while Section 5 presents the
experimental results. We discuss the key findings of the study and conclude
the paper in Section 6.

##  2 Related Work

Recent studies have used ML for the problem of test case prioritization.
Machalica uses a boosted decision tree approach to learn a classifier for
predicting a probability of a test case failing based on code changes and and
subset of test cases [18]. The approach was shown to reduces the testing cost
by a factor of two, while ensuring that over 95% of individual test failures
and detected. Chen proposes another predictive test prioritization approach
based on XGBoost [19]. It studies test case distribution analysis evaluating
the fault detection capability of actual regression testing. The approach has
been used in practice, and has shown to significantly reduce testing cost.
Motivated by the success of these two approaches based on gradient boosting,
we selected the $GBDT$ as an evaluation candidate for our study.

Busjaeger proposes a test case prioritization approach based on Support Vector
Machine (SVM) [20], to learn a binary classifier to order test cases based on
historical information. The approach has shown to outperform non-ML-based test
case prioritization approaches in terms of fault-detection effectiveness.
Lachmann [21] uses SVM-Rank to prioritize test cases using test case failure
information. The evaluation shows that SVM based approach to test case
prioritization outperforms manual approaches by experts. Grano uses SVM and
Random Forest (RF) to build a regression predictive model for assessing test
branch coverage [22] for the purpose of efficient test case generation for CI
testing. The experimental results have shown good fault prediction accuracy of
SVM for test case prioritization, therefore, we selected SVM as evaluation
candidate in our study.

Several test case prioritization approaches have been proposed using different
forms of neural netowrks, such as Bayesian network [23], NN [24], ANN [25],
RNN [26]. Specifically, [23] integrates a feedback mechanism and a change
information gathering strategy to estimate the probability of a test case to
find bugs. The approach has showed to enable early fault detection. [24]
prioritizes test cases using a NN approach and the fault-proneness
distribution of different code areas. The approach has showed to improve the
effectiveness of coverage based test case prioritization. [25] uses the
combination of test case complexity information and software modification
information to train an ANN, to enable early fault detection. The approach has
showed to improve fault detection effectiveness. [26] proposes a gated
recurrent unit trained on the time series throughput information to perform
regression testing of web services. The results have shown good fault
prediction performance. Following a good fault-prediction performance of these
studies, we included the ANN approach in our evaluation study.

There are studies using reinforcement learning (RL) for test case
prioritization, which focus on maximizing a reward when failing test cases are
prioritized higher [27] or on using simpler ML models for RL policy design
[28]. Lima proposes a multi-armed bandit (MAB) approach to test case
prioritization in continuous integration [29], which showed to outperform the
RL approach in terms of fault-detection. However, we experimented with these
approaches for test prioritization and they showed to be computationally
expensive [30]. Furthermore, Bertolino [31] conducts an extensive experimental
study comparing RL against supervised learning for test case prioritization,
and concludes that the RL approach is less efficient on this specific task.
Because of our experience with RL and the experience reported by Bertolino, we
did not select the RL and MAB approaches for our evaluation study, as our goal
is to build a fast-running test case prioritization approach that can satisfy
strict time constraints of short CI cycles.

In the same study [31], Bertolino reports the best performing ML approach to
test case prioritization in terms of fault-detection effectiveness are MART
and LambdaMART. Motivated by this finding, we include LambdaRank in our
evaluation study. LambdaRank is from the same family of learning to rank
algorithms as MART, and we include it instead of MART, as MART is based on
gradient boosted decision trees which we have already included in our study.

##  3 Learning Based Test Prioritization

In CI development practices, testing is time-constrained and produces
voluminous test history $H$, as CI cycles run fast and frequently. The test
history $H$ contains test execution information for each CI cycle $C_{i}$,
denoted as cycle history, where $i=1...n$ and $n$ is the number of CI cycles.
Each cycle history consists of a test suite $T=\\{T_{1},T_{2},...,T_{n}\\}$
run in that cycle and the time budget of the cycle $B$. Each test suite $T$
contains the pass/fail execution status and execution time of each test case
$t_{i}$.

Given $H$, collected in runs in previous CI cycles, the goal of the learning-
based test case prioritization is to predict which test cases will be
effective in detecting faults in the current CI cycle $C_{n+1}$, ranked
according to their probability of detecting faults. In addition to fault
detection effectiveness, some approaches use test execution time $t$ as
another prioritization criteria, which can be combined together [17] to ensure
that failing test cases are ordered higher, and among the failing test cases,
those that execute faster are ordered higher.

In history-based test case prioritization, historical test failure records may
be weighted, such that the highest failure weight corresponds to the failure
exposed in the most recent test case execution and the failure in every
precedent test execution is weighted lower. This ensures that the test cases
that failed in the most recent run will be ordered higher (thus executed
first), followed by a number of "older" failed test cases, depending on the
available time budget $B$. Such "older" failed test cases are execution
candidates as well, because tests can be flipping from fail to pass to fail
again, as illustrated in Figure 2. In case of ties, i.e. two or more test
cases have the same failure probability, test cases should be ranked in the
order of the shortest execution time $t$. We can define the problem of
learning based regression test prioritization as follows:

For a test case $T_{i}$ belonging to a regression test suite
$T=\\{T_{1},T_{2},...,T_{n}\\}$, the goal of learning is to find a function
$g:T\to C$, mapping the test case $T_{i}$ to a class $C_{i}$ (test rank)
belonging to $C=\\{C_{1},C_{2},...,C_{m}\\}$, where $T_{2}$ is ranked higher
than $T_{1}$ if $g(T_{2})>g(T_{1})$, $m$ is the number of test ranks. In
binary classification $C\in\\{0,1\\}$. Each $T_{i}$ has its execution time
$t_{i}$ and $n$ historical execution results
$\\{R_{i,1},R_{i,2},...R_{i,n}\\}$, where $R\in\\{0,1\\}$ denotes a test pass
or fail, and $n$ denotes the number of CI cycles (test executions). Although
it is possible that the value of $t_{i}$ varies across different cycles, in
this work we assume that $t_{i}$ is the average execution time of a test case
across its CI cycles, as done in [17].

Figure 2: Test history consisting of 15 CI cycles. Cycle 1 is the most recent
and has the highest weight, while cycle 15 is the oldest and has the lowest
wight. Test cases can change execution result between pass and fail in
consecutive executions (CI cycles). Red: fail, Green: pass, Grey:
inconclusive. In this work, we only deal with pass and fail test results.

###  3.1 Selection of ML Approaches for Test Prioritization in CI

As discussed in the related work, there are many ML approaches for test case
prioritization. However, as we are interested in improving the efficiency of
test prioritization in the CI practice, which is highly time-constrained, in
our industrial case study we were looking for a time-efficient ML approach
that can serve the need of generating prioritized test suites quickly. For
example, we have previously experimented with RL for test case prioritization
in comparison with the NN approach on four industrial datasets [30], and have
found the total runtime of the RL approach to be around 50 times higher than
the runtime of the NN approach. This is consistent with the results reported
by Bertolino [31]. Therefore, we excluded RL approaches from this comparative
study. Driven by the requirement to build a fast-running ML approach to test
prioritization, we implemented four simpler types of classifiers for learning
to prioritize regression tests, which have previously showed good fault
detection performance, as discussed in the related work. The classifiers are
learned on historical test execution results generated throughout several
months of testing. For our evaluation study we selected the following ML
classifiers: Support Vector Machine (SVM) classifier, Artificial Neural
Network (ANN) classifier, Gradient Boosted Decision Tree (GBDT) classifier,
and LambdaRank with NN (LRN) classifier.

##  4 Experimental Evaluation

The goal of the experimental study is to evaluate and compare the performance
of four ML-based test case prioritization approaches discussed in Section 3
with the aim of answering the following research questions:

  1. RQ1

How does the length of test execution history used for learning to prioritize
test cases impact the fault-prediction performance of ML approaches?

  2. RQ2

Which ML approach is more effective in predicting test cases with higher
fault-detection effectiveness, for a given time budget, and how do they
compare to heuristic-based test case prioritization approaches?

  3. RQ3

Which ML approach is more time-efficient in a test prioritization task, and
how do they compare to heuristic-based test case prioritization approaches?

###  4.1 Experimental Dataset

We perform experimental evaluation on three industrial datasets used for
system-level testing in CI: Cisco, ABB, Google. Cisco dataset is used for
testing video conferencing systems, provided by Cisco Systems. ABB dataset
111https://bitbucket.org/HelgeS/atcs-data/src/master/ is used for testing
painting robot software, provided by ABB robotics. Google dataset
222https://code.google.com/archive/p/google-shared-dataset-of-test-suite-
results/ is from a large scale continuous testing infrastructure provided by
Google [32]. The datasets contain the information about the number of test
cases, the number of test executions (CI cycles) for each test case and the
historical fault-detection effectiveness of each test case in each execution
as pass or fail.

We summarize the datasets in Table LABEL:tab1.

Table 1: Evaluation datasets. Dataset | # test cases | # test executions | % failed test cases
---|---|---|---
Cisco | 550 | 6050 | 0.43
ABB | 1488 | 149700 | 0.28
Google | 5507 | 12439910 | 0.01

###  4.2 Evaluation Baselines

We compare the ML models for test prioritization one against the other, as
well as against the automated TP approach $ROCKET$ [17] that has previously
shown to improve the effectiveness of manual practice of test selection at
Cisco, and the $Random$ approach.

$ROCKET$ prioritizes a set of test cases in CI testing based on historical
test execution status and test execution duration. The basic principle of
$ROCKET$ is that given the statuses of test cases’ previous runs in successive
CI cycles and their average execution time, the algorithm computes a priority
value for each test case such to maximize early fault detection. More
information about $ROCKET$ can be found here [17]. We varied the length of
historical information used for prioritization by $ROCKET$ from the most
recent 20% to the whole test history size available, with an increment of 20%.
Variable length of test execution history is not applicable to $Random$
heuristic, because it orders test cases randomly, without considering their
historical fault-detection effectiveness during test selection.

###  4.3 Evaluation Metrics

We perform the comparison in terms of the following metrics:

APFD as the weighted average of the percentage of faults detected.

TDFT as the time to detect the first fault by a prioritized test suite.

TDLF as the time to detect the last fault by a prioritized test suite.

TRAIN as the training time of a ML model for test prioritization.

PART as the running time of a prioritization algorithm, i.e. ranking time.

###  4.4 Experimental Setup

First, for the evaluated ML-based approaches, for the purpose of model
learning, we used a varying length of test history for all three datasets
(Cisco, ABB and Google), from the most recent 20% (approximately corresponding
to the most recent 20% of CI cycles) to the whole test history available, with
an increment of 20%, which we denote as $H1$-$H5$. The basic idea of ML is
that more data yields better performance. However, in the case of CI testing,
using more historical cycles for learning may or may not mean better
prediction performance [33], since some of the previous faults might have been
fixed in previous CI cycles and in that case they are no longer good
predictors of failing test cases. Next, we ran the 20 learned ML models for
each of the three experimental test suites: Cisco, ABB and Google to produce
prioritized test suites. Next, we ran the two heuristic-based test
prioritization approaches, $ROCKET$ and $Random$, for all three datasets.

In the next part of the experiment, we selected the learned classifiers with
the best size of test history used for model learning and produced the
prioritized test suites. Next, we run the prioritized test suites to evaluate
their fault-detection effectiveness using five varying values of the time
budget ($B1$-$B5$). $B5$ corresponds to the average time required to run the
whole test suite, and $B1$ corresponds to 20% of that same budget. The
remaining time budgets increase from $B1$ to $B5$ with increments of 20%. By
decreasing the time budget, we can assess the effectiveness of a test suite to
detect failing test cases earlier, because a well performing ML predictor
would prioritize failing test cases higher.

In the final part of the experiment, we measured the time effectiveness of the
TP approaches in terms of training time (for the ML approaches), ranking time,
time to detect the first and last fault, and compared them with the heuristic-
based TP approaches. We measure all the metrics on the Cisco, ABB and Google
datasets.

Training the ML models requires parameter tuning. Specifically, to achieve
good performance of the $GBDT$ model, we experimented with two
hyperparameters, learning rate and n_estimators. The learning rate affects the
rate of adding new trees to the model. For example, a lower learning rate
usually gives a more generalized learner. However, a lower learning rate needs
more time for model training, and it requires a higher number of trees. Many
trees may lead to overfitting. Therefore, choosing an optimal learning rate
and n_estimators is important for good performance of the $GBDT$ model.
Similarly, the performance of the learned NN classifier is dependent on
different parameters, such as the number of hidden layers and their sizes,
activation function, and the number of epochs. To learn a well performing
classifier, we performed an exhaustive hyperparameter tuning. We trained
several classification models, while varying the number of hidden layers, and
layer sizes for each layer. ReLu was used as the activation function for the
hidden layers. Each network had 50 epochs, the training process of each
network was iterated ten times, while measuring the average Mean Square Error
(MSE) and Standard Deviation (SD) of MSE for all five networks. Finally, we
chose the best performing target 3-layer network with the minimal MSE and SD.

##  5 Results and Analysis

In this section, we first analyse the experimental results answering the
research questions, and discuss main threats to the validity of the reported
results.

###  5.1 RQ1: Effect of Test History Size on Fault-prediction Performance

We show the fault-detection effectiveness of history-based TP approaches for
different lengths of test history used for learning to prioritize in Figure 3.
Overall, our experimental results indicate that the fault-prediction
performance of the history-based approaches for TP (both ML based and
$ROCKET$) varies depending on how much test execution history is used in
learning to prioritize. Specifically, for the shortest length of test history
($H1$), all TP approaches achieve low performance. As the length of test
history increases ($H2$), the fault-prediction performance of all TP
approaches increases across all datasets. Increasing the length of test
history further ($H3$) has a positive effect on all TP approaches for the
Cisco and ABB datasets. However, for the Google dataset we see a decrease in
the performance for all TP approaches except $ANN$ in $H3$. Increasing the
length of test history further ($H4$) has a negative effect on all TP
approaches across all datasets except $ANN$ for the Google dataset. Overall,
we see that there is a less negative effect on $ANN$ compared to other ML
approaches approaches. However, the results show that $ROCKET$ is more
negatively affected by using older test history than the ML approaches. As we
continue to increase the length of test history ($H5$) the performance of all
approaches decreases, and more significantly for $ROCKET$ than for the ML
approaches. Among the ML approaches specifically, we see that the $ANN$
approach is the less sensitive to using older test history than other ML
approaches. Also the $ANN$ approach showed to be the most sensitive to using
younger test history (for example, it has the worst performance out of all ML
approaches for $H3$ on the Cisco and ABB datasets.

In summary, the results indicate that the size of test execution history used
for learning to prioritize affects the fault-prediction performance of TP
approaches. For the Cisco and ABB experimental datasets, the optimal size of
test history has shown to be $H3$, which corresponds to 60% of test history.
For the Google datasets, the optimal size of test history in our experiment
was 40%. This implies that the optimal size of test execution history
decreases with the increase of test cycles. For example, the Google datasets
has longer test history of 2259 cycles, while the Cisco and ABB datasets have
only around 100 cycles. This may also mean that the optimal size of test
history is dependent on the frequency of bug fixing and code commits, i.e. the
frequency of CI cycles. For datasets with longer test history less percentage
of it should be used for test prioritization compared to the datasets with
shorter history.

Figure 3: Performance of TP approaches in terms of APFD for different size of
test history used for learning to prioritize ($H1$-$H5$) across three
datasets: Cisco, ABB, and Google.

###  5.2 RQ2: Fault-detection Effectiveness for Different Time Budget

To answer this research question, we use the ML models with the best
configuration of test history size, $H3$ for the Cisco and ABB datasets and
$H2$ for the Google dataset. We compare the fault-detection performance of the
four ML models and two heuristics in terms of APFD, relative to the time
budget available for running prioritized test suites. The results are shown in
Figure 4. Columns $B1$-$B5$ correspond to five different values of the time
budget, starting from 20% of the average overall time required to run a test
suite, with increments of 20%.

The results indicate that the $LRN$ approach and $ROCKET$ approach achieve
similar performance on average. Both approaches perform better for longer time
budgets, with $LRN$ having a slightly higher APFD for longer time budgets
compared to $ROCKET$, and $ROCKET$ a slightly higher APFD for shorter time
budgets compared to $LRN$ for some datasets, e.g. Cisco and ABB. It is
expected that longer time budget enables higher fault-detection, as there is
more time available for testing, more test cases can be executed and more
faults detected. $GBDT$ comes as the next best-performing approach, followed
by $SVM$, on all datasets except Cisco. For this particular dataset, $SVM$
slightly outperforms $GBDT$. $ANN$ approach has the worst fault-detection
performance for short time budgets out of all ML-based approaches. Its
performance improves for larger time budgets. Furthermore, $Random$ has the
absolute worst fault-detection performance for short time budgets out of all
evaluated approaches, while it fault-detection effectiveness improves for
larger time budgets.

Figure 4: Performance of TP approaches in terms of average APFD for different
size of test budget ($B1-B5$) across three datasets: Cisco, ABB, Google.

###  5.3 RQ3: Time Effectiveness

Time effectiveness is measured using four metrics: TDFF, TDLF, TRAIN, and
PART. We report all the metrics in terms of the percentage of the time budget
of a CI cycle.

In terms of the time to detect the first fault (TDFF), $LRN$ has the best
performance, which is comparable to $SVM$. The next best performing approach
is $ROCKET$, followed by $GDBT$. The $ANN$ model has the worst ability to
detect faults early out of all ML based approaches. However, $Random$ has the
worst performance out of all evaluated approaches.

In terms of the time to detect the last fault (TDLF), $LRN$ shows to be a
superior approach, followed by $SVM$ and $ROCKET$ which have comparable
performance. The next best-performing approach is $GBDT$, followed by $ANN$.
$Random$ shows the worst performance.

In terms of the ML model training time (TRAIN), $LRN$ performs the best,
followed by the $GBDT$ approach. $SVM$ is the third best performing approach
in terms of training time, followed by $ANN$.

In terms of the total running time of the prioritization algorithm (PART),
$Random$ has the best performance. This is expected, since it uses a basic
random test selection which is computationally cheap. The results further show
that all ML approaches outperform $ROCKET$, which is expected. The $ANN$
approach has the best performance out of all ML approaches. $GBDT$ is the next
best-performing approach, followed by $LRN$ and $SVM$. Average TRAIN and PART
times for the three datasets Cisco, ABB, and Google are shown in Table
LABEL:tab2.

Table 2: Time metrics: average TRAIN and PART across Cisco, ABB, and Google
datasets.

| Cisco | ABB | Google
---|---|---|---
| TRAIN [s] | PART [s] | TRAIN [s] | PART [s] | TRAIN [s] | PART [s]
LRN | 25 | 2 | 60 | 3 | 155 | 17
SVM | 40 | 2.25 | 95 | 3 | 190 | 18
GBDT | 35 | 1.5 | 90 | 2 | 175 | 15
ANN | 50 | 1.35 | 105 | 1.9 | 199 | 10
ROCKET | - | 65 | - | 125 | - | 3050
Random | - | 1.25 | - | 1.8 | - | 9

##  6 Discussion and Conclusion

Test prioritization in continuous integration has the potential to improve the
effectiveness and speed of fault detection. Machine learning has recently been
proposed as an efficient approach for improving the scalability of test
prioritization. Motivated by these findings, we set out to understand the
relative fault-prediction performance of selected ML approaches for test case
prioritization in continuous integration. We specifically focus on two
parameters of continuous integration: test history size used for training ML
models for test prioritization, and the size of time budget available for CI
cycles.

We selected four ML approaches that have shown good performance in test case
prioritization in the literature (support vector machines, gradient boosting
decision trees, neural networks, and LambdaRank with neural network) and
designed a systematic experimental study comparing the four ML approaches one
against the other and against the two heuristics for test prioritization. We
compared the approaches in terms of time-effectiveness and fault-prediction
effectiveness of prioritized test suites, answering three research questions.
Our results show that the length of test execution history used for learning
to prioritize test cases impacts the fault-prediction performance of ML
approaches. For these datasets, our findings indicate that the optimal size of
test history used for learning to prioritize is from 40% to 60%. When
comparing different ML models for test prioritization, we observed that the
performance of $ANN$ was the least sensitive to using older test history. At
the same time, the $ANN$ approach showed the worst performance for short test
history among all other evaluated ML approaches. Next, our results show that
in terms of fault-prediction effectiveness for a given time budget, the best
performing approach for a short time budget in terms of the APFD metric is
$LRN$, while $ANN$ showed to have the worst fault-detection performance for a
short time budget compared to the other evaluated ML-based approaches.
Finally, in terms of time-effectiveness (time to detect the first and the last
fault), the best performing approach is $LRN$. In terms of ranking time, the
best performing ML approach is $ANN$.

## References

## References

  * [1] N. Niu, S. Brinkkemper, X. Franch, J. Partanen, J. Savolainen, Requirements engineering and continuous deployment, IEEE software 35 (2) (2018) 86–90.
  * [2] T. Savor, M. Douglas, M. Gentili, L. Williams, K. Beck, M. Stumm, Continuous deployment at facebook and oanda, in: 2016 IEEE/ACM 38th International Conference on Software Engineering Companion (ICSE-C), IEEE, 2016, pp. 21–30.
  * [3] C. Parnin, E. Helms, C. Atlee, H. Boughton, M. Ghattas, A. Glover, J. Holman, J. Micco, B. Murphy, T. Savor, et al., The top 10 adages in continuous deployment, IEEE Software 34 (3) (2017) 86–95.
  * [4] D. Marijan, A. Gotlieb, M. Liaaen, A learning algorithm for optimizing continuous integration development and testing practice, in: Software: Practice and Experience, 2019, pp. 192–213.  doi:doi.org/10.1002/spe.2661.
  * [5] D. Marijan, M. Liaaen, Practical selective regression testing with effective redundancy in interleaved tests, in: Proceedings of the 40th International Conference on Software Engineering: Software Engineering in Practice, ICSE-SEIP ’18, Association for Computing Machinery, New York, NY, USA, 2018, p. 153–162.  doi:10.1145/3183519.3183532.
URL https://doi.org/10.1145/3183519.3183532

  * [6] D. Marijan, M. Liaaen, S. Sen, Devops improvements for reduced cycle times with integrated test optimizations for continuous integration, in: 2018 IEEE 42nd Annual Computer Software and Applications Conference (COMPSAC), Vol. 01, 2018, pp. 22–27.  doi:10.1109/COMPSAC.2018.00012.
  * [7] A. Shi, P. Zhao, D. Marinov, Understanding and improving regression test selection in continuous integration, in: 2019 IEEE 30th International Symposium on Software Reliability Engineering (ISSRE), IEEE, 2019, pp. 228–238.
  * [8] S. Ali, Y. Hafeez, S. Hussain, S. Yang, Enhanced regression testing technique for agile software development and continuous integration strategies, Software Quality Journal 28 (2) (2020) 397–423.
  * [9] G. Rothermel, R. H. Untch, C. Chu, M. J. Harrold, Prioritizing test cases for regression testing, IEEE Transactions on software engineering 27 (2001) 929–948.
  * [10] D. Marijan, Multi-perspective regression test prioritization for time-constrained environments, in: 2015 IEEE International Conference on Software Quality, Reliability and Security, 2015, pp. 157–162.  doi:10.1109/QRS.2015.31.
  * [11] D. Marijan, M. Liaaen, Test prioritization with optimally balanced configuration coverage, in: 2017 IEEE 18th International Symposium on High Assurance Systems Engineering (HASE), 2017, pp. 100–103.  doi:10.1109/HASE.2017.26.
  * [12] D. Marijan, M. Liaaen, A. Gotlieb, S. Sen, C. Ieva, Titan: Test suite optimization for highly configurable software, in: 2017 IEEE International Conference on Software Testing, Verification and Validation (ICST), 2017, pp. 524–531.  doi:10.1109/ICST.2017.60.
  * [13] S. Sen, D. Marijan, C. Ieva, A. Grime, A. Sander, Modeling and verifying combinatorial interactions to test data intensive systems: Experience at the norwegian customs directorate, IEEE Transactions on Reliability 66 (1) (2017) 3–16.  doi:10.1109/TR.2016.2618121.
  * [14] H. Hemmati, Z. Fang, M. V. Mantyla, B. Adams, Prioritizing manual test cases in rapid release environments, Software Testing, Verification and Reliability 27\.
  * [15] H. Srikanth, M. Cashman, M. B. Cohen, Test case prioritization of build acceptance tests for an enterprise cloud application: An industrial case study, Journal of Systems and Software 119 (2016) 122–135.
  * [16] S. Elbaum, G. Rothermel, J. Penix, Techniques for improving regression testing in continuous integration development environments, in: Proceedings of the 22nd ACM SIGSOFT International Symposium on Foundations of Software Engineering, 2014, p. 235–245.
  * [17] D. Marijan, A. Gotlieb, S. Sen, Test case prioritization for continuous regression testing: An industrial case study, in: 2013 IEEE International Conference on Software Maintenance, 2013, pp. 540–543.  doi:10.1109/ICSM.2013.91.
  * [18] M. Machalica, A. Samylkin, M. Porth, S. Chandra, Predictive test selection, in: 2019 IEEE/ACM 41st International Conference on Software Engineering: Software Engineering in Practice (ICSE-SEIP), 2019, pp. 91–100.  doi:10.1109/ICSE-SEIP.2019.00018.
  * [19] J. Chen, Y. Lou, L. Zhang, J. Zhou, X. Wang, D. Hao, L. Zhang, Optimizing test prioritization via test distribution analysis, in: Proceedings of the 2018 26th ACM Joint Meeting on European Software Engineering Conference and Symposium on the Foundations of Software Engineering, ESEC/FSE 2018, Association for Computing Machinery, New York, NY, USA, 2018, p. 656–667.  doi:10.1145/3236024.3236053.
URL https://doi.org/10.1145/3236024.3236053

  * [20] B. Busjaeger, T. Xie, Learning for test prioritization: An industrial case study, in: Proceedings of the 2016 24th ACM SIGSOFT International Symposium on Foundations of Software Engineering, FSE 2016, Association for Computing Machinery, New York, NY, USA, 2016, p. 975–980.  doi:10.1145/2950290.2983954.
URL https://doi.org/10.1145/2950290.2983954

  * [21] R. Lachmann, S. Schulze, M. Nieke, C. Seidl, , I. Schaefer, System-level test case prioritization using machine learning, in: 15th International Conference on Machine Learning and Applications, 2016, p. 361–368.
  * [22] G. Grano, T. V. Titov, S. Panichella, H. C. Gall, How high will it be? using machine learning models to predict branch coverage in automated testing, in: 2018 IEEE Workshop on Machine Learning Techniques for Software Quality Evaluation (MaLTeSQuE), 2018, pp. 19–24.  doi:10.1109/MALTESQUE.2018.8368454.
  * [23] S. Mirarab, L. Tahvildari, An empirical study on bayesian network-based approach for test case prioritization, in: 2008 1st International Conference on Software Testing, Verification, and Validation, 2008, pp. 278–287.  doi:10.1109/ICST.2008.57.
  * [24] M. Mahdieh, S.-H. Mirian-Hosseinabadi, K. Etemadi, A. Nosrati, S. Jalali, Incorporating fault-proneness estimations into coverage-based test case prioritization methods, Inf. Softw. Technol. 121 (2020) 106269.
  * [25] H. Jahan, Z. Feng, S. Mahmud, P. Dong, Version specific test case prioritization approach based on artificial neural network, in: Journal of Intelligent and Fuzzy Systems, Vol. 36, 2019, p. 6181–6194.
  * [26] M. Hasnain, M. F. Pasha, C. H. Lim, I. Ghan, Recurrent neural network for web services performance forecasting, ranking and regression testing, in: 2019 Asia-Pacific Signal and Information Processing Association Annual Summit and Conference (APSIPA ASC), 2019, pp. 96–105.  doi:10.1109/APSIPAASC47483.2019.9023052.
  * [27] T. Shi, L. Xiao, K. Wu, Reinforcement learning based test case prioritization for enhancing the security of software, In 2020 IEEE 7th International Conference on Data Science and Advanced Analytics (DSAA) (2020) 663–672.
  * [28] L. Rosenbauer, A. Stein, R. Maier, D. Patzel, J. Hahner, Xcs as a reinforcement learning approach to automatic test case prioritization, In Proceedings of the 2020 Genetic and Evolutionary Computation Conference Companion (2020) 1798–1806.
  * [29] J. A. do Prado Lima, S. R. Vergilio, A multi-armed bandit approach for test case prioritization in continuous integration environments, IEEE Transactions on Software Engineering.
  * [30] A. Sharif, D. Marijan, M. Liaaen, Deeporder: Deep learning for test case prioritization in continuous integration testing, in: 2021 IEEE International Conference on Software Maintenance and Evolution (ICSME), 2021, pp. 525–534.  doi:10.1109/ICSME52107.2021.00053.
  * [31] A. Bertolino, A. Guerriero, B. Miranda, R. Pietrantuono, S. Russo, Learning-to-rank vs ranking-to-learn: Strategies for regression testing in continuous integration, in: In 42nd International Conference on Software Engineering (ICSE), 2020.
  * [32] A. M. S. Elbaum, J. Penix, The google dataset of testing results, Available: https://code.google.com/p/ google-shared-dataset-of-test-suite-results.
  * [33] D. Marijan, M. Liaaen, Effect of time window on the performance of continuous regression testing, in: 2016 IEEE International Conference on Software Maintenance and Evolution (ICSME), 2016, pp. 568–571.  doi:10.1109/ICSME.2016.77.