Note that in the soundness theorem below is important that the $\CGT$ proof
corresponding to the $\RGT$ proof not only derives the same sequent $\Gamma
\sdash A$ but furthermore also has the same computational content. It is easily
observed that neither $\strip$ nor $\embed$ change the computational content of
the proofs involved.

If $\RGT \vdash \Gamma \sdash A$ via $\Pi$ then $\CGT \vdash \Gamma \sdash
A$ via $\strip(\embed(\Pi))$.

Let $\TF$ be a finite fragment of $\CGT$. To conclude completeness of $\RGT$
relative to $\CGT$, we
construct a proof morphism $\search \colon \Sss(\TF) \to \CGT$. For this, recall that
$\Sss(\TF)$ is the `proof search system' induced by the derivation rules in $\TF$
and the trace interpretation of $\CGT$.

The function $\search \colon \Sss(\Seq_\TF) \to \Seq_\RGT$ is defined as

\[\search(\Gamma \sdash A; (\Theta, \sigma)) \coloneq \widehat{\Theta}
\rsep \Gamma^\sigma \sdash A\]

where for any $S \subseteq \Theta$, $\widehat{S} \in \Theta^*$ is the
duplicate-free sequence of length
$\abs{S}$, consisting of the elements of $S$ which is strictly sorted
according to $\Theta$. Recalling that $(\Theta, \sigma)$ is $K$-sparse, the notation
$\Gamma^\sigma \coloneq \Gamma^\sigma_1$ is recursively defined by

\[
\Gamma^\sigma_i \coloneq
\begin{cases}
A^\varepsilon, \Gamma'^\sigma_i & \text{ if } \Gamma = A, \Gamma'
\text{ with } A \neq N \\
N^{\hat{S}}, \Gamma'^\sigma_{i + 1} & \text{ if } \Gamma = N, \Gamma'
\text{ with } \sigma(i) = \{S\} \\
N^\varepsilon, \Gamma'^\sigma_i & \text{ if } \Gamma = N, \Gamma'
\text{ with } \sigma(i) = \emptyset \\
\varepsilon & \text{ if } \Gamma = \varepsilon
\end{cases}
\]

The function can be extended into a proof morphism $\search \colon \Sss(\TF) \to \RGT$.

Towards this claim, first pick some $\Rrr(\Theta, \sigma) \in \Sss(\TF)$ arranged as follows

\[
\inference[$\Rrr(\Theta, \sigma)$]{
\Gamma_1 \sdash B_1 ; (\Theta_1, \sigma_1) \quad
\ldots \quad
\Gamma_n \sdash B_n ; (\Theta_n, \sigma_n)
{\Gamma \sdash A ; (\Theta, \sigma)}
\]

Then there is $R \in \TF$ with $\rho(R) = (\Gamma \sdash A, \Gamma_1
\sdash B_1, \ldots,
\Gamma_n \sdash B_n)$ and morphisms $r_i \colon \iota(\Gamma \sdash A)
\to \iota(\Gamma_i \sdash B_i)$ given by
the trace interpretation. Then for each $i \leq n$ there is $(\Theta, \sigma)
\gstep{r_i} (\Theta_i, \sigma_i)$ with the expanded sequence
the expanded sequence

\[(\Theta, \sigma) \step{R_{\gamma_1}} (\Theta_r^1, \sigma_r^1) \ldots
\step{R_{\gamma_k}} (\Theta_r^k, \sigma_r^k)
\step{P} (\Theta_p, \sigma_p) \step{r_i} (\Theta_i,
\sigma_i) \step{T} (\Theta_i, \sigma_i) \]

in which the initial $R_\gamma$- and $P$-steps are shared between all $i \leq
n$ (see <Ref>). Observe that because of the structure of the
trace interpretation for Cyclic Gödel's T, there will never be two stacks on
the same field of a Safra board in the expanded sequence, meaning the thinning
does not change $\Theta_i$ and $\sigma_i$. Similarly to <Ref>, we may derive
the following in reset Gödel's T:

$\widehat{\Theta_1} \rsep \Gamma^{\sigma_1}_1 \sdash B_1$
$\widehat{\Theta_n} \rsep \Gamma^{\sigma_n}_n \sdash B_n$
$\widehat{\Theta_r^k}  \rsep \Gamma^{\sigma_r^k} \sdash A$

$\widehat{\Theta_0}  \rsep \Gamma^{\sigma_0} \sdash A$

That is, first apply all possible $\textsc{Reset}_a$-rules, starting at the
$\Theta_0$-greatest $a$. Because $\Gamma^{\sigma}$ annotates instances of $N$
to which $\sigma$ `assigns' no stack with $N^\varepsilon$, the population
step does not need to be replicated in the preproof as $\Gamma^{\sigma_r^k}
= \Gamma^{\sigma_p}$. Complete the preproof by applying the rule corresponding
to $R \in \TF$. Observe that the rules of reset Gödel's T again annotate
instances of $N$ to which $\sigma_i$ does not assign a stack with
$N^\varepsilon$, meaning the premises are indeed $\widehat{\Theta_i} \vdash
\Gamma_i^{\sigma_i} \sdash B_i$. As the thinning transition does not change
$\sigma_i$, it does not need to be replicated in the preproof.

An argument analogous to that given for $\elab$ in <Ref> shows that
$\search$ maintains the soundness condition.

Similarly to soundness, for completeness it is again important that the
computational content of the proof remain unchanged.

If $\CGT \vdash \Gamma \sdash A$ via $\Pi$ then $\RGT \vdash
\Gamma \sdash A$ via a proof $\Pi'$ such that
$\strip(\embed(\Pi'))$ is an unfolding of $\Pi$.

§.§ Modal $\mu$-Calculus

The modal $\mu$-calculus ($\mML$) extends the classical modal logic $K$ with a
fixed-point quantifiers $\nu x. \varphi$ and $\mu x. \varphi$, denoting the
greatest and least fixed-point, respectively. The $\mu$-calculus has been
central to the field of cyclic proof theory:
The first cyclic proof system was given for
$\mML$ <cit.> and $\mML$ (and its variants such as
$\mu$MALL and higher-order $\mu$-calculi) have been studied the most in the
field of cyclic proof theory.

In this section we construct two reset proof systems for the modal
$\mu$-calculus, called $\FRmML$ (<Ref>) and $\BRmML$
(<Ref>), which correspond to two different
natural formulations of the trace condition of $\mML$: one in terms of the
booleans $\BB$ and one in terms of the failure algebra $\FF$. This also
demonstrates that the same derivation system can induce multiple quite distinct
reset proof systems if there are multiple sensible trace interpretations for it.

The first reset proof system was given for satisfiability of $\mML$ by Jungteerapanich
in <cit.> and later reformulated by
Stirling <cit.> into a reset proof system for
validity. The latter system is often called the Jungteerapanich-Stirling ($\JS$)
system in the literature. In <Ref> we recall the system $\JS$ and
compare it to the systems $\FRmML$ and $\BRmML$. This comparison highlights
the likely biggest shortcoming of our approach: The reset proof systems in our
article are constructed solely based on the trace condition without deeper
insight into the semantics of the logic in question.

§.§.§ Cyclic Modal $\mu$-Calculus

Our presentation of $\mML$ is based on the presentation given
in <cit.>.
For a set $\prop$ of propositional letters a countable set $\var$ of variables,
the $\mu$-formulas are given by the following grammar:

\[\varphi \in \form \langeq p ~|~ \neg p ~|~ x ~|~ \varphi \wedge \varphi
~|~ \varphi \vee \varphi ~|~ \Box \varphi ~|~ \Diamond \varphi ~|~ \mu
x.\varphi ~|~ \nu x. \varphi
\quad p \in \prop, x \in \var \]

If $x, y \in \var$ occur in $\varphi$, $x$ subsumes $y$,
writing $x <_\varphi y$, if $\sigma y.\psi$ occurs as a
subformula of $\varphi$ for some $\sigma \in \{\mu, \nu\}$ and $\psi$, and
furthermore $x$ is free in $\sigma y.\psi$.
If the relation $<_\varphi$ is a strict preorder, one calls $\varphi$
well-named. Henceforth, we only consider sequents $\Gamma$ where $\Gamma$ is a set of
well-named formulas.

The sequents of $\mML$ are finite sets $\Gamma$ of well-named $\mu$-formulas.
Write $\Gamma, \varphi$ to mean $\Gamma \cup \{\varphi\}$ and $\Gamma,
\Gamma'$ to mean $\Gamma \cup \Gamma'$.
The set of $\mML$-sequents is denoted $\Seq_{\mML}$.
The derivation rules of $\mML$ are the following:

[Ax]p, p

[Wk]ΓΓ, φ

[$\vee$]Γ, φ, ψΓ, φ∨ψ

[$\wedge$]Γ, φ    Γ, ψΓ, φ∧ψ

[Mod]Γ, φΓ, φ

[$\mu$]Γ, φ[μx. φ/ x]Γ, μx. φ

[$\nu$]Γ, φ[νx. φ/ x]Γ, νx. φ

In the rules above, $\varphi[\psi / x]$ denotes the formula resulting from
replacing all instances of the variable $x$ in $\varphi$ by the formula $\psi$.
This is a partial operation which is only defined if $x$ does is not bound in
$\varphi$ by some fixed-point quantifier $\nu x$ or $\mu x$. Writing
$\varphi[\psi / x]$ is to be understood as a tacit claim that this the operation
is defined on these arguments.

As noted previously, the modal $\mu$-calculus $\mML$ can be given at least two
natural trace interpretations, one in terms of the booleans $\BB$ and one in
terms of the failure algebra $\FF$. We distinguish the two trace interpretations
by denoting them $\iota_\Aa$ where $\Aa$ is the activation algebra over which
the interpretation in question is defined. The interpretation $\iota_\FF$
corresponds to the `usual' formulation of the global trace condition of the
$\mu$-calculus as a parity condition in terms of the subsumption hierarchy
$<_\varphi$. In fact, this global trace condition was the original motivation
for the concept of activation algebras <cit.>.

For a derivation rule $R \in \mML$ with $\rho(R) = (\Gamma, \Delta_1, \ldots,
\Delta_n)$ call $\varphi' \in \Delta_i$ a
precursor of $\varphi \in \Gamma$, writing $\varphi' \leftarrow_R^i
\varphi$, if either
$\varphi$ is principal in $R_i$, i.e. $\varphi$ is `altered by
$R_i$', and $\varphi'$ is one of the formula
occurrences resulting from $\varphi$ via $R$
or if $\varphi$ is not principal in $R_i$ and $\varphi = \varphi'$.

Writing $V_\nu(\varphi) \coloneq \{x ~|~ x \text{ is bound by } \nu \text{ in
} \varphi\}$, the trace interpretation $\iota_\FF \colon \mML \to \TT_\FF$ is given by

\[
\iota_\FF(\Gamma) \coloneq \{(\varphi, x) ~|~ \varphi \in \Gamma \text{ and
} x \in V_\nu(\varphi)\}
\]

and for any $R \in \mML$ with $\rho(R) = (\Gamma, \Delta_1, \ldots, \Delta_n)$
the trace maps $r_i \colon \iota_\FF(\Gamma) \to \iota_\FF(\Delta)$ are defined by
\(
r_i \coloneq \{((\varphi, x), a^*, (\varphi', x)) ~|~ \varphi' \leftarrow_R^i \varphi \}
\) where $a^*$ is defined by

\[
a^* \coloneq
\begin{cases}
2, & \text{ if }R_i \text{ instance of } \mu, \varphi = \mu y.\theta, \varphi' = \theta[\mu y.\theta / y] \text{ and } y <_{\varphi} x,  \\
1, & \text{ if } R_i \text{ instance of } \nu, \varphi = \nu x.\theta, \varphi' = \theta[\nu x. \theta / x], \\
0, & \text{ otherwise.}
\end{cases}
\]

The trace interpretation $\iota_\BB$ for $\mML$ is defined by `tracking'
individual fixed-point quantifier instances in the sequent and finding a
greatest fixed-point quantifier which is unfolded infinitely often and never
`erased' by the unfolding of a higher quantifier.
Call a sequence $a \in \BB^*$ a subformula address and define a partial addressing
function $\varphi \addr a$ as follows:

\[
\varphi \addr \varepsilon \coloneq \varphi
\qquad \quad
\varphi_0 \bullet \varphi_1 \addr ia \coloneq \varphi_i \addr a
\qquad \quad
\ocircle \varphi \addr 0a \coloneq \varphi \addr a
\]

where $\bullet \in \{\wedge, \vee\}$ and $\ocircle \in \{\neg, \Box,
\Diamond\} \cup \{\mu x, \nu x ~|~ x \in \var\}$. Define the set of
$\nu$-addresses of a formula as $N(\varphi) \coloneq \{a \in \BB^* ~|~ \varphi
\addr a = \nu x. \psi\}$. Given $x \in \var$, define the set of open $x$
addresses in $\varphi$ by $O_x(\varphi) \coloneq \{a \in \BB^* ~|~ \varphi
\addr a = x \text{ and } \forall a' < a, \psi.~\varphi \addr a' \neq \nu x.
\psi \wedge \varphi \addr a' \neq \mu x. \psi \}$.

The trace interpretation $\iota_\BB \colon \mML \to \TT_\BB$ is defined by
\(\iota_\BB(\Gamma) \coloneq \{(\varphi, a) ~|~ \varphi \in \Gamma \wedge a
\in N(\varphi)\}\). For each rule $R \in \mML$ with $\rho(R) = (\Gamma,
\Delta_1, \ldots, \Delta_n)$ which is not a fixed-point rule, the trace maps
$r_i \colon \iota_\BB(\Gamma) \to \iota_\BB(\Delta_i)$ simply `track' the
fixed-point instances. For instance, if $R$ is the following instance of the

\[
\inference[$\vee$]{\Gamma, \varphi_0, \varphi_1}{\Gamma, \varphi_0 \vee \varphi_1}
\]

then $r_1 \coloneq \{((\psi, a), 0, (\psi, a)) ~|~ (\psi, a) \in
\iota_\BB(\Gamma)\} \cup \{((\varphi_0 \vee \varphi_1, ia), 0, (\varphi_i,
a)) ~|~ ia \in N(\varphi_0 \vee \varphi_1)\}$. Now suppose $R$ was an
instance of a fixed-point rule

\[
\inference[$\sigma$]{\Gamma, \varphi[\sigma x. \varphi / x]}{\Gamma, \sigma x. \varphi}
\]

\begin{align*}
r_1 \coloneq\,& \{(v, 0, v) ~|~ v \in \iota_\BB(\Gamma)\} ~\cup \\
& \{((\sigma x. \varphi, \varepsilon), b, (\varphi[\sigma x. \varphi / x], a) ~|~ a \in O_x(\varphi)\} ~\cup \\
& \{((\sigma x. \varphi, 0a), 0, (\varphi[\sigma x. \varphi / x], a) ~|~ a \in N(\varphi)\} ~\cup \\
& \{((\sigma x. \varphi, 0a), 0, (\varphi[\sigma x. \varphi / x], a'0a) ~|~ a \in N(\varphi), a' \in O_X(\varphi)\}
\end{align*}

where $b = 0$ iff $\sigma = \mu$. Spelling out all the details of this
definition would quickly become unwieldy, so we rely on the reader's
intuition. A detailed account of a very similar trace condition can be found
in <cit.>.

Henceforth, we write $\mML$ to denote the cyclic proof systems $\iota_\FF(\mML)$
and $\iota_\BB(\mML)$. There is no need to distinguish between the two as both
trace interpretations induce the same cyclic proof system: Precisely the same
preproofs satisfy the global trace condition specified via $\iota_\BB$ as that
specified via $\iota_\FF$. Nonetheless, they induces two different reset proof

§.§.§ $\FF$-Reset Modal $\mu$-Calculus

We first present a reset proof system $\FRmML$ corresponding to
$\iota_\FF(\mML)$ (pronounced “$\FF$-reset modal

The sequents of $\FRmML$ are expressions of the form $\Theta
\rsep \Gamma$ where the control $\Theta$ is a sequence of distinct characters,
called the control,
and $\Gamma$ is a set of pairs $(\varphi, \sigma)$ of $\mu$-formulas $\varphi$
and an annotation, a set of assignments $x_1 \mapsto u_1, \ldots, x_n \mapsto u_n$ where $\{x_1,
\ldots, x_n\} = V_\nu(\varphi)$, $u_1, \ldots, u_n$ are subsequences of
$u_i \sqsubseteq \Theta$ and each variable $x \in V_\nu(\varphi)$ is part of
precisely one assignment. For simplicity of notation, we often treat such
sequences $\sigma$ simply as a functions mapping $V_\nu(\varphi)$ to
subsequences of $\Theta$. The set of sequents $\FRmML$ is denoted
Analogously to Safra boards, a letter $a \in \Theta$ is covered in $\Gamma$ if for every
$(\varphi, \sigma) \in \Gamma$ and every $x \in V_\nu(\varphi)$, if $a \in
\sigma(x)$ then it is not at the last position of that sequence.

The derivation rules of the $\FF$-reset modal $\mu$-calculus ($\FRmML$)
follow. Denote by $\Theta'$ the control from which all letters not
occurring in any annotation in the corresponding $\Gamma$ are removed. Similarly, $\sigma'$
denotes the annotation from which all assignments $x \mapsto u$ with $x
\not\in V_\nu(\varphi)$ in the corresponding $\mu$-formula $\varphi$ have been

[Ax]Θ(p, ε), (p, ε)

[Wk]Θ' ΓΘΓ, (φ, ε)

[$\vee$]ΘΓ, (φ, σ'), (ψ, σ')ΘΓ, (φ∨ψ, σ)

[$\wedge$]Θ' Γ, (φ, σ')     Θ' Γ, (ψ, σ')ΘΓ, (φ∧ψ, σ)

[Mod]ΘΓ, (φ, σ)ΘΓ, (φ, σ)

[$\mu$]Θ' Γ, (φ[μx. φ/ x], σ∖x)ΘΓ, (μx.
φ, σ)

[$\nu$]Θa Γ, (φ[νx. φ/ x],
(σ, x ↦ua))   a ∉ΘΓ, (νx.
φ, (σ, x ↦u))

Θ' Γa   a  covered in  Γ

[\(\RMerge\)]Θ' Γ, (φ,
_Θ(σ, σ'))ΘΓ, (φ, σ), (φ, σ')

Where $\Diamond \Gamma \coloneq \{(\Diamond \varphi, \sigma) ~|~ (\varphi,
\sigma) \in \Gamma\}$ and $\sreset{\Gamma}{x} \coloneq \{(\varphi,
\sreset{\sigma}{a}) ~|~ (\varphi, \sigma) \in \Gamma\}$ and the various
annotations used above are defined below

ε     if  x <_νx. φ y

σ(y)      otherwise

u      if  σ(x) = uav

σ(x)      otherwise

_Θ(σ, σ')(x) min_Θ(σ(x), σ'(x))

Write $\varepsilon$ for the annotation $x_1 \mapsto \varepsilon, \ldots,
x_n \mapsto \varepsilon$.
A $\FRmML$-preproof is a proof
every pair of bud $t
\in \dom(\beta)$ and companion $\beta(t)$ has an invariant, i.e. there
exists a letter $a$ such that $a$ occurs in all of the controls
$\Theta$ between $t$ and $\beta(t)$, the prefix of $a$ in the controls
$\Theta$ remains constant and the $\textsc{Reset}_a$ rule
is applied between $t$ and $\beta(t)$.
A proof is a proof of a $\mu$-sequent $\Gamma$, writing
$\FRmML \vdash \Gamma$, if its root
is labeled $\varepsilon \rsep \{(\varphi, \varepsilon) ~|~ \varphi \in \Gamma\}$.

The $\RMerge{}$ rule is somewhat inelegant and in some cases subsumed by $\RWk$.
It is required to simulate the thinning step of greedy runs in the completeness
proof. We conjecture that, every instance of $\RMerge$ that could be
needed to construct $\FRmML$-proofs corresponding to $\mML$-proofs is subsumed
by $\RWk$. Indeed, the Jungteerapanich-Stirling
system <cit.> for the modal $\mu$-calculus features
an analogous $\RThin$-rule which always chooses one of the two
$\varphi$-instances and which is sufficient to prove completeness. However,
proving that $\RMerge$ is superfluous would likely be as involved as a direct
completeness proof for $\FRmML$ with regards to the semantics of the modal
$\mu$-calculus. We thus forgo this `ergonomic optimization' as the goal of our
article is to derive concrete reset proof systems without having to spend much

Soundness of $\FRmML$ with regards to $\mML$ is proven by constructing a proof
morphism $\embed \colon \FRmML \to \mML$.

There exists a function $\embed \colon \Seq_{\FRmML} \to \Rrr(\Seq_{\mML})$ which is defined by

\[\embed(\Theta \rsep \Gamma) \coloneq \ol{\Gamma} ; (\ol{\Theta}, \sigma_\Gamma) \]

where $\ol{\Theta}$ is the set $\{u \in \Theta\}$ ordered
according to the letters' positions in $\Theta$, $\ol{\Gamma} \coloneq
\{\varphi ~|~ (\varphi, \sigma) \in \Gamma\}$ and $\sigma_\Gamma$ is defined as

\[
\sigma_\Gamma((\varphi, x), 0) \coloneq \{\{a \in \sigma(x)\} ~|~ (\varphi, \sigma) \in \Gamma \}
\qquad \qquad
\sigma_\Gamma((\varphi, x), e) \coloneq \emptyset \quad \text{if } e \in \{1, 2\}.
\]

The function can be extended into a proof morphism $\embed \colon \FRmML \to \Rrr(\mML)$.

The main complication in completing this morphism is that for $\Theta \rsep
\Gamma$, there may be $(\varphi, \sigma), (\varphi, \sigma') \in \Gamma$ with
$\sigma \neq \sigma'$, i.e. two instances of the same formula with
different annotation. The $\embed$-function `collapses' the two annotated
formulas into one instance of a formula in which each $\nu$-variable is
annotated by two stacks.

A simple example in which this causes complications is the $\RWk$-rule.
Suppose the $\RWk$-instance removed $(\varphi, \sigma)$ from $\Gamma,
(\varphi, \sigma'), (\varphi, \sigma)$
with $\sigma \neq \sigma'$. Then $\ol{\Gamma,
(\varphi, \sigma'), (\varphi, \sigma)} = \ol{\Gamma}, \varphi$. Thus, to
simulate $\RWk$, the corresponding $\RWk$-rule of
$\Rrr(\mML)$ need not be applied; only some annotations need to be removed from
$\varphi$. Thus, the simulation is as given below.

$\Gamma, \psi ; (\ol{\Theta'}, \sigma_{\Gamma,
(\varphi, \sigma')}) $

$\ol{\Gamma}, \ol{\psi} ; (\ol{\Theta}, \sigma_{\Gamma,
(\varphi, \sigma'), (\varphi, \sigma)}) $

\[
\inference[\textsc{Wk}]{\Theta' \rsep \Gamma, (\varphi, \sigma')}{\Theta \rsep \Gamma,
(\varphi, \sigma'), (\varphi, \sigma)}
\quad
\stackrel{\embed}{\leadsto}
\quad
\usebox{\mypt}
\]

Similar issues with `collapsing' can arise in the rules $\vee$, $\wedge$,
$\nu$ and $\mu$.
For an example, consider a sequent $\Theta \rsep \Gamma_0$ with $\Gamma_0$ as below and $\sigma \neq
\sigma'$. For simplicity, suppose there were no more `copies' of $\varphi \vee
\psi$ in $\Gamma$. To embed an application of the $\vee$-rule $\Theta \rsep \Gamma_2$,
one must first apply the $\Rrr(\mML)$-correspondent of $\vee$ with $\varphi \vee
\psi$ both principal and part of the `context' $\ol{\Gamma}, \varphi \vee \psi$ to
$\ol{\Gamma_0} ; (\ol{\Theta}, \sigma_{\Gamma_0})$.
However, because of the `collapsing' of identical formulas, this only yields
$\ol{\Gamma_1} ; (\ol{\Theta}, \sigma_{\Gamma_1})$ because the trace
interpretation $r \colon \iota_\FF(\Gamma, \varphi \vee \psi, \varphi \vee \psi)
\to \iota_\FF(\Gamma, \varphi \vee \psi, \varphi, \psi)$ contains
$(\varphi \vee \psi, 0, \varphi \vee \psi)$ as well as $(\varphi \vee \psi, 0,
\varphi)$ and $(\varphi \vee \psi, 0, \psi)$. Noting $\ol{\Gamma_1} =
\ol{\Gamma_2}$, the desired premise $\ol{\Gamma_2} ; (\ol{\Theta},
\sigma_{\Gamma_2})$ can be reached with an application of the $\RWeak$-rule of $\Rrr(\mML)$.

\begin{align*}
\Gamma_0 \coloneq\,& \Gamma, (\varphi \vee \psi, \sigma), (\varphi \vee \psi, \sigma') \\
\Gamma_1 \coloneq\,& \Gamma, (\varphi \vee \psi, \sigma), (\varphi \vee \psi, \sigma'), (\varphi, \sigma), (\psi, \sigma), (\varphi, \sigma'), (\psi, \sigma') \\
\Gamma_2 \coloneq\,& \Gamma, (\varphi \vee \psi, \sigma), (\varphi, \sigma'), (\psi, \sigma')
\end{align*}

In terms of preproofs, this yields:

$\ol{\Gamma}, \varphi \vee \psi, \varphi, \psi; (\ol{\Theta}, \sigma_{\Gamma_2})$

$\ol{\Gamma}, \varphi \vee \psi, \varphi, \psi; (\ol{\Theta}, \sigma_{\Gamma_1})$
$\ol{\Gamma}, \varphi \vee \psi; (\ol{\Theta}, \sigma_{\Gamma_0})$

\[
\inference[$\vee$]{\Theta \rsep \Gamma, (\varphi \vee \psi, \sigma),
(\varphi, \sigma'), (\psi, \sigma')}{\Theta \rsep \Gamma, (\varphi \vee \psi,
\sigma), (\varphi \vee \psi, \sigma')}
\quad
\stackrel{\embed}{\leadsto}
\quad
\usebox{\mypt}
\]

If there were more `copies' $(\varphi \vee \psi, \sigma'') \in \Gamma$ with
$\sigma \neq \sigma'' \neq \sigma'$ then the stacks corresponding to
$(\varphi, \sigma'')$ and $(\psi, \sigma'')$ also need to be removed by the
$\RWeak$-application. If there is only one `copy' of $\varphi \vee \psi$ in
$\Gamma$, then $\varphi \vee \psi$ need not be part of the `context'
$\ol{\Gamma}$ in the $\vee$-application and no application of $\RWeak$ is
needed. The `collapsing'-related issues that can arise when embedding instances of the rules
$\wedge$, $\nu$ and $\mu$ are analogous and can be dealt with in an analogous manner.

If `collapsing'-related issues are dealt with as described in the previous
paragraph, the $\nu$-rule of $\FRmML$ can simply be translated as the
corresponding instance of the $\nu$-rule in $\Rrr(\mML)$.
While the operation $\sigma\,\uh\,a$ involved in the
$\nu$-rule of $\FRmML$ is paralleled by the corresponding $\nu$-rule in
$\Rrr(\mML)$, this is not the case for the operation $\sigma \setminus x$ of the $\mu$-rule.
Consider the sequent
$b \rsep \Gamma_0$ with
$\Gamma_0 \coloneq (\mu x. \nu y. x, y \mapsto b)$. The corresponding
$\Rrr(\mML)$-sequent is
$\ol{\Gamma_0} ; (\ol{b}, \sigma_{\Gamma_0})$ with
$\sigma_{\Gamma_0}((\mu x. \nu y. x, y), a) \coloneq \{\{b\}\}$ for $a = 0$
and $\sigma_{\Gamma_0}((\mu x. \nu y. x, y), a) \coloneq \emptyset$ otherwise.
Applying the $\mu$-rule to this sequent yields $\nu y. \mu x. \nu y. x;
(\ol{b}, \sigma')$ with $\sigma'((\nu y. \mu x. \nu y. x, y), a) \coloneq
\{\{b\}\}$ for $a = 2$ and $\sigma'((\nu y. \mu x. \nu y. x, y), a) \coloneq
\emptyset$ otherwise. On the other hand, applying the $\mu$-rule to $b \rsep
\Gamma_0$ yields $\rsep \Gamma_1$ with $\Gamma_1 \coloneq (\nu y. \mu x. \nu y. x, y \mapsto \varepsilon)$.
Thus, an application of the $\RWeak$-rule removing the stack $\{b\}$ from
$((\nu y. \mu x. \nu y. x, y), 2)$, yielding $\sigma''$ with $\sigma'((\nu y. \mu x. \nu y. x, y), a) \coloneq
\emptyset$ on all $a \in \FF$, is needed. Furthermore, an application of the
$\RPop$-rule is required to add an empty stack to $((\nu y. \mu x. \nu y. x, y), 0)$.

$\nu y. \mu x. \nu y. x; (\emptyset, \sigma_{\Gamma_1})$

$\nu y. \mu x. \nu y. x; (\emptyset, \sigma'')$

$\nu y. \mu x. \nu y. x; (\ol{b}, \sigma')$
$\ol{\Gamma_0} ; (\ol{b}, \sigma_{\Gamma_0})$

\[
\inference[$\mu$]{\rsep (\nu y. \mu x. \nu y. x, y \mapsto \varepsilon)}{b \rsep (\mu x. \nu y. x, y \mapsto b)}
\quad
\stackrel{\embed}{\leadsto}
\quad
\usebox{\mypt}
\]

More complicated cases with more $\nu$-variables can be dealt with in an
analogous manner.

The $\RMod$-rule simply corresponds to the $\RMod$-rule of $\Rrr(\mML)$. No
`collapsing'-related complications can arise in its translation as all
formulas are principal in applications of the $\RMod$-rule. The
$\RReset_a$-rule directly corresponds to the $\RReset_a$-rule of $\Rrr(\mML)$.
It is easily observed that  is always simulated by a suitable
instance of .

If $\FRmML \vdash \Gamma$ then $\mML \vdash \ol{\Gamma}$.

Let $\TF$ be a finite fragment of $\mML$. To prove completeness, one constructs
a proof morphism $\search \colon \Sss(\TF) \to \FRmML$ embedding the proof search system
for $\TF$ into $\FRmML$.

There exists a function $\search \colon \Sss(\Seq_\TF) \to \Seq_{\FRmML}$ with

\[\search(\Gamma; (\Theta, \sigma)) \coloneq \widehat{\Theta}
\rsep \Gamma^\sigma\]

where for any $S \subseteq \Theta$, $\widehat{S} \in \Theta^*$ is the
duplicate-free sequence of length
$\abs{S}$, consisting of the elements of $S$ which is strictly sorted
according to $\Theta$. The notation
$\Gamma^\sigma \coloneq \{(\varphi, \sigma \uh \varphi) ~|~ \varphi
\in \Gamma\}$ with $(\sigma \uh \varphi)(x) \coloneq \widehat{\sigma((\varphi, x), 0)}$.

The function can be extended to a proof morphism $\search \colon \Sss(\TF) \to \FRmML$.

Towards this claim, first pick some $\Rrr(\Theta, \sigma) \in \Sss(\TF)$ arranged as follows

\[
\inference[$\Rrr(\Theta, \sigma)$]{
\Gamma_1; (\Theta_1, \sigma_1) \quad
\ldots \quad
\Gamma_n; (\Theta_n, \sigma_n)
{\Gamma; (\Theta, \sigma)}
\]

Then there is $R \in \TF$ with $\rho(R) = (\Gamma, \Gamma_1, \ldots,
\Gamma_n)$ and morphisms $r_i \colon \iota_\FF(\Gamma)
\to \iota_\FF(\Gamma_i)$ given by
the trace interpretation. Then for each $i \leq n$ there is $(\Theta, \sigma)
\gstep{r_i} (\Theta_i, \sigma_i)$ with the expanded sequence
the expanded sequence

\[(\Theta, \sigma) \step{R_{\gamma_1}} (\Theta_r^1, \sigma_r^1) \ldots
\step{R_{\gamma_k}} (\Theta_r^k, \sigma_r^k)
\step{P} (\Theta_p, \sigma_p) \step{r_i} (\Theta^*_i,
\sigma^*_i) \step{T} (\Theta_i, \sigma_i) \]

in which the initial $R_\gamma$- and $P$-steps are shared between all $i \leq
n$ (see <Ref>). Similarly to <Ref>, we may derive
the following in $\FRmML$:

$\widehat{\Theta_1}\rsep \Gamma_1^{\sigma_1}$

$\widehat{\Theta_1^*}\rsep \Gamma^0_1$
$\widehat{\Theta_n}\rsep \Gamma_n^{\sigma_n}$

$\widehat{\Theta_n^*}\rsep \Gamma^0_n$
$\widehat{\Theta_r^k} \rsep \Gamma^{\sigma_r^k}$

$\widehat{\Theta_0} \rsep \Gamma^{\sigma_0}$

That is, first apply all possible $\textsc{Reset}_{\gamma_i}$-rules, starting at the
$\Theta_0$-greatest $\gamma_0$. Because $\Gamma^{\sigma}$ annotates $\nu$-variables
to which $\sigma$ assigns no stack with the empty stack $\varepsilon$, the population
step does not need to be replicated in the preproof as $\Gamma^{\sigma_r^k}
= \Gamma^{\sigma_p}$. Continue by applying the rule corresponding
to $R \in M$. Observe that while the controls resulting from this application
matches $\Theta_i^*$, the sequents will be some sequent $\Gamma^0_i$ which
might contain multiple copies of the same formula with different
annotations (analogously to the `collapsing' issues in
<Ref>). In such cases, there is some $(\varphi, x)$ to which
$\sigma^*_i$ assigns two or more stacks. The greedy run uses a thinning to reestablish
the property that each quantifier is assigned at most one stack. In $\FRmML$,
this can be replicated by applying the $\RMerge$-rule to all formulas
$(\varphi, \sigma), (\varphi, \sigma') \in \Gamma_i^0$. Note that the
order of applications and choice of which two `$\varphi$-instances' to
pick for $\RMerge$-applications does not matter as the resulting sequent will
always be $\widehat{\Theta_i} \rsep \Gamma_i^{\sigma_i}$.

An argument analogous to that given for $\elab$ in <Ref> shows that
$\search$ maintains the soundness condition. Crucially, this relies on the
fact that an accepting Safra board run through a proof in $\Sss(\TF)$ can
never `enter some state' $((\varphi, x), 2)$. If it did, from that point onwards, the run can
never reach any $((\psi, x), a)$ with $a < 2$ anymore, meaning only finitely
$\RReset$s could take place from that point onwards. Thus, `dropping' the
stacks on $((\varphi, x), 2)$ as the function $\search \colon \Sss(\TF) \to \FRmML$
does not hinder the maintainance of the soundness condition.

If $\mML \vdash \Gamma$ then $\FRmML \vdash
\Gamma$.

As can be observed, most issues in establishing both $\embed$ and $\search$ as
proof morphisms surround the `collapsing' of formula identities. A simple
solution to circumvent all issues of this kind is be to take the sequents of
$\mML$ to be lists of formulas in which there can be distinct occurrences of the
same formula (and defining $\FRmML$ with similar list-like sequents). We chose
to not do this as this would mark a departure from the presentation of $\mML$
in <cit.>. A central goal of this article is
to give `recipes' for generating reset system which do not require any
modifications to the original cyclic proof system. Doing so for this example
would thus have violated this goal. Nonetheless, we recommend readers who may be
running into similar problems when generating reset systems for their cyclic
proof systems consider making such a modification in order to lighten their
proving load.

§.§.§ $\BB$-Reset Modal $\mu$-Calulus

We next present a reset proof system $\BRmML$ corresponding to $\iota_\BB(\mML)$
(pronounced “$\BB$-reset modal $\mu$-calculus”).

The system uses $\mu$-formulas with annotated quantifiers. That is, each
$\nu$-quantifier $\nu^u x. \varphi$ is annotated with a sequence of distinct
characters $u$:

\[\varphi \in \form_\BB \langeq p ~|~ \neg p ~|~ x ~|~ \varphi \wedge \varphi
~|~ \varphi \vee \varphi ~|~ \Box \varphi ~|~ \Diamond \varphi ~|~ \mu
x.\varphi ~|~ \nu^u x. \varphi
\quad p \in \prop, x \in \var \]

Given $\varphi \in \form_\BB$, write $\ol{\varphi} \in \form$ for the
$\mu$-formula obtained by removing the annotations in $\varphi$. Given a
sequence $\Theta$ of distinct letters, define a
partial function $\merge_\Theta \colon \form_\BB \times \form_\BB \to \form_\BB$ such that
$\merge_\Theta(\varphi, \psi)$ is defined on $\varphi,
\psi \in \form_\BB$ iff $\ol{\varphi} = \ol{\psi}$ and the annotations in
$\varphi, \psi$ are subsequences of $\Theta$. The definition is given

_Θ(a, a) a

_Θ(φ_0 ∙φ_1, ψ_0 ∙ψ_1) _Θ(φ_0, ψ_0) ∙_Θ(φ_1, ψ_1)

(φ, ψ) (φ, ψ)

(ν^u x. φ, ν^v x. ψ) ν^min_Θ(u, v) x.
(φ, ψ)

where $a \in \prop \cup \var$, $\bullet \in \{\wedge, \vee\}$ and $\ocircle \in \{\neg, \Box,
\Diamond\} \cup \{\mu x ~|~ x \in \var\}$ and $\min_\Theta(u, v)$ is the
minimal sequence according to the ordering $<_\Theta$ defined in <Ref>.

A letter $a$ is covered in $\varphi$ if in every annotation $u$ in
$\varphi$ such that $a$ appears in $u$, $a$ is not at the last position of $u$.
This notion extends to sets $\Gamma$ of annotated formulas. The reset
operation $\sreset{\varphi}{a}$ is defined below:

pa p

φ∙ψa (φa) ∙(ψa)

φa (φa)

ν^u x. φa ν^u' x. φa
where  u'
u      if  σ(x) = uav

σ(x)      otherwise

where $p \in \prop \cup \var$, $\bullet \in \{\wedge, \vee\}$ and $\ocircle \in \{\neg, \Box,
\Diamond\} \cup \{\mu x ~|~ x \in \var\}$.

The sequents of $\BRmML$ are expressions $\Theta \rsep \Gamma$,
where the control $\Theta$ is a sequence of distinct characters and
$\Gamma$ is a finite set of formulas from $\form_\BB$ such that each quantifier
$\sigma^u x. \varphi$ occurring in $\Gamma$ is annotated with a subsequence of
Write $\varphi^\epsilon$ for a formula $\varphi$ in which all
quantifiers are annotated with the empty sequence $\varepsilon$, extending
this notation to sets of formulas $\Gamma$.
The set of $\BRmML$-sequents is denoted by $\Seq_{\BRmML}$.

The derivation rules of $\BRmML$ are given below. Denote by $\Theta'$ the
control from which all letters not occurring in any annotation in $\Gamma$
are removed.

[Ax]Θp, p

[Wk]Θ' ΓΘΓ, φ

[$\vee$]ΘΓ, φ, ψΘΓ, φ∨ψ

[$\wedge$]Θ' Γ, φ    Θ' Γ, ψΘΓ, φ∧ψ

[Mod]ΘΓ, φΘΓ, φ

[$\mu$]ΘΓ, φ[μx. φ/ x]ΘΓ, μx. φ

[$\nu$]Θa Γ, φ[ν^ua x. φ/ x]
a ∉ΘΘΓ, ν^u x. φ

Θ' Γa   a  covered in  Γ

[\(\RMerge\)]Θ' Γ, ξ  _Θ(φ,
ψ) = ξΘΓ, φ, ψ

A $\BRmML$-preproof is a proof if
every pair of bud $t
\in \dom(\beta)$ and companion $\beta(t)$ has an invariant, i.e. there
exists a letter $a$ such that $a$ occurs in all of the controls
$\Theta$ between $t$ and $\beta(t)$, the prefix of $a$ in the controls
$\Theta$ remains constant and the $\textsc{Reset}_a$ rule
is applied between $t$ and $\beta(t)$.
A $\BRmML$-proof is a proof
of $\Gamma$ if its root
is labeled $\varepsilon \rsep \Gamma^\varepsilon$.
Write $\BRmML \vdash \Gamma $ if there is a proof of $\Gamma$ in $\BRmML$.

Soundness of $\BRmML$ with regards to $\mML$ is proven by constructing a proof
morphism $\embed \colon \BRmML \to \mML$.

There exists a function $\embed \colon \Seq_{\BRmML} \to \Rrr(\Seq_{\mML})$ which is defined by

\[\embed(\Theta \rsep \Gamma) \coloneq \ol{\Gamma} ; (\ol{\Theta}, \sigma_\Gamma) \]

where $\ol{\Theta}$ is the set $\{u \text{ occurs in } \Theta\}$ ordered
according to the letters' positions in $\Theta$, $\ol{\Gamma}$ is $\Gamma$
with all annotations removed and $\sigma_\Gamma$ is defined as below:

\[
(\ol{\varphi}, i) \mapsto \{\{a \text{ occurs in } u\} ~|~ \psi \in \Gamma
\text{ and } \ol{\psi} = \ol{\varphi} \text{ and } \psi \addr i = \nu^u x.
\xi\} \text{ for each } \varphi \in \Gamma \text{ and } i \in N(\varphi)
\]

The function can be extended into a proof morphism $\embed \colon \BRmML \to \mML$.

As with $\BRmML$, the main complication in constructing this morphism is that
for $\Theta \rsep \Gamma \in \Seq'$ there may be two formulas $\varphi, \psi \in
\Gamma$ with $\ol{\varphi} = \ol{\psi}$, i.e. two instances of the same formula
with different annotation. The $\embed$-function `collapses' the two annotated
formulas into one instance of a formula in which each $\nu$-instance is
annotated by two stacks. Both the kinds of complications which can arise and
their treatment using the $\mML$-rule $\RWk$ and the $\Rrr(\mML)$-rule $\RWeak$
are completely analogous to those in $\FRmML$. Hence, we refer the reader to for a
more exhaustive treatment of these issues <Ref>.

Each $\BRmML$ rule is translated to its $\Rrr(\mML)$-counterpart. The rule
is always simulated by a suitable instance of .

If $\BRmML \vdash \Gamma$ then $\mML \vdash \ol{\Gamma}$.

Let $\TF$ be a finite fragment of $\mML$. To prove completeness, one constructs
a proof morphism $\search \colon \Sss(\TF) \to \BRmML$ embedding the proof search system
for $\TF$ into $\BRmML$.

There exists a function $\search \colon \Sss(\Seq_{\TF}) \to \Seq_{\BRmML}$ with

\[\search(\Gamma; (\Theta, \sigma)) \coloneq \widehat{\Theta}
\rsep \Gamma^\sigma\]

where for any $S \subseteq \Theta$, $\widehat{S} \in \Theta^*$ is the
duplicate-free sequence of length
$\abs{S}$, consisting of the elements of $S$ which is strictly sorted
according to $\Theta$. The notation
$\Gamma^\sigma \coloneq \{\varphi^{\sigma \uh \varphi}_\varepsilon ~|~ \varphi
\in \Gamma\}$ with $(\sigma \uh \varphi)(a) \coloneq \sigma(\varphi, a)$ and
$\varphi^{\widehat{\sigma}}_a$ is recursively defined by

\[
c^{\widehat{\sigma}}_a \coloneq c
\qquad
(\varphi \bullet \psi)^{\widehat{\sigma}}_a \coloneq
\varphi^{\widehat{\sigma}}_{a0} \bullet \psi^{\widehat{\sigma}}_{a1}
\qquad
(\ocircle \varphi)_a^{\widehat{\sigma}} \coloneq \ocircle \varphi_{a0}^{\widehat{\sigma}}
\qquad
(\nu x. \varphi)_a^{\widehat{\sigma}} \coloneq
\begin{cases}
\nu^{\widehat{S}} x. \varphi^{\widehat{\sigma}}_{a0} & \text{ if } \widehat{\sigma}(i) \coloneq \{S\} \\
\nu^\varepsilon x. \varphi^{\widehat{\sigma}}_{a0} & \text{ otherwise}
\end{cases}
\]

where $c \in \prop \cup \var$, $\bullet \in \{\wedge, \vee\}$ and $\ocircle \in \{\neg, \Box,
\Diamond\} \cup \{\mu x ~|~ x \in \var\}$.

The function can be extended to a proof morphism $\search \colon \Sss(\TF) \to \BRmML$.

Towards this claim, first pick some $\Rrr(\Theta, \sigma) \in \Sss(\TF)$ arranged as follows

\[
\inference[$\Rrr(\Theta, \sigma)$]{
\Gamma_1; (\Theta_1, \sigma_1) \quad
\ldots \quad
\Gamma_n; (\Theta_n, \sigma_n)
{\Gamma; (\Theta, \sigma)}
\]

Then there is $R \in \TF$ with $\rho(R) = (\Gamma, \Gamma_1, \ldots,
\Gamma_n)$ and morphisms $r_i \colon \iota_\BB(\Gamma)
\to \iota_\BB(\Gamma_i)$ given by
the trace interpretation. Then for each $i \leq n$ there is $(\Theta, \sigma)
\gstep{r_i} (\Theta_i, \sigma_i)$ with the expanded sequence
the expanded sequence

\[(\Theta, \sigma) \step{R_{\gamma_1}} (\Theta_r^1, \sigma_r^1) \ldots
\step{R_{\gamma_k}} (\Theta_r^k, \sigma_r^k)
\step{P} (\Theta_p, \sigma_p) \step{r_i} (\Theta^*_i,
\sigma^*_i) \step{T} (\Theta_i, \sigma_i) \]

in which the initial $R_\gamma$- and $P$-steps are shared between all $i \leq
n$ (see <Ref>). Similarly to <Ref>, we may derive
the following in $\BRmML$:

$\widehat{\Theta_1}\rsep \Gamma_1^{\sigma_1}$

$\widehat{\Theta_1^*}\rsep \Gamma^0_1$
$\widehat{\Theta_n}\rsep \Gamma_n^{\sigma_n}$

$\widehat{\Theta_n^*}\rsep \Gamma^0_n$
$\widehat{\Theta_r^k} \rsep \Gamma^{\sigma_r^k}$

$\widehat{\Theta_0} \rsep \Gamma^{\sigma_0}$

That is, first apply all possible $\textsc{Reset}_{\gamma_i}$-rules, starting at the
$\Theta_0$-greatest $\gamma_0$. Because $\Gamma^{\sigma}$ annotates fixed-points
to which $\sigma$ `assigns' no stack with $\nu^\varepsilon$, the population
step does not need to be replicated in the preproof as $\Gamma^{\sigma_r^k}
= \Gamma^{\sigma_p}$. Continue by applying the rule corresponding
to $R \in M$. Observe that while the controls resulting from this application
matches $\Theta_i^*$, the sequents will be some sequent $\Gamma^0_i$ which
might contain multiple copies of the `same' formula with different
annotation (similarly to $\sigma_i^*$ assigning multiple stacks to some of its
arguments). A simple example in which this occurs is if $\Gamma = \varphi,
\psi \vee \xi$ with $\ol{\varphi} = \ol{\psi}$ but $\varphi \neq \psi$. If the
$\vee$-rule is applied to this sequent, the resulting sequent $\Gamma_1^0 =
\varphi, \psi, \xi$ contains two `copies' of $\ol{\varphi}$ (corresponding
to $\sigma_1^*$ assigning multiple stacks to some of the quantifiers in
$\ol{\varphi}$). In such cases, the greedy run uses a thinning to reestablish
the property that each quantifier is assigned at most one stack. In $\BRmML$,
this can be replicated by applying the $\RMerge$-rule to all formulas
$\varphi, \psi \in \Gamma_i^0$ with $\ol{\varphi} = \ol{\psi}$. Note that the
order of applications and choice of which two `$\ol{\varphi}$-instances' to
pick for $\RMerge$-applications does not matter as the resulting sequent will
always be $\widehat{\Theta_i} \rsep \Gamma_i^{\sigma_i}$.

An argument analogous to that given for $\elab$ in <Ref> shows that
$\search$ maintains the soundness condition.

If $\mML \vdash \Gamma$ then $\BRmML \vdash
\Gamma$.

§.§.§ The Jungteerapanich-Stirling System

The first reset proof system was put forward by
Jungteerapanich <cit.> for the modal
$\mu$-calculus. The system is a tableaux system which induces a decision
algorithm for satisfiability of $\mu$-sequents. Later, the system was converted
to a regular validity proof system by
Stirling <cit.>. The latter system is usually
called the Jungteerapanich-Stirling ($\JS$) in the literature. While the system
is also inspired by the Safra construction (see <cit.> for details) the final system
is quite bespoke, as we point out later. Soundness and completeness are
proven directly with regards to the semantics of the modal $\mu$-calculus,
rather than the arguments relying on automata theory we employ in this article.
As $\JS$ is well-known in the field of cyclic proof theory, it is of interest to
compare our systems $\FRmML$ and $\BRmML$ to it. Our presentation of $\JS$
slightly differs from that given in <cit.> to
better fit with the notation style of this article.

The system $\JS$ assumes some fixed linear ordering $<$ on the variables which
are denoted in capital letters $X, Y, Z$. For the remainder of this section, we
only consider formulas $\varphi$ which are well-named and in which the
subsumption order $<_\varphi$ coincides with the variable ordering $<$. A finite
collection of well-named formulas can always be $\alpha$-renamed such that this
property is fulfilled.
For each variable $X$ there is an infinite supply of
names $x_1, x_2, \ldots$ associated with $X$. The names are distinct
between distinct variables.

Sequents of $\JS$ are expressions $\Theta \rsep \Gamma$ where $\Gamma$ is
a finite set of annotated $\mu$-formulas $\varphi^u$ and the control $\Theta$ is a finite,
repetition-free sequence of names of variables occurring in the formulas
$\varphi^u \in \Gamma$. The
annotations $u$ of $\varphi^u \in \Gamma$ are subsequences $u \sqsubseteq
\Theta$ of $\Theta$.
Furthermore, they must be ordered according to the
ordering $<$ of variables, i.e. if a name $x$ of $X$ and a name $y$ of $Y$
appear in $u$ and $X < Y$ then $x$ must occur before $y$ in $u$.

For $u \sqsubseteq \Theta$ denote by $u \uh X$ the
subsequence of $u$ from which all names corresponding to variables $Y > X$ have
been removed. For two names $x, y \in \Theta$ write $x \sqsubset_\Theta y$
if either $x$ is a name for $X$ and $y$ is a name for $Y$ with $X < Y$ or if $x$
and $y$ are names for the same variable $X$ and $x$ occurs before $y$ in
$\Theta$. This extends to sequences $u, v \sqsubseteq \Theta$, writing $u
\sqsubset_\Theta v$ if $u$ contains the $\sqsubset_\Theta$-least name which
occurs in only one of the two sequences.

The derivation rules of $\JS$ are given below. Write $\Theta'$ to
denote the control $\Theta$ from which all names not occurring in annotations
in the corresponding $\Gamma$ were removed.

[]ΘΓ, p^u, p^v

[$\vee$]ΘΓ, φ^u, ψ^uΘΓ, φ∨ψ^u

[$\wedge$]ΘΓ, φ^u   ΘΓ, ψ^uΘΓ, φ∧ψ^u

[$\Box$]ΘΓ, φ^uΘΓ, φ^u

[$\mu$]Θ' Γ, φ[μX. φ/ X]^u XΘΓ, μX. φ^u

[$\nu$]Θ' x Γ, φ[νX. φ/
X]^(u X)x   x  fresh  X nameΘΓ, νX. φ^u

[]Θ' Γ, φ^u   u ⊏_ΘvΘΓ, φ^u, φ^v

[$\RReset_{x}$]Θ' Γ, φ_1^ux,
…, φ_n^ux   x  not in  ΓΘΓ, φ_1^uxx_1u_1,
…, φ_n^uxx_nu_n

A $\JS$-preproof is a proof if
every pair of bud $t
\in \dom(\beta)$ and companion $\beta(t)$ has an invariant, i.e. there
exists a name $x$ such that $x$ occurs in all of the controls
$\Theta$ between $t$ and $\beta(t)$ and the $\textsc{Reset}_x$ rule
is applied between $t$ and $\beta(t)$.
A $\JS$-proof is a proof
of $\Gamma$ if its root
is labeled $\varepsilon \rsep \Gamma^\varepsilon$.

A $\mu$-formula is guarded if a $\Box$ occurs on the paths between a
binder $\nu X$ or $\mu X$ and each of its bound variables $X$. The following is
proven in <cit.>.

If $\gamma$ is closed and guarded then $\JS \vdash \gamma$ iff $\gamma$ is valid.

It is clear at a glance that the systems $\BRmML$ and $\JS$ are quite
different: While $\BRmML$ annotates quantifier instances, the annotations of
$\JS$ concern formulas in $\Gamma$ and their $\nu$-variables (it is easily
observed that the annotations can never be extended with $\mu$-variables). Their
commonality ends at both systems being reset proof systems for the modal
$\mu$-calculus. The
comparison between $\FRmML$ and $\JS$ will turn out much more revealing.

In a way, the annotations of $\FRmML$ and $\JS$ `track' the same trace
values: The $\nu$-variables of each formula in $\Gamma$ on a per-formula basis.
In $\FRmML$ this is obvious: Each formula $\varphi$ in $\Gamma$ comes with an assignment
$\sigma$ which assigns each of variable $X$ bound by $\nu X$ in $\varphi$ a
subsequence of the control $\Theta$. In $\JS$ this is a more subtle observation:
At first glance, annotations are only per formula $\varphi$. However, these annotations
consist only[This is not quite accurate. Rather, the names in the
annotations are for variables which occurred `hereditarily' in the formula.
For example, the formula $\nu X. \nu Y. Y$, after two applications of the
$\nu$-rule, will be unfolded to $\nu Y. Y$ annotated by a sequence $xy$, with the obvious variable
correspondences, even though $X$ does not occur in $\nu Y. Y$ `anymore'.
However, these `anomalies' will only ever occur as prefixes of annotations
which `eventually' do not impact proof search anymore.] of variables which
occur in $\varphi$. The $\mu$- and $\nu$-rules ensure that the names in the
annotation are ordered by the global ordering $<$ on variables. In this sense,
the annotation $u$ of $\varphi^u$ can be separated into subsequences of names
$x_1 \ldots x_n$, for each variable $X$ in $\varphi$, tracking the progress  of
each trace value $(\varphi, X)$ (in the sense of the $\iota_\FF$ GTC for

In that light, it can be observed that the $\mu$-rule of the two
systems is essentially the same: It `cancels' all progress made by
$\nu$-variables subsumed by the unfolded $\mu$-formula by removing their
associated annotations.

The ordering $\sqsubset_\Theta$ is the lexicographic ordering comparing first
according to the global ordering $<$ on variables and subsequently according to
`age ordering' given by positions in $\Theta$. This illustrates the most
significant point of departure between $\FRmML$ and $\JS$: The design of $\JS$
takes into account some deeper insights into the semantics of the
modal $\mu$-calculus, specifically the role of the subsumption ordering
$<_\varphi$ in the validity condition.

Another instance of these insights comes
into play is the $\nu$-rule: When unfolding the $\nu$-quantifier of a formula
$\nu X. \varphi^u$ in $\JS$, the resulting annotation is $(u \uh X)x$, `clearing
off' the annotations of variables subsumed by $X$. This is necessary to ensure
that the names in the annotation remain ordered according to the global variable
order $<$ (otherwise the name $x$ would likely be appended after names of
subsumed variables, disturbing this ordering property). The completeness of this
rule hinges on a semantic insight: If there is a successful trace on a
$\nu$-variable in a formula, all `higher' $\nu$-variables subsuming it must also
have a successful trace. Thus, forgetting the progress of `lower'
$\nu$-variables upon progress in `higher' $\nu$-variables does not endanger
completeness. Partly, Jungteerapanich and Stirling can `get away with this' as
they prove soundness and completeness directly with regards to the semantics of
the modal $\mu$-calculus, `skipping' the automata theoretic considerations we
make in this article. Proving a similar result in the more generic setting of
trace categories with subsumption orders on their trace objects is highly
intricate. The system $\FRmML$ does thus not employ this kind of
`optimization' as this would have marked a departure from our original goal of
generating reset proof systems in a simple, `effortless' manner.

Another such point of difference between $\JS$ and $\FRmML$ is the $\RThin$-rule
of $\JS$. It should be noted that the only reason that $\JS$ only features this
strict thinning rule instead of a more general weakening rule is that it was
originally designed as a tableaux system for proof search in the modal
$\mu$-calculus. The $\RThin$-rule is the weakest rule which yields completeness
for the system (its purpose being analogous to the thinning steps of Safra
boards). However, the addition of a general weakening rule which allowed the
discarding of arbitrary formulas from $\Gamma$ would leave the soundness of
$\JS$ unchanged. The interesting point of comparison between $\JS$ and $\FRmML$
in this regard lies in $\RThin$ of $\JS$ and $\RMerge$ of $\FRmML$ recalled

\[
\inference[\RThin]{\Theta' \rsep \Gamma, \varphi^u \quad u \sqsubset_\Theta v}{\Theta \rsep \Gamma, \varphi^u, \varphi^v}
\qquad \qquad
\inference[\(\RMerge\)]{\Theta' \rsep \Gamma, (\varphi,
\merge_\Theta(\sigma, \sigma'))}{\Theta \rsep \Gamma, (\varphi, \sigma), (\varphi, \sigma')}
\]

Both rules are included for essentially the same reason: To mirror the thinning
step in the greedy Safra board runs required for completeness. The $\RThin$-rule
once again embodies a semantic insight: It is sufficient to `keep' the formula
which has the `best progress' on the highest variable. To illustrate this point,
suppose $\Theta$ was $x_1y_1x_2$, corresponding to variables $X$ and $Y$ in
$\varphi$, and that the sequent contained two copies of $\varphi$:
$\varphi^{x_1x_2}$ and $\varphi^{x_1y_1}$. In this case, an application of
$\RThin$ would discard $\varphi^{x_1y_1}$, essentially because $x_1x_2$ `has
better $X$-progress'. This is `complete' as `success' in `lower' variables
always entails `success' in `higher' variables as elaborated in the previous
paragraph. On the other hand, the $\RMerge$-rule of $\FRmML$ does once more not
embody this insight. Consider the analogous case: A control $\Theta$ of form $abc$ and
two annotated copies of $\varphi$ given by $(\varphi, (X \mapsto ac, Y \mapsto
\varepsilon))$ and $(\varphi, (X \mapsto a, Y \mapsto b))$. In this case, the
$\RMerge$-rule `keeps' the annotation $X \mapsto ac$ and the annotation
$Y \mapsto b$ in the resulting merged annotation of $\varphi$, the `best'
annotation for each separate variable, respectively. This is required to mirror
the thinning steps of greedy Safra board runs, which do the same. While it would
likely also be sound and complete for $\RMerge$ in $\FRmML$ to instead always
`keep' the annotation $\sigma$ which has the `best' annotation for the `highest'
variable, proving this would once again be extremely intricate.

§ CONCLUSION

We have shown that to each cyclic proof system $\RR$ with a soundness condition
specified in terms of an activation algebra $\Aa$, there is an associated cyclic
proof system $\Rrr(\RR)$ with a $\RReset$-based soundness condition. The
construction of $\Rrr(\RR)$ is fully independent of the underlying logic of $\RR$,
only relying on the specification of the global trace condition in terms of
$\Aa$. The equivalence of $\RR$ and $\Rrr(\RR)$ is proven via cyclic proof
system homomorphisms and a proof system $\Sss(\RR)$ tailored to easing proof search.
The method of cyclic proof system homomorphisms allows the
equivalence between $\RR$ and $\Rrr(\RR)$ to be extended to bespoke
$\RReset$-based proof systems $\TS$, as
demonstrated in <Ref>. This strategy is applied to present equivalent
reset systems for cyclic arithmetic, Gödel's
T and the modal $\mu$-calculus.

Our approach comes with some shortcomings. First, while broad, the scope of
applicability of our results is not universal. We have only demonstrated
how to give corresponding reset systems to cyclic proof systems with
$\TT_\Aa$-specifiable global trace conditions. There are some global trace
conditions which likely cannot be specified this way, for example that given by Hazard
for transfinite expressions <cit.>.
Furthermore, the soundness of the original system $\RR$ must be a global trace
condition for our method to apply. We did not consider other kinds of soundness conditions, such as
induction orders <cit.>, bouncing
threads <cit.> or trace
manifolds <cit.>.

Another shortcoming is that the naïve cyclic system $\Rrr(\RR)$ generated from a suitable cyclic
proof system $\RR$ can be `unwieldy'. For each concrete reset system we give in
<Ref>, some modifications were necessary to make the resulting
system pleasant for human use, specifically in finding a good `syntax' for
sequents of the concrete reset system. More generally, we believe that to
turn $\Rrr(\RR)$ into a `pleasant' system, some amount of human
creativity is still required.

One of the biggest strengths of the method we have described, its independence
of semantic considerations about the logic, is also one of its biggest
drawbacks: The systems generated by our method do not take advantage of semantic
insights into the logic in question and proving the equivalence of our systems
and other reset systems from the literature may take considerable effort.
Jungteerapanich's reset system for the modal \( \mu
\)-calculus <cit.> provides an example of
a $\RReset$-system designed using deep semantic insight in a manner $\Rrr(\mML)$
for both trace interpretations of $\mML$ does not (this is discussed in greater
detail in <Ref>).

It should be noted that $\Rrr(\RR)$ describes merely one way of
designing reset proof systems.
The reset proof system given in <cit.> provides an
example of the potential for variation.
The reset rule $\text{RS}(\kappa)$ utilised in that system corresponds
to the following transition on Safra boards: Fix
a board $(\Theta, \sigma) \in \Sb(\Aa, X)$ and pick a covered $\kappa \in
\Theta$. Define the set of $C(\kappa)$ of children of $\kappa$ as

\[
\coloneq \bigl\{\text{min}_\Theta \{\gamma \in S ~|~ \kappa < \gamma\} \bigm| x \in X, a \in
\Aa, S \in \sigma(a, x) \text{ and } \kappa \in S\bigr\}.
\]

If every $\gamma \in
C(\kappa)$ is also covered, one may perform a `reset operation' yielding the
board $(\Theta \setminus C(\kappa), \sigma \setminus C(\kappa))$ where $(\sigma
\setminus C(\kappa))(x, a) \coloneq \{S \setminus C(\kappa) \mid S \in \sigma(x,
a)\}$. Replacing the reset transitions of <Ref> with this variant of
the reset condition would yield an abstract reset proof system
enjoying the same soundness and completeness properties as our chosen form of $\Rrr(\RR)$, albeit requiring
slight modifications to their proofs. Most likely there are multiple
permissible alternatives to the `reset machinery' we
present in this article. We chose to only
cover one, namely the one the closest to the traditional Safra construction for
Rabin automata.

Related work

We are aware of three articles designing reset systems for cyclic proof systems:
Jungteerapanich-Stirling <cit.>,
Afshari et al. <cit.> and Afshari
et al. <cit.>.

Jungteerapanich <cit.> and
Stirling <cit.> propose reset proof systems for the
modal $\mu$-calculus, respectively for satisfiability and validity. These are
the first reset systems in the cyclic proof theory literature. A comparison
between their validity system and the systems we derive for validity of the
$\mu$-calculus in this article can be found in <Ref>. The upshot is that
while also inspired by the Safra construction, their system also incorporates
multiple insights into the semantics of the $\mu$-calculus which our systems

Afshari et al. <cit.> give a reset proof system for the
first-order $\mu$-calculus. It is based on the cyclic proof system
for the first-order $\mu$-calculus with ordinal approximations put forward by
Sprenger and
Dam <cit.>.
The crucial insight underpinning its design is that the mechanism of ordering
ordinal variables in the Sprenger-Dam system is already very similar to the control of
the Jungteerapanich-Stirling system. Thus, the Sprenger-Dam system is
extended into a reset system in a very natural manner.

Afshari et al. <cit.> give a reset proof system for
full computation tree logic ($\mathrm{CTL}^*$). Their system is a hypersequent
calculus and thus requires a more intricate trace condition. The annotations
used in their reset condition are either empty or one letter. In this, their system falls
in between the `full' reset proof systems, such as $\JS$, that for the
first-order $\mu$-calculus or ours, and the `mere' path condition systems
discussed in a subsequent paragraph.

It should be noted that
all of the aforementioned reset systems were designed by combining automata
theoretic considerations, specifically the Safra construction, and semantic
insights about the logic for which the systems were constructed. In both cases,
this resulted in systems which are more elegant than the systems we generate in
this article. It should however be noted that designing such elegant systems
requires considerable effort. Furthermore, we believe that for many technical
purposes of cyclic proof theory, the naïve reset proof systems derived in this
article shall prove sufficient.

The literature also contains articles on cyclic proof systems with path
conditions, i.e. whose trace conditions allow each simple cycle of the preproof
to be considered separately, which are not strictly reset proof systems
because their soundness condition is implemented in a simpler manner. Specifically,
Marti and Venema <cit.> demonstrate that for
the alternation-free fragment of the $\mu$-calculus, the
Jungteerapanich-Stirling system can be simplified to a system in which formulas
are annotated with one “one bit of information” (said to be in focus or
out of focus, respectively) and which does not need a $\RReset$-rule. The
resulting system still possesses a path condition.
Rooduijn <cit.> gives a very similar path
condition for cyclic proof systems of modal logics with the master modality.
It should be noted that all positive properties of reset proof systems we have
mentioned in this article, such as their suitability for proof theoretic
investigations and proof search, extend to all cyclic proof systems with path

Cyclic proof systems with path conditions, such as reset proof systems, have
proven well-suited to proof theoretic investigations. So far, the results which
employ them are in the areas of
interpolation <cit.>
and the translation of proof of cyclic proof systems into proofs in non-cyclic
proof systems with suitable induction
axioms <cit.>. However, there seems to be no
reason to assume that cyclic proof systems with path conditions might not also
prove useful in proving other properties, such as $\RCut$-elimination, or
investigations of the computational contents of cyclic proofs.

Future work

The results of this article open up many avenues of future research. As noted
previously, reset proof systems have proven to be valuable tools in the arsenal
of cyclic proof theory. With reset systems for many more cyclic proof systems
now available `off the shelf', we hope to see more proof theoretic
investigations using reset proof systems in the future. This could proof
especially valuable to the proof theories of logics with features particularly
well-suited to cyclic proof systems, such as fixed-points and inductive

This article elaborated on the relationship between the global trace condition
and the reset path condition using the abstract notion of trace put forward
in <cit.>. There are further soundness
conditions for cyclic proofs, such as induction
orders <cit.>, bouncing
threads <cit.> and trace
manifolds <cit.>. We hope to `complete the
picture' in the future by investigating these other soundness conditions and
their relationships in this abstract setting. An interesting aspect to explore
in this direction is the fact in some reset proof systems, an induction order
can essentially be `read off' the system's proofs. An example of such a system
is that for Gödel's T given in <Ref>. However, this is not true
for all reset proof systems. For example, the system for Peano arithmetic in
<Ref> does not possess this property.

Missing 'biblatex' package
The bibliography requires the 'biblatex' package.

abstractWe introduce a path-based cyclic proof system for ﬁrst-order mu-calculus, the extension of ﬁrst-order logic by second-order quantiﬁers for least and greatest ﬁxed points of deﬁnable monotone functions. We prove soundness of the system and demonstrate it to be as expressive as the known trace-based cyclic systems of Dam and Sprenger. Furthermore we establish cut-free completeness of our system for the fragment corresponding to the modal mu-calculus.
journaltitleLogic Journal of the IGPL
shortjournalLogic Journal of the IGPL
titleCyclic proofs for the ﬁrst-order µ-calculus
fshari et al. - Cyclic proofs for the ﬁrst-order µ-calculus.pdf:application/pdf;Snapshot:/home/user/Zotero/storage/5JHYABDY/6653082.html:text/html

Dagstuhl, Germany

Schloss Dagstuhl–Leibniz-Zentrum fuer Informatik

booktitle31st EACSL Annual Conference on Computer Science Logic (CSL 2023)
noteTo appear
seriesLeibniz International Proceedings in Informatics (LIPIcs)
titleA Cyclic Proof System for Full Computation Tree Logic
circular proofs,sequent calculus,coinduction,finitization,fixed points,induction,inf,linear logic,muMALL,non-wellfounded proofs,proof-search

abstractWe present two finitary cut-free sequent calculi for the modal μ-calculus. One is a variant of Kozen's axiomatisation in which cut is replaced by a strengthening of the induction rule for greatest fixed point. The second calculus derives annotated sequents in the style of Stirling's `tableau proof system with names' (2014) and features a generalisation of the ν-regeneration rule that allows discharging open assumptions. Soundness and completeness for the two calculi is proved by establishing a sequence of embeddings between proof systems, starting at Stirling's tableau-proofs and ending at the original axiomatisation of the μ-calculus due to Kozen. As a corollary we obtain a new, constructive, proof of completeness for Kozen's axiomatisation which avoids the usual detour through automata and games.
booktitle2017 32nd Annual ACM/IEEE Symposium on Logic in Computer Science (LICS)
eventtitle2017 32nd Annual ACM/IEEE Symposium on Logic in Computer Science (LICS)
titleCut-free completeness for modal mu-calculus
WQ/8005088.html:text/html;IEEE Xplore Full Text PDF:/home/user/Zotero/storage/XV9QVIF9/Afshari and Leigh - 2017 - Cut-free completeness for modal mu-calculus.pdf:application/pdf
Automata,Calculus,Cost accounting,Games,Reactive power,Semantics,Syntactics,Proofs with Names

Springer International Publishing

abstractIt is known that the modal $$\mu $$μ-calculus has the Craig interpolation property, indeed uniform interpolation. We prove Lyndon interpolation for the calculus, a strengthening of Craig interpolation which is not implied by uniform interpolation. The proof utilises ‘cyclic’ sequent calculus and provides an algorithmic construction of interpolants from valid implications. This direct approach enables us to derive a correspondence between the shape of interpolants and existence of sequent calculus proofs.
booktitleLanguage, Logic, and Computation
seriesLecture Notes in Computer Science
titleLyndon Interpolation for Modal μ-Calculus
fshari_Leigh_2022_Lyndon Interpolation for Modal $$-mu $$-Calculus.pdf:application/pdf
Sequent calculus,Lyndon interpolation,Cyclic proofs,Modal \(\mu \)-calculus

Springer International Publishing

abstractWe show how to construct uniform interpolants in the context of the modal µ-calculus. D’Agostino and Hollenberg (2000) were the ﬁrst to prove that this logic has the uniform interpolation property, employing a combination of semantic and syntactic methods. This article outlines a purely proof-theoretic approach to the problem based on insights from the cyclic proof theory of µ-calculus. We argue the approach has the potential to lend itself to other temporal and ﬁxed point logics.
booktitleAutomated Reasoning with Analytic Tableaux and Related Methods
isbn978-3-030-86058-5 978-3-030-86059-2
noteSeries Title: Lecture Notes in Computer Science
shorttitleUniform Interpolation from Cyclic Proofs
titleUniform Interpolation from Cyclic Proofs: The Case of Modal Mu-Calculus
YEJ/Afshari et al. - 2021 - Uniform Interpolation from Cyclic Proofs The Case.pdf:application/pdf

Springer International Publishing

abstractCyclic proof systems permit derivations that are finite graphs in contrast to conventional derivation trees. The soundness of such proofs is ensured by a condition on the paths through the derivation graph, known as the global trace condition. To give a uniform treatment of such cyclic proof systems, Brotherston proposed an abstract notion of trace. We extend Brotherston’s approach into a category theoretical rendition of cyclic derivations, advancing the framework in two ways: First, we introduce activation algebras which allow for a more natural formalisation of trace conditions in extant cyclic proof systems. Second, accounting for the composition of trace information allows us to derive novel results about cyclic proofs, such as introducing the Ramsey trace condition.
booktitleLogic, Language, Information, and Computation
seriesLecture Notes in Computer Science
titleAbstract Cyclic Proofs
bstract Cyclic Proofs.pdf:/home/user/Zotero/storage/QW97D544/Afshari_Wehr_2022_Abstract Cyclic Proofs.pdf:application/pdf
Category Theory,Cyclic Proof Theory,Mu-Calculus

New York, NY, USA

Association for Computing Machinery

abstractGiven that (co)inductive types are naturally modelled as fixed points, it is unsurprising that fixed-point logics are of interest in the study of programming languages, via the Curry-Howard (or proofs-as-programs) correspondence. This motivates investigations of the structural proof-theory of fixed-point logics and of their cut-elimination procedures. Among the various approaches to proofs in fixed-point logics, circular – or cyclic – proofs, are of interest in this regard but suffer from a number of limitations, most notably from a quite restricted use of cuts. Indeed, the validity condition which ensures soundness of non-wellfounded derivations and productivity of their cut-elimination prevents some computationally-relevant patterns of cuts. As a result, traditional circular proofs cannot serve as a basis for a theory of (co)recursive programming by lack of compositionality: there are not enough circular proofs and they compose badly. The present paper addresses some of these limitations by developing the circular and non-wellfounded proof-theory of multiplicative additive linear logic with fixed points () beyond the scope of the seminal works of Santocanale and Fortier and of Baelde et al. We define bouncing-validity: a new, generalized, validity criterion for , which takes axioms and cuts into account. We show soundness and cut elimination theorems for bouncing-valid non-wellfounded proofs: as a result, even though bouncing-validity proves the same sequents (or judgments) as before, we have many more valid proofs at our disposal. We illustrate the computational relevance of bouncing-validity on a number of examples. Finally, we study the decidability of the criterion in the circular case: we prove that it is undecidable in general but identify a hierarchy of decidable sub-criteria.
booktitleProceedings of the 37th Annual ACM/IEEE Symposium on Logic in Computer Science
seriesLICS '22
shorttitleBouncing Threads for Circular and Non-Wellfounded Proofs
titleBouncing Threads for Circular and Non-Wellfounded Proofs: Towards Compositionality with Circular Proofs
ge/CCK9TNXP/Baelde et al. - 2020 - Bouncing threads for infinitary and circular proof.pdf:application/pdf;Baelde et al_2022_Bouncing Threads for Circular and Non-Wellfounded Proofs.pdf:/home/user/Zotero/storage/HSFLCSZ3/Baelde et al_2022_Bouncing Threads for Circular and Non-Wellfounded Proofs.pdf:application/pdf

University of Edinburgh

abstractInductive definitions are the most natural means by which to represent many families of structures occurring in mathematics and computer science, and their corresponding induction / recursion principles provide the fundamental proof techniques by which to reason about such families. This thesis studies formal proof systems for inductive definitions, as needed, e.g., for inductive proof support in automated theorem proving tools. The systems are formulated as sequent calculi for classical first-order logic extended with a framework for (mutual) inductive definitions. The default approach to reasoning with inductive definitions is to formulate the induction principles of the inductively defined relations as suitable inference rules or axioms, which are incorporated into the reasoning framework of choice. Our first system LKID adopts this direct approach to inductive proof, with the induction rules formulated as rules for introducing atomic formulas involving inductively defined predicates on the left of sequents. We show this system to be sound and cut-free complete with respect to a natural class of Henkin models. As a corollary, we obtain cut-admissibility for LKID. The well-known method of infinite descent `a la Fermat, which exploits the fact that there are no infinite descending chains of elements of well-ordered sets, provides an alternative approach to reasoning with inductively defined relations. Our second proof system LKIDw formalises this approach. In this system, the left-introduction rules for formulas involving inductively defined predicates are not induction rules but simple case distinction rules, and an infinitary, global soundness condition on proof trees — formulated in terms of “traces” on infinite paths in the tree — is required to ensure soundness. This condition essentially ensures that, for every infinite branch in the proof, there is an inductive definition that is unfolded infinitely often along the branch. By an infinite descent argument based upon the well-foundedness of inductive definitions, the infinite branches of the proof can thus be disregarded, whence the remaining portion of proof is well-founded and hence sound. We show this system to be cutfree complete with respect to standard models, and again infer the admissibility of cut. The infinitary system LKIDw is unsuitable for formal reasoning. However, it has a natural restriction to proofs given by regular trees, i.e. to those proofs representable by finite graphs. This restricted “cyclic” proof system, CLKIDw, is suitable for formal reasoning since proofs have finite representations and the soundness condition on proofs is thus decidable. We show how the formulation of our systems LKIDw and CLKIDw can be generalised to obtain soundness conditions for a general class of infinite proof systems and their corresponding cyclic restrictions. We provide machinery for manipulating and analysing the structure of proofs in these essentially arbitrary cyclic systems, based primarily on viewing them as generating regular infinite trees, and we show that any proof can be converted into an equivalent proof with a restricted cycle structure. For proofs in this “cycle normal form”, a finitary, localised soundness condition exists that is strictly stronger than the general, infinitary soundness condition, but provides more explicit information about the proof. Finally, returning to the specific setting of our systems for inductive definitions, we show that any LKID proof can be transformed into a CLKIDw proof (that, in fact, satisfies the finitary soundness condition). We conjecture that the two systems are in fact equivalent, i.e. that proof by induction is equivalent to regular proof by infinite descent.
noteAccepted: 2006-10-31T15:56:10Z
titleSequent calculus proof systems for inductive definitions

abstractCircular and non-wellfounded proofs have become an increasingly popular tool for metalogical treatments of systems with forms of induction and/or recursion. In this work we investigate the expressivity of a variant CT of G\"odel's system T where programs are circularly typed, rather than including an explicit recursion combinator. In particular, we examine the abstraction complexity (i.e. type level) of C, and show that the G\"odel primitive recursive functionals may be typed more succinctly with circular derivations, using types precisely one level lower than in T. In fact we give a logical correspondence between the two settings, interpreting the quantifier-free type 1 theory of level n+1 T into that of level n C and vice-versa. We also obtain some further results and perspectives on circular 'derivations', namely strong normalisation and confluence, models based on hereditary computable functionals, continuity at type 2, and a translation to terms of $\T$ computing the same functional, at all types.
journaltitlearXiv:2012.14421 [cs, math]
titleA circular version of Gödel's T and its abstraction complexity
ge/6SVF7UH5/Das - 2021 - A circular version of Godel's T and its abstract.pdf:application/pdf;arXiv.org Snapshot:/home/user/Zotero/storage/ELRZSASF/2012.html:text/html;arXiv.org Snapshot:/home/user/Zotero/storage/49PURPQ9/2012.html:text/html;Das_2021_A circular version of G-odel's T and its abstraction complexity.pdf:/home/user/Zotero/storage/IYVY4KNG/Das_2021_A circular version of G-odel's T and its abstraction complexity.pdf:application/pdf
ematics - Logic

notePublisher: Wiley-Blackwell
titleÜber Eine Bisher Noch Nicht Benützte Erweiterung des Finiten Standpunktes
ödel_1958_Über Eine Bisher Noch Nicht Benützte Erweiterung des Finiten Standpunktes.pdf:application/pdf;Snapshot:/home/user/Zotero/storage/4QIWT69J/GDEBEB.html:text/html

Dagstuhl, Germany

Schloss Dagstuhl – Leibniz-Zentrum für Informatik

booktitle30th EACSL Annual Conference on Computer Science Logic (CSL 2022)
noteISSN: 1868-8969
seriesLeibniz International Proceedings in Informatics (LIPIcs)
titleCyclic Proofs for Transfinite Expressions
azard_Kuperberg_2022_Cyclic Proofs for Transfinite Expressions.pdf:application/pdf;Snapshot:/home/user/Zotero/storage/CRZRUZWD/15743.html:text/html
cyclic proofs,transfinite automata,transfinite expressions

University of Edinburgh

titleTableau Systems for the Modal µ-Calculus
Proofs with Names

Dagstuhl, Germany

Schloss Dagstuhl–Leibniz-Zentrum für Informatik

booktitle29th EACSL Annual Conference on Computer Science Logic (CSL 2021)
noteISSN: 1868-8969
seriesLeibniz International Proceedings in Informatics (LIPIcs)
titleA Cyclic Proof System for HFLN
:/home/user/Zotero/storage/A9BDFG2C/Kori et al. - 2021 - A Cyclic Proof System for HFL_ℕ.pdf:application/pdf;Snapshot:/home/user/Zotero/storage/M7976KXR/13463.html:text/html
Cyclic proof,fixed-point logic,higher-order logic,sequent calculus

booktitleTheory of Computation
seriesTexts in Computer Science
titleSafra’s Construction
ecture 27.pdf:application/pdf
ic Order,Start State,Visible Color

Springer International Publishing

abstractWe introduce a cut-free sequent calculus for the alternation-free fragment of the modal \(\mu \)-calculus. This system allows both for infinite and for finite, circular proofs and uses a simple focus mechanism to control the unravelling of fixpoints along infinite branches. We show that the proof system is sound and complete for the set of guarded valid formulas of the alternation-free \(\mu \)-calculus.
booktitleAutomated Reasoning with Analytic Tableaux and Related Methods
seriesLecture Notes in Computer Science
titleA Focus System for the Alternation-Free μ-Calculus
ystem for the Alternation-Free $$mu $$-C.pdf:application/pdf
Alternation-free mu-calculus,Circular proof system,Completeness,Infinitary proof system,Soundness,Proofs with Names

abstractGiven a formula of the propositional μ-calculus, we construct a tableau of the formula and define an infinite game of two players of which one wants to show that the formula is satisfiable, and the other seeks the opposite. The strategy for the first player can be further transformed into a model of the formula while the strategy for the second forms what we call a refutation of the formula. Using Martin's Determinacy Theorem, we prove that any formula has either a model or a refutation. This completeness result is a starting point for the completeness theorem for the μ-calculus to be presented elsewhere. However, we argue that refutations have some advantages of their own. They are generated by a natural system of sound logical rules and can be presented as regular trees of the size exponential in the size of a refuted formula. This last aspect completes the small model theorem for the μ-calculus established by Emerson and Jutla (1988). Thus, on a more practical side, refutations can be used as small objects testifying incorrectness of a program specification expressed by a μ-formula, we illustrate this point by an example.
journaltitleTheoretical Computer Science
shortjournalTheoretical Computer Science
titleGames for the μ-calculus
e/user/Zotero/storage/U3GBI649/main.pdf:application/pdf;ScienceDirect Full Text PDF:/home/user/Zotero/storage/MFI3SA4R/Niwiński and Walukiewicz - 1996 - Games for the μ-calculus.pdf:application/pdf;ScienceDirect Snapshot:/home/user/Zotero/storage/DMM3NLA6/0304397595001360.html:text/html;Snapshot:/home/user/Zotero/storage/M9RE8G4P/0304397595001360.html:text/html

Seattle, WA, USA

abstractIn this paper we improve the complexity of solving Rabin and Streett games to approximately the square root of previous bounds. We introduce direct Rabin and Streett ranking that are a sound and complete way to characterize the winning sets in the respective games. By computing directly and explicitly the ranking we can solve such games in time O(mnk+1kk!) and space O(nk) for Rabin and O(nkk!) for Streett where n is the number of states, m the number of transitions, and k the number of pairs in the winning condition. In order to prove completeness of the ranking method we give a recursive ﬁxpoint characterization of the winning regions in these games. We then show that by keeping intermediate values during the ﬁxpoint evaluation, we can solve such games symbolically in time O(nk+1k!) and space O(nk+1k!). These results improve on the current bounds of O(mn2kk!) time in the case of direct (symbolic) solution or O(m(nk2k!)k) in the case of reduction to parity games.
booktitle21st Annual IEEE Symposium on Logic in Computer Science (LICS'06)
eventtitle21st Annual IEEE Symposium on Logic in Computer Science (LICS'06)
titleFaster Solutions of Rabin and Streett Games
nueli - 2006 - Faster Solutions of Rabin and Streett Games.pdf:/home/user/Zotero/storage/LPAS5I5N/Piterman and Pnueli - 2006 - Faster Solutions of Rabin and Streett Games.pdf:application/pdf

abstractIn this paper we revisit Safra's determinization constructions for automata on infinite words. We show how to construct deterministic automata with fewer states and, most importantly, parity acceptance conditions. Determinization is used in numerous applications, such as reasoning about tree automata, satisfiability of CTL*, and realizability and synthesis of logical specifications. The upper bounds for all these applications are reduced by using the smaller deterministic automata produced by our construction. In addition, the parity acceptance conditions allows to use more efficient algorithms (when compared to handling Rabin or Streett acceptance conditions).
journaltitleLogical Methods in Computer Science
notePublisher: Episciences.org
titleFrom Nondeterministic Büchi and Streett Automata to Deterministic Parity Automata
volumeVolume 3, Issue 3
iterman - From Nondeterministic Bu¨ chi and Streett Automata.pdf:application/pdf;Piterman_2007_From Nondeterministic Büchi and Streett Automata to Deterministic Parity.pdf:/home/user/Zotero/storage/FUZS32QN/Piterman_2007_From Nondeterministic Büchi and Streett Automata to Deterministic Parity.pdf:application/pdf

Cambridge University Press

abstractFirst published in 1998, this textbook is a broad but rigourous survey of the theoretical basis for the design, definition and implementation of programming languages and of systems for specifying and proving programme behaviour. Both imperative and functional programming are covered, as well as the ways of integrating these aspects into more general languages. Recognising a unity of technique beneath the diversity of research in programming languages, the author presents an integrated treatment of the basic principles of the subject. He identifies the relatively small number of concepts, such as compositional semantics, binding structure, domains, transition systems and inference rules, that serve as the foundation of the field. Assuming only knowledge of elementary programming and mathematics, this text is perfect for advanced undergraduate and beginning graduate courses in programming language theory and also will appeal to researchers and professionals in designing or implementing computer languages.
titleTheories of Programming Languages

Springer International Publishing

abstractAt LICS 2013, O. Lahav introduced a technique to uniformly construct cut-free hypersequent calculi for basic modal logics characterised by frames satisfying so-called ‘simple’ first-order conditions. We investigate the generalisation of this technique to modal logics with the master modality (a.k.a. reflexive-transitive closure modality). The (co)inductive nature of this modality is accounted for through the use of non-well-founded proofs, which are made cyclic using focus-style annotations. We show that the peculiarities of hypersequents hinder the usual method of completeness via infinitary proof-search. Instead, we construct countermodels from maximally unprovable hypersequents. We show that this yields completeness for a small (yet infinite) subset of simple frame conditions.
booktitleAutomated Reasoning with Analytic Tableaux and Related Methods
seriesLecture Notes in Computer Science
titleCyclic Hypersequent Calculi for Some Modal Logics with the Master Modality
FR/Rooduijn_2021_Cyclic Hypersequent Calculi for Some Modal Logics with the Master Modality.pdf:application/pdf
Cyclic proofs,Hypersequent calculi,Master modality,Modal logic,Non-well-founded proofs

IEEE Computer Society

abstractAutomata on infinite words were introduced by J.R. Buchi (1962) in order to give a decision procedure for S1S, the monadic second-order theory of one successor. D.E. Muller (1963) suggested deterministic omega -automata as a means of describing the behavior of nonstabilising circuits. R. McNaughton (1966) proved that classes of languages accepted by nondeterministic Buchi automata and by deterministic Muller automata are the same. His construction and its proof are quite complicated, and the blow-up of the construction is double exponential. The author presents a determinisation construction that is simpler and yields a single exponent upper bound for the general case. This construction is essentially optimal. It can also be used to obtain an improved complementation construction for Buchi automata that is also optimal. Both constructions can be used to improve the complexity of decision procedures that use automata-theoretic techniques.
booktitleProceedings of the 29th Annual Symposium on Foundations of Computer Science
seriesSFCS '88
titleOn the complexity of omega -automata
EEE Xplore Full Text PDF:/home/user/Zotero/storage/C7LPVG6C/Safra - 1988 - On the complexity of omega -automata.pdf:application/pdf;Notes.pdf:/home/user/Zotero/storage/W2DBJQ9B/Safra_1988_On the complexity of omega -automata.pdf:application/pdf
i automata,complexity,decision procedures,deterministic automata,omega -automata,Circuits,Costs,H infinity control,Laser sintering,Logic,Mathematics,Upper bound

Berlin, Heidelberg

abstractCyclic proof provides a style of proof for logics with inductive (and coinductive) definitions, in which proofs are cyclic graphs representing a form of argument by infinite descent. It is easily shown that cyclic proof subsumes proof by (co)induction. So cyclic proof systems are at least as powerful as the corresponding proof systems with explicit (co)induction rules. Whether or not the converse inclusion holds is a non-trivial question. In this paper, we resolve this question in one interesting case. We show that a cyclic formulation of first-order arithmetic is equivalent in power to Peano Arithmetic. The proof involves formalising the meta-theory of cyclic proof in a subsystem of second-order arithmetic.
booktitleFoundations of Software Science and Computation Structures
seriesLecture Notes in Computer Science
titleCyclic Arithmetic Is Equivalent to Peano Arithmetic
impson - 2017 - Cyclic Arithmetic Is Equivalent to Peano Arithmeti.pdf:application/pdf

abstractWe investigate a Gentzen-style proof system for the first-order μ-calculus based on cyclic proofs, produced by unfolding fixed point formulas and detecting repeated proof goals. Our system uses explicit ordinal variables and approximations to support a simple semantic induction discharge condition which ensures the well-foundedness of inductive reasoning. As the main result of this paper we propose a new syntactic discharge condition based on traces and establish its equivalence with the semantic condition. We give an automata-theoretic reformulation of this condition which is more suitable for practical proofs. For a detailed comparison with previous work we consider two simpler syntactic conditions and show that they are more restrictive than our new condition.
issn0988-3754, 1290-385X
journaltitleRAIRO - Theoretical Informatics and Applications
notePublisher: EDP Sciences
titleOn global induction mechanisms in a μ-calculus with explicit approximations
napshot:/home/user/Zotero/storage/BSH63ENM/ita0317.html:text/html;Sprenger and Dam - 2003 - On global induction mechanisms in a μ -calc.pdf:/home/user/Zotero/storage/ZNBF6YTV/Sprenger and Dam - 2003 - On global induction mechanisms in a μ -calc.pdf:application/pdf;Sprenger and Dam - 2003 - On global induction mechanisms in a μ -calc.pdf:/home/user/Zotero/storage/CSE8AWJU/Sprenger and Dam - 2003 - On global induction mechanisms in a μ -calc.pdf:application/pdf
approximants.,circular proofs,global consistency condition,Inductive reasoning,well-foundedness,μ-calculus

Berlin, Heidelberg

abstractIn this paper we study induction in the context of the firstorder μ-calculus with explicit approximations. We present and compare two Gentzen-style proof systems each using a different type of induction. The first is based on finite proof trees and uses a local well-founded induction rule, while the second is based on (finitely represented) ω-regular proof trees and uses a global induction discharge condition to ensure externally that all inductive reasoning is well-founded. We give effective procedures for the translation of proofs between the two systems, thus establishing their equivalence.
booktitleFoundations of Software Science and Computation Structures
seriesLecture Notes in Computer Science
shorttitleOn the Structure of Inductive Reasoning
titleOn the Structure of Inductive Reasoning: Circular and Tree-Shaped Proofs in the μCalculus
prenger and Dam - 2003 - On the Structure of Inductive Reasoning Circular .pdf:application/pdf;Springer Full Text PDF:/home/user/Zotero/storage/Q4VCZJQ9/Sprenger and Dam - 2003 - On the Structure of Inductive Reasoning Circular .pdf:application/pdf
Derivation Tree,Explicit Approximation,Induction Hypothesis,Inductive Reasoning,Proof System

abstractFixpoints are an important ingredient in semantics, abstract interpretation and program logics. Their addition to a logic can add considerable expressive power. One general issue is how to define proof systems for such logics. Here we examine proof systems for modal logic with fixpoints. We present a tableau proof system for checking validity of formulas which uses names to keep track of unfoldings of fixpoint variables as devised by Jungteerapanich.
journaltitleElectronic Proceedings in Theoretical Computer Science
shortjournalElectron. Proc. Theor. Comput. Sci.
titleA Proof System with Names for Modal Mu-calculus
Computer Science - Logic in Computer Science,Proofs with Names

University of Amsterdam

titleAn Abstract Framework for the Analysis of Cyclic Derivations
typeMSc thesis