Grounded in the need for abstraction (B II), [α]ψ → [α β]ψ can only be adopted as a sound axiom schema if α and β do not share state, and if program β does not interfere with the contract ψ, i.e., (i) ψ has no free variables bound by β (with exceptions), and (ii) ψ does not depend on communication channels written by β (except for channels joint with α). This extensive side condition would need nontrivial soundness-critical implementations of dLCHP axiom schemata. Still, uniform substitution can be lifted with only small changes locally checking for clashes with written channels, and prohibited variables or channels.

The modularity of uniform substitution is the key to the parsimonious implementation [23] of the theorem prover KeYmaera X [11] for differential dynamic logic dL and differential game logic dGL [29], thus paving the way for a straightforward theorem prover implementation of dLCHP. Since dLCHP conservatively generalizes dL [6], its uniform substitution calculus inherits the complete [33] axiomatic treatment of differential equation invariants [30]. All proofs are in [7].

### **2 Dynamic Logic of Communicating Hybrid Programs**

This section briefly recaps dLCHP [6], the dynamic logic of communicating hybrid programs (CHPs). It combines hybrid programs [28] with CSP-style communication and parallelism [15]. By assumption-commitment (ac) reasoning [22,46,47], dLCHP allows compositional verification of parallelism in dL. For uniform substitution, function and predicate symbols, and program constants are added.

#### **2.1 Syntax**

The set of variables V = VR ∪VN ∪VT has real (VR), integer (VN), and trace (VT ) variables. For each x ∈ VR, the differential symbol x is in VR, too. The designated variable μ ∈ VR represents the shared global time. The set of channel names is Ω. By convention x, y ∈ VR, n ∈ VN, h ∈ VT , ch ∈ Ω, and z ∈ V . Channel set Y ⊆ Ω is (co)finite. Vectorial expressions are denoted ¯e. Moreover, fM, gM are M-valued function symbols and p, q, r are predicate symbols, where argument sorts are annotated by : M1,..., Mk. Finally, a, b are program constants.

**Definition 1 (Terms).** *Terms consist of real* (TrmR)*, integer* (TrmN)*, channel* (TrmΩ)*, and trace* (TrmT ) *terms, and are defined by the grammar below, where* θ, θ1, θ2 ∈ Q[VR] ⊂ TrmR *are polynomials in* VR*:*

Real terms are polynomials in VR enriched with function symbols f R(Y, e¯) (including constants c ∈ Q) only depending on communication along channels Y and terms ¯e, differential terms (θ) , and val(te) and time(te), which access the value and the timestamp of the last communication in te, respectively. By convention, θ ∈ Q[VR] denotes a pure polynomial in VR without (·) , val(·), and time(·) as they occur in programs. For simplicity, we do not define Q[VR] ⊂ TrmR as a fifth term sort but use the convention that function symbols gR can only be replaced with Q[VR]-terms. Integer terms are variables n, function symbols f N(Y, e¯) (including constants 0, 1), addition, and length |te| of trace term te. 1 The function symbol f Ω(Y, e¯) includes constants ch ∈ Ω, and chan(te) is channel access. Trace terms record the communication history of programs. They encompass variables h, function symbols fT (Y, e¯) (including the empty trace ), communication items ch, θ1, θ2 with value θ1 and timestamp θ2, projection

1 Omitting multiplication results in decidable Presburger arithmetic [34].

te ↓ Y onto channels Y , and access te[ie] of the ie-th item in te. Where useful, op(¯e) denotes built-in function symbols of fixed interpretation, e.g., *·* + *·*.

dLCHP's context-sensitive program and formula syntax presumes notions of free and bound variables (Sect. 2.3) defined on the context-free syntax:

**Definition 2 (Programs).** Communicating hybrid programs *are defined by the following grammar, where* θ ∈ Q[VR] *is a polynomial in* VR *and* χ ∈ FOLR *is a formula of first-order real-arithmetic. In* α β*, the subprograms must not share state but can share time and history, i.e.,* BV(α) ∩ BV(β) ⊆ {μ, μ } ∪ VT *.* 2

$$\begin{aligned} \alpha, \beta ::= a \{ Y, \bar{z} \} \mid x := \theta \mid x := \* \mid ? \chi \mid \{ x' = \theta \& \chi \} \mid \alpha; \beta \mid \alpha \cup \beta \mid \alpha^\* \mid \\\ ch(h) ! \theta \mid ch(h) ? x \mid \alpha \parallel \beta \end{aligned}$$

The program constant a(|Y, z¯|) restricts the written channels to Y ⊆ Ω and the bound variables to ¯z ⊆ VR ∪ VT , where Y and ¯z are (co)finite. Instead of a(|Y, z¯|), write a if Y and ¯z can be arbitrary. Assignment x := θ updates x to θ, nondeterministic assignment x := ∗ assigns an arbitrary real value to x, and the test ?χ does nothing if χ holds and aborts the computation otherwise. The continuous evolution {x = θ&χ} follows the ODE x = θ for any duration as long as formula χ is not violated. The global time μ evolves with every continuous evolution according to ODE μ = 1. Sequential composition α; β executes β after α, choice α ∪ β executes α or β nondeterministically, α∗ repeats α zero or more times, ch(h)!θ sends θ along channel ch, and ch(h)?x receives a value into variable x along channel ch. The trace variable h records communication. Finally, α β executes α and β in parallel synchronized in global time μ.

*Example 3.* The program ct∗ ve∗ models a simplified cruise control [24]. The vehicle ve repeatedly receives a target velocity vtr ve from the controller ct along channel tar. The target vtr ct sent by ct is in range [0, V ]. Hence, ve's velocity vve stays in range [0, V ] within the > 0 time units till the next communication if vve ∈ [0, V ] held initially. The evolution {t = 1} allows passage of time in ct.

$$\begin{aligned} \mathsf{ct} \equiv v\_{\mathsf{ct}}^{\mathrm{tr}} &:=\*; ? (0 \le v\_{\mathsf{ct}}^{\mathrm{tr}} \le V); \mathsf{tar}(h)! v\_{\mathsf{ct}}^{\mathrm{tr}}; \{t'=1\} \\ \mathsf{v} \mathbf{e} \equiv \mathsf{tar}(h)? v\_{\mathsf{v}\bullet}^{\mathrm{tr}}; a\_{\mathsf{v}\bullet} &:= \frac{v\_{\mathsf{v}\bullet}^{\mathrm{tr}} - v\_{\mathsf{v}\bullet}}{\epsilon}; t\_0 := \mu; \{v\_{\mathsf{v}\bullet}^{\prime} = a\_{\mathsf{v}\bullet} \& \,\mu - t\_0 \le \epsilon\} \end{aligned}$$

**Definition 4 (Formulas).** *Formulas are defined by the grammar below for relations* ∼*, terms* e1, e2 ∈ Trm *of equal sort, and* z ∈ V *. Moreover, the acformulas are unaffected by state change in* α*, i.e.,* (FV(A)∪FV(C))∩BV(α) ⊆ VT *.*

$$<\varphi, \psi, \mathsf{A}, \mathsf{C} ::= e\_1 \sim e\_2 \mid p(Y, \bar{e}) \mid \neg \varphi \mid \varphi \land \psi \mid \forall z \, \varphi \mid [\alpha] \psi \mid [\alpha] \lcorner [\mathsf{A}, \mathsf{C}] \psi$$

The formulas combine first-order dynamic logic with ac-reasoning. Predicate symbols p(Y, e¯) depend on channels Y and terms ¯e. The ac-box [α]{A,C}ψ

2 Previous work [6] disallows reading of variables bound in parallel as their change is not observable. This restriction is conceptually desirable but not soundness-critical. Here we drop it for simplicity, but it could be maintained by US as well.

expresses that C holds after each communication event and ψ in the final state, for all runs of α whose incoming communication satisfies A. Other connectives ∨, →, ↔ and quantifiers ∃z ϕ ≡ ¬∀z ¬ϕ can be derived. The relations ∼ include = for all term sorts, ≥ on real and integer terms, and prefixing on trace terms.

By convention, the predicate symbol qR can only be replaced with formulas of first-order real arithmetic. It serves as placeholder for tests χ in CHPs.

*Example 5.* The cruise control from Example 3 is safe if its velocity stays in range [0, V ]. This can be expressed with the formula ϕ → [ct∗ ve∗]ψsafe, where ψsafe ≡ 0 ≤ vve ≤ V and ϕ ≡ ψsafe ∧ > 0 ∧ V > 0.

#### **2.2 Semantics**

A *trace* τ = (τ1, ..., τk) is a finite chronological sequence of communication events τi = chi, di, si , where chi ∈ Ω, and di ∈ R is the communicated value, and si ∈ R is a timestamp such that si ≤ sj for 1 ≤ i<j ≤ k. A *recorded trace* τ = (τ1, ..., τk) additionally carries a trace variable hi ∈ VT with each event, i.e., τi = hi, chi, di, si . For variable z ∈ VM and M ∈ {R, N, T }, let type(z) = M. A *state* v maps each z ∈ V to a value v(z) ∈ type(z). The sets of traces, recorded traces, and states are denoted T , Trec, and S, respectively.

For d ∈ type(z), the state vd z is the modification of v at z to d. For τ ∈ Trec, the trace τ (h) ∈ T is obtained from the subsequence of τ carrying h ∈ VT by removing the carried variable. *State-trace concatenation* v · τ ∈ S for τ ∈ Trec, appends τ (h) to v at h for all h ∈ VT . The *projection* τ ↓ Y of (recorded) trace τ is the subsequence of all communication events in τ whose channel is in Y ⊆ Ω. The *state projection* v ↓ Y ∈ S modifies v at h to v(h) ↓ Y for all h ∈ VT .

An *interpretation* I assigns a function I(fM : M1,..., Mk) :×k i=1 Mi → M to each function symbol fM that is smooth in all real-valued arguments if M = R, and a relation I(p : M1,..., Mk) ⊆×k i=1 Mi to each k-ary predicate symbol p.

**Definition 6 (Term Semantics).** *The* valuation Iv[[e]] ∈ R ∪ N ∪ Ω ∪ T *of term* e *in interpretation* I *and state* v *is defined as follows:*

$$\begin{aligned} Iv[z] &= v(z) \\ Iv[f(Y, e\_1, \ldots, e\_k)] &= I(f)(I\ddot{v}[e\_1], \ldots, I\ddot{v}[e\_k]) \quad \text{where } \ddot{v} = v \downarrow Y \\ Iv[\mathtt{op}(e\_1, \ldots, e\_k)] &= \mathtt{op}(Iv[e\_1], \ldots, Iv[e\_k]) \quad \text{for builtin } \mathtt{op} \in \{\cdot + \cdot, \cdot \downarrow Y, \ldots\} \\ Iv[\boldsymbol{\theta}/\boldsymbol{\theta}] &= \sum\_{\boldsymbol{x} \in V\_{\mathbb{R}}} v(\boldsymbol{x}') \frac{\partial Iv[\boldsymbol{\theta}]}{\partial \boldsymbol{x}} \end{aligned}$$

The projection ˜v = v ↓ Y ensures that f(Y, e¯) only depends on Y , i.e., the communication in v along channels Y does not matter. The differentials (θ) have a semantics describing the local rate of change of θ [30].

The denotational semantics of CHPs [6] combines dL's Kripke semantics [30] with a linear history semantics [47] and a global notion of time. Denotations are subsets of D = S×Trec × S⊥ with S⊥ = S ∪ {⊥}. Final state ⊥ marks an unfinished computation, i.e., it still can be continued or was aborted due to a failing test. If (w = ⊥ and τ τ ), where is the prefix relation on traces, or (τ , w )=(τ,w), then (τ , w ) is a prefix of (τ,w) written (τ , w ) (τ,w). Since (even empty) communication of unfinished computations is still observable, denotations D ⊆ D of CHPs are prefix-closed and total, i.e., (v, τ, w) ∈ D and (τ , w ) (τ,w) implies (v, τ , w ) ∈ D, and ⊥D ⊆ D with ⊥D = S×{} × {⊥}. Moreover, all (v, τ, w) ∈ D are chronological, i.e., v(μ) ≤ w(μ) and when τ = (τ1,...,τk) = and let τi(μ)=(hi, chi, di, si )(μ) = si, then v(μ) ≤ τ1(μ) and if w = ⊥, then τk(μ) ≤ w(μ). Note that τ is chronological as all traces are.

The interpretation I(a(|Y, z¯|)) ⊆ D of a program constant a(|Y, z¯|) is a prefixclosed and total set of chronological computations that (i) only communicate along (write) channels Y and (ii) only bind variables ¯z. More precisely, for all (v, τ, w) ∈ I(a(|Y, z¯|)), we have (i) τ ↓ Y - = , and (ii) v = w on VT and w · τ = v on ¯z-. For D,M ⊆ D, we define D⊥ = {(v, τ, ⊥) | (v, τ, w) ∈ D}, and (v, τ, w) ∈ D
M if (v, τ1, u) ∈ D and (u, τ2, w) ∈ M exist with τ = τ1 ·τ2. For states wα, wβ, the merged state wα ⊕ wβ is ⊥ if one of the substates wα or wβ is ⊥. Otherwise, wα ⊕ wβ = wα on BV(α) and wα ⊕ wβ = wβ on BV(α)- (or, equivalently by syntactic well-formedness, on BV(β) and BV(β), respectively). If Y is the set of all channel names occurring in α, we write τ ↓ α for τ ↓ Y .

 Communication τ of α1 α2 is implicitly characterized via its subsequences for the subprograms. By τ = τ ↓ (α1 α2), there is no non-causal communication. Joint communication and the whole computation are synchronized in global time by the projections and by wα1 = wα2 on {μ, μ }, respectively. Likewise, by projection, communication is synchronously recorded by trace variables.

 In particular,* ∅ ϕ*.*

In item 6 and 7, reachable worlds are built from states v and w, and communication τ , as change of state *and* communication are observable. The strict prefix ≺ for the assumption in case (commit) in item 6 excludes (when A ≡ C) the circularity that commitment C can be shown in states where it is assumed.

#### **2.3 Static Semantics**

In the uniform substitution process, checks of free and bound variables, as well as accessed and written channels, separate sound from unsound axiom instantiations. As parallelism requires fine-grained control over channels, the static semantics for dL [30] is lifted to a communication-aware static semantics for dLCHP. It uses accessed channels to characterize the subsequence of a communication trace influencing truth of a formula even more precisely than free variables.

To precisely grasp free and bound variables, and accessed and written channels, Definition 9 gives a semantic characterization. In this section, formulas are considered truth-valued, i.e., Iv[[φ]] = **tt** if Iv φ and Iv[[φ]] = **ff** if Iv φ.

**Definition 9 (Static semantics).** *For term or formula* e*, and program* α*, free variables* FV(e) *and* FV(α)*, bound variables* BV(α)*, accessed channels* CN(e)*, and written channels* CN(α) *form the static semantics.*

FV(e) = {z ∈ V | ∃I, v, v˜ *such that* v = ˜v *on* {z} *and* Iv[[e]] = Iv˜[[e]]} CN(e) = {*ch* ∈ Ω | ∃I, v, v˜ *such that* v ↓ {*ch*}- = ˜v ↓ {*ch*} *and* Iv[[e]] = Iv˜[[e]]} FV(α) = {z ∈ V | ∃I, v, v, τ, w ˜ *such that* v = ˜v *on* {z} *and* (v, τ, w) ∈ I[[α]]*, and there is no* (˜v, τ, ˜ w˜) ∈ I[[α]] *such that* τ˜ = τ *and* w = ˜w *on* {z}-} BV(α) = {z ∈ V | ∃I,(v, τ, w) ∈ I[[α]] *such that* w = ⊥ *and* (w · τ )(z) = v(z)} CN(α) = {*ch* ∈ Ω | ∃I,(v, τ, w) ∈ I[[α]] *such that* τ ↓ {*ch*} = }

The already subtle static semantics of hybrid systems [30] becomes even more subtle with communication and parallelism. For example, CHPs (silently) synchronize with the global time μ, which is free and bound in ODEs, and the differential μ is bound, i.e.,μ ∈ FV({x = θ & χ}) and μ, μ ∈ BV({x = θ & χ}) if the evolution has a run of non-zero duration, regardless of whether μ occurs in x. Since reachable worlds of CHPs consist of communication *and* state, bound variables BV(α) of program α compare v with the state-trace concatenation w · τ instead of missing τ . Consequently, h ∈ BV(ch(h)!θ) ⊆ FV(ch(h)!θ), which also reflects that the initial communication never gets lost.

**Lemma 10 (Bound effect property).** *The sets* BV(α) *and* CN(α) *are the smallest sets with the* bound effect property for program α*. That is,* v = w *on* VT *and* v = w · τ *on* BV(α) *if* w = ⊥*, and* τ ↓ CN(α)-= *for all* (v, τ, w) ∈ I[[α]]*.*

By the following *communication-aware* coincidence property, terms and formulas only depend on their free variables, which for trace variables can be further refined to the subtraces whose channels are accessed. This subtrace-level precision is crucial in the soundness proof of the parallel injection axiom as it allows to drop β from [α β]ψ only if β does not write channels of ψ that are not also written by α. The signature Σ(·) of an expression denotes all occurring symbols.

**Lemma 11 (Coincidence for terms and formulas).** *The sets* FV(e) *and* CN(e) *are the smallest sets with the* communication-aware coincidence property for term or formula e*. That is, if* v ↓ CN(e)=˜v ↓ CN(e) *on* FV(e) *and* I = J *on* Σ(e)*, then* Iv[[e]] = Jv˜[[e]]*. In particular, for formula* φ*:* Iv φ *iff* Jv˜ φ*.*

Programs communicate but do *not* depend on the recorded history, thus the coincidence property for programs is not communication-aware. However, programs can produce the same communication starting from coinciding states.

**Lemma 12 (Coincidence for programs).** *The set* FV(α) *is the smallest set with the* coincidence property for program α*. That is, if* v = ˜v *on* X ⊇ FV(α)*, and* I = J *on* Σ(α)*, and* (v, τ, w) ∈ I[[α]]*, then* (˜v, τ, ˜ w˜) ∈ J[[α]] *exists such that* w = ˜w *on* X*, and* τ = ˜τ *, and (*w = ⊥ *iff* w˜ = ⊥*).*

# **3 Uniform Substitution for dL**CHP

In dLCHP, a uniform substitution [30] σ maps function and predicate symbols to terms (of equal sort) and formulas, respectively, while substituting the arguments of the symbol for their placeholders in the replacement, and program constants are mapped to CHPs. For example, σ = {f(*·*)→ *·* + 1, a → ch(h)?v; {x = v}} replaces all occurrences of function symbol f with *·* + 1 while the reserved 0-ary function symbol *·* marks the positions for the parameter of f in the replacement. Moreover, σ replaces the program constant a with the program ch(h)?v; {x = v}.

The key to sound uniform substitution is that new free variables must not be introduced into a context where they are bound [8]. In the presence of communication, likewise, *new channel access must not be introduced into contexts* where the channel is written (B I). For parallelism, substitution *must not reveal internals* of the parallel context to the local abstraction of a subprogram (B II), and must not violate state disjointness. The one-pass approach [32] used for dLCHP postpones these checks *and* simply applies the substitution recursively while collecting written variables and channels as taboo set (Fig. 2), thus operates linearly in the input. Clashes between the taboo, and new free variables and channel access are only checked locally at the replacement site. Likewise, clashes between the permitted channels and variables of a program constant, and its replacement program are checked locally.

The substitution operator σU,W Z (α) for program α takes an input taboo U ⊆ V ∪ Ω and a parallel context W ⊆ V , and returns, if defined, the substitution result and a set of output taboos Z ⊆ V ∪ Ω. For terms and formulas, the substitution operator σU only takes a taboo U ⊆ V ∪Ω as input. The substitution process clashes, i.e., prevents unsound instantiation, if it were to introduce a free variable or accessed channel into a context where it is bound (B I) *or* if it were to write variables and channels violating abstraction (B II). Moreover, substitution preserves well-formedness of programs and formulas, i.e., substitution clashes if replacements were to violate well-formedness.

**Fig. 2.** Application of uniform substitution for taboo U and parallel context W, where WU,γ ≡ W ∪ (BV(σU,W (γ) \ ({μ, μ- } ∪ VT )) for any program γ, and e ↓ Y for term e is recursive push down of projection ↓Y , where p(Y0, e) ↓ Y ≡ p(Y0 ∩ Y,e).

The side condition (FV(σf(*·*)) ∪ CN(σf(*·*))) ∩ U = ∅ implements locally that the replacement for f must not introduce free parameters that are tabooed by U (B I). The substitution {*·* → σU (e ↓ Y )}∅ is responsible for the argument e, 3 where ∅ suffices as the taboo U is already checked on e ↓ Y . By the projection, e↓Y only depends on channels Y . Quantification ∀z taboos the bound variable z. Program α in a box or ac-box has an empty parallel context ∅.

The substitution σU,W Z (α) computes the output taboo Z by adding the written variables and channels of program α to U, e.g., real variable x for assignment x := θ and for receiving ch(h)?x additionally channel ch and trace variable h. The output taboo Z is passed to ac-formulas and postconditions of boxes and ac-boxes for recursive checks for clashes w.r.t. (B I). Crucially for soundness, Lemma 13 below proves that σU,W Z (·) correctly computes the output taboo Z.

The taboo U∪W passed to nested expressions contains the parallel context W to prevent free variables in replacements of function and predicate symbols that are bound in parallel. This prepares the substitution process to preserve the syntax restrictions for parallel composition from previous work [6].4 Substitution for evolution {x = θ & χ} considers that the global time μ, μ is always implicitly bound regardless of whether it occurs in x, x . The fixpoint notation σZ,W Z (α) for the replacement of repetition α∗ ensures that the output taboo of the first iteration is tabooed in the subsequent iterations [32]. Computing the parallel context of α and β in case α β requires one additional pass for both subprograms because what they potentially bind after substitution adds to the parallel context of the respective other subprogram.

**Lemma 13 (Correct output taboo).** *Application* σU,W Z (α) *of uniform substitution retains input taboo* U *and correctly adds the bound variables and written channels of program* α*, i.e.,* Z ⊇ U ∪ BV(σU,W Z (α)) ∪ CN(σU,W Z (α))*.*

The side condition of σU,W Z (a(|Y, z¯|)) maintains local abstraction of subprograms (B II) because the replacement cannot bind more than a(|Y, z¯|), thus cannot bind variables and channels of an abstraction that is independent of a(|Y, z¯|). This also preserves state-disjointness (well-formedness) of parallel programs.

#### **3.1 Semantic Effect of Uniform Substitution**

The key ingredients for proving soundness of uniform substitution are Lemma 16 and 17 below. They prove that the effect of the syntactic transformation applied by uniform substitution can be equally mimicked by semantically modifying the interpretation of function and predicate symbols, and program constants. This adjoint interpretation σ∗ wI for interpretation I and state w changes how symbols are interpreted according to their syntactic replacements in the substitution σ.

3 Extension to vectorial arguments is straightforward.

4 For α β, the restriction is (V(α) ∩ BV(β)) ∪ (V(β) ∩ BV(α)) ⊆ {μ, μ- } ∪ VT [6]. However, in this paper, programs obey a less restrictive syntax for simplicity.

**Definition 14 (Adjoint substitution).** *For interpretation* I *and state* w*, the* adjoint interpretation σ∗ wI *changes the meaning of function and predicate symbols, and program constants according to the substitution* σ *evaluated in state* w*:*

$$\begin{aligned} &\sigma\_w^\* I(f^{\mathbb{M}} : \mathbb{M}\_{\text{arg}}) : \mathbb{M}\_{\text{arg}} \to \mathbb{M}; d \mapsto I^d\_\cdot w[\sigma f(\cdot)] \quad \text{where } \mathbb{M}, \mathbb{M}\_{\text{arg}} \in \{\mathbb{R}, \mathbb{N}, \Omega, T\} \\ &\sigma\_w^\* I(p : \mathbb{M}\_{\text{arg}}) = \{d \in \mathbb{M}\_{\text{arg}} \mid I^d\_\cdot w \succeq \sigma p(\cdot)\} \quad \text{where } \mathbb{M}\_{\text{arg}} \in \{\mathbb{R}, \mathbb{N}, \Omega, T\} \\ &\sigma\_w^\* I(a[\!\!\!/ \!f, \bar{z}] \!\!\} = I[\!\!\! \!a \,] \end{aligned}$$

We follow the observation for dGL [32] that the more liberal one-pass substitution requires stronger coincidence between the substitution and the adjoint on neighborhoods of the original state. Where the dGL soundness proof has succeeded by a neighborhood semantics of state on taboos, the dLCHP proof succeeds with a generalization to a neighborhood semantics of state and communication on taboos. The neighborhood of a state consists of its variations:

**Definition 15 (Variation).** *For a set* U ⊆ V ∪ Ω*, a state* v *is a* U-variation of state w *if* v *and* w *only differ on variables or projections onto channels in* U*, i.e.,* v ↓ (U- ∩ Ω) = w ↓ (U- ∩ Ω) *on* U-∩ V *.*

The proofs of Lemma 16 and 17 follow a lexicographic induction on the structure of substitution, and term, formula, or program. In Lemma 17, the induction is mutual for formulas and programs.

**Lemma 16 (Semantic uniform substitution).** *The term* e *evaluates equally over* U*-variations under uniform substitution* σU *and adjoint interpretation* σ∗ wI*, i.e.,* Iv[[σU (e)]] = σ∗ wIv[[e]] *for all* U*-variations* v *of* w*.*

**Lemma 17 (Semantic uniform substitution).** *The formula* φ *and the program* α *have equal truth value and semantics, respectively, over* U*-variations under uniform substitution* σU *and adjoint interpretation* σ∗ wI*, i.e.,*

*1. for all* U*-variations* v *of* w*:* Iv σU (φ) *iff* σ∗ wIv φ *2. for all* (U ∪W)*-variations* v *of* w*:* (v, τ, o) ∈ I[[σU,W Z (α)]] *iff* (v, τ, o) ∈ σ∗ wI[[α]]

#### **3.2 Uniform Substitution Proof Rule**

The proof rule US for uniform substitution is the single point of truth for the sound instantiation of axioms (plus renaming of bound variables [30] and written channels, e.g., [x := θ]ψ(x) to [y := θ]ψ(y) and [ch(h)?x]ψ(ch) to [dh(h)?x]ψ(dh). Soundness of the rule, i.e., that validity of its premise implies validity of the conclusion, immediately follows from Lemma 17. Since the substitution process starts with no taboos, σ(φ) is short for σ∅(φ). If the substitution clashes, i.e., σ∅(φ) is not defined, then rule US is not applicable.

**Theorem 18 (**US **is sound).** *The proof rule* US *is sound.*

$$\frac{\phi}{\sigma(\phi)}\text{ us}$$

Unlike dL [30] and dGL [32], dLCHP has a context-sensitive syntax for programs and formulas (see Definition 2 and Definition 4). By Proposition 19, uniform substitution, however, preserves syntactic well-formedness. Since all axioms in Sect. 4 will be well-formed, only well-formed formulas can be derived in dLCHP.

**Proposition 19 (**US **preserves well-formedness).** *The result* σU (φ) *(if defined) of applying uniform substitution to a well-formed formula* φ *is wellformed.*

### **4 Axiomatic Proof Calculus**

Figure 3 presents a sound proof calculus for dLCHP. The significant difference to dLCHP's schematic calculus [6] is that it completely abandons soundness-critical side conditions, internalizing them syntactically in the axioms. Only axiom **[]**W**A** was adjusted to obtain a symbolic representation and an ac-version K**AC** of modal modus ponens is included. Now, distribution of ac-boxes over conjuncts **[]AC***∧* and ac-monotonicity M**[***·***]AC** derive from K**AC**, thus are dropped. Except for the small changes soundness is inherited from the schematic axioms [6].

Algebraic laws for reasoning about traces [6] can be easily adapted to uniform substitution as well [7]. Decidable first-order real arithmetic [41] and Presburger arithmetic [34] have corresponding oracle proof rules [6].

*Remark 20.* To obtain a truly finite list of axioms from Fig. 3, symbolic (co)finite sets can be finitely axiomatized as a boolean algebra together with extensionality, which can be unrolled to a finite disjunction for (co)finite sets [7].

**Parallel Composition.** The parallel injection axiom **[ ]AC** in Fig. 3 decomposes parallel CHPs by local abstraction (B II). Unlike dLCHP's [6] and Hoarestyle [46,47] schematic calculi for ac-reasoning, axiom **[ ]AC** internalizes the noninterference property [6, Def. 7] that determines valid instances of formula

$$[\alpha]\_{\{\mathsf{A},\mathsf{C}\}}\psi \to [\alpha \parallel \beta]\_{\{\mathsf{A},\mathsf{C}\}}\psi \tag{1}$$

purely syntactically. To focus on noninterference, a(|Ya, z¯a|) wf b(|Yb, z¯b|) abbreviates well-formed parallel composition a(|Ya, z¯a|) b(|Yb,(¯zb ∩ z¯- a) ∪ {μ, μ } ∪ VT |) using operator wf for program constants a(|Ya, z¯a|), b(|Yb, z¯b|). This notation ensures disjoint parallel state except for the global time μ, μ and recorder variables VT .

Intuitively, axiom **[ ]AC** restricts β in Eq. (1) such that α overapproximates the behavior of α β influencing A, C, or ψ. For this purpose, noninterference internalized in b(|Yb ∩ (Y - ∪ Ya), z¯-|) forbids b to bind variables ¯z that are free in the postcondition p(Y, z¯), and Y forbids b to bind channels Y (except for channels Ya written by a because joint parallel communication can already be observed from a, too). Moreover, parallel programs always agree on the global time μ, μ and the communication recorded by trace variables VT . Therefore, the operator wf explicitly allows their sharing even if ¯z disallows it. Note that Ya and Y , and ¯za and ¯z may overlap but can also be disjoint.

$$\begin{array}{lcl} [\![\![\![\![\![\![\![\![\![\![\![\![\![\![\![\![\![\![\![\![\![\![\![\![\![\![\![\![\![\![\![\![\!\!]\!]\!]\!]\!]\!]\!]\!]\!\!}\!]\!\!]\!\!}\!\!]\!\![\![\![\![\![\![\![\![\![\!\!]\!]\!]\!]\!]\!]\!\!\!}\!\!\!}\!\!\!\!}\!\!\!\![\![\![\![\![\![\![\![\![\![\!\!]\!]\!]\!]\!]\!]\!\!\!]\!\!\!}\!\!\!\!\!}\!\!\!\!\!\!\!\!\!}\!\!\!\!\!\![\![\![\![\![\![\![\![\![\![\![\![\![\![\![\![\![\![\![\![\![\![\![\![\![\!.\!]\!]\!]\!]\!]\!]\!]\!]\!\!}\!\!\!}\!\!\!\!\!}\!\!\!\!\!\!}\!\!\!\!\!\!\!}\!\!\!\!\!\!}\!\!\!\!\!\!}\!\!\!\!\!\!\!\!}\!\!\!\!\!\!\!}\!\!\!\!\!\!\!\!}\!\!\!\!\!\!\!}\!\!\!\!\!\!\!\!}\!\!\!\!\!\!\!\!}\!\!\!\!\!\!\!\!}\!\!\!\!\!\!\!\!\!}\!\!\!\!\!\!\!\!\!}\!\!\!\!\!\!\!\!\!\!\!\!}\!\!\!\!\!\!\!\!\!\!\!\!\!\!}\!\!\!\!\!\!\!\!\!\!\!\!\!\!\!\!}\!\!\!$$

**Fig. 3.** dLCHP proof calculus

Despite its asymmetric shape, axiom **[ ]AC** decomposes [αβ](φ∧ψ) into [α]φ and [β]ψ (if they mutually do not interfere) via independent proofs for [αβ]φ and [αβ]ψ, which drop either α or β by **[ ]AC** modulo commutativity.

**Axiom System.** For each program statement, there is either a dynamic or an ac-axiom because the respective other version derives by axiom **[]***-,* or **[***-***]AC**. Axioms **[:=]**, **[:***∗***]**, and **[?]** are as in dL [30]. Axioms **[;]AC**, **[***∪***]AC**, and **[** *∗***]AC** for decomposition, and I**AC** for induction carefully generalize their versions in differential [30] dynamic [14] logic to ac-reasoning. Sending is handled step-wise via flattening the assumption-commitments by axiom **[**ch**!]AC** and axiom **[**ch**!]** that executes the effect onto the recorder h. The duality **[**ch**?]AC** turns receiving into arbitrary sending, which only synchronizes if it agrees with the parallel context on the value. Usage of axiom W**[]AC** is for convenience. Axiom **[***μ***]** materializes the flow of global time μ such that dL's axiomatization of continuous evolution [30] gets applicable, which requires ODE shape ¯x = f R(¯x). The axiomatic proof

rules G**AC**, MP, *∀*, and CE are an ac-version of G¨odels generalization rule, modus ponens, quantifier elimination, and contextual equivalence, respectively.

The axiom **[]**W**A** can weaken assumptions. Its slight change compared to dLCHP's schematic calculus [6] exploits that the compositionality condition WA is only required for a's reachable worlds. Interestingly, dLCHP's monotonicity rule M**[***·***]AC** [6] does not derive from modal modus ponens K**AC** and G¨odel generalization G**AC** in analogy to dL [30] but needs W**[]AC** handling monotonicity of assumptions, which does not fit into G**AC** because necessitating the assumption in G**AC** would render the derivation of [α]{ T ,T}T by G**AC** impossible.

Axioms using postcondition P ≡ p(Y, z¯), e.g., in **[;]AC**, allow any replacement of P since accessed channels Y ⊆ Ω and free variables ¯z ⊆ VR ∪ VT can be arbitrary. Replacements of assumptions R ≡ r(Y, h¯) and commitments Q ≡ q(Y, h¯) can instead only mention trace variables h¯ ⊆ VT bound in their context. This reflects that trace variables are the only interface between the program α and the ac-formulas A and C in an ac-box [α]{A,C}ψ (well-formedness).

**Theorem 21 (Soundness).** *The proof calculus for* dLCHP *presented in Fig. 3 is sound as an instantiation of the schematic calculus [6].*

**Clashes.** Clashes sort out unsound instantiations of axioms. Unlike in dL and dGL [30,32] whose clashes are solely due to tabooed variables in terms and formulas, clashes in dLCHP can also be due to tabooed channels, and even due to taboos in programs. For example, the substitution σ = {a → gh(h)!1, b → ch(h)!2, p→ψ, r →T, q →T} with ψ ≡ |h ↓ ch| > 0 ∧ |h ↓ dh| > 0 ∧ y < 0 clashes below, where Y = {ch, dh}, and ¯z ≡ h, y, and R ≡ r(Y ), and Q ≡ q(Y ). Writing channel ch in the replacement for b would break the local abstraction of a as ch is accessed in ψ but not written in the replacement for a, thus the clash indeed sorts out an unsound instantiation.

$$\frac{[a\{\{\text{gh}\},h\}]\_{\{\text{R},\text{Q}\}}p(Y,\bar{z}) \to [a\{\{\text{gh}\},h\} \parallel\_{\text{wf}} b\{\{\text{ch}\} \cap (Y^{\text{E}} \cup \{\text{gh}\})\}, \bar{z}^{\text{E}}]\}\_{\{\text{R},\text{Q}\}}p(Y,\bar{z})}{[\text{gh}(h)!1]\_{\{\text{T},\text{T}\}}\psi \to [\text{gh}(h)!1 \parallel \text{ch}(h)!2]\_{\{\text{T},\text{T}\}}\psi} \ \ \ \forall \text{class} \rangle$$

In contrast, σ = {a→ch(h)?x; gh(h)!1, b →ch(h)!2, p→ψ, r →T, q →T} does not clash below, where Y = {ch, dh}, and Ya = {ch, gh}, and other abbreviations are as above, because ch ∈ Y - ∪ Ya = {dh}-. Intuitively, the ch-communication of b remains observable after dropping b from the parallel composition as it is joint with a.

$$\frac{\begin{array}{c} \ast\\ \end{array}}{\begin{array}{c} [a\{Y\_{a},h,x\}\big]\_{\{\mathsf{R},\mathsf{Q}\}} p(Y,\overline{z}) \rightarrow [a\{Y\_{a},h,x\}\big]\_{\{\mathsf{wf}\}} b\{\{\mathsf{ch}\}\cap\{Y^{\mathsf{C}}\cup Y\_{a}\},\overline{z}^{\mathsf{Q}}\}\big]\_{\{\mathsf{R},\mathsf{Q}\}} p(Y,\overline{z})\\ \hline [\mathsf{ch}(h)?x;\mathsf{g}(h)!1\big]\_{\{\mathsf{T},\mathsf{T}\}}\psi \rightarrow [(\mathsf{ch}(h)?x;\mathsf{g}(h)!1)\parallel\{\mathsf{ch}(h)!2\big]\_{\{\mathsf{T},\mathsf{T}\}}\psi\end{array}}{\text{US}} \text{US}$$

Also note that by the operator wf for well-formed parallel composition, the recorder variable h can be shared without causing a clash above. However, clashes prevent instantiation that would violate syntactic well-formedness of programs (Definition 2) by binding the same state variable in parallel:

$$\frac{[a\{\emptyset,x\}]\_{\{r,q\}}p(x,y) \to [a\{\emptyset,x\}\parallel\_{\text{wf}}b\{\emptyset,\{x,y\}^{\mathbb{C}}\}]\_{\{r,q\}}p(x,y)}{[x:=y]\_{\{\tau,\tau\}}y = x \to [x:=y \parallel x:=0]\_{\{\tau,\tau\}}y = x} \text{ } \neq \text{classh}$$

Well-formedness of programs and formulas is ensured in the axioms by wellformed parallel composition wf and limitation to trace variables h¯ in Rj ≡ rj (Y, h¯) and Qj ≡ qj (Y, h¯) in ac-boxes [α]{R*j* ,Q*j* }ψ in Fig. 3, respectively. By Proposition 19, uniform substitution always preserves well-formedness.

*Example 22.* The proof tree below decomposes safety (Example 5) of cruise control (Example 3) into safety 1 of controller ct and branch 2 to be continued to safety of the vehicle ve. The lower subproof introduces the ac-formulas

$$\mathsf{A} \equiv \mathsf{C} \equiv \left( |h \downarrow \text{tar}| > 0 \to 0 \le \mathsf{va1}(h \downarrow \text{tar}) \le V \right),$$

using axiom **[]**W**A** to abstract from the communication between ct and ve. The upper subproof uses the parallel injection axiom **[ ]AC** to drop ve. Uniform substitution US does not clash as the commitment C only refers to joint communication of ct and ve. Other applications of US (e.g., for **[]**W**A**) are omitted. Rule Prop denotes propositional reasoning. Abbreviations are as follows: α ≡ a(|tar, vtr ct , t, t , μ, μ , h|), R ≡ r(tar, h), Q ≡ q(tar, h), P ≡ p(tar).

#### **5 Related Work**

Uniform substitution for differential dynamic logic dL [30] generalizes Church's uniform substitution for first-order logic [8, §35, 40]. Unlike the lifting from dL to differential game logic dGL [31], dLCHP generalizes into the complementary direction of communication and parallelism. Unlike schematic calculi [2,19,27, 44,46], whose treacherous schematic simplicity relies on encoding all subtlety of parallel systems in significant soundness-critical side conditions, our development builds upon a minimalistic non-schematic parallel injection axiom *and* sound instantiation encapsulated in uniform substitution. This provides a new, more atomic and more modular understanding of parallel systems overcoming the root cause for large soundness-critical prover kernels [5,9,12,16,18,36]. Usage of uniform substitution reduced the kernel of the theorem prover KeYmaera from 105 kLOC to 2 kLOC in KeYmaera X [23]. We expect dLCHP's integration into KeYmaera X to stay in the same order of magnitude.

To the best of our knowledge, assumption-commitment reasoning [22,46] 5 has no tool support, which might be due to vast implementation effort. The latter can be underpinned by analogy with tools [5,9,16,18,36] for verification of sharedvariables concurrency, some of which use rely-guarantee reasoning [36,39]. Unlike uniform substitution for dLCHP that enables a straightforward implementation of a small prover kernel, they all rely on large soundness-critical code bases. Unlike refinement checking for CSP [12] and discrete-time CSP [4], dLCHP supports safety properties of dense-time hybrid systems. Contrary to our goal of small prover kernels, implementations of model checkers [12] are inherently large.

Beyond embeddings of concurrency reasoning for discrete systems into proof assistants [3,25,26,38], dLCHP can verify parallel hybrid systems synchronizing in shared global time. The latter imposes even more complicated binding structures than parallel or hybrid systems alone but dLCHP's uniform substitution calculus continues to manage them in a modular way.

The recent tool HHLPy [37] for hybrid CSP (HCSP) [17] is limited to the sequential fragment. Unlike extending HHLPy to parallelism, which would require extensive soundness-critical side conditions and a treatment of the duration calculus, integrating dLCHP into KeYmaera X [11] boils down to adding a finite list of concrete object level formulas as axioms and only small changes to the uniform substitution process. In contrast to dLCHP's compositional parallel systems calculus [6], HCSP calculi [13,20,42] are non-compositional [6] as they either unroll exponentially many interleavings from the operational semantics [13,42] or can only decompose independent parallel components [20] causing limited ability to reason about complex systems. Former HCSP tools [43,45] only implement a non-compositional calculus [20] reinforcing the significance of our approach for managing parallel hybrid systems reasoning. Other hybrid process algebras defer to model checkers for reasoning [10,21,40]. Further discussion of dLCHP is in [6].

### **6 Conclusion**

This paper introduced a sound one-pass uniform substitution calculus for the dynamic logic of communicating hybrid programs dLCHP thereby mastering the significant challenge of developing simple sound proof calculi for parallel hybrid systems with communication. Uniform substitution can separate even notoriously complicated binding structures from parallelism with communication in multi-dynamical logics into axioms and their instantiation. In the case of dLCHP,

5 Assumption-commitment and rely-guarantee reasoning are specific patterns for message-passing and shared variables concurrency, respectively. The broader assumeguarantee principle has been used across diverse areas for various purposes.

this applies to channel access in predicates and the need for local abstraction of subprograms in parallel statements, and it even turns out that uniform substitution can maintain a context-sensitive syntax along the way. Thanks to uniform substitution, parallel systems reasoning reduces to multiple uses of an asymmetric parallel injection axiom.

Now, with uniform substitution a straightforward implementation of dLCHP in KeYmaera X is only one step away.

**Acknowledgments.** This project was funded in part by the Deutsche Forschungsgemeinschaft (DFG) – 378803395 (ConVeY), an Alexander von Humboldt Professorship, and by the AFOSR under grant number FA9550-16-1-0288.

### **References**

**Open Access** This chapter is licensed under the terms of the Creative Commons Attribution 4.0 International License (http://creativecommons.org/licenses/by/4.0/), which permits use, sharing, adaptation, distribution and reproduction in any medium or format, as long as you give appropriate credit to the original author(s) and the source, provide a link to the Creative Commons license and indicate if changes were made.

The images or other third party material in this chapter are included in the chapter's Creative Commons license, unless indicated otherwise in a credit line to the material. If material is not included in the chapter's Creative Commons license and your intended use is not permitted by statutory regulation or exceeds the permitted use, you will need to obtain permission directly from the copyright holder.

# An Isabelle/HOL Formalization of the SCL(FOL) Calculus

Martin Bromberger1 , Martin Desharnais1,2(B) , and Christoph Weidenbach1

1 Max Planck Institute for Informatics, Saarland Informatics Campus, Saarbrücken, Germany<EMAIL_ADDRESS>2 Graduate School of Computer Science, Saarland Informatics Campus,

Saarbrücken, Germany

Abstract. We present an Isabelle/HOL formalization of Simple Clause Learning for first-order logic without equality: SCL(FOL). The main results are formal proofs of soundness, non-redundancy of learned clauses, termination, and refutational completeness. Compared to the unformalized version, the formalized calculus is simpler and more general, some results such as non-redundancy are stronger and some results such as non-subsumption are new. We found one bug in a previously published version of the SCL Backtrack rule. Compared to related formalizations, we introduce a new technique for showing termination based on non-redundant clause learning.

Keywords: interactive theorem proving · automated theorem proving · first-order logic · CDCL · SCL · non-redundant clause learning

### 1 Introduction

The SCL ("Clause Learning from Simple Models" or simply "Simple Clause Learning") family of calculi lifts a conflict-driven clause learning (CDCL) approach to first-order logic: SCL(FOL) is for first-order logic without equality [8,10], SCL(T) is for first-order logic with theories [6], SCL(EQ) is for firstorder logic with equality [12], and HSCL is for exhaustive partial models exploration in first-order logic without equality [7]. In its original formulation [10], SCL(FOL) required exhaustive propagation and a precise strategy for the application of the rules in order to learn non-redundant clauses. This was improved upon by SCL(T) [6] by dropping exhaustive propagation and weakening the strategy, i.e., any run according to the strategy in [10] is also a run according to the strategy in [6]. The SCL(FOL) version presented in Bromberger et al. [8] integrates those changes and additionally refines the Backtrack rule.

We present an Isabelle/HOL formalization of the non-executable specification of SCL(FOL) based on and developed in parallel to Bromberger et al. The main results are soundness, non-redundancy of learned clauses, termination, and refutational completeness. In contrast to the goal of Bromberger et al. to guide toward an implementation, our goal is to be as simple and general as possible. For that, we (i) simplified the calculus (e.g., no more explicity tracking of decision levels), (ii) generalized the calculus (e.g., multiple acceptable positions in the Backtrack rule), (iii) strengthened existing theorems (e.g., Theorem 11 on non-redundancy), and (iv) proved new theorems (e.g., Corollary 12 on nonsubsumption).

This work is part of the IsaFoL (Isabelle Formalization of Logic) effort [2], which aims at developing a library of results about logical calculi. The Isabelle theory files are available in the *Archive of Formal Proofs* (AFP) [9] and amount to more than 11 000 lines of source text. They build heavily upon many other entries of the AFP: (i) First\_Order\_Terms [17] for first-order terms, term substitutions, and MGU; (ii) Ordered\_Resolution\_Prover [14–16] for the clausal calculus, clause substitutions, Herbrand interpretation, and compactness of firstorder logic; and (iii) Saturation\_Framework\_Extensions [5,18] for entailment of the clausal calculus. We contributed many lemmas and definitions back to both the Isabelle distribution and the aforementioned AFP entries (e.g., over 50 to First\_Order\_Terms). We made heavy use of the Isar language [19] to write structured proofs, the Sledgehammer tool [13] for proof automation, and locales [1]—Isabelle's parameterized module system—to structure our development and reuse existing components from the AFP entries. To ease associating the main results in this paper with their counterparts in the Isabelle development, names in monospace are taken verbatim from the formalization.

The formalization follows the basic ideas of the existing formalizations of the first-order resolution calculus [16] and propositional CDCL calculi [3,4]. Compared to propositional logic, first-order logic adds a number of challenges: the extra term level requires to consider variables, substitutions, groundings, and the concept of factorization. To preserve completeness, propagation of ground literals must not be exhaustive anymore, resulting in a level-wise exploration w.r.t. a bounding atom. Inside this bound, the calculus always terminates. If one level does not suffice to find a refutation, the bound can be increased and exploration can be continued. For unsatisfiable formulas, we prove the existence of a bound sufficient to derive ⊥, which guarantees that only finitely many levels need to be explored.

The paper is now organized as follows. Section 2 recaps the SCL(FOL) calculus from Bromberger et al. as the basis of our formalization presented in Sect. 3. We first present the Isabelle formalization of the abstract rules of the SCL(FOL) calculus. Then we prove invariants preserved by the rules starting from the initial state, Lemma 1. Subsequently, we prove soundness, Theorem 7, non-redundancy of learned clauses, Theorem 11, termination with respect to a fixed bound, Theorem 18, and finally refutational completeness with respect to an appropriate bound, Theorem 20. We discuss important aspects of the formalization and proof ideas here and refer the reader to the formalization for more details. The paper ends with a short conclusion of the obtained results.

### 2 The SCL(FOL) Calculus

We shortly repeat basic first-order logic notions and the SCL(FOL) calculus presented in Bromberger et al. We consider an untyped, first-order logic without equality. A *term* is defined inductively as either a variable x or a function application f( −→t ) for a constant f and a (possibly-empty) list of terms −→t . An *atom* is a predicate symbol applied to a list of term arguments. A *literal* is either a positive atom A or a negative atom ¬A. For literals we write L or K. The atom of a literal may be selected with atom(A) = A and atom(¬A) = A. The complement of a literal is defined as comp(A) = ¬A and comp(¬A) = A. A disjunctive *clause* is a finite multiset of literals. For clauses we write C or D. We use the syntax L ∨ C and C ∨ D synonymously with the multiset sums {L} + C and C + D respectively. We also use the syntax ⊥ synonymously with the empty multiset {}. All variables in clauses are to be understood as universally quantified.

*Substitutions* are total unary functions from variables to terms. A substitution σ may be applied to a variable x, a term t, an atom A, a literal L, or a clause C, denoted xσ, tσ, Aσ, Lσ, or Cσ respectively. Substitution application is leftassociative, i.e., Cσ1σ2 = (Cσ1)σ2. The domain of a substitution σ is defined as dom(σ) = {x | xσ = x}. The composition of two substitutions σ1 and σ2 is defined as the function σ1 ◦ σ2 = (λx. xσ1σ2). A substitution γ is a *grounding* for a term t, an atom A, a literal L, or a clause C if tγ, Aγ, Lγ, or Cγ are respectively ground, i.e., if they do not contain variables. A substitution ρ is a *renaming* if it is injective and xρ is a variable for all variables x. The *inverse* of a renaming ρ is any function ρ−1 from terms to variables such that ρ−1 (xρ) = x for all variables x. The *restriction* of a substitution σ to a set of variables V is defined as the function (λx. if x ∈ V then xσ else x). A substitution σ is *idempotent* if σ ◦ σ = σ. A substitution υ is a *unifier* for a set of terms T if t1υ = t2υ for all terms t1 ∈ T and t2 ∈ T. A substitution μ is a *most general unifier* (MGU) for a set of terms T if μ is a unifier for T and there exists a substitution σ such that μ ◦ σ = υ for all unifiers υ for T. A substitution μ is an *idempotent, most general unifier* (IMGU) for a set of terms T if μ is a unifier for T and μ ◦ υ = υ for all unifiers υ for T; note that μ is an IMGU iff it is both idempotent and a MGU.

When formalizing logical calculi, IMGUs are preferable because they allow to apply groundings to a term both directly and after applying an IMGU, i.e., tγ = tμγ for all terms t, groundings γ, and IMGU μ. Non-idempotent MGU do not have this property as the following counter-example shows. Consider the terms t1 = f(x, y, z) and t2 = f(w, y, z), the grounding γ = {x → a, y → b, z → c, w → a}, and the non-idempotent MGU μ = {x → w, y → z, z → y} where x, y, z, w are variables and a, b, c are ground constants, then we have t1γ = f(a, b, c) = f(a, c, b) = t1μγ. In published literature, an IMGU is often meant instead of an MGU; the idempotency requirement is often kept implicit because standard implementations for computing MGUs actually produce IMGUs.

The function gnd(C) = {Cγ | Cγ is ground} expresses the set of all groundings of a clause C. The function gnd(N)=(- C ∈ N. gnd(C)) expresses the set of all groundings of a set of clauses N; its subset whose clauses are restricted to atoms less than or equal to a bound β w.r.t. an order ≺B is defined as gndBβ(N) = {C ∈ gnd(N)| ∀L ∈ C. atom(L) B β}. Note that gnd(gnd(N)) = gnd(N). The strict order ≺B is total on ground literals and is such that for each β there are only finitely many literals L with L ≺B β. An example of such an order could be KBO without zero-weight symbols. Note that LPO does not satisfy the last condition of a ≺B order although it is a well-founded and total order.

Herbrand entailment is defined as (I |=H N ←→ (∀C ∈ N. I |=H C)) for a set of clauses N, (I |=H C ←→ (∃L ∈ C. I |=H L)) for a clause C, (I |=H A ←→ A ∈ I), and (I |=H ¬A ←→ A /∈ I) for a literal with atom A; note that the symbol |=H is overloaded. Ground entailment is defined as (N1 |=G N2 ←→ (∀I.I |=H N1 −→ I |=H N2)). First-order entailment is defined as (N1 |= N2 ←→ gnd(N1) |=G gnd(N2)). A set of ground clauses N is satisfiable if there exists a Herbrand interpretation I such that I |=H N; otherwise, it is unsatisfiable.

An annotated literal is the pairing of a literal with an annotation. We call it a *decision literal* when the annotation is a natural number n indicating the literal's level (i.e., that it is the nth decision) and a *propagation literal* when the annotation is a closure of the clause the literal originated from. The literal of an annotated literal K is denoted lit(K) and the annotation is denotated ann(K). The level of a clause is the maximum level of its literals. A *trail* is a finite sequence of annotated ground literals: it grows from left to right. The empty trail is written and appending a new annotated literal K to a trail Γ is written Γ,K. The concatenation of two trails Γ1 and Γ2 is written Γ2, Γ1. A trail Γ can be converted to a set with set(Γ).

A literal L is true under trail Γ if L ∈ {lit(K)|K ∈ set(Γ)}. A literal L is false under trail Γ if comp(L) ∈ {lit(K)|K ∈ set(Γ)}. A literal L is defined in a trail Γ if L is true or false under Γ; otherwise, it is undefined. A clause C is true under trail Γ if (∃L ∈ C. L is true under Γ). A clause C is false under trail Γ if (∀L ∈ C. L is false under Γ). A clause C is defined in a trail Γ if (∀L ∈ C. L is defined in Γ); otherwise, it is undefined.

The SCL(FOL) calculus is defined as a transition system operating on states (Γ; N;U; β; k; C) where Γ is a trail, N is a finite set of initial clauses, U is a finite set of learned clauses, β is a bounding atom restricting the considered ground literals, k is a natural number counting the number of decisions taken in Γ, and C is either or a clause closure (C; γ) such that Cγ is ground and false in Γ. The initial state is (; N; ∅; β; 0; ) for some initial clause set N and bound β.

The transition relation ⇒SCL is a mapping between states. The rules below are from Bromberger et al. and serve as a reference for the Isabelle formalization described in Sect. 3.

Propagate (Γ; N;U; β; k; ) ⇒SCL (Γ, Lγ((C0∨L)μ;γ) ; N;U; β; k; ) if (C ∨L) ∈ (N ∪U), C = C0∨C1, C1γ = Lγ∨···∨Lγ, C0γ does not contain Lγ, μ is the IMGU of the literals in C1 and L, (C ∨L)γ is ground, (C ∨L)γ ≺B {β}, C0γ false under Γ, and Lγ is undefined in Γ.

Decide (Γ; N;U; β; k; ) ⇒SCL (Γ, Lγk+1; N;U; β; k + 1; ) if L ∈ C for a C ∈ (N ∪U), Lγ is a ground literal undefined in Γ, and Lγ ≺B β. Conflict (Γ; N;U; β; k; ) ⇒SCL (Γ; N;U; β; k; (C; γ)) if C ∈ (N ∪ U), Cγ is false under Γ for a grounding substitution γ.

These rules construct a (partial) model via the trail Γ for N ∪ U until a conflict, i.e., a clause false under Γ is found. The above rules always terminate, because there are only finitely many ground literals L with L ≺B β. It might be necessary to successively increase β for full refutational completeness.

Skip (Γ,K; N;U; β; k; (C; γ)) ⇒SCL (Γ; N;U; β; k − i; (C; γ)) if comp(K) does not occur in Cγ, if K is a decision literal then i = 1; otherwise, i = 0.

Factorize (Γ; N;U; β; k; (C ∨ L ∨ L ; γ)) ⇒SCL (Γ; N;U; β; k; ((C ∨ L)μ; γ)) if Lγ = L γ and μ = IMGU(L, L ).

Note that this rule may be used multiple times if the conflicting clause contains more than two duplicates of a given literal or if multiple distinct literals have duplicates.

$$\begin{array}{ll} \mathsf{Resolve} & (\Gamma, K \gamma\_D ^{(D \vee K; \gamma\_D)}; N; U; \beta; k; (C \vee L; \gamma\_C)) \\ & \Rightarrow\_{\mathrm{SCL}} & (\Gamma, K \gamma\_D ^{(D \vee K; \gamma\_D)}; N; U; \beta; k; ((C \vee D) \mu; \gamma\_C \circ \gamma\_D)) \\ \mathrm{if } K \gamma\_D = \mathrm{comp}(L \gamma\_C), \, \mu = \mathrm{IMGU}(K, \mathrm{comp}(L)). \end{array}$$

The clauses D ∨ K and C ∨ L are assumed to have disjoint variables.

Backtrack (Γ0, K, Γ1, comp(Lγ)k; N;U; β; k; (C ∨ L; γ)) ⇒SCL (Γ0; N;U ∪ {C ∨ L}; β; j; )

if Cγ is of level i < k, and Γ0, K is the minimal trail subsequence such that there is a grounding substitution γ with (C ∨ L)γ is false under Γ0, K but not in Γ0, and Γ0 is of level j.

The clause C ∨L added by the rule Backtrack to U is called a *learned clause*. The empty clause ⊥ can only be generated by rule Resolve or be already present in N, hence, as usual for CDCL-style calculi, the generation of ⊥ together with the clauses in N ∪ U represent a resolution refutation.

A sequence of SCL rule applications is called a *reasonable run* if the rule Decide does not enable an immediate application of rule Conflict. A sequence of SCL rule applications is called a *regular run* if it is a reasonable run and the rule Conflict has precedence over all other rules.

### 3 Formalization of the SCL(FOL) Calculus

The formalization introduces some new concepts absent from Sect. 2. A multiset C can be converted to a set, i.e., without duplicates, with set(C). The multiplicity of an element x in a multiset C is denoted by count(C, x). The cardinality of a multiset—the sum of the multiplicities of its elements—is denoted by |C|. The multiset whose only element is x with multiplicity n is denoted by repeat(n, x); note that count(repeat(n, x), x) = n, and set(repeat(n, x)) = {x} if n > 0. The multiset extension of an order on literals extends the order to multisets containing literals; we use the Huet-Oppen specification [11], one of several equivalent alternatives for this extension. The *adaptation* of a substitution σ to a renaming ρ is a function whose domain is the renamed domain of σ and whose codomain is the same as σ; it is defined as the function (λx. if x ∈ {yρ | y ∈ dom(σ)} then (ρ−1 x)σ else x). A substitution γ is a *merged grounding* of a grounding γA for a set of variables A and a grounding γB for a set of variables B if (A ∩ B = {} −→ (∀x ∈ A. xγA is ground) −→ (∀x ∈ B. xγB is ground) −→ (∀x ∈ A. xγ = xγA) ∧ (∀x ∈ B. xγ = xγB)); an example of a function that fulfills this specification is (λx. if x ∈ A then xγA else xγB). The length of a trail Γ is denoted by |Γ|. The nth right-most element of a trail Γ is denoted by Γ[n]; we use zero-based indexing where the right-most element is the 0th element. The Herbrand interpretation of a trail Γ is defined as HI(Γ)=(- K ∈ set(Γ). case lit(K) of A ⇒ {A}|¬A ⇒ {}).

The formalization also changes some existing concepts. No distinction is made between *atoms* and terms, so first-order terms are used everywhere in place of atoms. The level annotation of a *decision literal* is not required anymore and replaced by a † marker, it is now written K = (K; †) for some literal K. A *propagation literal* is written (KγD)(K;D;γD) = (KγD; (D; K; γD)) for some literal K, clause D, and grounding γD. Note that the propagated literal is explicitly separated from its clause in the closure annotation; this eases the formulation of the additional invariants 5 and 6 of Lemma 1., that the respective clause is always false under the respective trail. For the *trail* Γ,K, the Isabelle formalization uses the constructor List.Cons K Γ which actually grows from right to left. However, we keep the well-established left-to-right convention in this paper because it significantly eases the presentation. An state is a tuple (Γ;U; C) where Γ is a trail, U is a finite set of learned clauses, and C is an optional clause closure. The individual components can be selected with trail((Γ;U; C)) = Γ, learned((Γ;U; C)) = U, and conflict((Γ;U; C)) = C. The *initial state* is (; {}; ), i.e., empty trail, no learned clauses, and no conflicting closure. The finite set of initial clauses N and the bounding atom β are no longer stored in the state but are rather parameters of the transition relation; this was done to highlight the fact that they are never modified by any rule. The natural number k counting the number of decisions, used in Sect. 2 to determine an appropriate backtracking point, turned out not to be necessary and was dropped entirely. We assume the existence of a binary relation on atoms ≺B such that (∀β. {t|t ≺B β} is finite) but dropped the requirement for ≺B to be a strict order total on ground terms. We also don't lift ≺B to literals and clauses, but always use it at the atom level. We define the relation B as the reflexive closure of ≺B.

The transition relation ⇒N,β SCL is a binary predicate between states and is parameterized by the finite set N of initial clauses and the bounding atom β. It is defined as the disjunction of the following rules. Following each rule, we highlight the main differences from Sect. 2 not already covered.

Propagate (Γ;U; ) ⇒N,β Propagate (Γ,(Lμγ)(Lμ;C0μ;γ) ;U; ) if (L∨C) ∈ (N ∪U), γ is a grounding for L∨C, (∀K ∈ (L∨C). atom(Kγ) B β), C0 = {K ∈ C | Kγ = Lγ}, C1 = {K ∈ C | Kγ = Lγ}, C0γ is false under Γ, Lγ is undefined in Γ, and μ is an IMGU for all terms in {atom(K)| K ∈ (L ∨ C1)}.

Compared to Sect. 2, we express the splitting of C into C0 and C1 formally as set operations and replace ≺B with B. This replacement has no effect on the results but allowing the bound β to be in gndBβ(N) eases the proof of Lemma 21, where the largest element of the (finite) unsatisfiable core is directly used as new bound. There are also situations where the maximal element of a signature is required to derive a contradiction: a non-strict bound requires to artificially extend the signature while a non-strict bound does not.

Decide (Γ;U; ) ⇒N,β Decide (Γ,(Lγ);U; ) if (L∨C) ∈ N, γ is a grounding for L, Lγ is undefined in Γ, and atom(Lγ) B β.

Compared to Sect. 2, we replace ≺B with B and take the decision literal from N instead of N ∪ U. The ground instances of literals of U are a subset of the ground instances of literals of N so it is redundant to also consider U here.

Conflict (Γ;U; ) ⇒N,β Conflict (Γ;U; (C; γ)) if C ∈ (N ∪ U), γ is a grounding for C, and Cγ is false under Γ.

Skip (Γ,K;U; (C; γ)) ⇒N,β Skip (Γ;U; (C; γ)) if comp(lit(K)) ∈/ Cγ.

Factorize (Γ;U; (L ∨ L ∨ C; γ)) ⇒N,β Factorize (Γ;U; ((L ∨ C)μ; γ)) if Lγ = L γ and μ is the IMGU for the terms atom(L) and atom(L ).

Resolve (Γ;U; (L ∨ C; γC )) ⇒N,β Resolve (Γ;U; ((CρC ∨ DρD)μ; γ)) if Γ = Γ ,(KγD)(K;D;γD) , and KγD = comp(LγC ), ρC and ρD are renamings such that the variables of (L∨ C)ρC and (K ∨ D)ρD are disjoint, μ is the IMGU for the terms atom(L)ρC and atom(K)ρD, γ C and γ D are adaptations of γC and γD to the renamings ρC and ρD respectively, and γ is a merged grounding of γ C for the variables of (L ∨ C)ρC and γ D for the variables of (K ∨ D)ρD.

Note that the definition of merged grounding implies the following equalities: μ ◦ γ = γ, LρC γ = LγC , CρC γ = CγC , KρDγ = KγD, and DρDγ = DγD.

Compared to Sect. 2, we explicitly rename the merged clauses to avoid variable-name clashes instead of assuming disjoint variables, and use an abstract specification for the merged grounding instead of forcing substitution composition. The latter makes our rule more general by allowing more freedom to an implementation.

Backtrack (Γ, Γ ,K;U; (L ∨ C; γ)) ⇒N,β Backtrack (Γ; {L ∨ C} ∪ U; ) if K = comp(Lγ) and (γ . (L ∨ C)γ is ground and false under Γ).

Compared to Sect. 2, we allow backtracking to any non-conflicting trail instead of specifying the position. This makes our rule more general by, again, allowing more freedom to an implementation. The minimally backtracking strategy introduced in Definition 4 brings back equivalence to the Backtrack rule of Sect. 2.

Isabelle Technicalities. We define the SCL rules in the scl\_fol\_calculus locale. It fixes an abstract binary relation ≺B as a locale parameter and assumes that it bounds a finite number of atoms. It also fixes an abstract function to generate variable renamings as a locale parameter and assumes its correctness; this function is not required for the specification of the calculus but is required in multiple proofs. Most of the following definitions and theorems are in the context of this locale. Each SCL rule is defined separately as an inductive predicate. Having separate definitions allows to refer to the rules individually in subsequent definitions and theorems. Using inductive predicates, as opposed to plain definitions, is convenient because Isabelle automatically generates some useful introduction and elimination lemmas, and configures structured Isar syntax for case analysis.

From the SCL rules, we can prove a number of invariants about states. Most of them are intuitive while few are technicalities of the Isabelle formalization. We will use the invariants as hypotheses for many of the main lemmas and theorems.

Lemma 1 (scl\_state\_invariants). *Let* (Γ;U; C) *be an state w.r.t.* ⇒N,β *SCL . The following invariants hold for the initial state* (; {}; ) *and are each individually preserved by the SCL rules.*

	- *–* ∀DKγΓ Γ. Γ = Γ ,(Kγ)(K;D;γ), Γ −→ Dγ *is false under* Γ *–* ∀C γ. C = (C; γ) −→ Cγ *is false under* Γ
	- *–* ∀K ∈ *set*(Γ). ∀DK γ. *ann*(K)=(D; K; γ) −→ *lit*(K) = Kγ
	- *–* ∀K ∈ *set*(Γ). ∀DK γ. K = (Kγ)(K;D;γ) −→ *comp*(Kγ) ∈/ Dγ
	- ∀K ∈ D. ∃D ∈ N. ∃K ∈ D . ∃σ. K σ = K
	- *–* ∀K ∈ *set*(Γ). ∃L ∈ N ∪ U. ∃σ. Lσ = *lit*(K)

The SCL calculus is defined as a transition system where many decisions are deferred to strategies.  We say that a strategy S *restricts* a transition system T (or symmetrically that T is *restricted* by S) if (∀x y. S x y −→ T x y). Note that strategies can be chained to iteratively apply more restrictions.

We define the reasonable and regular strategies restricting the ⇒N,β SCL relation in order to prove the main results of this paper.

Definition 2. *The reasonable strategy* ⇒N,β *Rea-SCL restricts the SCL calculus by preventing decisions that immediately lead to a conflict. Such situations could be replaced by a propagation. Formally:*

$$S \Rightarrow\_{\text{Rea-SCL}}^{N,\beta} S' \quad \longleftrightarrow \quad S \Rightarrow\_{SCL}^{N,\beta} S' \land (S \Rightarrow\_{Decide}^{N,\beta} S' \longrightarrow (\nexists S'' \Rightarrow\_{Conific}^{N,\beta} S''))$$

Definition 3. *The regular strategy* ⇒N,β *Reg-SCL restricts the reasonable strategy by prioritizing the conflict rule to any other. Formally:*

$$S \Rightarrow\_{Reg\text{-}SCL}^{N,\beta} S' \quad \longleftrightarrow \quad S \Rightarrow\_{Reg\text{-}SCL}^{N,\beta} S' \land \{ (\exists S' \, '\, S \Rightarrow\_{Conflect}^{N,\beta} S' \prime) \longrightarrow S \Rightarrow\_{Conflect}^{N,\beta} S' \}$$

While not required for the coming results, we also define the minimally backtracking strategy to express the constraint on the backtracking position found in Sect. 2.

Definition 4. *The minimally backtracking strategy* ⇒N,β *Min-Bac-SCL restricts the regular strategy by requiring that backtracking removes the shortest possible suffix of the trail. Formally:*

$$S \Rightarrow\_{Min \cdot{Bac \cdot{}} \cdot{Bac \cdot{}} \cdot{SCL}}^{N, \beta} S' \quad \longleftrightarrow S \Rightarrow\_{Reg \cdot{SCL}}^{N, \beta} S' \land (S \Rightarrow\_{Backtrack}^{N, \beta} S' \longrightarrow) \\ \text{trail}(S') \text{ is the longest prefix of } \text{trail}(S) \\ \text{not } \text{in } \text{conflict } \text{with the } \text{leural} \text{ clause})$$

All three strategies build on one-another and ultimately restrict the SCL relation. We can express this formally as implications, of which the first can be used to show that coming results (e.g., Corollaries 13 and 19) also hold for the minimally backtracking strategy.

Lemma 5 (strategy\_restrictions). *The minimally backtracking strategy restricts the regular strategy, which restricts the reasonable strategy, which restricts the SCL calculus. Formally:*

*–* ∀NβSS . S ⇒N,β *Min-Bac-SCL* S −→ S ⇒N,β *Reg-SCL* S *–* ∀NβSS . S ⇒N,β *Reg-SCL* S −→ S ⇒N,β *Rea-SCL* S *–* ∀NβSS . S ⇒N,β *Rea-SCL* S −→ S ⇒N,β *SCL* S

The bounding atom β restricts the calculus to only consider the finitely many ground atoms less than or equal to β w.r.t. ≺B; this will play an important role in the termination proof. When SCL terminates, it either derived a contradiction, or it found a model for the bounded groundings of the initial clauses. Because β is usually chosen heuristically, the model might be unsatisfactory for the considered use case and one may want to continue execution with a bigger bound. This is allowed if the new bound properly extends the previous bound β w.r.t. B.

Theorem 6 (monotonicity\_wrt\_bound). *If the ground atoms bound by* β *are a subset of the ground atoms bound by* β *, formally if* (∀A. A *is ground* −→ A B β −→ A B β )*, then the SCL, reasonable SCL, regular SCL, and minimally backtracking transitions w.r.t.* β *are also transitions w.r.t.* β *, formally*

*–* ∀NSS . S ⇒N,β *SCL* S −→ S ⇒N,β- *SCL* S *, –* ∀NSS . S ⇒N,β *Rea-SCL* S −→ S ⇒N,β- *Rea-SCL* S *, –* ∀NSS . S ⇒N,β *Reg-SCL* S −→ S ⇒N,β- *Reg-SCL* S *, and –* ∀NSS . S ⇒N,β *Min-Bac-SCL* S −→ S ⇒N,β- *Min-Bac-SCL* S *.*

Theorem 6 implies that all properties w.r.t. a bound β also hold w.r.t. a compatible bound β . Its hypothesis is fulfilled if B is transitive on ground atoms, β and β are ground atoms, and β B β . The bounding atom could even be increased at any point in an SCL run, not just when the calculus terminated.

The different rules and strategies considered so far express a single step of computation for the SCL calculus; they offer a good level of granularity to both understand and mechanize the details of the calculus. But many results of the following sections ought to express properties of the calculus as a whole. We express such results in terms of a run from the initial state. A *run* is the reflexive, transitive closure of a rule or strategy, e.g. S (⇒N,β SCL)∗ S is an SCL run from the state S to the state S .

The soundness of the individual SCL rules is shown by invariant 10. We now consider the soundness of terminating runs of the SCL calculus as a whole.

Theorem 7 (correct\_termination). *Let* S = (Γ;U; C) *be a state w.r.t.* ⇒N,β *SCL . If invariants 2, 3, 5, 6 and 10 hold for* S*, and if* S *is a stuck state with some restrictions, formally if*

$$\begin{array}{l} \mathsf{-} \not\exists S'.S \Rightarrow\_{Propageate}^{N,\beta} S',\\ \mathsf{-} \not\exists S'.S \Rightarrow\_{Decide}^{N,\beta} S' \land (\not\exists S''.S' \Rightarrow\_{Confict}^{N,\beta} S''),\\ \mathsf{-} \not\exists S'.S \Rightarrow\_{Confict}^{N,\beta} S',\\ \mathsf{-} \not\exists S'.S \Rightarrow\_{Skip}^{N,\beta} S',\\ \mathsf{-} \not\exists S'.S \Rightarrow\_{Resolve}^{N,\beta} S',\\ \mathsf{-} \not\exists S'.S \Rightarrow\_{Backtrack}^{N,\beta} S' \text{ and the backtracking is minimal,} \end{array}$$

*then either the conflicting clause* ⊥ *has been derived and the groundings gnd*(N) *of the initial clauses* N *are unsatisfiable, or there is no conflicting clause and the groundings gnd*Bβ(N) *of the initial clauses* N *are satisfiable by the trail, formally either*

$$-\ (\exists \gamma. \mathcal{C} = (\bot; \gamma)) \land (\nexists I. \ I \vdash\_{\mathcal{H}} \mathit{gnd}(N)), \ or \dots$$

*–* C = ∧ HI(Γ) |=H *gnd*Bβ(N)*.*

Note that no hypothesis restricts the usage of the Factorize rule because it is an optional step of conflict resolution that has no impact on satisfiability.

Theorem 7 holds for a family of strategies, in contrast to Theorem 5 from Bromberget et al., which was only shown for what is here called the minimally backtracking strategy. This family of strategies contains any strategy that preserves the required invariants and is restricted by the minimally backtracking strategy. From Lemma 5 we know that these two requirements are fulfilled by the SCL relation but also by the reasonable, regular, and minimally backtracking strategies. This leads to a more intuitive corollary based on runs.

Corollary 8 (correct\_termination\_strategies). *If an SCL, reasonable SCL, regular SCL, or minimally backtracking SCL run starting from the initial state* (; {}; ) *terminates in a state* S = (Γ;U; C)*, formally any of*

*–* (; {}; ) (⇒N,β *SCL*)∗ S ∧ (-S . S ⇒N,β *SCL* S )*, –* (; {}; ) (⇒N,β *Rea-SCL*)∗ S ∧ (-S . S ⇒N,β *Rea-SCL* S )*, –* (; {}; ) (⇒N,β *Reg-SCL*)∗ S ∧ (-S . S ⇒N,β *Reg-SCL* S )*, or –* (; {}; ) (⇒N,β *Min-Bac-SCL*)∗ S ∧ (-S . S ⇒N,β *Min-Bac-SCL* S )*,*

*then the conclusion of Theorem 7 holds.*

Note that each strategy is used with positive polarity in the "run" hypothesis and negative polarity in the "no-more-step" hypothesis. For this reason, it is impossible to provide a corollary with a single requirement to restrict or be restricted by any known strategy.

Traditional saturation-based calculi for first-order logic, e.g. Resolution and Superposition, can learn redundant clauses and thus their implementations require costly checks for non-redundancy. SCL(FOL) learns only non-redundant clauses. Thus, an implementation would not need to check for (forward) nonredundancy. We first repeat the definition of *standard redundancy* as found in [18].

Definition 9. *A clause* C *is redundant w.r.t. a set of clauses* N *and a strict order on clauses* ≺ *if* (∀C ∈ *gnd*(C). {D ∈ *gnd*(N)| D ≺ C } |=G C )*.*

We first prove non-redundancy w.r.t. a trail-induced dynamic order and then lift this result to non-redundancy w.r.t. a static order.

Definition 10. *A trail* Γ *induces a well-founded, strict partial order* ≺Γ *, total on all atoms in* Γ*'s literals. Assuming* Γ *has the form* L∗ n,...,L∗ 2,L∗ 1,L∗ 0 *for all* ∗ ∈ {†,(D, γD) *for some* D *and* γD}*, we have the following ordering.*

$$\vdash atom(L\_n) \prec^{\Gamma} \dots \prec^{\Gamma} atom(L\_2) \prec^{\Gamma} atom(L\_1) \prec^{\Gamma} atom(L\_0)$$

*In other words, "older" elements on the left are smaller than "newer" elements on the right. Formally:*

$$\forall t\_1 \prec^{\Gamma} t\_2 \longleftarrow \left( \exists i < |\Gamma|. \exists j < i. \, t\_1 = atom(\operatorname{lit}(\Gamma[i])) \land t\_2 = atom(\operatorname{lit}(\Gamma[j])) \right)$$

Compared to Bromberger et al., the trail-induced order is defined on atoms instead of literals and non-redundancy is proven for any lifting to literals.

Theorem 11 (dynamic\_non\_redundancy\_regular\_scl). *Following conflict resolution in a regular run, formally if*

$$\begin{array}{ll} - & (\epsilon; \{\}; \top) \left( \Rightarrow\_{Reg\text{-}SCL}^{N,\beta} \right)^{\*} (\varGamma; U; \top), \\ - & (\varGamma; U; \top) \Rightarrow\_{Conflict}^{N,\beta} \ S\_{1}, \\ - & S\_{1} \left( \Rightarrow\_{Skip, Factorize, Resolve}^{N,\beta} \right)^{+} S\_{n}, \; and \\ - & S\_{n} \Rightarrow\_{Backtrack}^{N,\beta} \ S\_{1+n}, \end{array}$$

*then neither is the learned clause* C = *conflict*(Sn) *generalized by any initial or learned clause, formally* (-D ∈ N ∪ U. ∃σ. Dσ = C)*, nor is it redundant w.r.t.* N ∪U *and the order we get by first lifting the trail-induced order* ≺Γ *from atoms to literals and then taking its multiset extension.*

Dynamic non-redundancy with respect to the trail-induced order does not by itself release an implementation from performing backward non-redundancy checks, but it is a strong guarantee on the quality of learned clauses. For backward redundancy checks an order needs to be used that encompasses all dynamic trail-induced orders. An order based on a strict multiset relation has this property. So for backward redundancy we can, e.g., delete subsumed clauses.

Corollary 12 (static\_non\_subsumption\_regular\_scl). *If a regular run starting from the initial state* (; {}; ) *learns a clause* C*, formally if*

$$\begin{array}{ll} - \ (\epsilon; \{\}; \top) \left( \Rightarrow\_{Reg\text{-}SCL}^{N,\beta} \right)^{\*} \ (\Gamma; U; (C; \gamma)) \ and \\ - \ (\Gamma; U; (C; \gamma)) \Rightarrow\_{Backtrack}^{N,\beta} \ S, \end{array}$$

*then* C *is not subsumed by any of the initial or learned clauses, formally* -D ∈ N ∪ U. ∃σ. Dσ ⊆ C*.*

All non-redundancy results can be generalized to an arbitrary strategy restricting the regular strategy. We only show one example here and refer the reader to the formalization for the others.

Corollary 13 (dynamic\_non\_redundancy\_strategy). *Following conflict resolution in the run of a strategy restricting regular SCL, formally if*

$$\begin{array}{ll} - & \left(\epsilon; \{\}\right); \top \right) (\Rightarrow\_{Strapy}^{N,\beta})^{\*} \left(\varGamma; U; \top\right), \\ - & \left(\Gamma; U; \top\right) \Rightarrow\_{Conflict}^{N,\beta} S\_{1}, \\ - & S\_{1} \left(\Rightarrow\_{Skip, Factorize, Resolve}\right)^{+} S\_{n}, \\ - & S\_{n} \Rightarrow\_{Backtrack}^{N,\beta} S\_{1+n}, \text{ and} \\ - & \forall S \, S'. \, S \Rightarrow\_{Strapy}^{N,\beta} S' \longrightarrow S \Rightarrow\_{Reg\*SCL}^{N,\beta} S', \end{array}$$

*then neither is the learned clause generalized by any initial or learned clause, formally* (-D ∈ N ∪ U. ∃σ. Dσ = C)*, nor is it redundant w.r.t.* N ∪ U *and the order we get by first lifting the trail-induced order* ≺Γ *from atoms to literals and then taking its multiset extension.*

During the development of this formalization, we discovered that the original Backtrack rule found in [6] allows to learn a duplicate of the last learned clause, which violates the stated non-redundancy of learned clauses. The original Backtrack rule ensures that the conflict closure is not false under the new trail, but the learned clause could still be in conflict w.r.t. another grounding. Following this conflict, the Backtrack rules would be immediately applicable and would learn the same clause again. This could only happen a finite number of times as backtracking reduces the length of the (finite) trail. As an example, consider the set of clauses N = {P(x), Q(y),¬Q(z)∨R(z),¬R(w)∨S(w),¬P(v)∨¬S(v)}, and a big enough β. The following SCL run was valid with the original Backtrack rule. Note that the notation for the trail was shortened to save space.

(; {}; ) (⇒N,β Decide) ∗ (P(a),Q(a),P(b),Q(b); {}; ) (⇒N,β Propagate) ∗ (P(a),Q(a),P(b),Q(b),R(b) (R(z);¬Q(z);z→b) ,S(b) (S(w);¬R(w);w→b) ; {}; ) ⇒N,β Conflict (P(a),Q(a),P(b),Q(b),R(b) (R(z);¬Q(z);z→b) ,S(b) (S(w);¬R(w);w→b) ; {}; (¬P (v)∨¬S(v); v →b)) ⇒N,β Resolve+Skip (P(a),Q(a),P(b),Q(b),R(b) (R(z);¬Q(z);z→b) ; {}; (¬P (v) ∨ ¬R(v); v →b)) ⇒N,β Resolve+Skip (P(a),Q(a),P(b),Q(b); {}; (¬P(v) ∨ ¬Q(v); v → b)) ⇒N,β Backtrack (P(a),Q(a),P(b); {¬P(v) ∨ ¬Q(v)}; ) ⇒N,β Conflict+Skip (P(a),Q(a); {¬P(v) ∨ ¬Q(v)}; (¬P(v) ∨ ¬Q(v); v →a)) ⇒N,β Backtrack (P(a); {¬P(v) ∨ ¬Q(v)}; )

This counterexample was only discovered when we failed to prove Theorem 11 in Isabelle. Note that this formalization is based on and was developed simultaneously to Bromberger et al., which originally inherited the Backtrack rule from [10]. The solution, which was promptly integrated into this formalization and Bromberger et al., is for the Backtrack rule to find a position without conflict w.r.t. the learned clause. Note that the original Backtrack rule reaches such a state after having learned the same clause finitely often, which has no effect on the set of learned clauses because sets ignore duplicates. Thus, the original Backtrack rule did not invalidate the other properties of the SCL calculus. This discovery is strong evidence of the usefulness of mechanized formalization for both published work and ongoing research: the Isabelle formalization lead to the discovery of a previously unknown bug and it guided the development of the refinement.

A calculus expressed as a state machine terminates if the transition relation starting from the initial state is well-founded following the arrow direction. We prove well-foundedness of regular SCL in three steps: (1) we first prove wellfoundedness of SCL without backtracking, denoted ⇒N,β SCL-no-Back ; (2) we then prove that a regular run can only learn finitely many clauses; and (3) from these two results we finally prove well-foundedness of regular SCL. Step 1 is novel to the formalization. Prior work in Bromberger et al. focuses exclusively on the Backtrack rule (step 2) in order to prove termination of regular SCL (step 3). Also novel to the formalization are decreasing measuring functions for steps 1 and 2.

Definition 14. *The measuring function* M3(N, β,S) *for SCL without backtracking maps a set of initial clauses* N*, a bounding atom* β*, and a state* S *to a 4-tuple. The tuple elements are (1) a boolean identifying whether the state is conflict-free, (2) a (finite) set overapproximating the literals that could be added to the trail, (3) a (finite) list overapproximating the numbers of resolution steps that could be performed at each position in the trail, and (4) the (finite) cardinality of the conflicting clause. Formally:*

$$\begin{aligned} \mathcal{M}\_1(\beta,\Gamma) &= \{L \, | \, atom(L) \preceq\_B \beta\} - \{list(K) \, | \, \mathcal{K} \in set(\Gamma)\} \\ \mathcal{M}\_2(\epsilon, C) &= \epsilon \\ \mathcal{M}\_2((\Gamma, K), C) &= \mathcal{M}\_2(\Gamma, C), 0 \\ \mathcal{M}\_2((\Gamma, (K\gamma)^{(K; D; \gamma)}), C) &= \operatorname{let}\, n = count(C, comp(K\gamma)) \text{ in } n \\ &= \mathcal{M}\_2(\Gamma, C \vee repeat(n, D\gamma)), n \\ \mathcal{M}\_3(N, \beta, (\Gamma; U; C; \top)) &= (True; \mathcal{M}\_1(\beta, \Gamma); \epsilon; 0) \\ \mathcal{M}\_3(N, \beta, (\Gamma; U; (C; \gamma))) &= (False; \{\}; \mathcal{M}\_2(\Gamma, C); |C|) \end{aligned}$$

With this, we can prove termination of SCL without backtracking (step 1).

Theorem 15 (termination\_scl\_without\_back). *SCL without backtracking is well-founded on all states reachable by an SCL-without-backtracking run starting from the initial state, formally on* {S |(; {}; ) (⇒N,β *SCL-no-Back*)∗ S}*.*

We now turn to proving termination of regular SCL with backtracking by first defining an appropriate measuring function.

Definition 16. *The measuring function* M4(β,S) *for the rule Backtrack maps a bounding atom* β *and a state* S *to a finite set of clauses without duplicates. It computes an over-approximation of the set of clauses that could still be learned modulo duplicates. Formally:*

$$\mathcal{M}\_4(\beta, S) := 2^{\{L \mid atom(L) \preceq\_B \beta\}} - \{set(C) \mid C \in \operatorname{gnd}(\operatorname{ learned}(S))\}$$

We then prove that it decreases every time we learn a new clause (step 2).

Lemma 17 (M*\_back\_after\_regular\_backtrack*). *Following conflict resolution in a regular run, formally if*

$$\begin{array}{ll} - & (\epsilon; \{\}; \top) \left( \Rightarrow\_{Reg\text{-}SCL}^{N,\beta} \right)^{\*} (\varGamma; U; \top), \\ - & (\varGamma; U; \top) \Rightarrow\_{Conf\text{-}Rict}^{N,\beta} \ S\_{1}, \\ - & S\_{1} \left( \Rightarrow\_{Skip, Factorize, Resolve}^{N,\beta} \right)^{+} S\_{n}, \; and \\ - & S\_{n} \Rightarrow\_{Backtrack}^{N,\beta} S\_{1+n}, \; then \end{array}$$

*1. the ground conflict is distinct from all groundings of initial and learned clauses modulo duplicates, formally* (∃C γ. *conflict*(Sn)=(C; γ) ∧ *set*(Cγ) ∈/ {*set*(D)| D ∈ *gnd*(N ∪ U)})*, and*

*2. the set of clauses that could potentially be learned strictly diminishes, formally* M4(β,S1+n) ⊂ M4(β,Sn)*.*

Lemma 17 is novel to the formalization. Together with Theorem 15 it allows us to prove termination of regular SCL with backtracking (step 3).

Theorem 18 (termination\_regular\_scl). *Regular SCL is well-founded on all states reachable by a regular-SCL run starting from the initial state, formally on* {S |(; {}; ) (⇒N,β *Reg-SCL*)∗ S}*.*

All termination results can be generalized to an arbitrary strategy restricting the regular strategy. We only show one example here and refer the reader to the formalization for the others.

Corollary 19 (termination\_strategy). *If a strategy restricts regular SCL, formally if* (∀S S . S ⇒N,β *Strategy* S −→ S ⇒N,β *Reg-SCL* S )*, then it is well-founded on all states reachable by a run using this strategy and starting from the initial state, formally on* {S |(; {}; ) (⇒N,β *Strategy*)∗ S}*.*

All theorems until now were first expressed and proven using invariants and then the versions expressed using runs were derived. However, Theorem 18 posed an interesting problem because its proof requires the backtracking step to have knowledge of the trail when a conflict last occurred. But this information is lost in the SCL state due to the Skip rule shrinking the trail. We did define an invariant that expresses the historical form of the trail and its properties derived from the regular strategy, but it is complex and the added value compared to working directly on a regular run is questionable. For simplicity, we chose not to present this invariant in this paper.

Together, soundness and termination allow us to prove refutational completeness of the regular SCL calculus w.r.t. a fixed bound.

Theorem 20 (completeness\_wrt\_bound). *If the groundings gnd*Bβ(N) *of the initial clauses* N *are unsatisfiable, then all regular SCL runs starting from the initial state terminate and derive the conflicting clause* ⊥*, formally*

Theorem 20 is only defined w.r.t. a bound, but fortunately we can prove that there must always exist an appropriate bound.

Lemma 21 (ex\_bound\_if\_unsat). *If the relation* ≺B *is a well-founded, strict order, total on ground atoms and the groundings gnd*(N) *of the initial clauses* N *are unsatisfiable, then there exists a bound* β *such that the groundings gnd*Bβ(N) *are unsatisfiable.*

Note that while Lemma 21 proves the existence of an appropriate bound, it provides no constructive way of finding one. What one can do is follow along Theorem 6 and iteratively increase a heuristically chosen bound until an appropriate one is found; if the set of initial clauses is unsatisfiable, this will terminate.

Isabelle Technicalities. Lemma 21's hypothesis that ≺B is a well-founded, total, strict order cannot be expressed as a theorem-local hypothesis. The reason is that the compactness theorem for clausal first-order logic requires terms to be an instance of the wellorder type class, which is not the case in the scl\_fol\_calculus locale, where the assumptions on the ≺B relation are kept minimal. Because Isabelle does not allow to instantiate a type class with a concrete type inside a locale or theorem, we define a new locale that extends scl\_fol\_calculus and adds a type class requirement on the first-order term constants. This enables the type-class system to automatically instantiate the wellorder type class for terms using the previously registered Knuth-Bendix order. We then instantiate the ≺B relation of scl\_fol\_calculus with the Knuth-Bendix order. This type class and locale gymnastic could be avoided if the formalization of the compactness theorem was refactored to offer a predicatebased version alongside the existing type-class-based version.

### 4 Conclusion

We generalized and formalized the SCL(FOL) calculus in Isabelle/HOL. The main results are formal proofs of soundness, non-redundancy of learned clauses, termination, and refutational completeness. Because the formalization was performed simultaneously to Bromberger et al., they could benefit from each other. A mechanized formalization must consider low-level details, but it is also the opportunity to identify the most import aspects of the theory and abstract over details needed in the context of an actual implementation. For example, we abstracted from the level of a state to define the Backtracking rule and replaced it with an abstract specification of the result. A level was used in all pen-anpaper presentations of the calculus in order to have a constructive way of going back to the maximal trail where the learned clause propagates. The abstraction supports investigation of several Backtrack rule versions and to base the soundness result on a version with a minimal requirement, i.e., the learned clause is no longer false with respect to the trail.

The formalization did uncover a small bug in the calculus, but also showed that its effect was very localized and naturally lead to a solution. Another benefit of the formalization is how much it supports refactoring and exploratory experimentation. When making a change to a definition or a conjecture, Isabelle immediately and exhaustively points to the parts that need to be adapted. Very often, proofs can automatically be adapted using proof automation tools such as Sledgehammer. This was invaluable to quickly try out ideas or change subtle parts of the calculus. One such example is in the Resolve rule, where the formalization first used substitution composition as found in the original calculus and latter replaced it by an abstract specification of merged grounding. This idea came from a private discussion sketching an eventual C implementation where it became clear that substitution composition would be a costly operation. We then introduced the abstract specification of merged grounding and fixed the formalization by following the mistakes reported by Isabelle.

Acknowledgments. We thank Sophie Tourret and Jasmin Blanchette for many fruitful discussions. We thank the anonymous reviewers for their constructive feedback on this paper.

### References

Schulz, S., Ternovska, E. (eds.) The 8th International Workshop on the Implementation of Logics, IWIL 2010, Yogyakarta, Indonesia, 9 October 2011. EPiC Series in Computing, vol. 2, pp. 1–11. EasyChair (2010). https://doi.org/10.29007/36dt

Open Access This chapter is licensed under the terms of the Creative Commons Attribution 4.0 International License (http://creativecommons.org/licenses/by/4.0/), which permits use, sharing, adaptation, distribution and reproduction in any medium or format, as long as you give appropriate credit to the original author(s) and the source, provide a link to the Creative Commons license and indicate if changes were made.

The images or other third party material in this chapter are included in the chapter's Creative Commons license, unless indicated otherwise in a credit line to the material. If material is not included in the chapter's Creative Commons license and your intended use is not permitted by statutory regulation or exceeds the permitted use, you will need to obtain permission directly from the copyright holder.

# **SCL(FOL) Can Simulate Non-Redundant Superposition Clause Learning**

Martin Bromberger1, Chaahat Jain1,2, and Christoph Weidenbach1(B)

1 Max Planck Institute for Informatics, Saarbr¨ucken, Germany

<EMAIL_ADDRESS>2 Graduate School of Computer Science, Saarbr¨ucken, Germany

**Abstract.** We show that SCL(FOL) can simulate the derivation of nonredundant clauses by superposition for first-order logic without equality. Superposition-based reasoning is performed with respect to a fixed reduction ordering. The completeness proof of superposition relies on the grounding of the clause set. It builds a ground partial model according to the fixed ordering, where minimal false ground instances of clauses then trigger non-redundant superposition inferences. We define a respective strategy for the SCL calculus such that clauses learned by SCL and superposition inferences coincide. From this perspective the SCL calculus can be viewed as a generalization of the superposition calculus.

**Keywords:** first-order reasoning · superposition · SCL · non-redundant clause learning

### **1 Introduction**

Superposition [1,2,18] is currently considered as the prime calculus for firstorder logic reasoning where all leading first-order theorem provers implement a variant thereof [14,16,20,22]. More recently, the family of SCL calculi (Clause Learning from Simple Models, or just Simple Clause Learning) [4,8,9,11,17] was introduced. There are first experimental results [3] available, and first steps towards an overall implementation [5,7].

The main differences between superposition and SCL for first-order logic without equality are: (i) superposition assumes a fixed ordering on literals whereas the ordering in SCL is dynamic and evolves out of the satisfiability of clauses, (ii) superposition performs single superposition left and factoring inferences whereas SCL typically performs several such inferences to derive a single learned clause, (iii) the superposition model operator is not effective on the non-ground clause level whereas the SCL model assumption is effective. For first-order logic without equality superposition reduces to ordered resolution combined with the powerful superposition redundancy criterion. Our simulation result cannot be one-to-one because an SCL learned clause is typically generated by several superposition inferences and superposition factoring inferences are performed by SCL only in the context of resolution inferences. The simulation result considers the

c The Author(s) 2023 ground case, where the superposition strategy used in the completeness proof only triggers non-redundant inferences [1]. We call this strategy SUP-MO, Definition 5. Overall first-order superposition completeness is then obtained by a lifting argument to the non-ground clause level. We actually show that a superposition refutation of some ground clause set can be simulated by an SCL refutation on the same clause set, such that they coincide on all superposition left (ordered resolution) inferences. For the superposition calculus we refer to [1] and for SCL to [9] where all main properties of both calculi have meanwhile been verified inside the Isabelle framework [10,19,21].

For example, consider a superposition refutation of the simple ground clause set

$$N\_{\rm{SUP}}^0 = \{ (C\_1) \; P(a) \lor P(a), \quad (C\_2) \; \neg P(a) \lor Q(b), \quad (C\_3) \; \neg Q(b) \}$$

with respect to a KBO [13], where all symbols have weight one, and precedence a ≺ b ≺ P ≺ Q. Superposition generates only non-redundant clauses. Then with respect to the usual superposition ordering extension to literals and clauses we get (C1) ≺KBO-SUP (C2) ≺KBO-SUP (C3) and the superposition model operator produces the Herbrand model N0 SUP,I = ∅. Now clause (C1) is the minimal false clause, triggering a factoring inference resulting in (C4) P(a) and clause set N1 SUP = N0 SUP ∪ {(C4) P(a)}. The clause P(a) cannot be derived by SCL because factoring is only preformed in the context of resolution inferences. Now (C4) is the smallest clause in N1 SUP and the superposition model operator produces N1 SUP,I = {P(a), Q(b)} with minimal false clause (C3). A superposition left inference between (C3) and (C2) generates (C5) ¬P(a) and N2 SUP = N1 SUP ∪ {(C5) ¬P(a)}. The generation of ¬P(a) can now be simulated by SCL by constructing the SCL trail [P(a)1Q(b){¬P (a)∨Q(b)}] out of N0 SUP = N0 SCL leading to the learned clause (C5) ¬P(a) and respective clause set N2 SCL = N0 SCL ∪ {(C5) ¬P(a)}. Note that P(a) could have also been propagated, see Sect. 2 rule Propagate, but this would eventually not lead to the learned clause (C5) ¬P(a) but ⊥. Finally, the superposition model operator produces N2 SUP,I = {P(a), Q(b)} with minimal false clause (C5) and infers ⊥. The SCL simulation generates the trail [P(a){P (a)}] and then learns ⊥ as well out of a conflict with (C5). Note that this SCL trail is based on a factoring of (C1) to P(a) that was the explicit first step of the superposition refutation. Recall that by using an exhaustive propagation strategy, SCL would start with the trail [P(a)P (a) Q(b){¬P (a)∨Q(b)}] and immediately derive ⊥. Exhaustive propagation is not a good strategy in general, because first-order logic clauses may enable infinitely many propagations. Even together with the typical SCL restriction to finitely many ground instances, there are exponentially many propagations possible, in general. Therefore, the *regular* strategy defined in [9] does not require exhaustive propagation, but guarantees non-redundant clause learning. The SCL-SUP strategy, Definition 8, and Definition 10, simulating superposition SUP-MO runs is also a regular strategy, Lemma 17.

The paper is now organized as follows. After repetition of the needed concepts of SCL and superposition, Sect. 2, the simulation result is contained in Sect. 3. We show that any superposition refutation of a ground clause set producing only non-redundant inferences through the SUP-MO strategy, can be simulated via the SCL-SUP strategy. Based on the 14 simulation invariants of Definition 7, we show the invariants by an inductive argument on the length of the superposition refutation, starting from the initial state, Lemma 13, for intermediate superposition inference steps Lemma 14, until the final refutation Lemma 15, and Lemma 16. For the simulation we do not consider selection in superposition inferences in favor of a less complicated presentation. The paper ends with a discussion of the obtained results. A full version of the paper including all proofs is available on arxiv [6].

### **2 Preliminaries**

We assume a first-order language without equality where N denotes a clause set; C, D denote clauses; L, K, H denote literals; A, B denote atoms; P, Q, R denote predicates; t, s terms; f, g, h function symbols; a, b, c constants; and x, y, z variables. Atoms, literals, clauses and clause sets are considered as usual, where in particular clauses are identified both with their disjunction and multiset of literals [9]. The complement of a literal is denoted by the function comp. The function atom(L) denotes the atomic part of a literal. Semantic entailment |= is defined as usual where variables in clauses are assumed to be universally quantified. Substitutions σ, τ are total mappings from variables to terms, where dom(σ) := {x | xσ = x} is finite and codom(σ) := {t | xσ = t, x ∈ dom(σ)}. Their application is extended to literals, clauses, and sets of such objects in the usual way. A term, atom, clause, or a set of these objects is *ground* if it does not contain any variable. A substitution σ is *ground* if codom(σ) is ground. A substitution σ is *grounding* for a term t, literal L, clause C if tσ, Lσ, Cσ is ground, respectively. The function mgu denotes the *most general unifier* of two terms, atoms, literals. We assume that any mgu of two terms or literals does not introduce any fresh variables and is idempotent. A *closure* is denoted as C · σ and is a pair of a clause C and a substitution σ that is grounding for C. The function ground returns the set of all ground instances of a literal, clause, or clause set with respect to the signature of the respective clause set.

A *(partial) model* M for a clause set N is a satisfiable set of ground literals. A ground clause C is true in M, denoted M |= C, if C ∩ M = ∅, and false otherwise. A ground clause set N is true in M, denoted M |= N if all clauses from N are true in M. A *(partial) Herbrand model* I for a clause set N is a set of ground atoms. A ground clause C is true in I, denoted I |=H C, if there is an atom A ∈ C such that A ∈ I, or there is a negative literal ¬A ∈ C such that A ∈ I, and false otherwise. A ground clause set N entails a ground clause C, denoted N |= C, if M |= C implies M |= {C} for all models M.

We identify sets and sequences whenever appropriate. However, the trail of an SCL run is always a sequence of ground literals.

Let ≺ denote a well-founded, total, strict ordering on ground literals. This ordering is then lifted to clauses and clause sets by its respective multiset extension. We overload ≺ for literals, clauses, clause sets if the meaning is clear from the context. The ordering is lifted to the non-ground case via instantiation: we define C ≺ D if for all grounding substitutions σ it holds Cσ ≺ Dσ. We define as the reflexive closure of ≺ and N C := {D | D ∈ N and D C}.

**Definition 1 (Clause Redundancy).** *A ground clause* C *is* redundant *with respect to a ground clause set* N *and an order* ≺ *if* N C |= C*. A clause* C *is* redundant *with respect to a clause set* N *and an order* ≺ *if for all* C ∈ ground(C) *it holds that* C *is redundant with respect to* ground(N)*.*

Let ≺B denote a well-founded, total, strict ordering on ground atoms such that for any ground atom A there are only finitely many ground atoms B with B ≺B A. For example, an instance of such an ordering could be KBO without zero-weight symbols. (Note that LPO does not satisfy the last condition of a ≺B ordering although it is a well-founded, total, strict ordering.) The ordering ≺B is lifted to literals by comparing the respective atoms and if the atoms of two literals are the same, then the negative version of the literal is larger than the positive version. It is lifted to clauses by a multiset extension.

*The SCL(FOL) Calculus:* The inference rules of SCL(FOL) [9] are represented by an abstract rewrite system. They operate on a problem state, a six-tuple (Γ; N;U; β; k; D) where Γ is a sequence of annotated ground literals, the *trail*; N and U are the sets of *initial* and *learned* clauses; β is a ground literal limiting the size of the trail; k counts the number of decisions; and D is either , ⊥ or a clause closure C · σ such that Cσ is ground and false in Γ. Literals in Γ are either annotated with a number, also called a level; i.e., they have the form Lk meaning that L is the k-th guessed decision literal, or they are annotated with a closure that propagated the literal to become true. A ground literal L is of *level* i with respect to a problem state (Γ; N;U; β; k; D) if L or comp(L) occurs in Γ and the first decision literal left from L (comp(L)) in Γ, including L, is annotated with i. If there is no such decision literal then its level is zero. A ground clause D is of *level* i with respect to a problem state (Γ; N;U; β; k; D) if i is the maximal level of a literal in D. The level of the empty clause ⊥ is 0. Recall D is a non-empty closure or or ⊥. Similarly, a trail Γ is of level i if the maximal literal in Γ is of level i.

A literal/atom L/A is *undefined* in Γ if neither L/A nor comp(L)/comp(A) occur in Γ. The start state of SCL is (; N; ∅; β; 0; ) for some initial clause set N and bound β. The below rules are exactly the rules from [9] and serve as a reference for our simulation proof in Sect. 3.

$$\begin{array}{ccccc}\textbf{Propagate} & \left(\varGamma;N;U;\beta;k;\top\right) & \Rightarrow\_{\text{SCL}} & \left(\varGamma,L\sigma^{(C\_0\vee L)\delta\cdot\sigma};N;U;\beta;k;\top\right) \\ \hfil\mathrel{1} & 1& \alpha\text{ }\dots\text{ }\tau\text{ }\ldots\text{ }\tau\text{ }\omega\text{ }\ \gamma\text{ }\ \alpha\text{ }\ \gamma\text{ }\ \sigma\text{ }\ \tau\text{ }\ \tau\text{ }\ \ldots\text{ }\tau\text{ }\ \end{array}$$

provided C ∨ L ∈ (N ∪ U), C = C0 ∨ C1, C1σ = Lσ ∨ ··· ∨ Lσ, C0σ does not contain Lσ, δ is the mgu of the literals in C1 and L, (C ∨ L)σ is ground, (C ∨ L)σ ≺β {β}, C0σ is false under Γ, and Lσ is undefined in Γ.

**Decide** (Γ; N;U; β; k; ) ⇒SCL (Γ, Lσk+1; N;U; β; k + 1; )

provided atom(L) occurs C for a C ∈ (N ∪ U), Lσ is a ground literal undefined in Γ, and Lσ ≺β β.

**Conflict** (Γ; N;U; β; k; ) ⇒SCL (Γ; N;U; β; k; D · σ)

provided D ∈ (N ∪ U), Dσ false in Γ for a grounding substitution σ.

**Skip** (Γ, L; N;U; β; k; D · σ) ⇒SCL (Γ; N;U; β; k − i; D · σ)

provided comp(L) does not occur in Dσ, if L is a decision literal then i = 1, otherwise i = 0.

**Factorize** (Γ; N;U; β; k; (D ∨ L ∨ L ) · σ) ⇒SCL (Γ; N;U; β; k; (D ∨ L)η · σ) provided Lσ = L σ, η = mgu(L, L ). **Resolve** (Γ, Lδ(C∨L)·δ; N;U; β; k; (D ∨ L ) · σ) ⇒SCL (Γ, Lδ(C∨L)·δ; N;U; β; k; (D ∨ C)η · σδ) provided Lδ = comp(L σ), η = mgu(L, comp(L )). **Backtrack** (Γ0, K, Γ1, comp(Lσ)k; N;U; β; k; (D ∨ L) · σ) ⇒SCL (Γ0; N;U ∪ {D ∨ L}; β; j; )

provided Dσ is of level i < k, and Γ0, K is the minimal trail subsequence such that there is a grounding substitution τ with (D ∨ L)τ is false in Γ0, K but not in Γ0, and Γ0 is of level j.

A sequence of rule applications of a particular calculus is called a *run* of the calculus. A *strategy* for a calculus restricts the set of runs we actually allow by imposing further conditions on the allowed rule applications.

**Definition 2 (SCL Runs).** *A sequence of SCL rule applications is called a* reasonable run *if the rule Decide does not enable an immediate application of rule Conflict. A sequence of SCL rule applications is called a* regular run *if it is a reasonable run and the rule Conflict has precedence over all other rules.*

All regular SCL runs are sound, only derive non-redundant clauses, always terminate, and SCL with a regular strategy is refutationally complete (for firstorder logic without equality) [9].

*The Superposition Calculus:* Superposition [1,2,18] is a calculus for first-order logic reasoning that also infers/learns new clauses like SCL. In contrast to SCL, it does these inferences based on a static ordering ≺ and, at the level of inference rules, independent of a partial model. A permissible ordering ≺ for the superposition calculus is always a well-founded, total, strict ordering on ground literals. This ordering is then lifted to clauses and clause sets by its respective multiset extension. A problem state in the superposition calculus is just a set N of clauses. The start state the initial clause set. Due to the restriction to firstorder logic without equality, the most basic version of the superposition calculus consists just of the following two rules (without selection):

**Superposition Left** (N {C1∨P(t1,...,tn), C2∨¬P(s1,...,sn)}) ⇒SUP (N ∪ {C1 ∨ P(t1,...,tn), C2 ∨ ¬P(s1,...,sn)}∪{(C1 ∨ C2)σ})

where (i) P(t1,...,tn)σ is strictly maximal in (C1 ∨ P(t1,...,tn))σ (ii) ¬P(s1,...,sn)σ is maximal, (iii) σ is the mgu of P(t1,...,tn) and P(s1,...,sn).

**Factoring** (N {C ∨ P(t1,...,tn) ∨ P(s1,...,sn)}) ⇒SUP (N ∪ {C ∨ P(t1,...,tn) ∨ P(s1,...,sn)}∪{(C ∨ P(t1,...,tn))σ}) where (i) P(t1,...,tn)σ is maximal in (C ∨ P(t1,...,tn) ∨ P(s1,...,sn))σ (ii) σ is the mgu of P(t1,...,tn) and P(s1,...,sn).

Let sfac(C) represent a clause obtained by exhaustively applying superposition Factoring on C. Recall, that superposition Factoring only applies to maximal positive literals. Let sfac(N) represent the clause set N after every clause has been exhaustively factorized by Superposition Factorization.

Although the superposition calculus itself is independent of a partial model and may learn non-redundant clauses, the completeness proof of superposition in [1] is based on a strategy that builds ground partial models according to the fixed ordering ≺, where minimal false ground instances of clauses then trigger non-redundant superposition inferences. Note that the completeness proof relies on a grounding of the clause set that may lead to infinitely many clauses. However, the strategy from the completeness proof can also be seen as a superposition strategy for an initial clause set, where all clauses are already ground. On ground, finite clause sets, superposition restricted to the strategy only infers non-redundant clauses, always terminates, and is complete. The partial model needed in each step of the strategy is constructed according to the following model operator:

**Definition 3 (Superposition Model Operator).** *Let* N *be a set of ground clauses. Then* NI *is the Herbrand model according to the superposition model operator for clause set* N *and it is constructed recursively over the partial Herbrand models* NC *for all* C ∈ N*:*

$$\begin{array}{lcl} N\_C = \bigcup\_{D \preccurlyeq C} \delta\_D & N\_I = \bigcup\_{C \in N} \delta\_C\\ \delta\_D = \begin{cases} \{B\} & if \ D = D' \lor B, \text{ \$B \textquotedblleft} t \text{ \$T\$}, \text{ \$B \textquotedblleft} t \text{ \$T\$}, \text{ \$S \textquotedblright} \\\ \emptyset & otherwise \end{cases} \end{array}$$

*We say that a clause* C *is* productive *(wrt. the model construction of a clause set* N*) if* δC = ∅*. We say that a clause* C produces *an atom* B *(wrt. the model construction of a clause set* N*) if* δC = {B}*.*

After constructing the model NI for a clause set N, the strategy selects the smallest clause in N that is false in NI . The strategy then selects a fitting inference rule based on the reason why the clause is false in NI . The newly inferred clause either changes the model in the next step or changes the smallest clause that is false. This is the strategy used in the superposition completeness proof [1].

**Definition 4 (Minimal False Clause).** *The minimal false clause* C ∈ N *is the smallest clause in* N *according to* ≺ *such that* NC ∪ δC |=H C*.*

#### **Definition 5 (Superposition Model-Operator Strategy: SUP-MO).** *The* superposition model-operator strategy *is defined over the minimal false clause with regards to the current clause set* N*. The strategy can encounter the following cases:*

The first two cases of the SUP-MO strategy also describe its final states according to [1]. In all other states there is always exactly one rule applicable according to the SUP-MO strategy, which also means that SUP-MO is never stuck.

**Lemma 6 (SUP-MO Applicability).** *Let* N *be a set of ground clauses. If* N *has a minimal false clause* C = ⊥*, then there exists exactly one rule applicable to* N *according to the SUP-MO strategy.*

### **3 SCL Simulates Superposition**

In general, it is not possible to simulate all inferences of the superposition calculus with SCL because SCL only learns/infers non-redundant clauses, whereas syntactic superposition inferences have no such guarantees. Moreover, the inferences by SCL are all based on conflicts according to a partial model driven by the satisfiability of clause instances, whereas the inferences by superposition are based on a static ordering ≺. We can mitigate these differences by restricting superposition with the SUP-MO strategy because SUP-MO has non-redundancy guarantees and it infers new clauses based on minimal false clauses with respect to a ground partial model.

Let N0 be a set of ground clauses, totally ordered by a superposition reduction ordering ≺. Let Ni (for i > 0) be the result of i steps of the superposition calculus applied to N0 according to the SUP-MO strategy, i.e., N0 ⇒SUP-MO N1 ⇒SUP-MO ... ⇒SUP-MO Ni . Again, all Ni are sets of ground clauses, totally ordered by a superposition reduction ordering ≺. The SCL strategy SCL-SUP that simulates superposition restricted to SUP-MO runs is defined inductively on the clause ordering ≺. To guide and to prove the correctness of our simulation, we assign to each SCL state and every clause some additional information. For this purpose, every SCL state is annotated with a triple (i, C, γ), where i is an integer that states that the SCL state simulates the superposition state Ni , C is the last clause that was used as a decision aid by the strategy, γ is a function such that γ(C) = sfac(C) if sfac(C) ∈ Ni and γ(C) = C otherwise, the SCL state also simulates the model construction for Ni upto Ni C-∪δC- , where C = γ(C). The annotated states are written (Γ; N0;U; β; k; E)(i,C,γ). The overall start state is then (; N0; ∅; β; 0; )(0,⊥,γ), where we assume β large enough so A ≺β β for all A ∈ atom(N0), ⊥ ∈ N0, and γ(C) = sfac(C) if sfac(C) ∈ N0 and γ(C) = C otherwise. We will later see that the annotated integer is not relevant for the actual choice of SCL rules by the SCL-SUP strategy but only to prove that the strategy actually simulates superposition. Moreover, we define a new ordering ≺γ based on our superposition ordering ≺ and function γ such that C ≺γ D if γ(C) ≺ γ(D).

**Definition 7 (State Simulation).** *Let* (Γ; N0;U; β; k; E)(i,D,γ) *be an SCL state for the input clauses* N0*. Let* L *be the maximal literal in* D *if* D = ⊥ *and the minimal literal according to* ≺ *otherwise. Let* N0 ⇒*SUP-MO* N1 ⇒*SUP-MO* ... ⇒*SUP-MO* Ni *be the superposition run following the SUP-MO strategy starting from the input clause set* N0*. Let* D = γ(D)*. Then we say that the SCL state* (Γ; N0;U; β; k; E)(i,D,γ) simulates Ni *and the model construction upto* Ni D- ∪ δD*if*

	- **(ix)** *for every clause* C ∈ Ni *with* C γ(D) *that produces an atom* B*, i.e.,* δC = {B}*, there exists* C ∈ N0 ∪ U *such that* C = γ(C ) *and* C γ D*.*
	- **(x)** Γ *contains only decisions if* E =
	- **(xi)** E ∈ {, ⊥} *iff* Γ = Γ Bsfac(D) *,* Γ *contains only decisions, there exists* E ∈ Ni *where* γ(E) = E = E *is the minimal false clause in* Ni *, and*

The above invariants can be summarized as follows: (i) All ground atoms encountered are known from the start and the trail bound β is large enough so SCL can Decide/Propagate them. (ii)–(iv) Every initial clause C or inferred clause by SUP-MO must coincide with an initial clause C or learned clause by SCL; this means on the one hand that for every clause C learned by SCL-SUP, SUP-MO infers a clause C that is identical up to factoring; on the other hand it means that for every clause C inferred by SUP-MO, SCL-SUP learns a clause C that entails C (i.e. C |= C) and is at most as large as C wrt. γ. (v)–(ix) The partial model constructed by SCL-SUP and SUP-MO coincide and any atom B in NC ∪ δC produced by clause D has a clause D on the SCL side that could propagate B and vice versa. (x)–(xiii) Ensure that any Conflict in SCL-SUP corresponds to a minimal false clause and that the trail is always constructed in such a way that the Resolve applications per Conflict call are limited to the maximal literal in the conflict; this property is needed or the next clause that would be learned by SCL no longer coincides with the clauses learned by SUP-MO. (xiv) Describes the final state in case the input clause set is unsatisfiable.

Now that we have defined how an SCL state must look like in order to simulate a superposition state, we define SCL-SUP, the SCL strategy that eventually simulates a SUP-MO run. First, note that not all states visited by SCL-SUP satisfy the invariants of Definition 7. However, the invariants hold again after each so-called *atomic sequence* of SCL-SUP steps. Second, one atomic sequence of SCL-SUP steps may skip over several successive superposition states. The reason is that SCL can and must skip all steps of SUP-MO that occur because the maximal literal in a clause is not strictly maximal, i.e., superposition Factoring steps. SCL performs factoring implicitly in its Propagation rule so SCL never has to explicitly simulate case (4) of Definition 5. Third, definition of the SCL-SUP strategy is split in two parts and each part describes some atomic sequences of SCL-SUP steps.

**Definition 8 (SCL Superposition Strategy: SCL-SUP Part 1).** *Let* S0 = (Γ; N0;U; β; k; )(i,C,γ) *be an SCL state with additional annotations for the strategy. Let* D *be the next largest clause from* C *in the ordering* ≺γ *with respect to the ground clause set* N0 ∪ U*. Let* L *be the maximal literal of* D*. Let* [¬A1,¬A2,... ¬An] *be all negative literals such that for all* i *we have* Ai ≺ L*, all* Ai *undefined in* Γ*,* Ai *occurs in* N0 ∪ U*, and* Ai ≺ Ai+1*. Let* D = γ(D) *be in* Ni *such that* sfac(D) = sfac(D )*. Let* j0 + 1 *be the number of occurrences of* L *in* D *and* j = i + j0*. Then the* SCL Superposition Strategy *(SCL-SUP) performs the following steps to* S0 *(possibly without any actual SCL rule applications, just changing the state annotation):*

*A (potentially empty) sequence of SCL rule applications according to SCL-SUP is called an* atomic sequence *of SCL-SUP steps if it starts from a state* S0 *and ends in a state* S2 *outlined in the cases (2a-c).*