11institutetext: Research Institute for Symbolic Computation (RISC)
Johannes Kepler University, Linz, Austria
<EMAIL_ADDRESS>22institutetext: Logic and Theory Group
Technical University of Vienna
<EMAIL_ADDRESS>
# Analysis of Clause set Schema Aided by Automated Theorem Proving: A Case
Study

[Extended Paper]

David Cerna 11 Alexander Leitsch 22

###### Abstract

The schematic CERES method [CERESS2] is a recently developed method of cut
elimination for proof schemata, that is a sequence of proofs with a recursive
construction. Proof schemata can be thought of as a way to circumvent adding
an induction rule to the LK-calculus. In this work, we formalize a schematic
version of the infinitary pigeonhole principle, which we call the Non-
injectivity Assertion schema (NiA-schema), in the LKS-calculus [CERESS2], and
analyse the clause set schema extracted from the NiA-schema using some of the
structure provided by the schematic CERES method. To the best of our
knowledge, this is the first application of the constructs built for proof
analysis of proof schemata to a mathematical argument since its publication.
We discuss the role of Automated Theorem Proving (ATP) in schematic proof
analysis, as well as the shortcomings of the schematic CERES method concerning
the formalization of the NiA-schema, namely, the expressive power of the
schematic resolution calculus. We conclude with a discussion concerning the
usage of ATP in schematic proof analysis.

##  1 Introduction

In Gentzen’s Hauptsatz [Gentzen1935], a sequent calculus for first order logic
was introduced, namely, the LK-calculus. He then went on to show that the cut
inference rule is redundant and in doing so, was able to show consistency of
the calculus. The method he developed for eliminating cuts from LK-derivations
works by inductively reducing the cuts in a given LK-derivation to cuts which
either have a reduced formula complexity and/or reduced rank [prooftheory].
This method of cut elimination is known as reductive cut elimination. A useful
result of cut elimination for the LK-calculus is that cut-free LK-derivations
have the subformula property, i.e. every formula occurring in the derivation
is a subformula of some formula in the end sequent. This property allows for
the construction of Herbrand sequents and other objects which are essential in
proof analysis.

However, eliminating cuts from LK-derivations does have its disadvantages,
mainly concerning the number of computations steps needed and the size of the
final cut-free proof. As pointed out by George Boolos in “Don’t eliminate cut”
[Dontelimcut], sometimes the elimination of cut inference rules from an LK-
proof can result in an non-elementary explosion in the size of the proof.
Though using cut elimination, it is also possible to gain mathematical
knowledge concerning the connection between different proofs of the same
theorem. For example, Jean-Yves Girard’s application of reductive cut
elimination to a variation of Fürstenberg-Weiss’ proof of Van der Waerden’s
theorem [ProocomWaerdens1987] resulted in the analytic proof of Van der
Waerden’s theorem as found by Van der Waerden himself. From the work of
Girard, it is apparent that interesting results can be derived from
eliminating cuts in “mathematical” proofs.

A more recently developed method of cut elimination, the CERES method [CERES],
provides the theoretic framework to directly study the cut structure of LK-
derivations, and in the process reduces the computational complexity of
deriving a cut-free proof. The cut structure is transformed into a clause set
allowing for clausal analysis of the resulting clause form. Methods of
reducing clause set complexity, such as subsumption and tautology elimination
can be applied to the characteristic clause set to reduce its complexity. It
was shown by Baaz & Leitsch in “Methods of cut Elimination”
[Baaz:2013:MC:2509679] that this method of cut elimination has a non-
elementary speed up over reductive cut elimination.

In the same spirit of Girard’s work, Baaz et al.
[Baaz:2008:CAF:1401273.1401552] applied the CERES method to a formalized
mathematical proof. At the time of applying the method to Fürstenberg’s proof
of the infinitude of primes, the CERES method had been generalized to higher-
order logic [CERESHIGH] and an attempt was made to apply this generalized
method to to the formal version of Fürstenberg’s proof. However, the
tremendous complexity of the higher-order clause set 111The individual clauses
of the clause set were very large, some containing over 12 literals, and
contained both higher order and first order free variables. Interactive
theorem provers could not handle these clause sets, nor could a human
adequately parse the clause set. suggested the use of an alternative method.
Instead of formalizing the proof as a single higher-order proof, formalize it
as a sequence of first-order proofs enumerated by a single numeric parameter,
of which indexes the number of primes assumed to exists. The resulting schema
of clause sets was refuted by a resolution schema resulting in Euclid’s
argument for prime construction. The resulting specification was produced on
the mathematical meta-level. At that time no object-level construction of the
refutation schema existed.

A mathematical formalizations of Fürstenberg’s proof requires induction. In
the higher-order formalization, induction is easily formalized as part of the
formula language. However in first-order, an induction rule needs to be added
to the LK-calculus. As it was shown in [CERESS2], Reductive cut elimination
does not work in the presence of an induction rule in the LK-calculus. Also,
other systems [Mcdowell97cut-eliminationfor] which provided cut elimination in
the presence of an induction rule do so at the loss of some essential
properties, for example the subformula property.

In “Cut-Elimination and Proof Schemata” [CERESS2], a version of the LK-
calculus was introduced (LKS-calculus) allowing for the formalization of
sequences of proofs as a single object level construction, i.e. the proof
schema, as well as a framework for performing cut elimination on proof
schemata. Cut elimination performed within the framework of [CERESS2] results
in cut-free proof schemata with the subformula property. Essentially, the
concepts found in [CERES] were generalized to handle recursively defined
proofs. It was shown in [CERESS2] that schematic characteristic clause sets
are always unsatisfiable, but it is not known whether a given schematic
characteristic clause set will have a refutation expressible within the
language provided for the resolution refutation schema. This gap distinguishes
the schematic version of the CERES method from the previously developed
versions.

In this work, we continue the tradition outlined above of providing a case
study of an application of a “new” method of cut elimination to a mathematical
proof. Though our example is relatively less grand than the previously chosen
proof it gives an example of a particularly hard single parameter induction.
We chose the tape proof, found in [TAPEPROOFNOEQ, tapeproofpaper,
TapeproofEX2], and generalize it by considering a codomain of size $n$ rather
than of size two. A well known variation of our generalization has been
heavily studied in literature under the guise of the Pigeonhole Principle
(PHP). Our generalization will be referred to as the Non-injectivity Assertion
(NiA). Though such a proof seems straight forward to formalize within the LKS-
calculus, without a change to the construction used in [tapeproofpaper], there
was a forced eigenvariable violation.

After formalizing the NiA as a proof schema (the NiA-schema) we apply the
schematic CERES method. In our attempt to construct an ACNF schema [CERESS2]
we heavily use Automated Theorem Provers (ATP), specifically SPASS
[SpassProver], to develop the understanding needed for construction of such a
schema. SPASS was used over other theorem provers mainly due to familiarity.
How theorem provers were used in our attempt to construct an ACNF schema will
be an emphasis of this work. As an end result, we were able to
“mathematically” express an ACNF schema of the NiA-schema to a great enough
extent to produce instances of the ACNF in the LK-calculus; in a similar way
as in the Fürstenberg’s proof analysis [Baaz:2008:CAF:1401273.1401552].
Though, in our case we have a refutation for every instance (only the first
few where found in [Baaz:2008:CAF:1401273.1401552]) . It remains an open
problem whether a more expressive language is needed to express the ACNF of
the NiA-schema in the framework of [CERESS2] . We conjecture that ATP will
play an important role in resolving this question as well as in future proof
analysis using the schematic CERES method.

The paper is structured as follows: In Sec. 2, we introduce the LKS-calculus
and the essential concepts from [CERESS2] concerning the schematic clause set
analysis. In Sec. 3 & 4, we formalize the NiA-schema in the LKS-calculus. In
Sec. 5, we extract the characteristic clause set from the NiA-schema and
perform normalization and tautology elimination. In Sec. 6, we analysis the
extracted characteristic clause set with the aid of SPASS. In Sec. 7, we
provide a (“mathematically defined”) ACNF schema of the extracted
characteristic clause set. In Sec. 8, we conclude the paper and discuss future
work.

##  2 The LKS-calculus and Clause set Schema

In this section we introduce the LKS-calculus which will be used to formalize
the NiA-schema, and the parts of the schematic CERES method concerned with
characteristic clause set extraction. We refrain from introducing the
resolution refutation calculus provided in [CERESS2] because it does not
particularly concern the work of this paper. Though we provide a resolution
refutation of the characteristic clause set of the NiA-schema, there is a good
reason to believe the constructed resolution refutation is outside the
expressive power of the current schematic resolution refutation calculus. More
specifically, the provided resolution refutation grows as a function of the
free parameter $n$ with respect to a constant change in depth, i.e. grows
wider faster than it grows deep. For more detail concerning the schematic
CERES method, see [CERESS2].

###  2.1 Schematic language, proofs, and the LKS-calculus

The LKS-calculus is based on the LK-calculus constructed by Gentzen
[Gentzen1935]. When one grounds the parameter indexing an LKS-derivation, the
result is an LK-derivation [CERESS2]. The term language used is extended to
accommodate the schematic constructs of LKS-derivations. We work in a two-
sorted setting containing a schematic sort $\omega$ and an individual sort
$\iota$. The schematic sort only contains numerals constructed from the
constant $0:\omega$, a monadic function $s(\cdot):\omega\rightarrow\omega$ and
a single free variable, the free parameter indexing LKS-derivations, of which
we represent using $n$.

The individual sort is constructed in a similar fashion to the standard first
order language [prooftheory] with the addition of schematic functions. Thus,
$\iota$ contains countably many constant symbols, countably many constant
function symbols, and defined function symbols. The constant function symbols
are part of the standard first order language and the defined function symbols
are used for schematic terms. Though, defined function symbols can also unroll
to numerals and thus can be of type $\omega^{n}\to\omega$. The $\iota$ sort
also has free and bound variables and an additional concept, extra variables
[CERESS2]. These are variables introduced during the unrolling of defined
function (predicate) symbols. We do not use extra variables in the
formalization of the NiA-schema, but they are essential for the refutation of
the characteristic clause set. Also important are the schematic variable
symbols which are variables of type $\omega\rightarrow\iota$. Essentially
second order variables, though, when evaluated with a ground term from the
$\omega$ sort we treat them as first order variables. Our terms are built
inductively using constants and variables as a base.

Formulae are constructed inductively using countably many constant predicate
symbols (atomic formulae), logical operators
$\vee$,$\wedge$,$\rightarrow$,$\neg$,$\forall$, and $\exists$, as well as
defined predicate symbols which are used to construct schematic formulae. In
this work iterated $\bigvee$ is the only defined predicate symbol used, and of
which has the following term algebra:

$\varepsilon_{\vee}=\bigvee_{i=0}^{s(y)}P(i)\equiv\left\\{\begin{array}[]{c}{\displaystyle\bigvee_{i=0}^{s(y)}P(i)\Rightarrow\bigvee_{i=0}^{y}P(i)\vee
P(s(y))}\\\ {\displaystyle\bigvee_{i=0}^{0}P(i)\Rightarrow
P(0)}\end{array}\right.$ (1)

From the above described term and formulae language we can provide the
inference rules of the LKE-calculus, essentially the LK-calculus [prooftheory]
plus an equational theory $\varepsilon$ (in our case $\varepsilon_{\vee}$ Eq.
1). This theory, concerning our particular usage, is a primitive recursive
term algebra describing the structure of the defined function(predicate)
symbols. The LKE-calculus is the base calculus for the LKS-calculus which also
includes proof links which will be described shortly.

######  Definition 1 ($\varepsilon$-inference rule)

$S\left[t\right]$ $(\varepsilon)$ $S\left[t^{\prime}\right]$

In the $\varepsilon$ inference rule, the term $t$ in the sequent $S$ is
replaced by a term $t^{\prime}$ such that, given the equational theory
$\varepsilon$, $\varepsilon\models t=t^{\prime}$.

To extend the LKE-calculus with proof links we need a countably infinite set
of proof symbols denoted by $\varphi,\psi,\varphi_{i},\psi_{j}\ldots$. Let
$S(\bar{x})$ by a sequent with schematic variables $\bar{x}$, then by the
sequent $S(\bar{t})$ we use to denote the sequent $S(\bar{x})$ where each of
the variables in $\bar{x}$ is replaced by the terms in the vector $\bar{t}$
respectively, assuming that they have the appropriate type. Let $\varphi$ be a
proof symbol and $S(\bar{x})$ a sequent, then the expression
$(\varphi(\bar{t}))$ $S(\bar{t})$ is called a proof link . For a variable
$n:\omega$, proof links such that the only arithmetic variable is $n$ are
called $n$-proof links .

######  Definition 2 (LKE-calculus [CERESS2])

The sequent calculus $\mathbf{LKS}$ consists of the rules of $\mathbf{LKE}$,
where proof links may appear at the leaves of a proof.

######  Definition 3 (Proof schemata [CERESS2])

Let $\psi$ be a proof symbol and $S(n,\bar{x})$ be a sequent such that
$n:\omega$. Then a proof schema pair for $\psi$ is a pair of
$\mathbf{LKS}$-proofs $(\pi,\nu(k))$ with end-sequents $S(0,\bar{x})$ and
$S(k+1,\bar{x})$ respectively such that $\pi$ may not contain proof links and
$\nu(k)$ may contain only proof links of the form  $(\psi(k,\bar{a}))$
$S(k,\bar{a})$ and we say that it is a proof link to $\psi$. We call
$S(n,\bar{x})$ the end sequent of $\psi$ and assume an identification between
the formula occurrences in the end sequents of $\pi$ and $\nu(k)$ so that we
can speak of occurrences in the end sequent of $\psi$. Finally a proof schema
$\Psi$ is a tuple of proof schema pairs for $\psi_{1},\cdots\psi_{\alpha}$
written as $\left\langle\psi_{1},\cdots\psi_{\alpha}\right\rangle$, such that
the $\mathbf{LKS}$-proofs for $\psi_{\beta}$ may also contain $n$-proof links
to $\psi_{\gamma}$ for $1\leq\beta<\gamma\leq\alpha$. We also say that the end
sequent of $\psi_{1}$ is a the end sequent of $\Psi$.

We will not dive further into the structure of proof schemata and instead
refer the reader to [CERESS2]. We now introduce the characteristic clause set
schema.

###  2.2 Characteristic Clause set Schema

The construction of the characteristic clause set as described for the CERES
method [CERES] required inductively following the formula occurrences of cut
formula ancestors up the proof tree to the leaves. However, in the case of
proof schemata, the concept of ancestors and formula occurrence is more
complex. A formula occurrence might be an ancestor of a cut formula in one
recursive call and in another it might not. Additional machinery is necessary
to extract the characteristic clause term from proof schemata. A set $\Omega$
of formula occurrences from the end-sequent of an LKS-proof $\pi$ is called a
configuration for $\pi$. A configuration $\Omega$ for $\pi$ is called relevant
w.r.t. a proof schema $\Psi$ if $\pi$ is a proof in $\Psi$ and there is a
$\gamma\in\mathbb{N}$ such that $\pi$ induces a subproof $\pi$ of
$\Psi\downarrow\gamma$ such that the occurrences in $\Omega$ correspond to
cut-ancestors below $\pi$ [thesis2012Tsvetan]. Note that the set of relevant
cut-configurations can be computed given a proof schema $\Psi$. To represent a
proof symbol $\varphi$ and configuration $\Omega$ pairing in a clause set we
assign them a clause set symbol $cl^{\varphi,\Omega}(a,\bar{x})$, where $a$ is
an arithmetic term.

######  Definition 4 (Characteristic clause term [CERESS2])

Let $\pi$ be an $\mathbf{LKS}$-proof and $\Omega$ a configuration. In the
following, by $\Gamma_{\Omega}$ , $\Delta_{\Omega}$ and $\Gamma_{C}$ ,
$\Delta_{C}$ we will denote multisets of formulas of $\Omega$\- and
$cut$-ancestors respectively. Let $r$ be an inference in $\pi$. We define the
clause-set term $\Theta_{r}^{\pi,\Omega}$ inductively:

  * •

if $r$ is an axiom of the form
$\Gamma_{\Omega},\Gamma_{C},\Gamma\vdash\Delta_{\Omega},\Delta_{C},\Delta$,
then
$\Theta_{r}^{\pi,\Omega}=\left\\{\Gamma_{\Omega},\Gamma_{C}\vdash\Delta_{\Omega},\Delta_{C}\right\\}$

  * •

if $r$ is a proof link of the form  $\psi(a,\bar{u})$
$\Gamma_{\Omega},\Gamma_{C},\Gamma\vdash\Delta_{\Omega},\Delta_{C},\Delta$
then define $\Omega^{\prime}$ as the set of formula occurrences from
$\Gamma_{\Omega},\Gamma_{C}\vdash\Delta_{\Omega},\Delta_{C}$ and
$\Theta_{r}^{\pi,\Omega}=cl^{\psi,\Omega}(a,\bar{u})$

  * •

if $r$ is a unary rule with immediate predecessor $r^{\prime}$ , then
$\Theta_{r}^{\pi,\Omega}=\Theta_{r^{\prime}}^{\pi,\Omega}$

  * •

if $r$ is a binary rule with immediate predecessors $r_{1}$, $r_{2}$, then

    * –

if the auxiliary formulas of $r$ are $\Omega$\- or $cut$-ancestors, then
$\Theta_{r}^{\pi,\Omega}=\Theta_{r_{1}}^{\pi,\Omega}\oplus\Theta_{r_{2}}^{\pi,\Omega}$

    * –

otherwise,
$\Theta_{r}^{\pi,\Omega}=\Theta_{r_{1}}^{\pi,\Omega}\otimes\Theta_{r_{2}}^{\pi,\Omega}$

Finally, define $\Theta^{\pi,\Omega}=\Theta_{r_{0}}^{\pi,\Omega}$ where
$r_{0}$ is the last inference in $\pi$ and
$\Theta^{\pi}=\Theta^{\pi,\emptyset}$. We call $\Theta^{\pi}$ the
characteristic term of $\pi$.

Clause terms evaluate to sets of clauses by $|\Theta|=\Theta$ for clause sets
$\Theta$, $|\Theta_{1}\oplus\Theta_{2}|=|\Theta_{1}|\cup|\Theta_{2}$,
$|\Theta_{1}\otimes\Theta_{2}|=\\{C\circ D\mid
C\in|\Theta_{1}|,D\in|\Theta_{2}|\\}$.

The characteristic clause term is extracted for each proof symbol in a given
proof schema $\Psi$, and together they make the characteristic clause set
schema for $\Psi$, $CL(\Psi)$.

##  3 “Mathematical” proof of the NiA Statement

In this section we provide a mathematical proof of the NiA statement (Thm.
3.1). The proof is very close in structure to the formal proof written in the
LKS-calculus, which can be found in Sec. 4. We skip the basic structure of the
proof and outline the structure emphasising the cuts. We will refer to the
interval $\left\\{0,\cdots,n-1\right\\}$ as $\mathbb{N}_{n}$. Let $rr_{f}(n)$
be the following sentence, for $n\geq 2$: There exists $p,q\in\mathbb{N}$ such
that $p<q$ and $f(p)=f(q)$, or for all $x\in\mathbb{N}$ there exists a
$y\in\mathbb{N}$ such that $x\leq y$ and $f(y)\in\mathbb{N}_{n-1}$.

###### Lemma 1

Let $f:\mathbb{N}\rightarrow\mathbb{N}_{n}$, where $n\in\mathbb{N}$, be total,
then $rr_{f}(n)$ or there exists $p,q\in\mathbb{N}$ such that $p<q$ and
$f(p)=f(q)$.

###### Proof

We can split the codomain into $\mathbb{N}_{n-1}$ and $\left\\{n\right\\}$, or
the codomain is $\left\\{0\right\\}$.

###### Lemma 2

Let $f$ be a function as defined in Lem. 1 and $2<m\leq n$, then if
$rr_{f}(m)$ holds so does $rr_{f}(m-1)$.

###### Proof

Apply the steps of Lem. 1 to the right side of the or in $rr_{f}(m)$.

###### Theorem 3.1

Let $f$ be a function as defined in Lem. 1 , then there exists
$i,j\in\mathbb{N}$ such that $i<j$ and $f(i)=f(j)$.

###### Proof

Chain together the implications of Lem. 2 and derive $rr_{f}(2)$, the rest is
trivial by Lem. 1.

This proof makes clear that the number of cuts needed to prove the statement
is parametrized by the size of the codomain of the function $f$. The formal
proof of the next section outlines more of the basic assumptions being that
they are needed for constructing the characteristic clause set.

##  4 NiA formalized in the LKS-calculus

In this section we provide a formalization of the NiA-schema whose proof
schema representation is
$\left\langle(\omega(0),\omega(n+1)),(\psi(0),\psi(n+1))\right\rangle$. Cut-
ancestors will be marked with a ∗ and $\Omega$-ancestors with ∗∗. Numerals
(terms of the $\omega$ sort) will be marked with $\overline{\cdot}$. We will
make the following abbreviations: $EQ_{f}\equiv\exists p\exists q(p<q\wedge
f(p)=f(q))$, $I(\overline{n})\equiv\forall x\exists y(x\leq
y\wedge\bigvee_{i=\overline{0}}^{\overline{n}}f(y)=\overline{i})$,
$I_{s}(\overline{n})\equiv\forall x\exists y(x\leq y\wedge f(y)=\overline{n})$
and $AX_{eq}(\overline{n})\equiv
f(\beta)=\overline{n}^{*},f(\alpha)=\overline{n}^{*}\vdash f(\beta)=f(\alpha)$
(the parts of $AX_{eq}(\overline{n})$ marked as cut ancestors are always cut
ancestors in the NiA-schema).

$\begin{array}[]{c}\vdash\alpha\leq\alpha^{*}\end{array}$
$\begin{array}[]{c}f(\alpha)=\overline{0}\vdash
f(\alpha)=\overline{0}^{*}\end{array}$ $\wedge:r$ $\begin{array}[]{c}\vdots\\\
\forall xf(x)=\overline{0}\vdash I(\overline{0})^{*}\end{array}$
$\begin{array}[]{c}s(\beta)\leq\alpha^{*}\vdash\beta<\alpha\end{array}$
$\begin{array}[]{c}AX_{eq}(\overline{0})\end{array}$ $\wedge:r$
$\begin{array}[]{c}\vdots\\\ I(\overline{0})^{*}\vdash EQ_{f}\end{array}$
$cut$ $\begin{array}[]{c}\forall xf(x)=0\vdash EQ_{f}\end{array}$

Figure 1: Proof symbol $\omega(0)$

$\begin{array}[]{c}\varphi(\overline{n+1})\end{array}$ .
$\begin{array}[]{c}I(\overline{n+1})^{*}\vdash EQ_{f}\end{array}$
$\begin{array}[]{c}\vdash\alpha\leq\alpha^{*}\end{array}$
$\begin{array}[]{c}\bigvee_{i=\overline{0}}^{\overline{n+1}}f(\alpha)=\overline{i}\vdash\bigvee_{i=\overline{0}}^{\overline{n+1}}f(\alpha)=\overline{i}^{*}\end{array}$
$\wedge:r$ $\begin{array}[]{c}\vdots\\\ \forall
x\bigvee_{i=\overline{0}}^{\overline{n+1}}f(x)=\overline{i}\vdash
I(\overline{n+1})^{*}\end{array}$ $cut$ $\begin{array}[]{c}\forall
x\bigvee_{i=\overline{0}}^{\overline{n+1}}f(x)=\overline{i}\vdash
EQ_{f}\end{array}$

Figure 2: Proof symbol $\omega(n+1)$

$\begin{array}[]{c}s(\beta)\leq\alpha^{*}\vdash\beta<\alpha\end{array}$
$\begin{array}[]{c}AX_{eq}(\overline{0})\end{array}$ $\wedge:r$
$\begin{array}[]{c}\vdots\\\ I_{s}(\overline{0})^{*}\vdash EQ_{f}\end{array}$

Figure 3: Proof symbol $\psi(0)$

$\begin{array}[]{c}max(\alpha,\beta)\leq\gamma^{**}\vdash\\\
\alpha\leq\gamma^{*}\end{array}$
$\begin{array}[]{c}f(\gamma)=\overline{0}^{**}\vdash\\\
f(\gamma)=\overline{0}^{*},\end{array}$ $\begin{array}[]{c}\vdots\end{array}$
$\begin{array}[]{c}f(\gamma)=\overline{n+1}^{**}\vdash\\\
f(\gamma)=n+1^{*},\end{array}$ $\begin{array}[]{c}\vdots\end{array}$
$\wedge:r$ $\begin{array}[]{c}\vdots\end{array}$
$\begin{array}[]{c}max(\alpha,\beta)\leq\gamma^{**}\vdash\\\
\beta\leq\gamma^{*}\end{array}$ $\wedge:r$
$\begin{array}[]{c}I(\overline{n+1})^{**}\vdash
I(\overline{n})^{*},I_{s}(\overline{n+1})^{*}\\\ \vdots\end{array}$

$\begin{array}[]{c}\vdots\\\ I(\overline{n+1})^{**}\vdash
I(\overline{n})^{*},I_{s}(\overline{n+1})^{*}\end{array}$
$\varphi(\overline{n})$ . $\begin{array}[]{c}I(\overline{n})^{*}\vdash
EQ_{f}\end{array}$ $cut$ $\begin{array}[]{c}I(\overline{n+1})^{**}\vdash
EQ_{f},I_{s}(\overline{n+1})^{*}\\\ \vdots\end{array}$

$\begin{array}[]{c}\vdots\\\ I(\overline{n+1})^{**}\vdash
EQ_{f},I_{s}(\overline{n+1})^{*}\end{array}$
$\begin{array}[]{c}s(\beta)\leq\alpha^{*}\vdash\beta<\alpha\end{array}$
$\begin{array}[]{c}AX_{eq}(\overline{n+1})\end{array}$ $\wedge:r$
$\begin{array}[]{c}\vdots\\\ I_{s}(\overline{n+1})^{*}\vdash
EQ_{f}\end{array}$ $cut$ $\begin{array}[]{c}I(\overline{n+1})^{**}\vdash
EQ_{f},EQ_{f}\end{array}$ $c:r$
$\begin{array}[]{c}I(\overline{n+1})^{**}\vdash EQ_{f}\end{array}$

Figure 4: Proof symbol $\psi(n+1)$

##  5 Characteristic Clause set Schema Extraction

The outline of the formal proof provided above highlights the inference rules
which directly influence the characteristic clause set schema of the NiA-
schema. Also to note are the configurations of the NiA-schema which are
relevant, namely, the empty configuration $\emptyset$ and a schema of
configurations $\Omega(\overline{n})\equiv\forall x\exists y(x\leq
y\wedge\bigvee_{i=\overline{0}}^{\overline{n}}f(y)=\overline{i})$. Thus, we
have the following:

$CL_{NiA}(0)\equiv\Theta^{\omega,\emptyset}(0)\equiv\left\\{\left(cl^{\psi,\Omega(\overline{0})}(\overline{0})\oplus\vdash\alpha\leq\alpha\right)\oplus\vdash
f(\alpha)=\overline{0}\right\\}$ (2a)
$cl^{\psi,\Omega(\overline{0})}(\overline{0})\equiv\Theta^{\psi,\Omega(\overline{0})}(0)\equiv\left\\{s(\beta)\leq\alpha\vdash\otimes
f(\alpha)=\overline{0},f(\beta)=\overline{0}\vdash\right\\}$ (2b)
${\scriptstyle
CL_{NiA}(\overline{n+1})\equiv\Theta^{\omega,\emptyset}(\overline{n+1})\equiv\left\\{\left(cl^{\psi,\Omega(\overline{n+1})}(\overline{n+1})\oplus\vdash\alpha\leq\alpha\right)\oplus\vdash\bigvee_{i=\overline{0}}^{\overline{n+1}}f(\alpha)=\overline{i}\right\\}}$
(2c) $\begin{array}[]{c}{\scriptstyle
cl^{\psi,\Omega(\overline{n+1})}(\overline{n+1})\equiv\Theta^{\psi,\Omega(\overline{n+1})}(\overline{n+1})\equiv\left\\{\left(cl^{\psi,\Omega(\overline{n})}(\overline{n})\oplus\left(s(\beta)\leq\alpha\vdash\otimes
f(\alpha)=\overline{n+1},f(\beta)=\overline{n+1}\vdash\right)\right)\right.}\\\
{\scriptstyle\left.\oplus\left(max(\alpha,\beta)\leq\gamma\vdash\alpha\leq\gamma\right)\oplus\left(max(\alpha,\beta)\leq\gamma\vdash\beta\leq\gamma\right)\right\\}}\end{array}$
(2d)

In the characteristic clause set schema $CL_{NiA}(\overline{n+1})$ presented
in Eq.2 tautologies are already eliminated. Evaluation of
$CL_{NiA}(\overline{n+1})$ yields the following clause set $C(n)$:

$\begin{array}[]{l}(C1)\ \vdash\alpha\leq\alpha,\ (C2)\
max(\alpha,\beta)\leq\gamma\vdash\alpha\leq\gamma,\ (C3)\
max(\alpha,\beta)\leq\gamma\vdash\beta\leq\gamma\\\ (C4_{0})\
f(\beta)=\overline{0},f(\alpha)=\overline{0},s(\beta)\leq\alpha\vdash\\\
\ldots\ldots\\\ \ldots\ldots\\\ (C4_{n})\
f(\beta)=\overline{n},f(\alpha)=\overline{n},s(\beta)\leq\alpha\vdash\\\ (C5)\
\vdash f(\alpha)=\overline{0},\cdots,f(\alpha)=\overline{n}\end{array}$

##  6 Clausal Analysis Aided by ATP

The result of characteristic clause set extraction for proof schemata is a
sequence of clause sets representing the cut structure (See Sec. 5), rather
than a single clause set representing the cut structure. Thus, unlike
applications of the first-order CERES method to formal proofs
[tapeproofpaper], where a theorem prover is used exclusively to find a
refutation, we can only rely on theorem provers for suggestions. Essentially,
we need the theorem provers to help with the construction of two elements of
the schematic resolution refutation: the induction invariants and the term
language.

For this clause set analysis, we exclusively used SPASS [SpassProver] in the
“out of the box mode”. We did not see a point to working with the
configurations of SPASS being that for sufficiently small instances of $C(n)$
it found a refutation, and our goal was not to find an elegant proof using the
theorem prover, but rather a refutation with the aid of the theorem prover;
the “out of the box mode” was enough for this goal222Also, using “out of the
box mode” allows for ease of reproducibility of our results when using the
same version of SPASS.. Though as a side note, refutations found by SPASS were
not the smallest, the resolution refutation that SPASS gave as output for
$C(4)$333See Sec. 9.6 used $(C5)$ in the refutation tree 1806 times. The
resolution refutation we provide used $(C5)$ only 65 times. Though, it is not
that our final refutation is wildly different, SPASS ended up deriving clauses
using derived clauses which could easily be derived from the initial clause
set.

An essential feature we were looking for in the refutations found by SPASS
were sequences of clauses which mimic the stepcase construction of the
induction axiom, i.e. $\forall x(\varphi(x)\rightarrow\varphi(x+1))$. An
example of such a sequence from the refutation of $C(4)$, of which will be the
basis of Thm. 7.1, is as follows:

$1[0:Inp]\ \|\|\ \Rightarrow\ eq(f(U),3)\ ,\ eq(f(U),2)\ ,\ eq(f(U),1)\ ,\
eq(f(U),0)*$
---
$2795[0:MRR:1.3,2764.0]\ \|\|\ \Rightarrow\ eq(f(U),3)\ ,\ eq(f(U),2)\ ,\
eq(f(U),1)$
$3015[0:MRR:2795.2,2984.0]\ \|\|\ \Rightarrow\ eq(f(U),3)\ ,\ eq(f(U),2)$
$3096[0:MRR:3015.1,3065.0]\ \|\|\ \Rightarrow\ eq(f(U),3)$
Figure 5: Recursive sequence found in the refutation of $C(4)$.

Essentially, if we where to interpret the initial clause as defining a
function (a function whose domain is the natural numbers and whose codomain is
the set $\left[0,n\right]$) we see that at first we assume the function has a
codomain of size $n$, and than we derive that it cannot have a codomain of
size $n$, but rather of size $n-1$, and so on, until we derive that its
codomain is empty, contradicting the original assumption, that is that the
codomain is non-empty (i.e. clause $(C5)$). This pattern can be found in other
instances of the refutation of $C(n)$.

This sequences seems to be an essential part, even the only part, needed to
define a recursive refutation of $C(n)$, though if and only if, $C(n)$ is
refutable with a total induction, of which such a refutation has not been
found and is unlikely to exists. Something which is not completely apparent in
SPASS refutation for $C(n)$, $n<4$, is the gap (in numbering) between clause
$1$ and clause $2795$ in Fig. 5. To derive clause $2795$ for clause $1$ in one
step we need to first derive the following clause:

$2764[0:MRR:2714.1,2749.1]\ \|\|\ eq(f(U),0)*\ \Rightarrow$

of which deriving is almost as difficult as deriving the sequence of Fig. 5.
Essentially to derive clause $2764$, the SPASS refutation eludes to the need
of an inner recursion bounded by the outer recursion. Essentially, we start
from a clause of the following form:
$\begin{array}[]{l}2272[0:Res:955.3,159.1]\ \|\|\ eq(f(U),0)*\ ,\ eq(f(V),1)*\
,\ eq(f(W),2)*\ ,\\\ eq(f(X),3)*\ \Rightarrow\end{array}$
stating that the codomain is empty and derive that this implies some element
$k$ is not in the codomain. Clause $2272$ is essential for Lem. 7 and is one
of the clauses of Lem. 4.

Up to this point we have an idea of the overall structure of the refutation,
but so far, we have not discussed the term structure and unifiers used by
SPASS. Essentially, how was the recursive max term construction of Def. 5
found? Looking at the following two derived clauses from $C(3)$ and $C(4)$ we
see that the nesting of the $\max$ term grows with respect to the free
parameter:
$20[0:Res:15.0,4.0]\ \|\|\ \Rightarrow\ le(U,max(max(max(V,U),W),X))$
$54[0:Res:19.0,4.0]\ \|\|\ \Rightarrow\ le(U,max(max(max(max(V,U),W),X),Y))$
However, in clause $20$ and $54$ the associativity is the opposite of Def. 5.
We found that the refutation of Sec. 7 is easier when we switch the
association of the max term construction. Also, both clause $20$ and $54$ do
not contain successor function ($s(\cdot)$) encapsulation of the variables
while Def. 5 does. The $s(\cdot)$ terms were added because of the clauses
$C4_{i}$. The literal $s(\alpha)\leq\beta$ enforces the addition of an
$s(\cdot)$ term anyway during the unification. This can be see in Lem. 3 and
Cor. 1, 2, & 3. However, we have not been able to prove the necessity of these
max function constructions, nor find a refutation without them.

The result of all these observations was Lem. 4. After proving that the Lem. 4
clause set is indeed derivable from $C(n)$ using resolution, we constructed it
to see what the SPASS refutation looked like for $C(4)$. We abbreviate the
term $max(max(max(s(x_{0}),s(x_{1})),s(x_{2})),s(x_{3}))$ by $m(\bar{x}_{4})$:

$1:eq(f(m(\bar{x}_{4})),2)\vee eq(f(m(\bar{x}_{4})),1)\vee
eq(f(m(\bar{x}_{4})),0)$
$2:\neg eq(f(x_{2}),2)\vee eq(f(m(\bar{x}_{4})),1)\vee
eq(f(m(\bar{x}_{4})),0)$
$3:\neg eq(f(x_{1}),1)\vee eq(f(m(\bar{x}_{4})),2)\vee
eq(f(m(\bar{x}_{4})),0)$
$4:\neg eq(f(x_{0}),0)\vee eq(f(m(\bar{x}_{4})),2)\vee
eq(f(m(\bar{x}_{4})),1)$
$5:\neg eq(f(x_{2}),2)\vee\neg eq(f(x_{1}),1)\vee eq(f(m(\bar{x}_{4})),0)$
$6:\neg eq(f(x_{2}),2)\vee\neg eq(f(x_{0}),0)\vee eq(f(m(\bar{x}_{4})),1)$
$7:\neg eq(f(x_{1}),1)\vee\neg eq(f(x_{0}),0)\vee eq(f(m(\bar{x}_{4})),2)$
$8:\neg eq(f(x_{1}),1)\vee\neg eq(f(x_{0}),0)\vee\neg eq(f(x_{2}),2)$

Figure 6: Clause set of Lem. 4 for $C(3)$.

Feeding this derived clause set to SPASS for several instances aided the
construction of the well ordering of Def. 9 and the structure of the
resolution refutation found in Lem. 7.

##  7 Refutation of the NiA-schema’s Characteristic Clause Set Schema

In this section we provide a refutation of $C(n)$ for every value of $n$. We
prove this result by first deriving a set of clauses which we will consider
the least elements of a well ordering. Then we show how resolution can be
applied to this least elements to derive clauses of the form
$f(\alpha)=\overline{i}\vdash$ for $0\leq i\leq n$. The last step is simply to
take the clause $(C5)$ from the clause set $C(n)$ and resolve it with each of
the $f(\alpha)=\overline{i}\vdash$ clauses.

###### Definition 5

We define the primitive recursive term $m(k,\overline{x},t)$, where
$\overline{x}$ is a schematic variable and $t$ a term, as follows:
$\left\\{m(k+1,\overline{x},t)\Rightarrow\right.$
$\left.m(k,\overline{x},max(s(x_{k+1}),t))\ ;\ m(0,t)\Rightarrow t\right\\}$

###### Definition 6

We define the resolution rule $res(\sigma,P)$ where $\sigma$ is a unifier and
$P$ is a predicate as follows:

$\begin{array}[]{c}\Pi\vdash P^{*},\Delta\end{array}$
$\begin{array}[]{c}\Pi^{\prime},P^{**}\vdash\Delta^{\prime}\end{array}$
$res(\sigma,P)$
$\begin{array}[]{c}\Pi\sigma,\Pi^{\prime}\sigma\vdash\Delta\sigma,\Delta^{\prime}\sigma\end{array}$

The predicates $P^{*}$ and $P^{**}$ are defined such that
$P^{**}\sigma=P^{*}\sigma=P$. Also, there are no occurrences of $P$ in
$\Pi^{\prime}\sigma$ and $P$ in $\Delta\sigma$.

This version of the resolution rule is not complete for unsatisfiable clause
sets, but simplifies the outline of the refutation.

###### Lemma 3

Given $0\leq k$ and $0\leq n$, the clause $\vdash t\leq m(k,\overline{x},t)$
is derivable by resolution from $C(n)$.

###### Proof

Let us consider the case when $k=0$, the clause we would like to show
derivability of is $\vdash t\leq m(0,t)$, which is equivalent to the clause
$\vdash t\leq t$, an instance of (C1). Assuming the lemma holds for all
$m<k+1$, we show that the lemma holds for $k+1$. By the induction hypothesis,
the instance $\vdash max(s(x_{k+1}),t^{\prime})\leq
m(k,\overline{x},max(s(x_{k+1}),t^{\prime}))$ is derivable. Thus, the
following derivation proves that the clause $\vdash t^{\prime}\leq
m(k+1,\overline{x}_{k+1},t^{\prime})$, where $t=max(s(x_{k+1}),t^{\prime})$
for some term $t^{\prime}$ is derivable:

$\begin{array}[]{c}(IH)\\\ \vdash P\end{array}$ $\begin{array}[]{c}(C3)\\\
max(\beta,\delta)\leq\gamma\vdash\delta\leq\gamma\end{array}$ $res(\sigma,P)$
$\begin{array}[]{c}\vdash t\leq
m(k,\overline{x},max(s(x_{k+1}),t))\end{array}$ $\varepsilon$
$\begin{array}[]{c}\vdash t\leq m(k+1,\overline{x},t)\end{array}$

$P=max(s(x_{k+1}),t)\leq m(k,\overline{x},max(s(x_{k+1}),t))$
$\sigma=\left\\{\beta\leftarrow s(x_{k+1}),\gamma\leftarrow
m(k,\overline{x},max(s(x_{k+1}),t)),\delta\leftarrow t\right\\}$

$\square$

See Sec. 9 for proofs of the following three corollaries.

###### Corollary 1

Given $0\leq k,n$, the clause $\vdash s(x_{k+1})\leq
m(k,\overline{x},max(s(x_{k+1}),t))$ is derivable by resolution from $C(n)$.

###### Corollary 2

Given $0\leq k$ and $0\leq n$, the clause $f(x_{k+1})=i,$
$f(m(k,\overline{x},max(s(x_{k+1}),t)))=i\vdash$ for $0\leq i\leq n$ is
derivable by resolution from $C(n)$.

###### Corollary 3

Given $0\leq k$ and $0\leq n$, the clause
$f(x_{k+1})=i,f(m(k,\overline{x}_{k},s(x_{k+1})))=i\vdash$ for $0\leq i\leq n$
is derivable by resolution from $C(n)$.

###### Definition 7

Given $0\leq n$, $-1\leq k\leq j\leq n$,a variable $z$, and a bijective
function $b:\mathbb{N}_{n}\rightarrow\mathbb{N}_{n}$ we define the following
formulae:

$c_{b}(k,j,z)\equiv\bigwedge_{i=0}^{k}f(x_{b(i)})=b(i)\vdash\bigvee_{i=k+1}^{j}f(m(n,\overline{x},z))=b(i).$

The formulae $c_{b}(-1,-1,z)\equiv\ \vdash$, and $c_{b}(-1,n,z)\equiv\
\vdash\bigvee_{i=0}^{n}f(z)=i$ for all values of $n$ .

###### Lemma 4

Given $0\leq n$, $-1\leq k\leq n$ and for all bijective functions
$b:\mathbb{N}_{n}\rightarrow\mathbb{N}_{n}$. the formula $c_{b}(k,n,z)$ is
derivable by resolution from C(n).

###### Proof

See Sec. 9.4. Greatest lower bounds of Def. 9.

###### Definition 8

Given $0\leq n$, $0\leq k\leq j\leq n$, and a bijective function
$b:\mathbb{N}_{n}\rightarrow\mathbb{N}_{n}$ we define the following formulae:

$c^{\prime}_{b}(k,j)\equiv\bigwedge_{i=0}^{k}f(x_{i+1})=b(i)\vdash\bigvee_{i=k+1}^{j}f(m(k,\overline{x}_{k},s(x_{k+1}))=b(i).$

###### Lemma 5

Given $0\leq n$, $0\leq k\leq n$ and for all bijective functions
$b:\mathbb{N}_{n}\rightarrow\mathbb{N}_{n}$. the formula $c^{\prime}_{b}(k,n)$
is derivable by resolution from C(n).

###### Proof

See Sec. 9.5.

###### Definition 9

Given $0\leq n$ we define the ordering relation $\lessdot_{n}$ over
$A_{n}=\left\\{(i,j)|i\leq j\right.$ $\left.\wedge 0\leq i,j\leq n\wedge
i,j\in\mathbb{N}\right\\}$ s.t. for $(i,j),(l,k)\in A_{n}$,
$(i,j)\lessdot_{n}(l,k)$ iff $i,k,l\leq n$, $j<n$, $l\leq i$, $k\leq j$, and
$i=l\leftrightarrow j\not=k$ and $j=k\leftrightarrow i\not=l$.

###### Lemma 6

The ordering $\lessdot_{n}$ over $A_{n}$ for $0\leq n$ is a complete well
ordering.

###### Proof

Every chain has a greatest lower bound, namely, one of the members of $A_{n}$,
$(i,n)$ where $0\leq i\leq n$, and it is transitive, anti-reflexive, and anti-
symmetric.

The clauses proved derivable by Lem. 5 can be paired with members of $A_{n}$
as follows, $c^{\prime}_{b}(k,n)$ is paired with $(k,n)$. Thus, each
$c^{\prime}_{b}(k,n)$ is essentially the greatest lower bound of some chain in
the ordering $\lessdot_{n}$ over $A_{n}$.

###### Lemma 7

Given $0\leq k\leq j\leq n$, for all bijective functions
$b:\mathbb{N}_{n}\rightarrow\mathbb{N}_{n}$ the clause $c^{\prime}_{b}(k,j)$
is derivable from C(n).

###### Proof

We will prove this lemma by induction over $A_{n}$. The base cases are the
clauses $c^{\prime}_{b}(k,n)$ from Lem. 5. Now let us assume that the lemma
holds for all clauses $c^{\prime}_{b}(k,i)$ pairs such that, $0\leq k\leq
j<i\leq n$ and for all clauses $c^{\prime}_{b}(w,j)$ such that $0\leq k<w\leq
j\leq n$, then we want to show that the lemma holds for the clause
$c^{\prime}_{b}(k,j)$. We have not made any restrictions on the bijections
used, we will need two different bijections to prove the theorem. The
following derivation provides proof:

$\begin{array}[]{c}(IH[k,j+1])\\\
\Pi_{b}(k),\vdash\Delta_{b}(k,j),P_{b}(j+1)\end{array}$
$\begin{array}[]{c}(IH[k+1,k+1])\\\
\Pi_{b^{\prime}}(k),f(x_{b^{\prime}(k+1)})=b^{\prime}(k+1)\vdash\end{array}$
$res(\sigma,P)$
$\begin{array}[]{c}\Pi_{b}(k),\Pi_{b^{\prime}}(k)\vdash\Delta_{b}(k,j)\end{array}$
$c:l$ $\begin{array}[]{c}\Pi_{b}(k)\vdash\Delta_{b}(k,j)\\\
c^{\prime}_{b}(k,j)\end{array}$

$P_{b}(k+1)=f(m(k,\overline{x}_{k},s(x_{k+1})))=b(k+1)$,

$\Pi_{b}(k)\equiv\bigwedge_{i=0}^{k}f(x_{b(i)})=b(i)$,

$\Delta_{b}(k,j)\equiv\bigvee_{i=k+1}^{j}f(m(k,\overline{x}_{k},s(x_{k+1})))=b(i),$
$\sigma=\left\\{x_{b^{\prime}(k+1)}\leftarrow
m(k,\overline{x}_{k},s(x_{k+1}))\right\\}$

We assume that $b^{\prime}(k+1)=b(j+1)$ and that $b^{\prime}(x)=b(x)$ for
$0\leq x\leq k$.

###### Theorem 7.1

Given $n\geq 0$, $C(n)$ derives $\vdash$.

###### Proof

By Lem. 7, The clauses $f(x)=0\vdash$ , $\cdots$ , $f(x)=n\vdash$ are
derivable. Thus, we can prove the statement by induction on the instantiation
of the clause set. When $n=0$, the clause (C5) is $\vdash f(x)=0$ which
resolves with $f(x)=0\vdash$ to derive $\vdash$. Assuming that for all
$n^{\prime}\leq n$ the theorem holds we now show that it holds for $n+1$. The
clause (C5) from the clause set $C(n+1)$ is the clause (C5) from the clause
set $C(n)$ with the addition of a positive instance of $\vdash
f(\alpha)=(n+1)$. Thus, by the induction hypothesis we can derive the clause
$\vdash f(\alpha)=(n+1)$. By Lem. 7 we can derive $f(x)=(n+1)\vdash$, and
thus, resolving the two derived clauses results in $\vdash$.

##  8 Conclusion

At the end of the introduction, we outlined some essential points to be
addressed in future work, i.e. finding a refutation which fits the framework
of [CERESS2] or showing that it is not possible and constructing a more
expressive language. Concerning the compression (see Sec. 9.7), knowing the
growth rate of the ACNF can help in the construction of a more expressive
language for the refutations, and will be part of the future investigation.
However, there is an interesting points which was not addressed, namely
extraction of a Herbrand system. The extraction of Herbrand system is the
theoretical advantage this framework has over the previously investigated
system [Mcdowell97cut-eliminationfor]444The schematic CERES method has the
subformula property. for cut elimination in the presence of induction, but
without a refutation within the expressive power of the resolution calculus,
the method of [CERESS2] cannot be used to extract a Herbrand system from our
refutation. We plan to investigate the extraction of a Herbrand system for the
NiA-schema given the current state of the proof analysis. Development of such
a method can help find Herbrand systems in other cases when the ACNF-schema
cannot be expressed in the calculus provided in [CERESS2].

##  9 Appendix

###  9.1 Proof of Lem. 1

$\begin{array}[]{c}(Lem.\ref{lem:first})\\\ \vdash P\end{array}$
$\begin{array}[]{c}(C2)\\\
max(\beta,\delta)\leq\gamma\vdash\beta\leq\gamma\end{array}$ $res(\sigma,P)$
$\begin{array}[]{c}\vdash s(x_{k+1})\leq
m(k,\overline{x},max(s(x_{k+1}),t))\end{array}$

$P=max(s(x_{k+1}),t)\leq m(k,\overline{x},max(s(x_{k+1}),t))$
$\sigma=\left\\{\beta\leftarrow s(x_{k+1}),\gamma\leftarrow
m(k,\overline{x},max(s(x_{k+1}),t)),\delta\leftarrow t\right\\}$

$\square$

###  9.2 Proof of Cor. 2

$\begin{array}[]{c}(Cor.\ref{cor:first})\\\ \vdash P\end{array}$
$\begin{array}[]{c}(C4_{i})\\\
f(\alpha)=i,f(\beta)=i,s(\alpha)\leq\beta\vdash\end{array}$ $res(\sigma,P)$
$\begin{array}[]{c}f(x_{k+1})=i,f(m(k,\overline{x}_{k},max(s(x_{k+1}),t)))=i\vdash\end{array}$

$P=s(x_{k+1})\leq m(k,\overline{x}_{k},max(s(x_{k+1}),t))$
$\sigma=\left\\{\alpha\leftarrow x_{k+1},\beta\leftarrow
m(k,\overline{x}_{k},max(s(x_{k+1}),t))\right\\}$

$\square$

###  9.3 Proof of Cor. 3

$\begin{array}[]{c}(Lem.\ref{lem:first})\\\ \vdash P\end{array}$
$\begin{array}[]{c}(C4_{i})\\\
f(\alpha)=i,f(\beta)=i,s(\alpha)\leq\beta\vdash\end{array}$ $res(\sigma,P)$
$\begin{array}[]{c}f(x_{k+1})=i,f(m(k,\overline{x},s(x_{k+1})))=i\vdash\end{array}$

$P=s(x_{k+1})\leq m(k,\overline{x}_{k},s(x_{k+1}))$
$\sigma=\left\\{\alpha\leftarrow x_{k+1},\beta\leftarrow
m(k,\overline{x}_{k},s(x_{k+1})))\right\\}$

$\square$

###  9.4 Proof of Cor. 4

We prove this lemma by induction on $k$ and a case distinction on $n$. When
$n=0$ there are two possible values for $k$, $k=0$ or $k=-1$. When $k=-1$ the
clause is an instance of (C5). When $k=0$ we have the following derivation:

$\begin{array}[]{c}(C5)\\\ c_{b}(-1,1,y)\end{array}$
$\begin{array}[]{c}(Cor.\ref{cor:second}[i\leftarrow b(0),k\leftarrow 0])\\\
f(x_{1})=b(0),f(max(s(x_{1}),z))=b(0)\vdash\end{array}$ $res(\sigma,P)$
$\begin{array}[]{c}c_{b}(0,1,z)\end{array}$

$P=f(max(s(x_{1}),z))=b(0)$ $\sigma=\left\\{y\leftarrow
max(s(x_{1}),z)\right\\}$

By $(Cor.\ref{cor:second}[i\leftarrow b(0),k\leftarrow 0])$ we mean take the
clause that is proven derivable by Cor. 2 and instantiate the free parameters
of Cor. 2, i.e. $i$ and $k$, with the given terms, i.e. $b(0)$ and $0$.
Remember that $b(0)$ can be either $0$ or $1$. We will use this syntax through
out the dissertion. When $n>0$ and $k=-1$ we again trivially have (C5). When
$n>0$ and $k=0$, the following derivation suffices:

$\begin{array}[]{c}(C5)\\\ c_{b}(-1,n,y)\end{array}$
$\begin{array}[]{c}(Cor.\ref{cor:second}[i\leftarrow b(0),k\leftarrow 0])\\\
f(x_{1})=b(0),f(max(s(x_{1}),z))=b(0)\vdash\end{array}$ $res(\sigma,P)$
$\begin{array}[]{c}c_{b}(0,n,z)\end{array}$

$P=f(max(s(x_{1}),z))=b(0)$ $\sigma=\left\\{y\leftarrow
max(s(x_{1}),z)\right\\}$

The main difference between the case for $n=1$ and $n>1$ is the possible
instantiations of the bijection at $0$. In the case of $n>1$, $b(0)=0\
\vee\cdots\vee\ b(0)=n$. Now we assume that for all $w<k+1<n$ and $n>0$ the
theorem holds, we proceed to show that the theorem holds for $k+1$. The
following derivation will suffice:

$\begin{array}[]{c}(IH)\\\ c_{b}(k,n,y)\end{array}$
$\begin{array}[]{c}(Cor.\ref{cor:second}[i\leftarrow b(k+1)])\\\
f(x_{k+1})=b(k+1),P\vdash\end{array}$ $res(\sigma,P)$
$\begin{array}[]{c}c_{b}(k+1,n,z)\end{array}$

$P=f(m(k,\overline{x}_{k},max(s(x_{k+1}),t)))=b(k+1)$
$\sigma=\left\\{y\leftarrow max(s(x_{k+1}),z)\right\\}$

$\square$

###  9.5 Proof of Lem. 5

We prove this lemma by induction on $k$ and a case distinction on $n$. When
$n=0$ it must be the case that $k=0$. When $k=0$ we have the following
derivation :

$\begin{array}[]{c}(C5)\\\ c_{b}(-1,0,y)\end{array}$
$\begin{array}[]{c}(Cor.\ref{cor:third}[i\leftarrow 0,k\leftarrow 0])\\\
f(x_{1})=0,f(s(x_{1}))=0\vdash\end{array}$ $res(\sigma,P)$
$\begin{array}[]{c}c^{\prime}_{b}(0,0)\end{array}$

$P=f(s(x_{1}))=0$ $\sigma=\left\\{y\leftarrow s(x_{1})\right\\}$

Remember that $b(0)$ can only be mapped to $0$. When $n>0$ and $k=0$, the
following derivation suffices:

$\begin{array}[]{c}(C5)\\\ c_{b}(-1,n,y)\end{array}$
$\begin{array}[]{c}(Cor.\ref{cor:third}[i\leftarrow b(0),k\leftarrow 0])\\\
f(x_{1})=b(0),f(s(x_{1}))=b(0)\vdash\end{array}$ $res(\sigma,P)$
$\begin{array}[]{c}c^{\prime}_{b}(0,n)\end{array}$

$P=f(s(x_{1}))=b(0)$ $\sigma=\left\\{y\leftarrow s(x_{1})\right\\}$

The main difference between the case for $n=0$ and $n>0$ is the possible
instantiations of the bijection at $0$. In the case of $n>0$, $b(0)=0\
\vee\cdots\vee\ b(0)=n$. Now we assume that for all $w\leq k$ the theorem
holds, we proceed to show that the theorem holds for $k+1$. The following
derivation will suffice:

$\begin{array}[]{c}(IH)\\\ c_{b}(k,n,y)\end{array}$
$\begin{array}[]{c}(Cor.\ref{cor:second}[i\leftarrow b(k+1)])\\\
f(x_{k+1})=b(k+1),P\vdash\end{array}$ $res(\sigma,P)$
$\begin{array}[]{c}c_{b}(k+1,n,z)\end{array}$

$P=f(m(k,\overline{x}_{k},max(s(x_{k+1}),t)))=b(k+1)$
$\sigma=\left\\{y\leftarrow max(s(x_{k+1}),z)\right\\}$

$\square$

###  9.6 SPASS Refutation of $C(n)$: Instance Four

The refutation provided in this section is almost identical to the output from
SPASS except for a few minor changes to the syntax to aid reading.

$1[0:Inp]\ \|\|\ \Rightarrow\ eq(f(U),3)\ ,\ eq(f(U),2)\ ,\ eq(f(U),1)\ ,\
eq(f(U),0)*$

$2[0:Inp]\ \|\|\ \Rightarrow\ le(U,U)*$

$3[0:Inp]\ \|\|\ le(max(U,V),W)*\ \Rightarrow\ le(U,W)$

$4[0:Inp]\ \|\|\ le(max(U,V),W)*\ \Rightarrow\ le(V,W)$

$5[0:Inp]\ \|\|\ le(s(U),V)*+\ ,\ eq(f(U),0)*\ ,\ eq(f(V),0)*\ \Rightarrow$

$6[0:Inp]\ \|\|\ le(s(U),V)*+\ ,\ eq(f(U),1)*\ ,\ eq(f(V),1)*\ \Rightarrow$

$7[0:Inp]\ \|\|\ le(s(U),V)*+\ ,\ eq(f(U),2)*\ ,\ eq(f(V),2)*\ \Rightarrow$

$8[0:Inp]\ \|\|\ le(s(U),V)*+\ ,\ eq(f(U),3)*\ ,\ eq(f(V),3)*\ \Rightarrow$

$9[0:Res:2.0,4.0]\ \|\|\ \Rightarrow\ le(U,max(V,U))$

$10[0:Res:9.0,4.0]\ \|\|\ \Rightarrow\ le(U,max(V,max(W,U)))$

$12[0:Res:2.0,3.0]\ \|\|\ \Rightarrow\ le(U,max(U,V))$

$13[0:Res:9.0,3.0]\ \|\|\ \Rightarrow\ le(U,max(V,max(U,W)))$

$15[0:Res:12.0,3.0]\ \|\|\ \Rightarrow\ le(U,max(max(U,V),W))$

$16[0:Res:12.0,4.0]\ \|\|\ \Rightarrow\ le(U,max(max(V,U),W))$

$19[0:Res:15.0,3.0]\ \|\|\ \Rightarrow\ le(U,max(max(max(U,V),W),X))$

$20[0:Res:15.0,4.0]\ \|\|\ \Rightarrow\ le(U,max(max(max(V,U),W),X))$

$23[0:Res:2.0,8.0]\ \|\|\ eq(f(U),3)\ ,\ eq(f(s(U)),3)*\ \Rightarrow$

$25[0:Res:10.0,8.0]\ \|\|\ eq(f(U),3)\ ,\ eq(f(max(V,max(W,s(U)))),3)*\
\Rightarrow$

$27[0:Res:12.0,8.0]\ \|\|\ eq(f(U),3)\ ,\ eq(f(max(s(U),V)),3)*\ \Rightarrow$

$28[0:Res:15.0,8.0]\ \|\|\ eq(f(U),3)\ ,\ eq(f(max(max(s(U),V),W)),3)*\
\Rightarrow$

$42[0:Res:2.0,7.0]\ \|\|\ eq(f(U),2)\ ,\ eq(f(s(U)),2)*\ \Rightarrow$

$43[0:Res:9.0,7.0]\ \|\|\ eq(f(U),2)\ ,\ eq(f(max(V,s(U))),2)*\ \Rightarrow$

$44[0:Res:10.0,7.0]\ \|\|\ eq(f(U),2)\ ,\ eq(f(max(V,max(W,s(U)))),2)*\
\Rightarrow$

$50[0:Res:12.0,7.0]\ \|\|\ eq(f(U),2)\ ,\ eq(f(max(s(U),V)),2)*\ \Rightarrow$

$52[0:Res:16.0,7.0]\ \|\|\ eq(f(U),2)\ ,\ eq(f(max(max(V,s(U)),W)),2)*\
\Rightarrow$

$54[0:Res:19.0,4.0]\ \|\|\ \Rightarrow\ le(U,max(max(max(max(V,U),W),X),Y))$

$59[0:Res:20.0,7.0]\ \|\|\ eq(f(U),2)\ ,\ eq(f(max(max(max(V,s(U)),W),X)),2)*\
\Rightarrow$

$69[0:Res:2.0,6.0]\ \|\|\ eq(f(U),1)\ ,\ eq(f(s(U)),1)*\ \Rightarrow$

$70[0:Res:9.0,6.0]\ \|\|\ eq(f(U),1)\ ,\ eq(f(max(V,s(U))),1)*\ \Rightarrow$

$74[0:Res:13.0,6.0]\ \|\|\ eq(f(U),1)\ ,\ eq(f(max(V,max(s(U),W))),1)*\
\Rightarrow$

$79[0:Res:16.0,6.0]\ \|\|\ eq(f(U),1)\ ,\ eq(f(max(max(V,s(U)),W)),1)*\
\Rightarrow$

$89[0:Res:2.0,5.0]\ \|\|\ eq(f(U),0)\ ,\ eq(f(s(U)),0)*\ \Rightarrow$

$90[0:Res:9.0,5.0]\ \|\|\ eq(f(U),0)\ ,\ eq(f(max(V,s(U))),0)*\ \Rightarrow$

$98[0:Res:12.0,5.0]\ \|\|\ eq(f(U),0)\ ,\ eq(f(max(s(U),V)),0)*\ \Rightarrow$

$123[0:Res:1.3,89.1]\ \|\|\ eq(f(U),0)\ \Rightarrow\ eq(f(s(U)),3)\ ,\
eq(f(s(U)),2)\ ,\ eq(f(s(U)),1)$

$159[0:Res:54.0,8.0]\ \|\|\ eq(f(U),3)\ ,\
eq(f(max(max(max(max(V,s(U)),W),X),Y)),3)*\ \Rightarrow$

$196[0:Res:1.3,90.1]\ \|\|\ eq(f(U),0)\ \Rightarrow\ eq(f(max(V,s(U))),3)\\\
\\\ eq(f(max(V,s(U))),2)\ ,\ eq(f(max(V,s(U))),1)$

$197[0:Res:1.3,98.1]\ \|\|\ eq(f(U),0)\ \Rightarrow\ eq(f(max(s(U),V)),3)\\\
\\\ eq(f(max(s(U),V)),2)\ ,\ eq(f(max(s(U),V)),1)$

$423[0:Res:196.3,79.1]\ \|\|\ eq(f(U),0)\ ,\ eq(f(V),1)\ \Rightarrow\\\ \\\
eq(f(max(max(W,s(V)),s(U))),3)\ ,\ eq(f(max(max(W,s(V)),s(U))),2)$

$450[0:Res:197.3,74.1]\ \|\|\ eq(f(U),0)\ ,\ eq(f(V),1)\ \Rightarrow\\\ \\\
eq(f(max(s(U),max(s(V),W))),3)\ ,\ eq(f(max(s(U),max(s(V),W))),2)$

$955[0:Res:423.3,59.1]\ \|\|\ eq(f(U),0)\ ,\ eq(f(V),1)\ ,\ eq(f(W),2)\\\ \\\
\Rightarrow\ eq(f(max(max(max(X,s(W)),s(V)),s(U))),3)$

$1009[0:Res:450.3,44.1]\ \|\|\ eq(f(U),0)\ ,\ eq(f(V),1)\ ,\ eq(f(W),2)\\\ \\\
\Rightarrow\ eq(f(max(s(U),max(s(V),s(W)))),3)$

$2272[0:Res:955.3,159.1]\ \|\|\ eq(f(U),0)*\ ,\ eq(f(V),1)*\ ,\ eq(f(W),2)*\\\
\\\ eq(f(X),3)*\ \Rightarrow$

$2273[0:MRR:1009.3,2272.3]\ \|\|\ eq(f(U),0)*+\ ,\ eq(f(V),1)*\\\ \\\
eq(f(W),2)*\ \Rightarrow$

$2301[0:MRR:450.3,2273.2]\ \|\|\ eq(f(U),0)\ ,\ eq(f(V),1)\\\ \\\ \Rightarrow\
eq(f(max(s(U),max(s(V),W))),3)$

$2450[0:Res:2301.2,25.1]\ \|\|\ eq(f(U),0)*\ ,\ eq(f(V),1)*\\\ \\\
eq(f(W),3)*\ \Rightarrow$

$2459[0:MRR:2301.2,2450.2]\ \|\|\ eq(f(U),0)*+\ ,\ eq(f(V),1)*\ \Rightarrow$

$2577[0:MRR:123.3,2459.1]\ \|\|\ eq(f(U),0)\ \Rightarrow\ eq(f(s(U)),3)\\\ \\\
eq(f(s(U)),2)$

$2578[0:MRR:196.3,2459.1]\ \|\|\ eq(f(U),0)\ \Rightarrow\\\
eq(f(max(V,s(U))),3)\ ,\ eq(f(max(V,s(U))),2)$

$2613[0:Res:2578.2,50.1]\ \|\|\ eq(f(U),0)\ ,\ eq(f(V),2)\ \Rightarrow\
eq(f(max(s(V),s(U))),3)$

$2615[0:Res:2578.2,52.1]\ \|\|\ eq(f(U),0)\ ,\ eq(f(V),2)\\\ \Rightarrow\
eq(f(max(max(W,s(V)),s(U))),3)$

$2676[0:Res:2615.2,28.1]\ \|\|\ eq(f(U),0)*\ ,\ eq(f(V),2)*\ ,\ eq(f(W),3)*\
\Rightarrow$

$2684[0:MRR:2613.2,2676.2]\ \|\|\ eq(f(U),0)*+\ ,\ eq(f(V),2)*\ \Rightarrow$

$2714[0:MRR:2577.2,2684.1]\ \|\|\ eq(f(U),0)\ \Rightarrow\ eq(f(s(U)),3)$

$2715[0:MRR:2578.2,2684.1]\ \|\|\ eq(f(U),0)\ \Rightarrow\
eq(f(max(V,s(U))),3)$

$2749[0:Res:2715.1,27.1]\ \|\|\ eq(f(U),0)*\ ,\ eq(f(V),3)*\ \Rightarrow$

$2764[0:MRR:2714.1,2749.1]\ \|\|\ eq(f(U),0)*\ \Rightarrow$

$2795[0:MRR:1.3,2764.0]\ \|\|\ \Rightarrow\ eq(f(U),3)\ ,\ eq(f(U),2)\ ,\
eq(f(U),1)$

$2796[0:Res:2795.2,69.1]\ \|\|\ eq(f(U),1)\ \Rightarrow\ eq(f(s(U)),3)\ ,\
eq(f(s(U)),2)$

$2797[0:Res:2795.2,70.1]\ \|\|\ eq(f(U),1)\ \Rightarrow\
eq(f(max(V,s(U))),3)\\\ eq(f(max(V,s(U))),2)$

$2831[0:Res:2797.2,50.1]\ \|\|\ eq(f(U),1)\ ,\ eq(f(V),2)\\\ \Rightarrow\
eq(f(max(s(V),s(U))),3)$

$2833[0:Res:2797.2,52.1]\ \|\|\ eq(f(U),1)\ ,\ eq(f(V),2)\\\ \Rightarrow\
eq(f(max(max(W,s(V)),s(U))),3)$

$2896[0:Res:2833.2,28.1]\ \|\|\ eq(f(U),1)*\ ,\ eq(f(V),2)*\ ,\ eq(f(W),3)*\
\Rightarrow$

$2904[0:MRR:2831.2,2896.2]\ \|\|\ eq(f(U),1)*+\ ,\ eq(f(V),2)*\ \Rightarrow$

$2934[0:MRR:2796.2,2904.1]\ \|\|\ eq(f(U),1)\ \Rightarrow\ eq(f(s(U)),3)$

$2935[0:MRR:2797.2,2904.1]\ \|\|\ eq(f(U),1)\ \Rightarrow\
eq(f(max(V,s(U))),3)$

$2969[0:Res:2935.1,27.1]\ \|\|\ eq(f(U),1)*\ ,\ eq(f(V),3)*\ \Rightarrow$

$2984[0:MRR:2934.1,2969.1]\ \|\|\ eq(f(U),1)*\ \Rightarrow$

$3015[0:MRR:2795.2,2984.0]\ \|\|\ \Rightarrow\ eq(f(U),3)\ ,\ eq(f(U),2)$

$3016[0:Res:3015.1,42.1]\ \|\|\ eq(f(U),2)\ \Rightarrow\ eq(f(s(U)),3)$

$3017[0:Res:3015.1,43.1]\ \|\|\ eq(f(U),2)\ \Rightarrow\ eq(f(max(V,s(U))),3)$

$3050[0:Res:3017.1,27.1]\ \|\|\ eq(f(U),2)*\ ,\ eq(f(V),3)*\ \Rightarrow$

$3065[0:MRR:3016.1,3050.1]\ \|\|\ eq(f(U),2)*\ \Rightarrow$

$3096[0:MRR:3015.1,3065.0]\ \|\|\ \Rightarrow\ eq(f(U),3)$

$3098[0:MRR:23.1,23.0,3096.0]\ \|\|\ \Rightarrow$

###  9.7 Growth Rate of Refutation

###### Definition 10

Let $Occ(x,r)$ be defined as the number of times the clause $x$ is used in the
refutation $r$.

###### Theorem 9.1

Let $r$ be the resolution refutation of Thm. 7.1 for the clause set $C(n)$,
then $Occ(C5,r)$ is the result of the following recurrence relation
$a(n+1)=(n+1)*a(n)+1$ and $a(0)=1$.

###### Proof

Let us consider the case for the clause set $C(0)$. This is the case when we
have only one symbol in the function’s range. If we compute the recurrence we
get $a(1)=a(0)+1=2$ Now let us assume it holds for all $m\leq n$ and show it
hold for $n+1$. In the proof of Lem. 7, when deriving $c^{\prime}_{b}(0,0)$
the literal $f(\alpha)=b(0)$ is in the antecedent for every clause higher in
the resolution derivation and it is never used in a resolution step . If we
remove this clause from the antecedent then we have a resolution refutation
for the clause $C(n)$, only if we rename the schematic sort terms accordingly.
To refute $C(n+1)$ we need to derive $n+1$ distinct $c^{\prime}_{b}(0,0)$
clauses and resolve them with a single instance of $(C5)$. Thus, we have the
equation, $Occ(C5^{n+1},r_{n+1})=(n+1)*Occ(C5^{n},r_{n})+1$ where $r_{n+1}$ is
the resolution refutation of Thm. 7.1 for the clause set $C(n+1)$ and $r_{n}$
is the resolution refutation of Thm. 7.1 for the clause set $C(n)$. Thus, the
theorem holds by induction.
$\square$

###### Corollary 4

The recurrence relation $a(n)=n\cdot a(n-1)+1$ and $a(0)=1$ is equivalent to
the equation:

$f(n)=n!\cdot\sum_{i=0}^{n}\frac{1}{i!}$

###### Proof

If we unroll the relation one we get,

$a(n)=n\cdot(n-1)\cdot a(n-2)+n+1=n\cdot(n-1)\cdot
a(n-2)+\frac{n!}{(n-1)!}+\frac{n!}{n!}$

Thus, unrolling the function $k$ times results in the following:

$a(n)=\left(\prod^{n}_{i=n-k+1}i\right)\cdot
a(n-k)+\sum^{n}_{i=n-k+1}\frac{n!}{i!}$

Now when we set $k=n$ we get,

$a(n)=n!+\sum^{n}_{i=1}\frac{n!}{i!}=\frac{n!}{0!}+\sum^{n}_{i=1}\frac{n!}{i!}=\sum^{n}_{i=0}\frac{n!}{i!}$

$\square$


# Case study of SARS-CoV-2 transmission risk assessment in indoor environments
using cloud computing resources

Kumar Saurabh
Masado Ishii
Hari Sundar
Iowa State University
Email<EMAIL_ADDRESS>University of Utah
Email<EMAIL_ADDRESS>University of Utah
Email<EMAIL_ADDRESS>Santi Adavani
Boshun Gao
RocketML Inc.
Email<EMAIL_ADDRESS>Iowa State University
Email<EMAIL_ADDRESS>Kendrick Tan
Adarsh Krishnamurthy
Baskar Ganapathysubramanian  Iowa State University
Email<EMAIL_ADDRESS>Iowa State University
Email<EMAIL_ADDRESS>Iowa State University
Email<EMAIL_ADDRESS>
###### Abstract

Complex flow simulations are conventionally performed on HPC clusters.
However, the limited availability of HPC resources and steep learning curve of
executing on traditional supercomputer infrastructure has drawn attention
towards deploying flow simulation software on the cloud. We showcase how a
complex computational framework–that can evaluate COVID-19 transmission risk
in various indoor classroom scenarios–can be abstracted and deployed on cloud
services. The availability of such cloud-based personalized planning tools can
enable educational institutions, medical institutions, public sector workers
(courthouses, police stations, airports, etc.), and other entities to
comprehensively evaluate various in-person interaction scenarios for
transmission risk. We deploy the simulation framework on the Azure cloud
framework, utilizing the Dendro-KT mesh generation tool and PETSc solvers. The
cloud abstraction is provided by RocketML cloud infrastructure. We compare the
performance of the cloud machines with state-of-the-art HPC machine TACC
Frontera. Our results suggest that cloud-based HPC resources are a viable
strategy for a diverse array of end-users to rapidly and efficiently deploy
simulation software.

##  I Motivation

Current and next-generation high-performance computing (HPC) resources play a
pivotal role in helping answer many of the fundamental questions related to
science and technology. However, the limited availability of HPC resources,
along with the steep learning curve needed to employ these resources
effectively, have limited the utilization of HPC resources to academic and
large industrial R&D groups. Additionally, standard HPC resource utilization
policies restrict the number of nodes available to the user and the number of
job instances per user. These limitations become a bottleneck, especially in
risk assessment and design exploration, where parametric studies need to be
performed that involve executing multiple instances of the simulation with
different simulation inputs. In this context, the availability of on-demand
cloud services suggests an attractive alternative for adaptive, interactive
scientific computing workloads.

The ubiquitous availability of cloud computing suggests a path to the
democratization of complex multi-physics simulations. Simulations–for example,
parametric studies of ventilation rates and seating arrangements in critical
public places such as courthouses, hospital waiting rooms, etc. to evaluate
transmission risk–are currently limited to deployment on HPC clusters that
require a steep learning curve to deploy, which disenfranchises non-computer
savvy scientists, decision-makers, and designers. Additionally, the data
visualization and analysis can be done in-situ without copying data from one
place to another. In this work, we propose a public cloud-based framework with
in-situ visualization and post-processing capabilities for scalable deployment
of fluid dynamics simulation using FEM discretization. Our results suggest
that the performance of such a framework is at par, if not better, with the
framework executed on state-of-the-art HPC resources.

##  II Background

A large fraction of engineered and natural systems are analyzed using
scientific simulation codes that involve numerical solutions of partial
differential equations (PDE). The Finite Element Method (FEM) is a widely
popular approach for the numerical solution of PDEs in complex domains, with
multiple $ billions/year spent in CAD and CAM (computer-aided design and
manufacturing) based FEM software alone [1]. The popularity arises from a
compelling set of properties, including the ability (a) to model arbitrary
geometries, (b) to change the order of representation (linear, quadratic, and
higher-order), (c) to utilize variational arguments that guarantee monotonic
convergence to the solution with improved discretization, and (d) to
seamlessly utilize a posteriori error estimates to adapt the mesh. Over the
past several years, we have developed a scalable FEM solver based on adaptive
octree mesh and deployed this framework for a diverse array of multi-physics
simulations–primarily on HPC resources [2, 3, 4, 5, 6, 7, 8].

In this work, we explore the deployment (and assess performance) of this FEM
framework on a public cloud computing facility. Cloud computing provides on-
demand access to computing resources, data storage, development, and
networking facilities via the internet. Cloud computing offers some key
benefits compared to the traditional HPC settings, in particular:

  * •

Lower IT costs: Cloud facilities enable the offloading of some or most of the
costs and effort of purchasing, installing, configuring, and managing on-
premises infrastructure. This can be especially significant for small research
groups.

  * •

Scale on demand: Instead of purchasing the capacity and waiting for the
arrival of hardware, the cloud enables on-demand access and elastic
scalability.

  * •

Choice of architecture: Cloud allows to choose from different types of
architecture, depending on the nature of codes. Some computer architectures
are tailored for compute-bound codes, whereas others provide good performance
for memory-bound codes. A traditional HPC cluster usually has limited
flexibility in terms of the availability of different types of machines. In
contrast, cloud computing allows the flexibility to choose the machines based
on the nature of the underlying code (compute-bound vs. memory-bound vs.
communication-bound).

  * •

End-to-end deployment: Cloud enables the full stack of software, starting from
development to testing to execution to visualization. The latter
aspect–visualization–is particularly appealing, as it allows for in-situ
visualization and analysis without extensive data movement. We note that some
federal HPC clusters, like TACC, have a dedicated visualization portal but are
not accessible on all of them.

In this paper, we seek to address the following three components of the
workshop:

  * •

On-demand and interactivity with performance, scaling, and cost efficiencies;

  * •

Application environment, integration and deployment technologies;

  * •

Workflow orchestration using public cloud and HPC data center resources.

##  III Problem Definition

COVID-19 has irreversibly changed how we consider transmission risk in indoor
environments. The Six-Foot Rule, for instance, is a guideline that does not
account for small aerosol droplets that are continuously mixed through an
indoor space. The distribution of aerosolized particles depends on a wide
array of factors (ventilation, airflow patterns that are impacted by
furniture, as well as the respiratory activity of the inhabitants. While
conventional risk assessment tools may indicate that a particular room is low-
risk on average, there may be specific locations in the room with
significantly higher risk for transmission–for example, where there is local
recirculation causing limited air exchange with the outside environment.
Assessing the localized risk becomes especially important if individuals are
seated in such locations for extended periods, increasing their cumulative
exposure time. We consider scenarios that impact first-responders, essential
workers, and K-12 students. For instance, courthouse activities require
participants (judges, clerks, petitioners, jurors) to remain sedentary over
long periods. Similarly, most classroom activities require K-12 students to
stay seated for extended periods. In such cases, it becomes imperative to
identify if specific locations have a higher risk and rank among alternate
seating arrangements.

In this context, high fidelity fluid/aerosol simulation is a viable approach
to evaluate various seating and operating scenarios, identify risk factors,
and rank order mitigation strategies. We aim to democratize such simulations
on cloud-based resources by integrating four sophisticated concepts to provide
very detailed estimates of aerosol distribution in indoor environments: (a) a
detailed flow physics simulation (called Large Eddy Simulations) that produces
significantly more accurate results while taking reasonable compute time, (b)
accounting for the thermal plumes created by heat released by humans and
electronics (which changes the flow in rooms), (c) immersogeometric analysis
that allows rapid exploration of a diverse array of configurations with
complex geometries, (d) a passive scalar transport based model that tracks the
spatial distribution of the aerosolized concentration. To our best knowledge,
parametric simulations of such high-fidelity simulations have not been
deployed on the cloud. The availability of such a cloud-based analysis
approach will allow education administrators (K-12), federal/state/local
government officials (courthouses, police stations), and hospital
administrators to make informed decisions on seating arrangements and
operating procedures.

In this work, we use Dendro-KT for efficient and automatic mesh generation.
Dendro-KT is an extension of previous Dendro versions to incomplete octrees.
Tree-based grid generation (quadtrees in 2D and octrees in 3D) is common in
computational sciences [9, 10, 4, 11, 12, 13, 14, 15, 16] largely due to its
simplicity and parallel scalability. The ability to efficiently refine (and
coarsen) regions of interest using tree-based data structures have made it
possible to deploy them on large-scale multi-physics simulations [17, 3, 4, 2,
18, 19, 20, 21]. The use of incomplete octrees enables the handling of any
arbitrary complex geometries, where the stated geometry is carved out from the
domain (Fig. 1). The framework’s simplicity and robustness lie in the fact
that complete mesh generation only needs a specification of In or Out (of the
geometry) for any queried point. Furthermore, the efficient matvec computation
is performed by traversing the trees rather than using any mesh-based data
structure to prevent indirect memory access.

(a) immersed

(b) carved out

Figure 1: Difference between the adaptive mesh for immersed and carved out for
the sphere case. In immersed case, we retain the full octree and this gives to
a significantly large number of elements and nodes compared to the carved out
case. It must be noted the elements that are inside the object do not
contribute to the accuracy of the solution. Eventually Dirichlet Boundary
condition are imposed on all the Innodes.

Once the mesh is created, we model the time-dependent transmission of the
viral load as a scalar transport equation that is advected by a statistically
steady-state flow field obtained from the solution of coupled Navier–Stokes
and Heat transfer solver. The well-established Variational Multiscale (VMS)
FEM [22] is used for the discretization. Dendro-KT interfaces with PETSc for
solving the system of equations. We have recently extensively validated and
demonstrated the capabilities of this framework [3, 8].

##  IV Workflow

In this section, we detail and demonstrate the deployment of our framework on
the cloud infrastructure.

###  IV-A Cloud Abstraction

Our target user for a cloud orchestrator is a researcher who has experience
using an HPC cluster at a university or a national lab and has never used
cloud computing. Ease-of-use and flexibility of using public cloud computing
resources are the two most important requirements. Specifically, a cloud
orchestrator that provides a graphical user interface (GUI) to 1) deploy and
manage CPU- and GPU-based HPC clusters pre-installed with MPI, BLAS/LAPACK,
and PETSc libraries along with a Slurm scheduler to simplify job management,
2) access to different IDEs like Jupyter Lab, VSCode for coding, compiling,
and debugging HPC software, and 3) access to visualization software like
Paraview for _in situ_ data visualization. We have explored several options
available on Microsoft Azure and AWS marketplaces [23, 24] and concluded that
they either lack in ease-of-use or flexibility necessary for a researcher who
has no exposure to cloud computing to conduct large-scale HPC experiments. In
Figure 2, we show different components of RocketML’s cloud orchestrator that
has been purpose-built to address a researcher’s needs to take complete
advantage of HPC on a public cloud for scientific computing applications.

Figure 2: RocketML cloud orchestrator for large-scale CFD simulations.

###  IV-B Mesh Creation

We first begin with mesh creation. As mentioned in Section II, Dendro-KT
framework requires the specification of In and Out for a given queried point.
The In-Out test is performed using Ray-Tracing. The input geometries are
provided in the form of a .stl file format. Several instances of the same
geometry, translated by some distance, can be grouped. An example of a config
file for such an operation is:

      geometries = (
      {
      mesh_path = "stl/human.stl"
      displacements = (
      {position = [0.65,0.0,0.8125]},
      {position = [1.625,0.0,0.73125]},
      )
      refine_lvl = 9
    })

where displacements are the shift from original position of .stl and
refine_lvl is the refinement level of the octree near the .stl. The octree
generation starts with a coarse mesh and is subsequently refined until the
required resolution is satisfied. We can similarly add multiple geometries.
This approach gives an automated way to generate mesh for different scenarios.
In the future, we plan to interface it with a GUI, where an application
scientist can use the drag-and-drop feature to add multiple objects or to
select the refine regions. Fig. 3 shows the adaptive mesh generated for the
classroom case.

Figure 3: Computation domain and adaptive mesh generated from Dendro-KT
framework.

###  IV-C Solver

We use PETSc as the linear solver for solving the system of equation AX=b.
PETSc is a very well validated scalable linear algebra solver, which has a
rich collection of preconditioners and solvers. Different PETSc options are
configurable from the config file itself. An example is shown below:

    solver_options_ht = {
      ksp_max_it = 500
      ksp_type = "bcgs"
      pc_type = "asm"
      ksp_atol = 1e-15
      ksp_rtol = 1e-15
      ksp_converged_reason = ""
    }

###  IV-D File I/O

We use a parallel .vtu file format to write the data into the file at the
user-defined interval. .vtu is an XML file format which enable a communication
free write. Each processor writes its share of data in a separate file. All
these files are later joined by another single .pvtu file, which is written by
$0^{th}$ rank processor.

###  IV-E Checkpointing

Machine failure is a common scenario when executing simulations on HPC
servers. Dendro-KT dumps the checkpoint file at user-defined intervals to keep
a backup of the solutions. The checkpoint files are binary files that contain
information about octree tree nodes and the solution vector. Similarly, to
file I/O, each processor dumps its chunk of data in a communication - free
fashion. If the code is killed for whatsoever reason, the user can restart the
simulation by loading the checkpoint file.

Additionally, the user has the option to increase the number of nodes once the
checkpoint is loaded. Dendro-KT will re-partition the domain if the number of
processors is increased. At this point, we have not implemented the ability to
restart with a decreased number of processors.

###  IV-F Visualization

We have deployed ParaView within the cloud framework for in-situ visualization
and related data–analysis. ParaView comes with pvpython (serial version) and
pvbatch (parallel version) which provide a seamless python interface.

As noted earlier, we rely on the config.txt file to pass input operation to
the code. In future, we plan to replace it with a GUI interface hosted on the
cloud platform for better interaction with the application user.

##  V Results

###  V-A Roofline Analysis

Figure 4: Figure showing roofline plot for the matvec for linear basis
function for two different meshes on Frontera. The plot was generated using
Intel Advisor.

As the first step, we conducted a roofline analysis on Frontera using Intel
advisor to check whether the framework is compute-bound or memory-bound.
Identifying this is important to identify and specify the type of cloud
machines for deploying the framework. Fig. 4 shows the single-core roofline
plot for the elemental matvec computation using linear basis function on
Frontera. We limit ourselves to using linear basis functions as this mimics
our application problem. We can see that the code is memory-bound, which is
along the lines of what we expect for any finite element code. Overall, we can
achieve a performance of about 4 GFLOP/s with an Arithmetic Intensity of
0.072, which corresponds to a bandwidth of approximately 60 GB/s.

######  Remark.

We have not used any hand-coded explicit vectorization to ensure the
portability of the code across various platforms and have relied on compiler
directives for vectorization.

###  V-B Performance on the Cloud

Based on the roofline analysis discussed in the previous section, we chose
Azure virtual machines that are suited for memory-bound computational
problems. This is an additional benefit of using cloud, where we can opt for a
virtual machine with specific hardware configuration based on computational
complexity of the problem at hand (memory-bound vs. compute-bound).
Specifically, we chose the Azure Da and HBv2 series virtual machines that are
built for memory-bound codes and compared the time-to-solution with the state-
of-the-art HPC cluster Frontera. Tab. I provides the functional specifications
of Frontera and virtual machines on cloud.

TABLE I: Functional specifications of CPUs on Microsoft Azure and Frontera.  Specification | Da-series | HBv2-series | Frontera
---|---|---|---
CPU |  | AMD EPYC
---
7452
| AMD EPYC
---
7V12
| Intel Xeon
---
Platinum 8280
Virtual CPU cores | 96 | 120 | 56
Physical cores | 48 | 120 | 56
Memory (GB) | 384 | 450 | 192
Clock rate (GHz) | 2.35 | 3.3 | 2.7

Scaling behavior comparison: To study the scaling behavior and time comparison
of our solver on these machines, we consider the classroom case (shown in Fig.
3) and solve the Navier–Stokes equation coupled with Heat Transfer. In both
the azure machines (Da series and HBV2 series), we only used 50% of the
available CPU cores per node (48 for Da series and 60 for HBv2 series)
mentioned in the Tab. I. We note that the specs take the hyper-threading into
account for Da-series with 2 threads per core. Since our code is only MPI
parallelized, we are able to use only half of the available cores. On Frontera
we used all 56 cores available per node. The overall mesh for scaling analysis
consisted of around 790 K elements with higher refinement near the body
(mannequin/tables) and inlet regions. We compared the three main components of
the solver: matrix assembly, vector assembly, and the total solve time. Fig. 5
shows the parallel cost (defined as total time multiplied by the number of
nodes used) and time taken on these three different machines. A straight line
parallel to X-axis indicates ideal scaling. We can see that the cloud machines
take significantly less time than Frontera, with the HBv2 series taking the
least amount of time. In particular, 10 time steps of the solver took 432s on
1 node of Frontera, while it took 132s on 1 node of HBv2 series machine.

Figure 5: Strong scaling for Navier Stokes + Heat Transfer:  Figure showing
the parallel cost (time $\times$ nodes) variation with increase in the number
of nodes. A straight line parallel to X-axis indicates ideal scaling.

Figure 6: Effect of memory bandwidth  Time comparison for different
distribution of processor across nodes. Total number of processor was kept
constant to 120, whereas the number of processor per node was varied.

(a) t=2s

(b) t=5s

(c) t=25s

(d) t=150s

(e) t=300s

(f) t=450s

Figure 7: Time evolution of the viral load concentration of the air due to a
simulated cough by a mannequin.

Explanation of observed scaling behavior: The two main architectural factors
responsible for the difference between Azure machines and Frontera are memory
bandwidth and cache size. The total peak memory bandwidth on the HBv2 node is
about 340GB/s and around 210GB/s on a Frontera CLX node. For memory-bound
workloads like CFD simulations, the higher memory bandwidth on the HBv2 node
would result in a better solve time. Each AMD EPYC 7742 CPU in HBv2 VMs has
256MB of L3 cache divided across 16 core complexes with four cores each (4MB
L3 per core, 4.5MB L2+L3 per core). Conversely, the Intel 8280 has only 38.5MB
of L3 cache (1.4MB L3 per core, 2.4MB L2+L3 per core). Codes that benefit from
high cache reuse would enormously benefit from the AMD Zen2 architecture,
resulting in a much higher “effective” memory bandwidth. This indicates that
an educated choice of the architecture for the code can lead to a significant
boost in the performance. Such flexibility is offered only by cloud, and not
on traditional HPC based clusters.

######  Remark.

We note that our code is general-purpose and does not contain any explicit
vectorization cache blocking or streaming operation, ensuring code
portability. This approach is common in most of the FEM / fluid dynamics code.
Explicit optimization such as vectorization/cache blocking can significantly
boost the time to solve but comes at the cost of portability on different
machines. Comparing the performance of hardware-specific optimized codes on
these machines is beyond the scope of the work.

Parallel efficiency: We also see a good parallel efficiency on all these
machines. Overall Frontera provides the best parallel efficiency (0.88) with
the solve time decreasing from 432s on 1 node to 122s on 4 nodes. The cloud
machines have a relatively low parallel efficiency of about 0.65. The
deviation from ideal scaling can be attributed to the increased iteration
count for the preconditioned solve. Interested readers are referred to [3] for
detailed discussion. Briefly, it is expected that bare-metal HPC servers will
have better parallel efficiency than virtual-machine-based cloud HPC servers
due to increased communication costs across nodes. Optimizing multi-node VM-
based HPC servers suggests the need to deploy new algorithms that minimizes
communication at the cost of increased (and/or redundant) computations.

Memory bandwidth effect: Memory bandwidth plays a pivotal role in overall
solve time, especially for memory bound codes. Therefore, we compare the
effect of memory bandwidth on our solver. The number of processors is kept
constant at 120, whereas the number of nodes is varied from 1 to 4 with a
varying number of processors per node. Note that 4 nodes have 30 processors
per node, and 1 node has 120 processors. With the increase in the number of
processors per node, the memory bandwidth per core decreases. For instance, on
the HB120rs_v2 (HBV series) machine, the memory bandwidth per core decreases
from 11.50 GB/s when using 30 cores/node to 2.88 GB/s while using all 120
cores. [25]. Fig. 6 shows the effect of the memory bandwidth of our solver. We
see a strong correlation between memory bandwidth and solve time. With the
increase in the memory bandwidth, the solve time decreases from around 112 s
with 120 cores/node to 80 s on 30 cores/node. However, we note that this
reduction in time comes at an increased cost of utilizing more nodes.

##  VI Application Results

(a) Without computer monitors

(b) With computer monitors

(c) Everyone wearing masks

(d) Increased occupancy

Figure 8: Classroom scenario: Evaluation of inhaled particles in different
classroom scenarios. The mannequin marked in the red is infected with COVID
and transmits the virus. The isocontours represent the regions of different
inhaled particle concentrations in space.

In this section, we illustrate results of our application case. We consider a
typical university classroom as illustrated in Fig. 3. The room has a length
of 9 ${m}$, a width of 9 ${m}$, and a height of 3.5 ${m}$ with a ventilation
system installed on the ceiling. The occupants are modeled using mannequins. A
representative resolved mesh is shown as an inset in this figure. The Reynolds
number based on the inlet air velocity and classroom height is estimated to be
$10^{5}$. The spatial discretization was performed using linear basis function
and the time discretization was performed using second order BDF2. A
dimensionless timestep of 1E-3 was used to carry out the simulation. Each
scenerio takes up to a final time of 2 dimensionless time units to reach the
stationary steady state (2K timestep), which required about a day of compute
time on HBV2 series machine. This resulted in the total cost of $ 340 for
simulating each scenario.

We evaluate the impact of one infected individual who coughs, releasing an
aerosolized load of viral particles. Fig. 7 plots the time evolution of the
viral load concentration of the air due to a simulated cough by a mannequin.
Notice that the aerosolized concentration plume rises and is recirculated by
the inlet air. The mixing with the inlet air dilutes the virus concentration,
but the inlet air helps spread the concentration across the room, potentially
impacting everyone in the classroom.

Finally, Fig. 8 shows the isocontours of viral particles concentration (at one
time-point) for different operating scenarios. We compare the different
scenarios in the classroom with (Fig. 8(a)) and without (Fig. 8(b)) monitors,
increased occupancy (Fig. 8(d)) and the situation where everyone wears a mask
(Fig. 8(c)). The mannequin colored in red is the infected person. The regions
of contours with inhaled particles $>$ 50 [26] are considered at a high risk
of transmission. We can see different scenarios lead to significantly
different regions of risk. Additionally, the wearing of masks significantly
reduced the risk of transmission and should therefore be encouraged. We defer
a detailed analysis and implication of these results to a companion
publication.

##  VII Conclusions

In this work, we deploy a scalable, adaptive framework on the cloud utilizing
Dendro-KT as a mesh generation tool and PETSc as a scalable linear algebra
solver to analyze the risk of COVID-19 transmission in different classroom
scenarios. The problem utilizes running different simulation instances, which
are easily deployable in a cloud-based setting. Further, we analyzed the
performance of the cloud-based resources to the state-of-the-art
supercomputer, specifically Frontera. With the proper choice of cloud
machines, we observe on par performance on the cloud, if not better, with the
supercomputers. This suggests that cloud based VM HPC servers offer a viable
approach to democratize and deploy complex simulation workflows. In the
future, we would like to simplify the deployment of the use-cases with more
GUI-friendly interfaces.

##  VIII Acknowledgments

We acknowledge partial support from NSF 1855902.

## References

  * [1] J. A. Cottrell, T. J. Hughes, and Y. Bazilevs, _Isogeometric analysis: toward integration of CAD and FEA_. John Wiley & Sons, 2009.
  * [2] M. A. Khanwale, K. Saurabh, M. Fernando, V. M. Calo, J. A. Rossmanith, H. Sundar, and B. Ganapathysubramanian, “A fully-coupled framework for solving cahn-hilliard navier-stokes equations: Second-order, energy-stable numerical methods on adaptive octree based meshes,” _arXiv preprint arXiv:2009.06628_ , 2020.
  * [3] K. Saurabh, B. Gao, M. Fernando, S. Xu, M. A. Khanwale, B. Khara, M.-C. Hsu, A. Krishnamurthy, H. Sundar, and B. Ganapathysubramanian, “Industrial scale large eddy simulations with adaptive octree meshes using immersogeometric analysis,” _Computers & Mathematics with Applications_, vol. 97, pp. 28–44, 2021.
  * [4] M. Fernando, D. Neilsen, H. Lim, E. Hirschmann, and H. Sundar, “Massively parallel simulations of binary black hole intermediate-mass-ratio inspirals,” _SIAM Journal on Scientific Computing_ , vol. 41, no. 2, pp. C97–C138, 2019.
  * [5] S. Xu, B. Gao, A. Lofquist, M. Fernando, M.-C. Hsu, H. Sundar, and B. Ganapathysubramanian, “An octree-based immersogeometric approach for modeling inertial migration of particles in channels,” _Computers & Fluids_, vol. 214, p. 104764, 2021.
  * [6] D. Neilsen, M. Fernando, H. Sundar, E. Hirschmann, and H. Lim, “Massively parallel simulations of binary black hole intermediate-mass-ratio inspirals,” _APS_ , vol. 2018, pp. D14–005, 2018.
  * [7] D. Neilsen, M. Fernando, H. Sundar, and E. Hirschmann, “Dendro-gr: A scalable framework for adaptive computational general relativity on heterogeneous clusters,” in _APS April Meeting Abstracts_ , vol. 2019, 2019, pp. G11–003.
  * [8] K. Saurabh, M. Ishii, M. Fernando, B. Gao, K. Tan, M.-C. Hsu, A. Krishnamurthy, H. Sundar, and B. Ganapathysubramanian, “Scalable adaptive pde solvers in arbitrary domains,” _arXiv preprint arXiv:2108.03757_ , 2021.
  * [9] T. Tu, D. R. O’Hallaron, and O. Ghattas, “Scalable parallel octree meshing for terascale applications,” in _SC’05: Proceedings of the 2005 ACM/IEEE conference on Supercomputing_. IEEE, 2005, pp. 4–4.
  * [10] M. Ishii, M. Fernando, K. Saurabh, B. Khara, B. Ganapathysubramanian, and H. Sundar, “Solving pdes in space-time: 4d tree-based adaptivity, mesh-free and matrix-free approaches,” in _Proceedings of the International Conference for High Performance Computing, Networking, Storage and Analysis_ , 2019, pp. 1–61.
  * [11] H. Sundar, R. S. Sampath, and G. Biros, “Bottom-up construction and 2: 1 balance refinement of linear octrees in parallel,” _SIAM Journal on Scientific Computing_ , vol. 30, no. 5, pp. 2675–2708, 2008.
  * [12] P. Bastian, M. Blatt, A. Dedner, C. Engwer, R. Klöfkorn, M. Ohlberger, and O. Sander, “A generic grid interface for parallel and adaptive scientific computing. part i: abstract framework,” _Computing_ , vol. 82, no. 2-3, pp. 103–119, 2008.
  * [13] D. M. Greaves and A. Borthwick, “Hierarchical tree-based finite element mesh generation,” _International Journal for Numerical Methods in Engineering_ , vol. 45, no. 4, pp. 447–471, 1999.
  * [14] M. Bader, _Space-filling curves: an introduction with applications in scientific computing_. Springer Science & Business Media, 2012, vol. 9.
  * [15] C. Burstedde, L. C. Wilcox, and O. Ghattas, “p4est: Scalable algorithms for parallel adaptive mesh refinement on forests of octrees,” _SIAM Journal on Scientific Computing_ , vol. 33, no. 3, pp. 1103–1133, 2011\.
  * [16] S. Popinet, “Gerris: a tree-based adaptive solver for the incompressible euler equations in complex geometries,” _Journal of Computational Physics_ , vol. 190, no. 2, pp. 572–600, 2003.
  * [17] M. W. Akhtar and S. J. Kleis, “Boiling flow simulations on adaptive octree grids,” _International journal of multiphase flow_ , vol. 53, pp. 88–99, 2013.
  * [18] J. Rudi, A. C. I. Malossi, T. Isaac, G. Stadler, M. Gurnis, P. W. Staar, Y. Ineichen, C. Bekas, A. Curioni, and O. Ghattas, “An extreme-scale implicit solver for complex pdes: highly heterogeneous flow in earth’s mantle,” in _Proceedings of the international conference for high performance computing, networking, storage and analysis_ , 2015, pp. 1–12.
  * [19] J. Bielak, O. Ghattas, and E. Kim, “Parallel octree-based finite element method for large-scale earthquake ground motion simulation,” _Computer Modeling in Engineering and Sciences_ , vol. 10, no. 2, p. 99, 2005.
  * [20] F. Losasso, F. Gibou, and R. Fedkiw, “Simulating water and smoke with an octree data structure,” in _ACM SIGGRAPH 2004 Papers_ , 2004, pp. 457–462.
  * [21] E. Kim, J. Bielak, and O. Ghattas, “Large-scale northridge earthquake simluation using octree-based multiresolution mesh method,” in _Proceedings of the 16th ASCE Engineering Mechanics Conference_. Seattle, WA, USA;, 2003.
  * [22] Y. Bazilevs, V. Calo, J. Cottrell, T. Hughes, A. Reali, and G. Scovazzi, “Variational multiscale residual-based turbulence modeling for large eddy simulation of incompressible flows,” _Computer methods in applied mechanics and engineering_ , vol. 197, no. 1-4, pp. 173–201, 2007.
  * [23] “Microsoft Azure Marketplace.” [Online]. Available: https://azure.microsoft.com/en-us/marketplace/
  * [24] “Amazon Web Services Marketplace.” [Online]. Available: https://aws.amazon.com/marketplace
  * [25] M. Azure. (2021) Optimal mpi process placement for azure hb series vms. [Online]. Available: https://techcommunity.microsoft.com/t5/azure-global/optimal-mpi-process-placement-for-azure-hb-series-vms/ba-p/2450663
  * [26] J. M. Kolinski and T. M. Schneider, “Superspreading events suggest aerosol transmission of sars-cov-2 by accumulation in enclosed spaces,” _Physical Review E_ , vol. 103, no. 3, p. 033109, 2021.