Petar Vukmirović
email: p.vukmirovic@vu.nl

Jasmin Blanchette
email: blanchette@vu.nl

Marijn J H Heule
email: marijn@cmu.edu

SAT-Inspired Eliminations for Superposition

Keywords: CCS Concepts:, Theory of computation → Automated reasoning, Logic and verification, Constraint and logic programming Theorem proving, first-order logic, superposition calculus, SAT solving

Optimized SAT solvers not only preprocess the clause set, they also transform it during solving as inprocessing. Some preprocessing techniques have been generalized to first-order logic with equality. In this article, we port inprocessing techniques to work with superposition, a leading first-order proof calculus, and we strengthen known preprocessing techniques. Specifically, we look into elimination of hidden literals, variables (predicates), and blocked clauses. Our evaluation using the Zipperposition prover confirms that the new techniques usefully supplement the existing superposition machinery.

INTRODUCTION

Automated reasoning tools have become much more powerful in the last few decades thanks to procedures such as conflict-driven clause learning (CDCL) [START_REF] Marques-Silva | Conflict-Driven Clause Learning SAT Solvers[END_REF] for propositional logic and superposition [START_REF] Bachmair | Rewrite-Based Equational Theorem Proving with Selection and Simplification[END_REF] for first-order logic with equality. However, the effectiveness of these procedures crucially depends on how the input problem is represented as a clause set. The clause set can be optimized beforehand (preprocessing) or during the execution of the procedure (inprocessing). In this article, we lift several preprocessing and inprocessing techniques from propositional logic to clausal first-order logic and demonstrate their usefulness in a superposition prover.

For many years, SAT solvers have used inexpensive clause simplification techniques such as hidden literal and hidden tautology elimination [START_REF] Marijn | Clause Elimination Procedures for CNF Formulas[END_REF][START_REF] Marijn | Efficient CNF Simplification Based on Binary Implication Graphs[END_REF] and failed literal detection [START_REF] William | Improvements to Propositional Satisfiability Search Algorithms[END_REF]Sect. 1.6]. We generalize these techniques to first-order logic with equality (Sect. 3). Since the generalization involves reasoning about infinite sets of literals, we propose restrictions to make them usable.

Variable elimination, based on Davis-Putnam resolution [START_REF] Davis | A Computing Procedure for Quantification Theory[END_REF], has been studied in the context of both propositional logic [START_REF] Chatalic | ZRES: The Old Davis-Putnam Procedure Meets ZBDD[END_REF][START_REF] Subbarayan | NiVER: Non-increasing Variable Elimination Resolution for Preprocessing SAT Instances[END_REF] and quantified Boolean formulas (QBFs) [START_REF] Biere | Resolve and Expand[END_REF]. The basic idea is to resolve all clauses with negative occurrences of a propositional variable (i.e., a nullary predicate symbol) against clauses with positive occurrences and delete the parent clauses. Eén and Biere [START_REF] Eén | Effective Preprocessing in SAT Through Variable and Clause Elimination[END_REF] refined the technique to identify a subset of clauses that effectively define a variable and use it to further optimize the clause set. This latter technique, variable elimination by substitution, has been an important preprocessor component in many SAT solvers since its introduction in 2004.

Specializing second-order quantifier elimination [START_REF] Gabbay | Quantifier Elimination in Second-Order Predicate Logic[END_REF][START_REF] Jürgen | SCAN-Elimination of Predicate Quantifiers[END_REF], Khasidashvili and Korovin [START_REF] Khasidashvili | Predicate Elimination for Preprocessing in First-Order Theorem Proving[END_REF] adapted variable elimination to preprocess first-order problems, yielding a technique we call singular predicate elimination. We extend their work along two axes (Sect. 4): We generalize Eén and Biere's refinement to first-order logic, resulting in defined predicate elimination, and explain how both types of predicate elimination can be used during the proof search as inprocessing.

The last technique we study is blocked clause elimination (Sect. 5). It is used in both SAT [START_REF] Järvisalo | Blocked Clause Elimination[END_REF] and QBF solvers [START_REF] Biere | Blocked Clause Elimination for QBF[END_REF]. Its generalization to first-order logic has produced good results when used as a preprocessor, especially on satisfiable problems [START_REF] Kiesl | Blocked Clauses in First-Order Logic[END_REF]. We explore more ways to use blocked clause elimination on satisfiable problems, including using it to establish equisatisfiability with an empty clause set or as an inprocessing rule. Unfortunately, we find that its use as inprocessing can compromise the refutational completeness of superposition.

All techniques are implemented in the Zipperposition prover (Sect. 6), allowing us to ascertain their usefulness (Sect. 7). The best configuration solves 160 additional problems on benchmarks consisting of all 13 495 first-order TPTP theorems [START_REF] Sutcliffe | The TPTP Problem Library and Associated Infrastructure-From CNF to TH0, TPTP v6.4.0[END_REF]. The raw experimental data are publicly available. 1This article expands on our FMCAD 2021 paper [START_REF] Vukmirović | SAT-inspired eliminations for superposition[END_REF]. It includes more examples, lemmas, and proofs as well as a discussion section. It also corrects a mistake in the handling of variables in Definition 5.2.

PRELIMINARIES

Our work relies on a clausal version of first-order logic. Some of our techniques and results apply only to the superposition calculus. This section provides a brief introduction to these concepts.

Clausal First-Order Logic

Our setting is many-sorted, or many-typed, first-order logic [START_REF] Gallier | Logic for Computer Science: Foundations of Automatic Theorem Proving[END_REF] with interpreted equality and a distinguished type (or sort) 𝑜. Each variable 𝑥 is assigned a non-Boolean type, and each symbol f is assigned a tuple (𝜏 1 , . . . , 𝜏 𝑛 , 𝜏) where 𝑛 ≥ 0, 𝜏 𝑖 are non-Boolean types, and 𝜏 is the result type. We distinguish between predicate symbols, with 𝑜 as the result type, and function symbols. Nullary function symbols are called constants. Terms are either variables 𝑥 or applications f(𝑡 1 , . . . , 𝑡 𝑛 ), of type 𝜏 where f is assigned (𝜏 1 , . . . , 𝜏 𝑛 , 𝜏), and each 𝑡 𝑖 is a term of type 𝜏 𝑖 . The parentheses are omitted if 𝑛 = 0. A term is ground if it contains no variables. We assume standard definitions and notations for positions, subterms, and contexts [START_REF] Baader | Term Rewriting and All That[END_REF]. We abbreviate a vector (𝑎 1 , . . . , 𝑎 𝑛 ) to ì 𝑎 𝑛 or ì 𝑎, and write f 𝑖 (𝑠) for the 𝑖-fold application of a unary symbol f (e.g., f 3 (𝑥) = f (f(f (𝑥)))).

An atom is an equation 𝑠 ≈ 𝑡 corresponding to an unordered pair {𝑠, 𝑡 }. A literal is an equation 𝑠 ≈𝑡 or a disequation 𝑠 𝑡. For every predicate symbol p, the notation p(ì 𝑠) abbreviates p(ì 𝑠) ≈ ⊤, and ¬p(ì 𝑠) abbreviates p(ì 𝑠) ⊤, where ⊤ is a distinguished constant of type 𝑜. We distinguish between predicate literals (¬) p(ì 𝑠) and functional literals 𝑠 ≈ 𝑡, where 𝑠 and 𝑡 are not of type 𝑜. Given a literal 𝐿, we overload notation and write ¬𝐿 to denote its complement. A clause 𝐶 is a finite multiset of literals, written as 𝐿 1 ∨ • • • ∨ 𝐿 𝑛 and interpreted disjunctively. Clauses are often defined as sets of literals, but superposition needs multisets; with multisets, an instance 𝐶𝜎 always has the same number of literals as 𝐶, a most convenient property. Given a clause set 𝑁 , 𝑁 ↓ 2 denotes the subset of its binary clauses:

𝑁 ↓ 2 = {𝐿 1 ∨ 𝐿 2 | 𝐿 1 ∨ 𝐿 2 ∈ 𝑁 }.
A substitution 𝜎 is a well-typed mapping from variables to terms such that the set {𝑥 | 𝜎 (𝑥) ≠ 𝑥 } is finite. Substitutions are written as {𝑥 1 ↦ → 𝑡 1 , . . . , 𝑥 𝑛 ↦ → 𝑡 𝑛 } or { ì 𝑥 ↦ → ì 𝑡 }. A substitution is a variable renaming if it is a bijection from a set of variables to a set of variables.

We assume the natural extensions of domain, valuation, interpretation, and model (as defined by Fitting [START_REF] Fitting | First-Order Logic and Automated Theorem Proving[END_REF]) from unsorted to many-sorted logic. The models we consider are normal-i.e., they interpret ≈ as an equality relation. Usual notions of (un)satisfiability and (in)validity are assumed. We write J |= 𝜉 𝑁 to denote that a model J satisfies a clause set 𝑁 , for a variable assignment 𝜉.

If J is a model of 𝑁 (i.e., it satisfies it under every variable assignment), we simply write J |= 𝑁 . Abusing notation, we write 𝑀 |= 𝑁 to denote that 𝑀 entails 𝑁 , i.e., that every model of 𝑀 is a model of 𝑁 .

A canonical model J is a normal model such that for every element 𝑑 in one of J's domains there exists a ground term 𝑡 such that J interprets 𝑡 as 𝑑. Canonical models generalize Herbrand models to first-order logic with equality: If a clause set is satisfiable, then it is satisfiable in a canonical model.

Superposition Provers

Superposition [START_REF] Bachmair | Rewrite-Based Equational Theorem Proving with Selection and Simplification[END_REF] is a calculus for clausal first-order logic that extends ordered resolution [START_REF] Bachmair | Resolution Theorem Proving[END_REF] with equality reasoning. It is refutationally complete: Given a finite, unsatisfiable clause set, it will eventually derive the empty clause. It is parameterized by a selection function that influences which of a clause's literals are eligible as the target of inferences. Moreover, it is compatible with the standard redundancy criterion, which can be used to delete a clause 𝐶 while preserving completeness of the calculus.

The redundancy criterion relies on an order ≻ that compares terms, literals, clauses, or finite clause sets. The order is used to determine whether clauses can be deleted. If 𝑁 is ground, 𝐶 can be deleted if it is entailed by ≺-smaller clauses in 𝑁 . This definition is lifted to nonground sets 𝑁 . The criterion can be used to delete a clause that is subsumed by another clause (e.g., p(a) ∨ q by p(𝑥)) or to simplify a clause 𝐶 into 𝐶 ′ , which amounts to adding 𝐶 ′ and then deleting 𝐶 as redundant with respect to 𝑁 ∪ {𝐶 ′ }. Subsumption and simplification are the main inprocessing mechanisms available to superposition provers. Some provers also implement clause splitting [START_REF] Fietzke | Labelled splitting[END_REF][START_REF] Riazanov | Splitting Without Backtracking[END_REF][START_REF] Voronkov | AVATAR: The Architecture for First-Order Theorem Provers[END_REF].

Superposition provers saturate the input problem with respect to the calculus's inference rules using the given clause procedure [START_REF] Avenhaus | DISCOUNT: A SYstem for Distributed Equational Deduction[END_REF][START_REF] Mccune | Otter-The CADE-13 Competition Incarnations[END_REF]. It partitions the proof state into a passive set P and an active set A. All clauses start in P. At each iteration of the procedure's main loop, the prover chooses a clause 𝐶 from P, simplifies it, and moves it to A. Then all inferences between 𝐶 and active clauses are performed. The resulting clauses are again simplified and put in P. The provers differ in which clauses are used for simplification: Otter-loop [START_REF] Mccune | Otter-The CADE-13 Competition Incarnations[END_REF] provers use both active and passive clauses whereas DISCOUNT-loop [START_REF] Avenhaus | DISCOUNT: A SYstem for Distributed Equational Deduction[END_REF] provers use only active clauses.

HIDDEN-LITERAL-BASED ELIMINATION

In propositional logic, binary clauses from a clause set 𝑁 can be used to efficiently discover literals 𝐿, 𝐿 ′ for which the implication 𝐿 ′ -■ → 𝐿 is entailed by 𝑁 's binary clauses-i.e., literals L, L' such that 𝑁 ↓ 2 |= 𝐿 ′ -■ → 𝐿. Heule et al. [START_REF] Marijn | Efficient CNF Simplification Based on Binary Implication Graphs[END_REF] introduced the concept of hidden literals to capture such implications.

Definition 3.1. Given a propositional literal 𝐿 and a propositional clause set 𝑁 , the set of propositional hidden literals for 𝐿 and 𝑁 is HL prop (𝐿, 𝑁

) = {𝐿 ′ | 𝐿 ′ ↩→ * prop 𝐿} \ {𝐿}, where ↩→ prop is defined such that ¬𝐿 1 ↩→ prop 𝐿 2 whenever 𝐿 1 ∨ 𝐿 2 ∈ 𝑁 . Moreover, HL prop (𝐿 1 ∨ • • • ∨ 𝐿 𝑛 , 𝑁 ) = 𝑛 𝑖=1 HL prop (𝐿 𝑖 , 𝑁 ).
Heule et al. used a fixpoint computation, but our definition based on the reflexive transitive closure is equivalent. Intuitively, a hidden literal can be added to or removed from a clause without affecting its semantics in models of 𝑁 . By eliminating hidden literals from 𝐶, we simplify it. By adding hidden literals to 𝐶, we might get a tautology 𝐶 ′ (i.e., a valid clause: |= 𝐶 ′ ), meaning that 𝑁 ↓ 2 |= 𝐶, thereby making 𝐶 a candidate for deletion. Note that HL prop (𝐿, 𝑁 ) is finite for a finite 𝑁 . Definition 3.2. Given 𝐿 ′ ∨ 𝐿 ∨ 𝐶 ∈ 𝑁 , if 𝐿 ′ ∈ HL prop (𝐿, 𝑁 ), hidden literal elimination (HLE) replaces 𝑁 by (𝑁 \ {𝐿 ′ ∨ 𝐿 ∨ 𝐶}) ∪ {𝐿 ∨ 𝐶}. Given 𝐶 ∈ 𝑁 , {𝐿 1 , . . . , 𝐿 𝑛 } = HL prop (𝐶, 𝑁 ), and We generalize hidden literals to first-order logic with equality by considering substitutivity of variables as well as congruence of equality. The generalized definition also enjoys the key property that 𝐿 ′ ∈ HL(𝐿, 𝑁 ) implies 𝑁 ↓ 2 |= 𝐿 ′ -■ → 𝐿. However, HL(𝐿, 𝑁 ) may be infinite even for predicate literals; for example, p(f 𝑖 (𝑥)) ∈ HL(p(𝑥), {p(𝑥) ∨ ¬p(f (𝑥))}) for every 𝑖.

𝐶 ′ = 𝐶 ∨ 𝐿 1 ∨ • • • ∨ 𝐿 𝑛 , if 𝐶 ′ is
Based on Definition 3.4, we can generalize hidden literal elimination and support a related technique called failed literal elimination:

𝐿 ′ ∨ 𝐿 ∨ 𝐶 HLE 𝐿 ∨ 𝐶 if 𝐿 ′ ∈ HL(𝐿, 𝑁 ) 𝐿 ∨ 𝐶 FLE 𝐶 if 𝐿 ′ , ¬𝐿 ′ ∈ HL(¬𝐿, 𝑁 )
Double lines denote simplification rules: When the premises appear in the clause set, the prover can use the redundancy criterion to replace them by the conclusions. The second rule, failed literal elimination, is inspired by the SAT technique of asserting ¬𝐿 if 𝐿 is a failed literal [START_REF] William | Improvements to Propositional Satisfiability Search Algorithms[END_REF]. It is easy to see that rule HLE is sound. From 𝐿 ′ ∈ HL(𝐿, 𝑁 ) we have 𝑁 |= 𝐿 ′ -■ → 𝐿 (i.e., ¬𝐿 ′ ∨ 𝐿). Performing subsumption resolution [START_REF] Bachmair | Resolution Theorem Proving[END_REF] between 𝐿 ′ ∨ 𝐿 ∨ 𝐶 and ¬𝐿 ′ ∨ 𝐿 yields the conclusion, which is therefore entailed by 𝑁 . For FLE, the condition 𝐿 ′ , ¬𝐿 ′ ∈ HL(¬𝐿, 𝑁 ) means that 𝑁 ↓ 2 |= {¬𝐿 ′ ∨ ¬𝐿, 𝐿 ′ ∨ ¬𝐿} |= ¬𝐿.

𝑠 ≈ 𝑡 ∨ 𝑢 [𝑠] ≈ 𝑢 [𝑡] ∨ 𝐶 CongHLE + 𝑢 [𝑠] ≈ 𝑢 [𝑡] ∨ 𝐶 𝑠 𝑡 ∨ 𝑢 [𝑠] 𝑢 [𝑡] ∨ 𝐶 CongHLE - 𝑠 𝑡 ∨ 𝐶
Hidden literals can be combined with unit clauses 𝐿 ′ to remove more literals:

𝐿 ′ 𝐿 ∨ 𝐶 UnitHLE if 𝐿 ′ 𝜎 ∈ HL(¬𝐿, 𝑁 ) 𝐿 ′ 𝐶
Given a unit clause 𝐿 ′ ∈ 𝑁 , the rule uses it to discharge 𝐿 ′ 𝜎 in 𝑁 |= 𝐿 ′ 𝜎 -■ → ¬𝐿. As a result, we have 𝑁 |= ¬𝐿, making it possible to remove 𝐿 from 𝐿 ∨ 𝐶. Next, we generalize hidden tautologies to first-order logic. Definition 3.7. A clause 𝐶 is a hidden tautology for a clause set 𝑁 if there exists a finite set {𝐿 1 , . . . , 𝐿 𝑛 } ⊆ HL(𝐶, 𝑁 ) such that 𝐶 ∨ 𝐿 1 ∨ • • • ∨ 𝐿 𝑛 is a tautology.

In general, hidden tautologies are not redundant and cannot be deleted during saturation, as shown by the following example.

Example 3.8. Consider the unsatisfiable set 𝑁 = {¬a, ¬b, a ∨ c, b ∨ ¬c}, the order a ≺ b ≺ c, and the empty selection function. The only possible superposition inference from 𝑁 is between the last two clauses, yielding the clause a ∨ b (after simplifying away ⊤ ⊤). This clause is a hidden tautology: We have HL(a ∨ b, 𝑁 ) = HL(a, 𝑁 ) ∪ HL(b, 𝑁 ) = {¬a, ¬b}, and there exists the set {¬a} ⊆ HL(a ∨ b, 𝑁 ) such that ¬a ∨ a ∨ b is a tautology. The hidden tautology a ∨ b is entailed by the larger clauses a ∨ c and b ∨ ¬c. If the hidden tautology a ∨ b is removed, the prover could enter an infinite loop, forever generating and deleting the hidden tautology and never getting the opportunity to derive the empty clause.

In practice, most provers use a variant of the given clause procedure. Removing hidden tautologies breaks the invariant of the procedure that all inferences between clauses in A are redundant. The end result is not that the prover diverges, but that it terminates without deriving the empty clause.

To observe this, assume the setting as in Example 3.8, and let P = 𝑁 and A = ∅. After moving the first three clauses from P to A (leaving us with P = {b ∨ ¬c} and A = {¬a, ¬b, a ∨ c}), no inferences are possible, and no new clauses are added to P. After the last clause is moved to A, the hidden tautology a ∨ b is produced. If it is deleted, the prover terminates with the unsatisfiable set A, but does not derive the empty clause.

To delete hidden tautologies during saturation, the prover could check that all the relevant clause instances encountered along the computation of HL are ≺-smaller than a given hidden tautology. However, this would be expensive and seldom succeed, given that superposition creates lots of nonredundant hidden tautologies. Instead, we propose to simplify hidden tautologies using the following rules:

𝐿 ∨ 𝐿 ′ ∨ 𝐶 HTR 𝐿 ∨ 𝐿 ′ if ¬𝐿 ′ ∈ HL(𝐿, 𝑁 ) and 𝐶 ≠ ⊥ 𝐿 ∨ 𝐶 FLR 𝐿 if 𝐿 ′ , ¬𝐿 ′ ∈ HL(𝐿, 𝑁 ) and 𝐶 ≠ ⊥
We call these techniques hidden tautology reduction and failed literal reduction, respectively. Both rules are sound. As with hidden literals, unit clauses 𝐿 ′ can be exploited:

𝐿 ′ 𝐿 ∨ 𝐶 UnitHTR if 𝐿 ′ 𝜎 ∈ HL(𝐿, 𝑁 ) and 𝐶 ≠ ⊥ 𝐿 ′ 𝐿
We give the simplification rules above (for hidden literal elimination, hidden tautology reduction, failed literal detection, and their variants) the collective name of hidden-literal-based elimination (HLBE). Yet another use of hidden literals is for equivalent literal substitution [START_REF] Marijn | Clause Elimination Procedures for CNF Formulas[END_REF]: If both 𝐿 ′ ∈ HL(𝐿, 𝑁 ) and 𝐿 ∈ HL(𝐿 ′ , 𝑁 ), we can often simplify 𝐿 ′ 𝜎 to 𝐿𝜎 in 𝑁 if 𝐿 ′ 𝜎 ≻ 𝐿𝜎. We want to investigate this further. Theorem 3.9. The rules HLE, FLE, CongHLE + , CongHLE -, UnitHLE, HTR, FLR, and UnitHTR are sound simplification rules.

Proof. It is easy to see that the deleted premises are entailed by the conclusions that replace them and that the conclusions' instances are ≺-smaller than the premises' instances, as required by the redundancy criterion. It remains to check soundness.

PREDICATE ELIMINATION

For propositional logic, variable elimination [START_REF] Eén | Effective Preprocessing in SAT Through Variable and Clause Elimination[END_REF] is one of the main preprocessing and inprocessing techniques. Following Gabbay and Ohlbach's ideas [START_REF] Gabbay | Quantifier Elimination in Second-Order Predicate Logic[END_REF], Khasidashvili and Korovin [START_REF] Khasidashvili | Predicate Elimination for Preprocessing in First-Order Theorem Proving[END_REF] generalized variable elimination to first-order logic with equality and demonstrated that it is effective as a preprocessor. We propose an improvement-defined predicate elimination-that can both eliminate more predicates and generate fewer clauses-and show that, with a minor restriction, predicate elimination can be integrated in a superposition prover without compromising its refutational completeness.

Khasidashvili and Korovin's preprocessing technique removes singular predicates (which they call "non-self-referential predicates") from the problem using so-called flat resolution. Definition 4.1. A predicate symbol is called singular for a clause set 𝑁 if it occurs at most once in every clause contained in 𝑁 .

Definition 4.2. Let 𝐶 = p(ì 𝑠 𝑛 ) ∨ 𝐶 ′ and 𝐷 = ¬p( ì 𝑡 𝑛 ) ∨ 𝐷 ′ be clauses with no variables in common. The clause 𝑠 1 𝑡 1 ∨ • • • ∨ 𝑠 𝑛 𝑡 𝑛 ∨ 𝐶 ′ ∨ 𝐷 ′ is a flat resolvent of 𝐶 and 𝐷 on p.
Given two clause sets 𝑀, 𝑁 , predicate elimination iteratively replaces clauses from 𝑁 containing the symbol p with all flat resolvents against clauses in 𝑀. Eventually, it yields a set with no occurrences of p. The sets 𝑀 and 𝑁 can be initialized to be the same set, but they can also be different sets; for example, with defined predicate elimination, 𝑀 will be a so-called definition set, whereas 𝑁 will be an arbitrary clause set in which p may be nonsingular. Definition 4.3. Let 𝑀, 𝑁 be clause sets and p be a singular predicate for 𝑀. Let be the following relation on clause set pairs and clause sets:

(1) (𝑀, {(¬) p(ì 𝑠) ∨ 𝐶 ′ } ⊎ 𝑁 ) (𝑀, 𝑁 ′ ∪ 𝑁 ) if 𝑁 ′
is the set that consists of all clauses (up to variable renaming) that are flat resolvents with (¬) p(ì 𝑠) ∨ 𝐶 ′ on p and a clause from 𝑀 as premises. The premises' variables are renamed apart.

(2) (𝑀, 𝑁 )

𝑁 if 𝑁 has no occurrences of p.

The resolved set 𝑀 ⋊ p 𝑁 is the clause set 𝑁 ′ such that (𝑀, 𝑁 ) * 𝑁 ′ . Lemma 4.4. Let 𝑀, 𝑁 be clause sets and p be a singular predicate for 𝑀. The resolved set 𝑁 ′ is reached in a finite number of steps, and it is unique up to variable renaming.

Proof. To show is terminating we use the following ordinal measure on clause sets:

𝜈 ({𝐷 1 , . . . , 𝐷 𝑛 }) = 𝜔 𝜈 (𝐷 1 ) ⊕ • • • ⊕ 𝜔 𝜈 (𝐷 𝑛 )
, where 𝜈 (𝐷) is the number of occurrences of p in 𝐷, 𝜔 is the first infinite ordinal, and ⊕ is the Hessenberg, or natural, sum, which is commutative. For every transition

(𝑀, {𝐶} ∪ 𝑁 ) (𝑀, 𝑁 ′ ∪ 𝑁 ), we have 𝜈 ({𝐶} ∪ 𝑁 ) > 𝜈 (𝑁 ′ ∪ 𝑁 ) because 𝜔 𝜈 (𝐶 ) > 𝜔 𝜈 (𝐶 ) -1 • |𝑁 ′ |. Eventually, a state (𝑀, 𝑁 ′ ) with 𝜈 (𝑁 ′ ) = 𝜔 0 • 𝑛 is reached.
Then, we apply the second rule of Definition 4.3 to obtain the resolved set 𝑁 ′ .

To show that 𝑁 ′ is unique, i.e., is confluent, it suffices to show (since is terminating and Newmann's lemma applies [START_REF] Baader | Term Rewriting and All That[END_REF]) that is locally confluent. In other words, whenever (𝑀, 𝑁 ) (𝑀, 𝑁 1 ) and (𝑀, 𝑁 ) (𝑀, 𝑁 2 ), there exists a set 𝑁 ′ such that (𝑀, 𝑁 1 ) (𝑀, 𝑁 ′ ) and (𝑀, 𝑁 2 ) (𝑀, 𝑁 ′ ).

There are two main sources of nondeterminism of : The choice of 𝐶 ∈ 𝑁 and the choice of the literal in 𝐶 to act on. Let us focus on the choice of 𝐶 in 𝑁 ; the same discussion applies for the choice of literal in 𝐶.

Let 𝑁 = {𝐶 1 } ⊎ {𝐶 2 } ⊎ 𝑁 ′ , where 𝐶 1 and 𝐶 2 are clauses with occurrences of p. Then, (𝑀, {𝐶

1 } ⊎ {𝐶 2 ∪ 𝑁 ′ }) (𝑀, 𝑁 ′ 1 ∪ {𝐶 2 ∪ 𝑁 ′ }) and (𝑀, {𝐶 2 } ⊎ {𝐶 1 ∪ 𝑁 ′ }) (𝑀, 𝑁 ′ 2 ∪ {𝐶 1 ∪ 𝑁 ′ }),
⋊ p 𝑁 - p ).
The result of SPE is satisfiable if and only if 𝑁 is satisfiable [30, Theorem 1], justifying SPE's use in a preprocessor. However, eliminating singular predicates aggressively can dramatically increase the number of clauses. To prevent this, Khasidashvili and Korovin suggested to replace 𝑁 by 𝑁 ′ only if 𝜆(𝑁 ′ ) ≤ 𝜆(𝑁 ) and 𝜇 (𝑁 ′ ) ≤ 𝜇 (𝑁 ), where 𝜆(𝑁 ) is the number of literals in 𝑁 and 𝜇 (𝑁 ) is the sum for all clauses 𝐶 ∈ 𝑁 of the square of the number of distinct variables in 𝐶.

Compared with what modern SAT solvers use, this criterion is fairly restrictive. We relax it to make it possible to eliminate more predicates, within reason. Let 𝐾 tol ∈ N be a tolerance parameter. A predicate elimination step from

𝑁 to 𝑁 ′ is allowed if 𝜆(𝑁 ′ ) < 𝜆(𝑁 ) + 𝐾 tol or 𝜇 (𝑁 ′ ) < 𝜇 (𝑁 ) or |𝑁 ′ | < |𝑁 | + 𝐾 tol .
A refinement, which we will not study, would be to gradually increment the tolerance 𝐾 tol , as is done in some SAT solvers.

SPE is effective, but an important refinement has not yet been adapted to first-order logic: variable elimination by substitution. Eén and Biere [START_REF] Eén | Effective Preprocessing in SAT Through Variable and Clause Elimination[END_REF] discovered that a propositional variable x can be eliminated without computing all resolvents if it is expressible as an equivalence x ← → 𝜑, where 𝜑, the "gate, " is an arbitrary formula that does not reference x. They extract from a set 𝑁 of propositional clauses into a definition set 𝐺, essentially the clausification of x ← → 𝜑, and 𝑅 = 𝑁 p \𝐺, the remaining clauses containing p. To eliminate x from 𝑁 while preserving satisfiability, it suffices to resolve clauses from 𝐺 against clauses from 𝑅, effectively substituting 𝜑 for x in 𝑅. Crucially, we do not need to resolve pairs of clauses from 𝐺 or pairs of clauses from 𝑅. We generalize this idea to first-order logic. A definition set 𝐺 corresponds intuitively to a definition by cases in mathematics-e.g.,

p( ì 𝑥) = ⊤ if 𝜑 ( ì 𝑥) ⊥ if 𝜓 ( ì 𝑥)
Part ( 4) states that the case conditions are mutually exclusive (e.g., ¬𝜑 ( ì 𝑥)∨¬𝜓 ( ì 𝑥)), and part (5) states that they are exhaustive (e.g., ì c . ¬𝜑 (ì c) ∧ ¬𝜓 (ì c)). Given a quantifier-free formula p( ì 𝑥) ← → 𝜑 ( ì 𝑥) with distinct variables ì 𝑥 such that 𝜑 ( ì 𝑥) does not contain p, any reasonable clausification algorithm would produce a definition set for p.

Example 4.8. Given the formula p(𝑥) ← → q(𝑥) ∧ (r(𝑥) ∨ s(𝑥)), a standard clausification algorithm [START_REF] Nonnengart | Computing Small Clause Normal Forms[END_REF] produces {¬p(𝑥) ∨ q(𝑥), ¬p(𝑥) ∨ r(𝑥) ∨ s(𝑥), p(𝑥) ∨ ¬q(𝑥) ∨ ¬r(𝑥), p(𝑥) ∨ ¬q(𝑥) ∨ ¬s(𝑥)}, which qualifies as a definition set for p.

Definition sets generalize Eén and Biere's gates. They can be recognized syntactically for formulas such as p( ì 𝑥) ← → 𝑖 q 𝑖 ( ì 𝑠 𝑖 ) or p( ì 𝑥) ← → 𝑖 q 𝑖 ( ì 𝑠 𝑖 ), or semantically: Condition (4) can be checked using the congruence closure algorithm, and condition (5) amounts to a propositional unsatisfiability check.

The key result about propositional gates carries over to definition sets. Proof. We show the contrapositive. Assume that for some J and 𝜉, J |= 𝜉 𝑁 ( ì 𝑥). Then let J ′ be a model that assigns each c 𝑖 the interpretation of 𝑥 𝑖 under J and 𝜉, and otherwise coincides with J. We obtain J ′ |= 𝑁 (ì c). □ Lemma 4.11. Let 𝐺 be a definition set for p and 𝑁 be an arbitrary clause set. If (𝐺, 𝑁 ) (𝐺, 𝑁 ′ ) for some 𝑁 ′ , then 𝐺 ∪ 𝑁 and 𝐺 ∪ 𝑁 ′ are equivalent.

Proof. Since flat resolution is sound, the nontrivial direction is to show that a model J of the set 𝐺 ∪ 𝑁 ′ is also a model of 𝐺 ∪ 𝑁 . Since the only clause in 𝑁 \ 𝑁 ′ is the clause 𝐶 = (¬) p(ì 𝑠 𝑛 ) ∨ 𝐶 ′ on which the step is performed, it suffices to show J |= 𝐶. Without loss of generality, we assume that the leading literal of 𝐶 is positive. Toward a contradiction, assume 𝜉 is a valuation such that J ̸ |= 𝜉 𝐶. p ). In all other cases, it is not applicable.

) such that J ̸ |= 𝜉 ′ 𝐷 ′ . The resolvent 𝑅 = 𝑥 1 𝑦 1 ∨ • • • ∨ 𝑥 𝑛 𝑦 𝑛 ∨ 𝐶 ′ ∨ 𝐷 ′ is
Hidden-literal-based techniques fit within the traditional framework of saturation, because they delete or reduce a clause based on the presence of other clauses. In contrast, predicate elimination relies on the absence of clauses from the proof state. We can still integrate it with superposition as follows: At every 𝑘th iteration of the given clause procedure, perform predicate elimination on A ∪ P, and add all new clauses to P.

One may wonder whether such an approach preserves the refutational completeness of the calculus. The answer is no.

To see why, consider the following binary splitting rule based on Riazanov and Voronkov [START_REF] Riazanov | Splitting Without Backtracking[END_REF]:

𝐶 ∨ 𝐷 BS p ∨ 𝐶 𝐷 ∨ ¬p
Provisos: 𝐶 and 𝐷 have no free variables in common, p is fresh, and p is ≺-smaller than 𝐶 and 𝐷. Since the conclusions are smaller than the premise, the rule can be applied aggressively as a simplification. But notice that the effect of splitting can be undone by singular predicate elimination, possibly giving rise to loops BS, SPE, BS, SPE, . . . . Under which conditions is predicate elimination refutationally complete? To answer this question, we employ the saturation framework of Waldmann, Tourret, Robillard, and Blanchette [START_REF] Waldmann | A Comprehensive Framework for Saturation Theorem Proving[END_REF][START_REF] Waldmann | accepted. A Comprehensive Framework for Saturation Theorem Proving[END_REF]. Let (FInf , Red) be the base calculus without predicate elimination-e.g., resolution or superposition inferences together with the standard redundancy criterion [4, Sect. 4.2]. The inference system FInf is a set of inferences (𝐶 𝑛 , . . . , 𝐶 1 , 𝐶 0 ), for 𝑛 ≥ 1, where 𝐶 𝑛 , . . . , 𝐶 1 are the premises and 𝐶 0 is the conclusion. 𝐶 1 is called the main premise. The redundancy criterion is a pair Red = (Red I , Red F ) where Red I determines which inferences can be omitted and Red F is used to remove clauses.

Next, consider an abstract proving process working on a single clause set. Let ▷ Red denote the transition relation that supports (1) adding arbitrary clauses and (2) removing clauses deemed useless by Red F . Typically, the added clauses are the result of performing inferences and are entailed by the premises, but other clauses can be added as well. A ▷ Red -derivation is a finite or infinite sequence of clause sets

𝑁 0 ▷ Red 𝑁 1 ▷ Red • • • .
We fix a finite set P of predicate symbols that may be subjected to predicate elimination. These might include all the predicate symbols occurring in the input problem, but exclude any symbols introduced by splitting or other rules. Given a clause or clause set 𝑁 , we write P(𝑁 ) to denote the set of all predicate symbols from P occurring in 𝑁 . Let ▷ P denote the elimination of a singular or defined predicate symbol from P. A mixed derivation consists of transitions either of the form 𝑁 ▷ P 𝑁 ′ or of the form 𝑁 ▷ Red 𝑁 ′ where P(𝑁 ) ⊇ P(𝑁 ′ ). Because P is finite, any mixed derivation consists of at most finitely many ▷ P transitions. Hence, in any derivation, there exists an index 𝑘 from which all transitions are standard ▷ Red -transitions.

This suggests the following path to completeness: Pretend that the transitions between 𝑁 0 and 𝑁 𝑘 are merely preprocessing and start the actual derivation at 𝑁 𝑘 . This works at the abstract level of derivations on single clause sets. It fails, however, for an actual saturation prover that distinguishes between passive and active clauses. Example 4. [START_REF] Davis | A Computing Procedure for Quantification Theory[END_REF]. In Example 4.15, the initial clause set was satisfiable. If it is unsatisfiable, we can even lose refutational completeness. To see why, we add the unit clauses ¬b and ¬c to the initial clause set of Example 4.15 to make it unsatisfiable. We repeat the same steps as above, including the subsumptions at the end, yielding the passive set { ¬b, ¬c } and the active set {c ∨ d, b ∨ ¬d }. Then, making ¬b and ¬c active triggers no inferences. The prover stops with an unsatisfiable four-clause active set that does not contain the empty clause.

A solution could be to move all active clauses to the passive set at step 𝑘 or later, but this would be costly, since it would force the prover to redo inferences whose conclusions might then have to be simplified or subsumed again. Instead, we salvage the existing completeness proof for GC, by resolving the issues concerning splitting and the GC invariant. Our approach is to weaken the redundancy criterion slightly, enough both to disable splitting on P-predicates and to ensure that inferences such as 𝜄 in Examples 4.15 and 4.16 are performed. The required weakening is so mild that it does not invalidate any practical simplification or subsumption techniques we are aware of, except of course splitting.

In accordance with the saturation framework, let F be the set of first-order Σ-clauses, let G be its ground subset, and let G be a function that maps an F-clause to the set of its G-clause instances and analogously for F-inferences. We define an extension G ♭ of G for Σ ♭ -clauses in an ad hoc nonclassical logic reminiscent of paraconsistent logics [START_REF] Carnielli | Logics of Formal Inconsistency[END_REF]. The signature Σ ♭ extends Σ with a distinguished predicate symbol ⊥ that is interpreted differently from ⊤. For Σ ♭ , the Boolean type 𝑜 may be interpreted as any set of cardinality at least 2.

The objective is to disallow the entailment that makes splitting and Examples 4.15 and 4.16 possible. The weaker entailment will be used to define a weaker redundancy criterion, which will curtail splitting. Properties such as soundness of the calculus can still be established using the standard entailment notion.

Definition 4.17. The operator ♭ translates Σ-literals to Σ ♭ -literals as follows, where p ∈ P, q ∉ P, and 𝑠, 𝑡 are non-Boolean terms:

p( ì 𝑡) ♭ = p( ì 𝑡) ⊥ q( ì 𝑡) ♭ = q( ì 𝑡) ≈ ⊤ (𝑠 ≈ 𝑡) ♭ = 𝑠 ≈ 𝑡 ¬ p( ì 𝑡) ♭ = p( ì 𝑡) ⊤ ¬ q( ì 𝑡) ♭ = q( ì 𝑡) ⊤ (𝑠 𝑡) ♭ = 𝑠 𝑡
The operator is lifted elementwise to G-clauses and G-clause sets. The weak entailment |= ♭ over G-clause sets is defined via an encoding into Σ ♭ -clauses: 𝑀 |= ♭ 𝑁 if and only if 𝑀 ♭ |= 𝑁 ♭ . The lifting to F-clauses and F-clause set is achieved in the standard way via grounding.

The following property of weak entailment will allow us to eliminate P-predicates without losing completeness: Lemma 4.18. Let 𝐶 be a clause that contains the predicate symbol p ∈ P and 𝐷 be a clause that does not contain p.

If 𝑁 ∪ {𝐶} |= ♭ {𝐷 }, then 𝑁 |= ♭ {𝐷 }.
Proof. Suppose J |= 𝑁 ♭ . We will define J ′ so that J ′ |= 𝑁 ♭ ∪ {𝐶 ♭ }, retrieve J ′ |= 𝐷 ♭ , and then argue that J |= 𝐷 ♭ . We take J ′ to coincide with J except that we extend the domain for 𝑜 with one fresh value and use this value as the interpretation of p( ì 𝑡) for all argument tuples ì 𝑡. This modification makes any p literal of 𝐶 ♭ true, and it preserves the truth of 𝑁 ♭ . By the hypothesis, J ′ |= 𝐷 ♭ . And since p does not occur in 𝐷, we have J |= 𝐷 ♭ . □ Note that the above lemma does not hold for classical entailment |=; indeed, {p ∨ q, ¬p ∨ q} |= {q} yet {p ∨ q} ̸ |= {q}. On the other hand, the law of excluded middle does hold for weak entailment: |= ♭ p ∨ ¬ p. In fact, all classical clausal tautologies are tautologies for |= ♭ .

The standard redundancy criterion Red is obtained by lifting a criterion on G-clauses to F-clauses. The same construction can be replicated using |= ♭ instead of |=, yielding the weak redundancy criterion Red ♭ . It is easy to check that the usual simplification techniques implemented in superposition provers can be justified using Red ♭ . Specifically, this concerns the following rules described by Schulz [42, Sects. 2.3.1 and 2.3.2]: deletion of duplicated literals, deletion of resolved literals, syntactic tautology deletion, semantic tautology deletion, rewriting of negative literals, positive simplify-reflect, negative simplify-reflect, clause subsumption, and equality subsumption. Moreover, rewriting of positive literals is possible if the rewriting clause is smaller than the rewritten clause (a condition that is also needed with |= but omitted by Schulz). Finally, destructive equality resolution cannot be justified with |=, let alone |= ♭ .

We instantiate the saturation framework with (FInf , Red ♭ ) to obtain a given clause prover GC. The prover operates on sets of labeled clauses (𝐶, 𝑙), where 𝐶 is a standard clause and 𝑙 ∈ L is a label. The active label identifies active clauses; all other clauses are passive. The prover takes the form of two rules, Process and Infer, restricted to prevent the introduction of P-predicates. We extend it with a third rule, PredElim, for predicate elimination, and call the extended prover GCP. The rules are as follows, using again the framework notations:

Process N ∪ M =⇒ GCP N ∪ M ′ where M ⊆ LRed ♭,⊐ F (N ∪ M ′ ), M ′ ↓ active = ∅, and P( ⌊M ′ ⌋) ⊆ P( ⌊N ∪ M⌋)

Infer N ∪ {(𝐶, 𝑙)} =⇒ GCP N ∪ {(𝐶,
PredElim N ∪ M =⇒ GCP N ∪ M ′
where N ∪ M ▷ P N ∪ M ′ and M ′ ↓ active = ∅ Here is a summary of the main framework notations:

• The letters M, N range over sets of labeled clauses. M↓ 𝑙 denotes the subset of clauses in M labeled with 𝑙. The operator ⌊ ⌋ erases all labels in a labeled clause or clause set. • FInf (𝑁 ) denotes the set of all base calculus inferences with premises in 𝑁 , and FInf (𝑁 , 𝑀) = FInf (𝑁 ∪ 𝑀) \ FInf (𝑁 \ 𝑀). The same notations are also available for the straightforward extension FLInf of FInf with labels. • LRed ♭,⊐ is the extension of the standard redundancy criterion Red ♭ defined using |= ♭ to nonground labeled clauses with subsumption (⊏). • Given a sequence (N 𝑖 ) 𝑖 , its limit (inferior) is N ∞ = 𝑖 𝑗 ≥𝑖 N 𝑗 .

The completeness proof follows the invariance-based argument found in the article by Waldmann et al. [START_REF] Waldmann | accepted. A Comprehensive Framework for Saturation Theorem Proving[END_REF] about the saturation framework. Proof. The base case is as in Waldmann et al.

For Process and Infer, the proof is essentially as in Waldmann et al., except that we also need to show that LRed ♭ I (N 𝑘 ) ⊆ LRed ♭ I (N 𝑘+1 ). This is a consequence of N 𝑘 ▷ LRed ♭,⊐ N 𝑘+1 and of properties (R2) and (R3) of redundancy criteria.

A new case to consider is that of a PredElim transition

N 𝑘 =⇒ GCP N 𝑘+1 . Let N 𝑘 = N ∪ M =⇒ GCP N ∪ M ′ = N 𝑘+1
, where N ∪ M ▷ P N ∩ M ′ and M ′ ↓ active = ∅. We assume without loss of generality that M ∩ M ′ = ∅. Let p be the eliminated predicate. Note that p occurs in every clause in M but in none of the clauses in N or M ′ . We must show FLInf (N 𝑘+1 ↓ active ) ⊆ LRed ♭ I (N 𝑘+1 ). As for Process, we have the inclusion FLInf (N 𝑘+1 ↓ active ) ⊆ FLInf (N 𝑘 ↓ active ), by the side condition that M ′ ↓ active = ∅. Moreover, by the induction hypothesis, FLInf (N 𝑘 ↓ active ) ⊆ LRed ♭ I (N 𝑘 ). Thus, FLInf (N 𝑘 ↓ active ) ⊆ LRed ♭ I (N ∪ M). Let 𝜄 ∈ FLInf (N↓ active ). By the argument above, we have 𝜄 ∈ LRed ♭ I (N ∪ M). We must show 𝜄 ∈ LRed ♭ I (N ∪ M ′ ). By definition of LRed ♭ I , it suffices to show that for every ground instance (𝐶 𝑛 , . . . , 𝐶 1 , 𝐶 0 ) of 𝜄, there exists a finite clause set D ⊆ G(N ) ∪ G(M ′ ) that is ≺-smaller than 𝐶 1 and such that {𝐶 𝑛 , . . . , 𝐶 2 } ∪ D |= ♭ {𝐶 0 }. Without loss of generality, we assume that D is the ≺-smallest such set; such a set exists because ≺ is well founded. By definition of N , p cannot occur in 𝐶 0 . By Lemma 4.18, if p occurred in 𝐷 ∈ D, we could remove 𝐷, but this would mean D is not minimal. As a result, D cannot contain clauses from G(M) and hence D ⊆ G(N ). Thus, 𝜄 ∈ LRed ♭ I (N ). By property (R2) of redundancy criteria, we have the desired result: 𝜄 ∈ LRed ♭ I (N ∪ M ′ ). □ Lemma 4.21. Let (N 𝑖 ) 𝑖 be a ▷ LRed ♭,⊐ -derivation. If Inv ♭ N (𝑖) holds for all indices 𝑖, then FLInf (N ∞ ↓ active ) ⊆ 𝑖 LRed ♭ I (N 𝑖 ) holds.

Proof. We assume 𝜄 ∈ FLInf (N ∞ ↓ active ) and show 𝜄 ∈ 𝑖 LRed ♭ I (N 𝑖 ) for some arbitrary 𝜄. For 𝜄 to belong to FLInf (N ∞ ↓ active ), all of its finitely many premises must be in N ∞ ↓ active . Therefore, there must exist an index 𝑘 such that N 𝑘 ↓ active contains all of them, and therefore 𝜄 ∈ FLInf (N 𝑘 ↓ active ). ) 𝑖 be a =⇒ GCP -derivation with N 0 ↓ active = ∅ and N ∞ ↓ 𝑙 = ∅ for every label 𝑙 ≠ active. If ⌊N 0 ⌋ is unsatisfiable, then some N 𝑖 contains the empty clause with some arbitrary label.

Proof. By Lemma 4.22, we know that there exists an index 𝑘 such that (N 𝑘+𝑖 ) 𝑖 is a fair ▷ LRed ♭,⊐derivation. Moreover, since ▷ LRed ♭,⊐ and ▷ P preserve unsatisfiability (by (R1) of redundancy criteria, Khasidashvili and Korovin's Theorem 1, and our Theorem 4.13), we have that ⌊N 𝑘 ⌋ is unsatisfiable. Since the base calculus (FLInf , LRed) is assumed to be statically refutationally complete with respect to |=, the calculus (FLInf , LRed ♭ ) with a weaker redundancy criterion is also statically complete with respect to |=, and by the saturation framework, (FLInf , LRed ♭,⊐ ) preserves this. Exploiting the equivalence of static and dynamic completeness (Lemmas 10 and 11 in Waldmann et al. [START_REF] Waldmann | accepted. A Comprehensive Framework for Saturation Theorem Proving[END_REF]), we conclude that some N 𝑘+𝑖 must contain a labeled empty clause. □

To summarize, we have shown that predicate elimination can be used as inprocessing in a superposition prover based on the given clause procedure, with one minor restriction: To avoid loops, predicate symbols arising from clause splitting should not be eliminated.

SATISFIABILITY BY CLAUSE ELIMINATION

The main approaches to show satisfiability of a first-order problem are to produce either a finite Herbrand model or a saturated clause set. Saturations rarely occur except for very small problems or within decidable fragments. In this section, we explore an alternative approach that establishes satisfiability by iteratively removing clauses while preserving unsatisfiability, until the clause set has been transformed into the empty set. So far, this technique has been studied only for QBF [START_REF] Heule | A Unified Proof System for QBF Preprocessing[END_REF]. We show that blocked clause elimination (BCE) can be used for this purpose. It can efficiently solve some problems for which the saturated set would be infinite. However, it can break the refutational completeness of a saturation prover. We conclude with a procedure that transforms SAT-Inspired Eliminations for Superposition 1:15 a finite Herbrand model into a sequence of clause elimination steps ending in the empty clause set, thereby demonstrating the theoretical power of clause elimination.

Kiesl et al. [START_REF] Kiesl | Blocked Clauses in First-Order Logic[END_REF] generalized blocked clause elimination to first-order logic. Their generalization uses flat 𝐿-resolvents, an extension of flat resolvents that resolves a single literal 𝐿 against 𝑚 literals of the other clause. Removing a blocked clause from a set preserves unsatisfiability [START_REF] Kiesl | Blocked Clauses in First-Order Logic[END_REF]. Kiesl et al. evaluated the effect of removing all blocked clauses as a preprocessing step and found that it increases the prover's success rate.

In fact, there exist satisfiable problems that cannot be saturated in finitely many steps regardless of the calculus's parameters but that can be reduced to an empty, vacuously satisfiable problem through blocked clause elimination.

Example 5.3. Consider the clause set 𝑁 consisting of 𝐶 = p(𝑥, 𝑥) and 𝐷 = ¬p(𝑦 1 , 𝑦 3 ) ∨ p(𝑦 1 , 𝑦 2 ) ∨ p(𝑦 2 , 𝑦 3 ). Note that if no literal is selected, all literals are eligible for superposition. In particular, the superposition of p(𝑥, 𝑥) into 𝐷's negative literal eventually needs to be performed regardless of the chosen selection function or term order, with the conclusion 𝐸 1 = p(𝑧 1 , 𝑧 2 ) ∨ p(𝑧 2 , 𝑧 1 ). Then, superposition of 𝐸 1 into 𝐷 yields 𝐸 2 = p(𝑧 1 , 𝑧 2 ) ∨ p(𝑧 2 , 𝑧 3 ) ∨ p(𝑧 3 , 𝑧 1 ). Repeating this process yields infinitely many clauses 𝐸 𝑖 = p(𝑧 1 , 𝑧 2 ) ∨ • • • ∨ p(𝑧 𝑖 , 𝑧 𝑖+1 ) ∨ p(𝑧 𝑖+1 , 𝑧 1 ) that cannot be eliminated using standard redundancy-based techniques.

In the example above, the clause 𝐷 is blocked by its second or third literal. If we delete 𝐷, 𝐶 becomes blocked in turn. Deleting 𝐶 leaves us with the empty set, which is vacuously satisfiable. The example suggests that using BCE during saturation might help focus the proof search. Indeed, Kiesl et al. ended their investigations by asking whether BCE can be used as an inprocessing technique in a saturation prover. Unfortunately, in general the answer is no: Example 5.4. Consider the unsatisfiable set 𝑁 = {𝐶 1 , . . . , 𝐶 6 }, where

𝐶 1 = ¬c ∨ e ∨ ¬a 𝐶 2 = ¬c ∨ ¬e 𝐶 3 = b ∨ c 𝐶 4 = ¬b ∨ ¬c 𝐶 5 = a ∨ b 𝐶 6 = c ∨ ¬b
Assume the simplification ordering a ≺ b ≺ c ≺ d ≺ e and the selection function that chooses the last negative literal of a clause as presented. Gray boxes indicate literals that can take part in superposition inferences. Only two superposition inferences are possible: from 𝐶 3 into 𝐶 4 , yielding the tautology 𝐶 7 = b ∨ ¬b , and from 𝐶 5 into 𝐶 6 , yielding 𝐶 8 = a ∨ c . Clause 𝐶 7 is clearly redundant, whereas 𝐶 8 is blocked by its first literal. If we allow removing blocked clauses, the prover enters a loop: 𝐶 8 is repeatedly generated and deleted. Thus, the prover will never generate the empty clause for this unsatisfiable set.

As with hidden tautologies, removing blocked clauses breaks the invariant of the given clause procedure that all inferences between clauses in A are redundant. To see this, assume the setting of Example 5.4, and let P = 𝑁 and A = ∅. Assume 𝐶 1 , 𝐶 2 , 𝐶 3 are moved to the active set. As there are no possible inferences between them, the proof state becomes A = {𝐶 1 , 𝐶 2 , 𝐶 3 } and P = {𝐶 4 , 𝐶 5 , 𝐶 6 }. After 𝐶 4 is moved to A, the conclusion 𝐶 7 is computed, but it is not added to P as it is redundant. Moving 𝐶 5 to A produces no new conclusions, but after 𝐶 6 is moved, 𝐶 8 is produced. However, if we allow eliminating blocked clauses, it will not be added to P as it is blocked. The prover then terminates with A = 𝑁 and P = ∅, even though the original set 𝑁 is unsatisfiable.

Although using BCE as inprocessing breaks the completeness of superposition in general, it is conceivable that a well-behaved fragment of BCE might exist. This could be investigated further.

Not only can BCE prevent infinite saturation (Example 5.3), but it can also be used to convert a finite Herbrand model into a certificate of clause set satisfiability. The certificate uses only blocked clause elimination and addition, in conjunction with a transformation to reduce the clause set to an empty set. This theoretical result explores the relationship between Herbrand models and satisfiability certificates based on clause elimination and addition. It is conceivable that it can form the basis of an efficient way to certify Herbrand models.

In propositional logic, asymmetric literals can be added to or removed from clauses, retaining the equivalence of the resulting clause set with the original one. Kiesl and Suda [START_REF] Kiesl | A Unifying Principle for Clause Elimination in First-Order Logic[END_REF] described an extension of this technique to first-order logic. Their definition of asymmetric literals can be relaxed to allow the addition of more literals, but the resulting set is then only equisatisfiable to the original one, not equivalent. This in turn allows us to show that a problem is satisfiable by reducing it to an empty problem, as is done in some SAT solvers.

For the rest of this section, we work with clausal first-order logic without equality. We use Herbrand models as canonical representatives of first-order models, recalling that every satisfiable set has a Herbrand model [START_REF] Fitting | First-Order Logic and Automated Theorem Proving[END_REF]Sect. 5.4]. Definition 5.5. A literal 𝐿 is a global asymmetric literal (GAL) for a clause 𝐶 and a clause set 𝑁 if for every ground instance 𝐶𝜎 of 𝐶, there exists a ground instance 𝐷𝜚 ∨ 𝐿 ′ 𝜚 of 𝐷 ∨ 𝐿 ′ ∈ 𝑁 \ {𝐶} such that 𝐷𝜚 ⊆ 𝐶𝜎 and ¬𝐿 ′ 𝜚 = 𝐿𝜎.

Every asymmetric literal is GAL, but the converse does not hold: Example 5.6. Consider a clause 𝐶 = p(𝑥, 𝑦) and a clause set 𝑁 = {q ∨ p(a, a)}. Then, ¬q is not an asymmetric literal for 𝐶 and 𝑁 , but it is a GAL for 𝐶 and 𝑁 .

Adding and removing GALs preserves and reflects satisfiability: Theorem 5.7. If 𝐿 is a GAL for the clause 𝐶 and the clause set 𝑁 , then the set (𝑁 \ {𝐶}) ∪ {𝐶 ∨ 𝐿} is satisfiable if and only if 𝑁 is satisfiable.

Proof. Let 𝑁 ′ = 𝑁 \ {𝐶} ∪ {𝐶 ∨ 𝐿}. The nontrivial direction is to prove that if 𝑁 ′ has a model, so does 𝑁 . If 𝑁 ′ has a model, it has an Herbrand model J. Clearly, J satisfies every clause in 𝑁 , with the possible exception of 𝐶. Assume there exists a ground instance 𝐶𝜎 falsified by J. Since 𝐿 is a GAL for 𝐶 and 𝑁 , then there exists a ground instance 𝐷𝜏 ∨ 𝐿 ′ 𝜏 of 𝐷 ∨ 𝐿 ′ ∈ 𝑁 ′ and ¬𝐿 ′ 𝜏 = 𝐿𝜎. If J |= 𝐿 ′ 𝜏, for 𝐶𝜎 ∨ 𝐿𝜎 to be satisfied by J, some literal in 𝐶𝜎 must be satisfied by J, contradicting that 𝐶𝜎 is falsified by J. If J ̸ |= 𝐿 ′ 𝜏 then some literal in 𝐷𝜏 must be satisfied. Since 𝐷𝜏 ⊆ 𝐶𝜎, we get the same contradiction. Therefore, J satisfies 𝑁 , as needed. □

For first-order logic without equality, a clause 𝐿 ∨ 𝐶 is blocked if all its 𝐿-resolvents are tautologies [START_REF] Kiesl | Blocked Clauses in First-Order Logic[END_REF]. The 𝐿-resolvent between 𝐿 ∨ 𝐶 and ¬𝐿 1 ∨ • • • ∨ ¬𝐿 𝑛 ∨ 𝐷 is (𝐶 ∨ 𝐷)𝜎, where 𝜎 is the most general unifier of the literals 𝐿, 𝐿 1 , . . . , 𝐿 𝑛 [START_REF] Bachmair | Resolution Theorem Proving[END_REF]. Given a Herbrand model J of a problem, the following procedure removes all clauses while preserving satisfiability:

(1) Let q be a fresh predicate symbol. For each atom p(ì 𝑠) in the Herbrand universe: If J |= p(ì 𝑠), add the clause q ∨ p(ì 𝑠); otherwise, add q ∨ ¬p(ì 𝑠). Adding either clause preserves satisfiability as both are blocked by q. (2) Since J is a model, for each ground instance 𝐶𝜎, there exists a clause q ∨ 𝐿 with 𝐿 ∈ 𝐶𝜎. We can transform 𝐶 ∈ 𝑁 into 𝐶 ∨ ¬q, since ¬q is a GAL for 𝐶 and 𝑁 . (3) Consider the clause q ∨ 𝐿 added by step 1. Since 𝐿 is ground and no clause q ∨ ¬𝐿 was added (since J is a model), the only 𝐿-resolvents are against clauses added by step 2. Since all of those clauses contain ¬q, the resolvents are tautologies. Thus, each q ∨ 𝐿 is blocked and can be removed in turn. (4) The remaining clauses all contain the literal ¬q. They can be removed by BCE as well. The procedure is limited to first-order logic without equality, since step 3 is justified only if is a predicate literal. (Otherwise, 𝐿 cannot block clause q ∨ 𝐿 [START_REF] Kiesl | Blocked Clauses in First-Order Logic[END_REF].) The procedure also terminates only for finite Herbrand models.

Example 5.8. Consider the satisfiable clause set 𝑁 = {r(𝑥) ∨ s(𝑥), ¬r(a), ¬s(b)} and a Herbrand model J over {a, b, r, s} such that r(b) and s(a) are the only true atoms in J. We show how to remove all clauses in 𝑁 using J by following the procedure above.

Let 𝑁 J = {q ∨ ¬r(a), q ∨ r(b), q ∨ s(a), q ∨ ¬s(b)}. We set 𝑁 ← 𝑁 ∪ 𝑁 J . This preserves satisfiability since all clauses in 𝑁 J are blocked. It is easy to check that ¬q is GAL for every clause in 𝑁 \ 𝑁 J . The only substitutions that need to be considered are {𝑥 ↦ → a} and {𝑥 ↦ → b} for r(𝑥) ∨ s(𝑥). So we set 𝑁 ← {¬q ∨ r(𝑥) ∨ s(𝑥), ¬q ∨ ¬r(a), ¬q ∨ ¬s(b)} ∪ 𝑁 J . Clearly, all clauses in 𝑁 J are blocked, so we set 𝑁 ← 𝑁 \ 𝑁 J . All clauses remaining in 𝑁 have a literal ¬q and can be removed, leaving 𝑁 empty as desired.

IMPLEMENTATION

Hidden-literal-based elimination, predicate elimination, and blocked clause elimination all admit efficient implementations in a superposition prover. In this section, we describe how to implement the first two sets of techniques. For BCE, we refer to Kiesl et al. [START_REF] Kiesl | Blocked Clauses in First-Order Logic[END_REF]. All techniques are implemented in the Zipperposition prover [START_REF] Cruanes | Superposition with Structural Induction[END_REF]. Zipperposition is designed for fast prototyping of improvements to superposition, but it implements many of the most successful heuristics from the E prover [START_REF] Schulz | Faster, Higher, Stronger: E 2.3[END_REF] and has recently become competitive [START_REF] Sutcliffe | The CADE-27 Automated Theorem Proving System Competition-CASC-27[END_REF].

Hidden-Literal-Based Elimination

For HLBE, an efficient representation of HL(𝐿, 𝑁 ) is crucial. Because this set may be infinite, we underapproximate it by restricting the length of the transitive chains via a parameter 𝐾 len . Given the current clause set 𝑁 , the finite map Imp[𝐿 ′ ] associates with each literal 𝐿 ′ a set of pairs (𝐿, 𝑀) such that 𝐿 ′ ↩→ 𝑘 𝐿, where 𝑘 ≤ 𝐾 len and 𝑀 is the multiset of clauses used to derive 𝐿 ′ ↩→ 𝑘 𝐿. Moreover, we consider only transitions of type (1) (as per Definition 3.4). The following algorithm maintains Imp dynamically, updating it as the prover derives and deletes clauses. It depends on the global variable Imp and the parameters 𝐾 len and 𝐾 imp .

procedure AddImplication(𝐿 a , 𝐿 c , 𝐶)

if Imp[𝐿 a 𝜎] ≠ ∅ for some renaming 𝜎 then (𝐿 a , 𝐿 c ) ← (𝐿 a 𝜎, 𝐿 c 𝜎) if there are no 𝐿, 𝐿 ′ , 𝑀, 𝜎 such that (𝐿 ′ , 𝑀) ∈ Imp[𝐿],

erase (𝐿 c , 𝑀) from Imp[𝐿 a ]
The algorithm views a clause 𝐿 ∨ 𝐿 ′ as two implications ¬𝐿 -■ → 𝐿 ′ and ¬𝐿 ′ -■ → 𝐿. It stores only one entry for all literals equal up to variable renaming (line 2). Each implication 𝐿 a -■ → 𝐿 c represented by the clause is stored only if its generalization is not present in Imp (line 4). Conversely, all instances of the implication are removed (line 6).

Next, the algorithm finds each implication stored in Imp that can be linked to 𝐿 a -■ → 𝐿 c : Either 𝐿 c becomes the new consequent (line 9) or 𝐿 a becomes the new antecedent (line 13). If 𝐿 c can be decomposed into 𝑢 [𝑠] 𝑢 [𝑡], rule (3) of Definition 3.4 allows us to store 𝑠 𝑡 in Imp[𝐿 a ] (line 18). This is an exception to the idea that transitive chains should use only rule [START_REF] Avenhaus | DISCOUNT: A SYstem for Distributed Equational Deduction[END_REF]. The application of rule (3) does not count toward the bound 𝐾 len . If 𝐿 a is of the form 𝑢 [𝑠] ≈ 𝑢 [𝑡], then Imp could be extended so that Imp[𝑠 ≈ 𝑡] = Imp[𝐿 a ], but this would substantially increase Imp's memory footprint.

In first-order logic, different instances of the same clause can be used along a transitive chain. For example, the clause 𝐶 = ¬p(𝑥) ∨ p(f(𝑥)) induces p(𝑥) ↩→ 𝑖 p(f 𝑖 (𝑥)) for all 𝑖. The algorithm discovers such self-implications (line 23): For each clause 𝐶 of the form ¬𝐿 ∨ 𝐿𝜎, where 𝜎 is some nonidempotent substitution, the pairs (𝐿𝜎 2 , {𝐶}), . . . , (𝐿𝜎 𝐾 imp +1 , {𝐶}) are added to Imp[𝐿], where 𝐾 imp is a parameter.

To track and untrack clauses efficiently, we implement the mapping Imp as a nonperfect discrimination tree [START_REF] Ramakrishnan | Term Indexing[END_REF]. Given a query literal 𝐿, this indexing data structure efficiently finds all literals 𝐿 ′ such that for some 𝜎, 𝐿 ′ 𝜎 = 𝐿 and Imp[𝐿 ′ ] ≠ ∅. We can use it to optimize all lookups except the one on line 9. For this remaining lookup, we add an index Imp -1 that inverts Imp, i.e., Imp -1 [𝐿] = {𝐿 ′ | Imp[𝐿 ′ ] = (𝐿, 𝑀) for some 𝑀 }. To avoid sequentially going through all entries in Imp when the prover deletes them, for each clause 𝐶 we keep track of each literal 𝐿 such that 𝐶 appears in Imp[𝐿]. Finally, we limit the number of entries stored in Imp[𝐿]-by default, up to 48 pairs in each Imp[𝐿] are stored.

To implement the HLE rule, we use Imp[𝐿] as follows: Given a clause 𝐶 = 𝐿 ∨ 𝐿 ′ ∨ 𝐶 ′ , if there are two literals 𝐿 1 , 𝐿 2 and a substitution 𝜎 such that (𝐿 2 , 𝑀) ∈ Imp[𝐿 1 ], 𝐶 ∉ 𝑀, 𝐿 1 𝜎 = 𝐿, and 𝐿 2 𝜎 = 𝐿 ′ , we remove 𝐿 from 𝐶. Literal 𝐿 can also be removed if 𝐿 1 𝜎 = ¬𝐿 ′ and 𝐿 2 𝜎 = ¬𝐿. Rule HTR is implemented analogously.

The UnitHTR rule relies on maintaining the index Unit, which is built as follows. Whenever the prover derives a unit clause 𝐶 = {𝐿}, we find all entries 𝐿 a in Imp such that 𝐿 a and 𝐿 are unifiable with the most general unifier 𝜎. Then, we set

Unit ← Unit ∪ {(𝐿 c 𝜎, 𝑀 ∪ {𝐶}) | (𝐿 c , 𝑀) ∈ Imp[𝐿 a ]}.
Given a clause 𝐿 ∨ 𝐶 ′ we apply UnitHLE by looking for (𝐿 ′ , 𝑀) ∈ Unit such that 𝐿 ′ 𝜎 = ¬𝐿, for some substitution 𝜎; we apply UnitHTR by looking for 𝐿 ′ such that 𝐿 ′ 𝜎 = 𝐿. The sets stored together with literals in Unit are used for building the proof object and to remove literals from Unit once a clause from the given set becomes redundant.

The same data structure is used for supporting FLE and FLR. When (𝐿 ′ , 𝑀) is added to Imp[𝐿], we check whether (¬𝐿 ′ , 𝑀 ′ ) ∈ Imp[𝐿] for some 𝑀 ′ . If so, (¬𝐿, 𝑀 ∪ 𝑀 ′ ) is added to Unit.

In propositional logic, the conventional approach constructs the binary implication graph for the clause set 𝑁 [START_REF] Marijn | Efficient CNF Simplification Based on Binary Implication Graphs[END_REF], with edges (¬𝐿, 𝐿 ′ ) and (¬𝐿 ′ , 𝐿) whenever 𝐿 ∨ 𝐿 ′ ∈ 𝑁 . To avoid traversing the graph repeatedly, solvers rely on timestamps to discover connections between literals. This relies on syntactic literal comparisons, which is very fast in propositional logic but not in first-order logic, because of substitutions and congruence.

Predicate Elimination

To implement portfolio predicate elimination, we maintain a record for each predicate symbol p occurring in the problem with the following fields: set of definition clauses for p, set of nondefinition clauses in which p occurs once, and set of clauses in which p occurs more than once. These records are kept in a priority queue, prioritized by properties such as presence of definition sets and number of estimated resolutions. If p is the highest-priority symbol that is eligible for SPE or DPE, we eliminate it by removing all the clauses stored in p's record from the proof state and by adding flat resolvents to the passive set. Eliminating a symbol might make another symbol eligible.

As an optimization, predicate elimination keeps track only of symbols that appear at most 𝐾 occ times in the clause set. For inprocessing, we use signals that the prover emits whenever a clause is added to or removed from the proof state and update the records. At the beginning of the 1st, (𝐾 iter + 1)st, (2𝐾 iter + 1)st, . . . iteration of the given clause procedure's loop body, predicate elimination is systematically applied to the entire proof state. The first application of inprocessing amounts to preprocessing. By default, 𝐾 occ = 512 and 𝐾 iter = 10. The same ideas and limits apply for blocked clause elimination.

The most important novel aspect of our predicate elimination implementation is recognizing the definition clauses for a symbol p in a clause set 𝑁 . It is performed as follows:

(1) Let 𝐺 = {𝐶 | 𝐶 = (¬) p( ì 𝑥) ∨ 𝐶 ′ , 𝐶 ∈ 𝑁 , ì 𝑥 are distinct, and the variables of 𝐶 ′ are all among ì 𝑥 }. If 𝐺 is empty, report failure; otherwise, continue.

(2) Rename all clauses in 𝐺 so that their only variables are ì 𝑥.

(3) Let ⌊𝐴⌋ be an injective function that assigns a propositional variable to each atom 𝐴. This function is lifted to literals by assigning ⌊¬𝐴⌋ = ¬𝑥, if ⌊𝑎⌋ = 𝑥, and to clauses elementwise. Furthermore, let 𝐸 = {⌊𝐶 ′ ⌋ | (¬) p( ì 𝑥) ∨ 𝐶 ′ ∈ 𝐺 }. If 𝐸 is satisfiable, report failure. Otherwise, let 𝐸 ′ be an unsatisfiable core of 𝐸 and 𝐺 ′ be the set of corresponding first-order clauses, and continue.

(4) If all resolvents in 𝐺 ′ p ⋊ p 𝐺 ′ ¬ p are tautologies, then 𝐺 ′ is a definition set for symbol p. Otherwise, report failure.

The invalidity of set 𝐸 in step 3 is checked using a SAT solver, which is already integrated in Zipperposition. As modern theorem provers (including E and Vampire) also use SAT solvers, the method can easily be implemented.

During experimentation, we noticed that recognizing definitions of symbols that occur in the conjecture often harms performance. Thus, Zipperposition recognizes definitions only for the remaining symbols.

In contrast to SAT practice, we do not combine predicate elimination and subsumption when predicate elimination is used as preprocessing.

EVALUATION

We measure the impact of our elimination techniques for various values of their parameters. As a baseline, we use Zipperposition's first-order portfolio mode, which runs the prover in 13 configurations of heuristic parameters in consecutive time slices. None of these configurations use our new techniques. To evaluate a given parameter value, we fix it across all 13 configurations and compare the results with the baseline.

The benchmark set consists of all 13 495 CNF and FOF TPTP 7.3.0 theorems [START_REF] Sutcliffe | The TPTP Problem Library and Associated Infrastructure-From CNF to TH0, TPTP v6.4.0[END_REF]. The experiments were carried out on StarExec servers [START_REF] Stump | StarExec: A Cross-Community Infrastructure for Logic Solving[END_REF] equipped with Intel Xeon E5-2609 CPUs clocked at 2.40 GHz. The portfolio mode uses a single CPU core with a CPU time limit of 180 s. The base configuration solves 7897 problems. The values in the tables indicate the number of problems solved minus 7897. Thus, positive numbers indicate gains over the baseline. The best result is shown in bold.

Hidden-Literal-Based Elimination

The first experiments use all implemented HLBE rules. To avoid overburdening Zipperposition, we can enable an option to limit the number of tracked clauses for hidden literals. Once the limit has been reached, any request for tracking a clause will be rejected until a tracked clause is deleted. We can choose which kind of clauses are tracked: only clauses from the active set A, only clauses from the passive set P, or both. We also vary the maximal implication chain length 𝐾 len and the number of computed self-implications 𝐾 imp .

In Zipperposition, every lookup for instances or generalizations of 𝑠 ≈ 𝑡 must be done once for each orientation of the equation. To avoid this inefficiency, and also because the implementation of hidden literals does not fully exploit congruence, we can disable tracking clauses with at least one functional literal. Clauses containing functional literals can then still be simplified.

Figures 1 and2 show the results, without and with functional literal tracking enabled, for 𝐾 len = 2 and 𝐾 imp = 0. The columns specify different limits on the number of tracked clauses, with ∞ denoting that no limit is imposed. The rows represent different kinds of tracked clauses. The results suggest that tracking functional literals is not worth the effort but that tracking predicate literals is. The best improvement is observed when both active and passive clauses are tracked. Normally DISCOUNT-loop provers [START_REF] Avenhaus | DISCOUNT: A SYstem for Distributed Equational Deduction[END_REF] such as Zipperposition do not simplify active clauses using passive clauses, but here we see that this can be effective. Figure 3 shows the impact of varying 𝐾 len and 𝐾 imp , when 500 clauses from the entire proof state are tracked. These results suggest that computing long implication chains is counterproductive.

𝐾 imp = 0 +9 +10 +7 +5 𝐾 imp = 1 +5 +11 +7 +4 𝐾 imp = 2 +6 +11 +8 +8

Predicate and Blocked Clause Elimination

For defined predicate elimination, the number of resolvents grows exponentially with the number of occurrences of p. To avoid this expensive computation, we limit the applicability of PPE to proof states for which p is singular. According to our informal experiments, full PPE, without this restriction, generally performs less well. Predicate elimination can be done using Khasidashvili and Korovin's criterion (K&K) or using our relaxed criterion with different values of 𝐾 tol . Figure 4 shows the results for SPE and PPE used as preprocessors. Our numbers corroborate Khasidashvili and Korovin's findings: SPE with K&K proves 70 more problems than the base, a 0.9% increase, comparable to the 1.8% they observe when they combine SPE with additional preprocessing. Remarkably, the number of additional proved problems more than doubles when we use our criterion with 𝐾 tol > 0, for both SPE and PPE.

Although this is not evident in Figure 4, varying 𝐾 tol substantially changes the set of problems solved. For example, when 𝐾 tol = 0, SPE proves 60 theorems not proved using 𝐾 tol = 50. The effect weakens as 𝐾 tol grows. When 𝐾 tol = 100, SPE proves only 13 problems not found when 𝐾 tol = 200. Similarly, the set of problems proved by SPE and PPE differs: When 𝐾 tol = 25, 14 problems are Performing BCE and variable elimination until fixpoint increases the performance of SAT solvers [START_REF] Järvisalo | Blocked Clause Elimination[END_REF]. We can check whether the same holds for superposition provers. In this experiment, we use the relaxed criterion with 𝐾 tol = 25 and HLBE which tracks up to 500 clauses from any clause set, 𝐾 len = 2, and 𝐾 imp = 0. We use each technique as preprocessing and inprocessing.

The results are summarized in Figure 5, where the + sign denotes the combination of techniques. We confirm the results obtained by Kiesl et al. about the performance of BCE as preprocessing: It helps prove 30 more problems from our benchmark set, increasing the success rate by roughly 0.4%. The same percentage increase was obtained Kiesl et al. Using BCE as inprocessing, however, hurts performance, presumably because of its incompatibility with the redundancy criterion.

For preprocessing, the combinations SPE+BCE and PPE+BCE performed roughly on a par with SPE and PPE, respectively. This stands in contrast to the situation with SAT solvers, where such a combination usually helps. It is also worth noting that the inprocessing techniques never outperform their preprocessing counterparts. The last column shows that combining HLBE with other elimination techniques overburdens the prover.

Satisfiability by Blocked Clause Elimination

Kiesl et al. found that blocked clause elimination is especially effective on satisfiable problems. To corroborate their results and ascertain whether a combination of predicate elimination and blocked clause elimination increases the success rate, we evaluate BCE on all 2273 satisfiable or TPTP FOF and CNF problems. The hardware and CPU time limits are the same as in the experiments above. Figure 6 presents the results.

The baseline establishes the satisfiability of 856 problems. We consider only preprocessing techniques, since BCE compromises refutational completeness-a saturation does not guarantee that the original problem was satisfiable. We note that recognizing definition sets makes almost no difference on satisfiable problems. The sets of problems solved by BCE and PPE differ-30 problems are solved by BCE and not by PPE.

SAT-Inspired Eliminations for Superposition 1:23

DISCUSSION AND RELATED WORK

We briefly surveyed related work in Sect. 1. In this section, we give a more detail overview and further discuss connections with the related work.

The research presented in this article is two-pronged. For SAT elimination techniques already generalized to preprocess first-order problems, we looked for ways to interleave them with the given clause procedure of a superposition prover, as inprocessing. For techniques that had not yet been ported to first-order logic, we looked for generalizations that allow both preprocessing and inprocessing.

Hidden tautology elimination was first described by Heule et al. [START_REF] Marijn | Clause Elimination Procedures for CNF Formulas[END_REF]. Better implementation that also supports hidden literal elimination was later described by the same group of authors [START_REF] Marijn | Efficient CNF Simplification Based on Binary Implication Graphs[END_REF]. We generalized the underlying theoretical concepts to first-order logic, and provided an efficient way to deal with the infinite number of hidden literals that arise with this generalization. More efficient graph-based techniques are yet to be explored.

Variable elimination, based on Davis-Putnam resolution [START_REF] Davis | A Computing Procedure for Quantification Theory[END_REF], has been studied in the context of both propositional logic [START_REF] Chatalic | ZRES: The Old Davis-Putnam Procedure Meets ZBDD[END_REF][START_REF] Subbarayan | NiVER: Non-increasing Variable Elimination Resolution for Preprocessing SAT Instances[END_REF] and QBF [START_REF] Biere | Resolve and Expand[END_REF]. It was generalized to first-order logic (as a preprocessor) by Khasidashvili and Korovin [START_REF] Khasidashvili | Predicate Elimination for Preprocessing in First-Order Theorem Proving[END_REF] yielding a technique called predicate elimination. An improvement of variable elimination that uses formula definition information has been popularized as a preprocessing and inprocessing technique for CDCL solvers by Eén and Biere [START_REF] Eén | Effective Preprocessing in SAT Through Variable and Clause Elimination[END_REF]. We generalized this improvement to first-order logic and combined it with Khasidashvili and Korovin's approach. With reasonable restrictions, this extension can be used as an inprocessing technique. In SAT and QBF, it was observed that allowing variable elimination to slightly increase in the clause set size improves performance [START_REF] Biere | Blocked Clause Elimination for QBF[END_REF]. We implemented a similar approach, achieving the double the number of additional proofs found compared to more restrictive approaches.

Blocked clause elimination is used in both SAT [START_REF] Järvisalo | Blocked Clause Elimination[END_REF] and QBF solvers [START_REF] Biere | Blocked Clause Elimination for QBF[END_REF]. Its generalization to first-order logic [START_REF] Kiesl | Blocked Clauses in First-Order Logic[END_REF] has showed positive effects when used as a preprocessor. We showed that blocked clauses cannot be removed during saturation, but that they can be effectively used to show satisfiability of the clause set. A combination of blocked clause elimination and variable elimination performs well in propositional logic [START_REF] Järvisalo | Blocked Clause Elimination[END_REF], but we observed no comparable improvement when their generalizations are combined.

Our general approach is one of many ways to combine ideas from SAT solving and first-order proving. Other noteworthy architectures that either incorporate a SAT solver or that generalize the CDCL calculus include DPLL(𝑇 ) with quantifier instantiation [START_REF] Barbosa | Congruence Closure with Free Variables[END_REF][START_REF] Mendonça De Moura | Efficient E-Matching for SMT Solvers[END_REF][START_REF] Reynolds | Revisiting Enumerative Instantiation[END_REF], DPLL(Γ + 𝑇 ) [START_REF] Maria | On Deciding Satisfiability by DPLL(Γ + 𝑇 ) and Unsound Theorem Proving[END_REF], labeled splitting [START_REF] Fietzke | Labelled splitting[END_REF], AVATAR [START_REF] Voronkov | AVATAR: The Architecture for First-Order Theorem Provers[END_REF], MCSAT [START_REF] De | A Model-Constructing Satisfiability Calculus[END_REF], CDSAT [START_REF] Paola Bonacina | Satisfiability Modulo Theories and Assignments[END_REF], SGGS [START_REF] Schmidt | SGGS Theorem Proving: An Exposition[END_REF], and SCL [START_REF] Fiori | SCL Clause Learning from Simple Models[END_REF].

CONCLUSION

We adapted several preprocessing and inprocessing elimination techniques implemented in modern SAT solvers so that they work in a superposition prover. This involved lifting the techniques to first-order logic with equality but also tailoring them to work in tandem with superposition and its redundancy criterion. Although SAT solvers and superposition provers embody radically different philosophies, we found that the lifted SAT techniques provide valuable optimizations.

We see several avenues for future work. First, the implementation of hidden literals could be extended to exploit equality congruence. Second, although blocked clause elimination is generally incomplete as an inprocessing technique, we hope to achieve refutational completeness for a substantial fragment of it. Third, predicate and blocked clause elimination, which thrives on the absence of clauses from the proof state, could be enhanced by tagging and ignoring generated clauses that have not yet been used to subsume or simplify untagged clauses. Fourth, predicate and blocked clause elimination could be extended to work with functional literals. Fifth, more SAT techniques could be adapted, including bounded variable addition [START_REF] Manthey | Automated Reencoding of Boolean Formulas[END_REF] and blocked clause addition [START_REF] Kullmann | On a generalization of extended resolution[END_REF]. Sixth, the techniques we covered could be adapted to work with other first-order calculi, or generalized further to work with higher-order calculi such as combinatory superposition [START_REF] Bhayat | A Combinator-Based Superposition Calculus for Higher-Order Logic[END_REF] and 𝜆-superposition [START_REF] Bentkamp | Superposition with lambdas[END_REF].

Definition 3 . 4 .

 34 Given a literal 𝐿 and a clause set 𝑁 , the set of hidden literals for 𝐿 and 𝑁 is HL(𝐿, 𝑁 ) = {𝐿 ′ | 𝐿 ′ ↩→ * 𝐿} \ {𝐿}, where ↩→ is defined so that (1) ¬𝐿 ′ 𝜎 ↩→ 𝐿𝜎 if 𝐿 ′ ∨ 𝐿 ∈ 𝑁 and 𝜎 is a substitution; (2) 𝑠 ≈𝑡 ↩→ 𝑢 [𝑠] ≈𝑢 [𝑡] for all terms 𝑠, 𝑡 and contexts 𝑢 [ ]; and (3) 𝑢 [𝑠] 𝑢 [𝑡] ↩→ 𝑠 𝑡 for all terms 𝑠, 𝑡 and contexts 𝑢 [ ]. Moreover, HL(𝐿 1 ∨ • • • ∨ 𝐿 𝑛 , 𝑁 ) = 𝑛 𝑖=1 HL(𝐿 𝑖 , 𝑁 ).

Example 3 . 5 .

 35 Consider the clause set 𝑁 = {p(𝑥) ∨ ¬p(f (𝑥)), p(f (f(𝑥))) ∨ a ≈ b} and the clause 𝐶 = f(a) f(b) ∨ p(𝑥). The first clause in 𝑁 induces p(f(𝑥)) ↩→ p(𝑥), p(f(f(𝑥))) ↩→ p(f(𝑥)), and hence p(f(f (𝑥))) ↩→ * p(𝑥). Together with the second clause in 𝑁 , it can be used to derive a b ↩→ * p(𝑥). Finally, using rule (3) of Definition 3.4, we derive f(a) f (b) ↩→ * p(𝑥)-that is, f (a) f (b) ∈ HL(p(𝑥), 𝑁 ). This allows us to remove 𝐶's first literal using HLE. Two special cases of HLE exploit equality congruence as embodied by conditions (2) and (3) of Definition 3.4 without requiring to compute the HL set:

Example 3 . 6 .

 36 Consider the clause set 𝑁 = {p(𝑥) ∨ q(f (𝑥)), ¬q(f(a)) ∨ f (b) ≈ g(c), f(𝑥) g(𝑦)} and the clause 𝐶 = ¬p(a) ∨ ¬q(b). The first clause in 𝑁 induces ¬q(f (a)) ↩→ p(a), whereas the second one induces f(b) g(c) ↩→ ¬q(f(a)). Thus, we have f(b) g(c) ↩→ * p(a)-that is, f(b) f(c) ∈ HL(p(a), 𝑁 ). By applying the substitution {𝑥 ↦ → b, 𝑦 ↦ → c} to the third clause in 𝑁 , we can fulfill the conditions of UnitHLE and remove 𝐶's first literal.

  Case HLE: We have 𝑁 , 𝐿 ′ |= 𝐿 by the side condition and must show 𝑁 , 𝐿 ′ ∨ 𝐿 ∨ 𝐶 |= 𝐿 ∨ 𝐶. Let J |= 𝑁 , 𝐿 ′ ∨ 𝐿 ∨ 𝐶. If J |= 𝐿 ′ , then we also have J |= 𝐿 thanks to the side condition and hence J |= 𝐿 ∨ 𝐶. Otherwise, we have J |= 𝐿 ∨ 𝐶, which is exactly what we need to show. Case FLE: We have 𝑁 , 𝐿 |= 𝐿 ′ and 𝑁 , 𝐿 |= ¬𝐿 ′ by the side condition. If J |= 𝑁 , 𝐿, then both J |= 𝐿 ′ and J |= ¬𝐿 ′ , an absurdity. Otherwise, we have J |= 𝐶, as desired. Case CongHLE + , CongHLE -: Obvious by congruence of equality. Case UnitHLE: We have 𝑁 , 𝐿 |= ¬𝐿 ′ 𝜎 by the side condition. If J |= 𝑁 , 𝐿, then 𝑁 |= ¬𝐿 ′ 𝜎. But since 𝐿 ′ ∈ 𝑁 , this is an absurdity. Otherwise, we have J |= 𝐶, as desired. Case HTR: We have 𝑁 , ¬𝐿 ′ |= 𝐿 by the side condition. If either J |= 𝐿 or J |= 𝐿 ′ , the desired result follows directly. Otherwise, from J |= ¬𝐿 ′ we also have J |= 𝐿 thanks to the side condition, contradicting J |= ¬𝐿. Case FLR: We have 𝑁 , 𝐿 ′ |= 𝐿 and 𝑁 , ¬𝐿 ′ |= 𝐿 by the side condition. Hence 𝑁 |= 𝐿, as desired. Case UnitHTR: We have 𝑁 , 𝐿 ′ 𝜎 |= 𝐿. Since 𝐿 ′ ∈ 𝑁 , we have 𝑁 |= 𝐿, as desired. □

Definition 4 . 7 .

 47 Let 𝐺 be a clause set and p be a predicate symbol. The set 𝐺 is a definition set for p if (1) p is singular for 𝐺; (2) 𝐺 consists of clauses of the form (¬) p( ì 𝑥) ∨ 𝐶 ′ (up to variable renaming), where the variables ì 𝑥 are distinct; (3) the variables in 𝐶 ′ are all among p's arguments ì 𝑥; (4) all clauses in 𝐺 + p ⋊ p 𝐺 - p are tautologies; and (5) 𝐸 (ì c) is unsatisfiable, where the environment 𝐸 ( ì 𝑥) consists of all subclauses 𝐶 ′ of any (¬) p( ì 𝑥) ∨𝐶 ′ ∈ 𝐺 and ì c is a tuple of distinct fresh constants substituted in for ì 𝑥.

Example 4 . 15 .

 415 The counterexample below is based on the given clause prover GC from the saturation framework. It shows how predicate elimination can break GC's key invariant, which states that all inferences between active clauses are redundant. Breaking the invariant means that the limit might be unsaturated, breaking the refutational completeness proof.We use superposition with the order a ≺ b ≺ c ≺ d and without selection. Assume a ∈ P and suppose we start with the satisfiable clause set ¬a ∨ d ¬a ∨ ¬d a ∨ b ∨ c c ∨ d b ∨ ¬d where gray boxes mark maximal literals. Suppose the prover makes c ∨ d and b ∨ ¬d active. From these two clauses, a superposition inference 𝜄 could derive the conclusion b ∨ c. However, the three passive clauses are ≺-smaller than 𝜄's main premise b ∨ ¬d and collectively entail 𝜄's conclusion. This means that 𝜄 is redundant and can be ignored. If the prover now eliminates the predicate a using SPE, the passive set is reduced to {b ∨ c ∨ d, b ∨ c ∨ ¬d}. Either clause is subsumed by an active clause, so the prover deletes it. It stops with the active set {c ∨ d, b ∨ ¬d}, which is unsaturated because 𝜄 is no longer redundant. The invariant is broken.

Lemma 4 . 19 .

 419 Every =⇒ GCP -derivation is a mixed derivation. Proof. The cases for Process and Infer are almost as in Waldmann et al., with adjustments to show that P-predicates cannot appear from nowhere. The case for ElimPred is trivial. □ Let Inv ♭ N (𝑘) denote the condition FLInf (N 𝑘 ↓ active ) ⊆ LRed ♭ I (N 𝑘 ). Notice the difference with the definition of the key invariant Inv N in the saturation framework, whose right-hand side is 𝑘 𝑖=0 Red L I (N 𝑖 ). We cannot use the big union starting at 𝑖 = 0 because we will need to truncate a sequence prefix of an a priori unknown length. The argument will still work thanks to monotonicity properties of redundancy criteria. Lemma 4.20. Let (N 𝑖 ) 𝑖 be a =⇒ GCP -derivation. If N 0 ↓ active = ∅, then Inv ♭ N (𝑘) holds for all indices 𝑘.

Definition 5 . 1 .

 51 Let 𝐶 = 𝐿 ∨ 𝐶 ′ and 𝐷 = 𝐿 1 ∨ • • • ∨ 𝐿 𝑚 ∨ 𝐷 ′ , where (1) 𝑚 ≥ 1, (2) the literals 𝐿 𝑖 are of opposite polarity to 𝐿, (3) 𝐿's atom is p(ì 𝑠 𝑛 ), (4) 𝐿 𝑖 's atom is p( ì 𝑡 𝑖 ) for each 𝑖, and (5) 𝐶 and 𝐷 have no variables in common. The clause 𝑚 𝑖=1 𝑛 𝑗=1 𝑠 𝑗 𝑡 𝑖 𝑗 ∨ 𝐶 ′ ∨ 𝐷 ′ is a flat 𝐿-resolvent of 𝐶 and 𝐷.Definition 5.2. Let 𝐶 = 𝐿 ∨ 𝐶 ′ be a clause and 𝑁 be a clause set. Let 𝑁 ′ consist of all clauses from 𝑁 \ {𝐶} with their variables renamed so that they share no variables with 𝐶. The clause 𝐶 is (equality-)blocked by 𝐿 in the set 𝑁 if all flat 𝐿-resolvents between 𝐶 and clauses in 𝑁 ′ are tautologies.

45 Fig. 1 .Fig. 2 .

 4512 Fig. 1. Impact of the number and kinds of tracked clauses on HLBE performance, when only predicate literals are tracked

Fig. 3 .Fig. 4 .

 34 Fig. 3. Impact of the parameters 𝐾 len and 𝐾 imp on HLBE performance

  a tautology, hidden tautology elimination (HTE) replaces 𝑁 by 𝑁 \ {𝐶}. Theorem 3.3. The result of applying HLE or HTE to a clause set 𝑁 is equivalent to 𝑁 . Proof. For HLE, assume we have a model of 𝑁 and 𝐿 ′ ∨ 𝐿 ∨ 𝐶 that does not satisfy 𝐿 ∨ 𝐶. Then the model must satisfy 𝐿 ′ , but since 𝑁 implies ¬𝐿 ′ ∨ 𝐿, it must also satisfy 𝐿 ∨ 𝐶, a contradiction. For HTE, it can be shown that the sets 𝑁 and 𝑁 ∪ {𝐶 ′ } \ {𝐶} are equivalent [28, Sect. 2.1]. Since the clause 𝐶 ′ is a tautology, 𝑁 and 𝑁 \ {𝐶} are equivalent. □

  Definition 4.5. Let 𝑁 be a clause set and p be a singular predicate for 𝑁 . Let 𝑁 + p consist of all clauses of the form p(ì 𝑠) ∨ 𝐶 ′ ∈ 𝑁 , let 𝑁 - p consist of all clauses of the form ¬p(ì 𝑠) ∨ 𝐶 ′ ∈ 𝑁 , let 𝑁 p = 𝑁 + p ∪ 𝑁 - p , and let 𝑁 p = 𝑁 \ 𝑁 p . Definition 4.6. Let 𝑁 be a clause set and p be a singular predicate for 𝑁 . Singular predicate elimination (SPE) of p in 𝑁 replaces 𝑁 by 𝑁 p ∪ (𝑁 +

	p

where 𝑁 ′ 1 and 𝑁 ′ 2 are sets of corresponding resolvents. Both steps can be joined (up to variable renaming) to (𝑀, 𝑁 ′ 1 ∪ 𝑁 ′ 2 ∪ 𝑁 ′ ), showing that is locally confluent. □ Next, it is useful to partition clause sets into subsets based on the presence and polarity of a singular predicate.

  Definition 4.9. Let 𝑁 be a clause set, p be a predicate symbol, 𝐺 ⊆ 𝑁 be a definition set for p, and 𝑅 = 𝑁 p \ 𝐺. Defined predicate elimination (DPE) of p in 𝑁 replaces 𝑁 by 𝑁 p ∪ (𝐺 ⋊ p 𝑅). Let 𝑁 ( ì 𝑥) be a clause set such that the variables of all clauses in it are among the argument 𝑛-tuple ì 𝑥, and let ì c be an 𝑛-tuple of distinct fresh constants. If 𝑁 (ì c) (i.e., 𝑁 ( ì 𝑥){ ì 𝑥 ↦ → ì c}) is unsatisfiable, then for every interpretation J and valuation 𝜉, J ̸ |= 𝜉 𝑁 .

	Lemma 4.10.

  Now consider the flat resolvent of 𝐶 and 𝐷 on p:𝑅 = 𝑥 1 𝑠 1 ∨ • • • ∨ 𝑥 𝑛 𝑠 𝑛 ∨ 𝐶 ′ ∨ 𝐷 ′ .Let 𝜁 be a valuation coinciding with 𝜉 on variables of 𝐶 and with 𝜉 ′ on ì 𝑥 Then 𝐺 ∪ 𝑁 is satisfiable if and only if 𝑁 is satisfiable.Proof. The nontrivial direction is to show that if 𝑁 is satisfiable, 𝐺 ∪ 𝑁 is as well. Let J be a model of 𝑁 . We construct a model J ′ of 𝐺 over the same universe as J. For any atom 𝐴 such that p does not occur in 𝐴 and for every 𝜉, we set J ′ |= 𝜉 𝐴 if and only if J |= 𝜉 𝐴. For any clause p( ì 𝑥 𝑛 ) ∨ 𝐶 ′ ∈ 𝐺 and any assignment 𝜉 such that J ̸ |= 𝜉 𝐶 ′ , we define J ′ so that J ′ |= 𝜉 p( ì 𝑥 𝑛 ). By construction, J ′ |= 𝐺 + p ∪ 𝑁 . It remains to show that J ′ |= 𝐺 -. Let 𝐶 = ¬p( ì 𝑥 𝑛 ) ∨ 𝐶 ′ ∈ 𝐺 and let 𝜉 be an arbitrary assignment. Toward a contradiction, assume J ′ ̸ |= 𝜉 𝐶, and consequently J ′ |= 𝜉 p( ì 𝑥 𝑛 ). By construction of J

Then, J ̸ |= 𝜉 p(ì 𝑠 𝑛 ). Consider an arbitrary clause 𝐷 = p( ì 𝑥 𝑛 ) ∨ 𝐷 ′ ∈ 𝐺 + p and a valuation 𝜉 ′ that assigns each 𝑥 𝑖 the interpretation of 𝑠 𝑖 under J and 𝜉. As J ̸ |= 𝜉 ′ p( ì 𝑥 𝑛 ) and J |= 𝐺, then J |= 𝜉 ′ 𝐷 ′ for every such clause 𝐷. However, by part (5) of Definition 4.7 and by Lemma 4.10, J ̸ |= 𝜉 ′ 𝐸 ( ì 𝑥 𝑛 ), where 𝐸 ( ì 𝑥 𝑛 ) is the environment associated with the definition set 𝐺. Therefore, there must exist a clause 𝐷 = ¬p( ì 𝑥 𝑛 ) ∨ 𝐷 ′ in 𝐺 - p such that J ̸ |= 𝜉 𝐷 ′ . 𝑛 . Clearly, J ̸ |= 𝜁 𝑅. Yet, 𝑅 ∈ 𝑁 ′ , and as J |= 𝑁 ′ , we reach a contradiction. □ Lemma 4.12. Let 𝐺 be a definition set for p and 𝑁 be a clause set with no occurrences of p. ′ , there exists a clause p( ì 𝑦 𝑛 ) ∨ 𝐷 ′ ∈ 𝐺 and an assignment 𝜉 ′ that assigns each 𝑦 𝑖 value of 𝜉 (𝑥 𝑖

  Theorem 4.13. The result of applying DPE to a clause set 𝑁 is satisfiable if and only if 𝑁 is satisfiable. Proof. Let p be a predicate symbol and 𝐺 ⊆ 𝑁 be the definition set used by DPE, and let 𝑅 = 𝑁 p \ 𝐺. Using Lemma 4.4, we get that there is a derivation (𝐺, 𝑅) 𝑛 (𝐺, 𝑅 ′ ) 𝑅 ′ . Applying Lemma 4.11 𝑛 times, we get that 𝐺 ∪ 𝑅 is equivalent to 𝐺 ∪ 𝑅 ′ . Finally, Lemma 4.12 gives us the desired result. □ Since there will typically be at most only a few defined predicates in the problem, it makes sense to fall back on SPE when no definition is found. Definition 4.14. Let 𝑁 be a clause set and p be a predicate symbol. If there exists a definition set 𝐺 ⊆ 𝑁 for p, portfolio predicate elimination (PPE) on p in 𝑁 replaces 𝑁 with 𝑁 p ∪(𝐺⋊ p 𝑅), where 𝑅 = 𝑁 p \𝐺. Otherwise, if p is singular in 𝑁 , it results in 𝑁 p ∪ (𝑁 +

a tautology, according to condition (4) of Definition 4.7. However, for a valuation that behaves like 𝜉 on ì 𝑥 and 𝜉 ′ on ì 𝑦, J ′ does not satisfy 𝑅 ∈ 𝑁 , contradicting our assumption. □ p ⋊ p 𝑁 -

  Since Inv N (𝑘) holds, 𝜄 ∈ LRed ♭ I (N 𝑘 ). Hence, 𝜄 ∈ 𝑖 LRed ♭ I (N 𝑖 ). □ Lemma 4.22. Let (N 𝑖 ) 𝑖 be a =⇒ GCP -derivation. If N 0 ↓ active = ∅ and N ∞ ↓ 𝑙 = ∅ for every label 𝑙 ≠ active, then there exists an index 𝑘 such that (N 𝑘+𝑖 ) 𝑖 is a fair ▷ LRed ♭,⊐ -derivation. Proof. By Lemma 4.19, there must exist an index 𝑘 such that the sequence (N 𝑘+𝑖 ) 𝑖 is a pure ▷ LRed ♭,⊐ -derivation. By Lemma 4.20, Inv ♭

N (𝑘 + 𝑖) holds for all indices 𝑖. Hence, by Lemma 4.21, FLInf (N ∞ ↓ active ) ⊆ 𝑖 LRed ♭ I (N 𝑘+𝑖 ). By the second hypothesis, this inclusion simplifies to FLInf (N ∞ ) ⊆ 𝑖 LRed ♭ I (N 𝑘+𝑖 ). □ Theorem 4.23. Let (N 𝑖

ACM Trans. Comput. Logic, Vol. 1, No. 1, Article 1. Publication date: January 2022.

https://doi.org/10.5281/zenodo.4552499

ACM Trans. Comput. Logic, Vol. 1, No. 1, Article 1. Publication date: January 2022. SAT-Inspired Eliminations for Superposition 1:11

ACKNOWLEDGMENTS

We are grateful to the maintainers of StarExec for letting us use their service. Uwe Waldmann participated in the search for a counterexample to completeness of BCE as inprocessing and confirmed that Example 5.4 is correct. He also suggested major simplifications and helped us debug the proofs of the claims about predicate elimination. Anne Baanen helped us define the nonclassical logic used to disallow splitting. Ahmed Bhayat, Armin Biere, Mathias Fleury, Wan Fokkink, Benjamin Kiesl, and the anonymous reviewers made some useful comments on our manuscript, and Mark Summerfield suggested many textual improvements. We thank them all.

Vukmirović and Blanchette's research has received funding from the European Research Council (ERC) under the European Union's Horizon 2020 research and innovation program (grant agreement No. 713999, Matryoshka). Blanchette's research has also received funding from the Netherlands Organization for Scientific Research (NWO) under the Vidi program (project No. 016.Vidi.189.037, Lean Forward). Heule is supported by the National Science Foundation (NSF) under grant CCF-2015445.

5

𝐿𝜎 = 𝐿 a , and 𝐿 ′ 𝜎 = 𝐿 c then for all (𝜎, 𝑀) such that (𝐿 c 𝜎, 𝑀) ∈ Imp[𝐿 a 𝜎] do erase all (𝐿 ′ , 𝑀 ′ ) such that 𝑀 ⊆ 𝑀 ′ from Imp[𝐿 a 𝜎] for all 𝐿 such that (𝐿 ′ , 𝑀) ∈ Imp [𝐿] and 𝐿 a 𝜎 = 𝐿 ′ for some 𝜎 do


Takeshi Saga

Hiroki Tanaka

Catherine Achard

Satoshi Nakamura

Catherine 2023 Pelachaud

Jieyeon Woo

Alexis Gerard

An Adaptive Virtual Agent Platform for Automated Social Skills Training

Keywords: CCS Concepts:, Human-centered computing → Interactive systems and tools;, Computer systems organization → Real-time system architecture virtual agent, adaptation, social skills training

. System setup of the proposed system. The system runs the user-capturing toolkits, behavior generation model, Greta, and SST evaluation.

Interlocutors adapt their verbal and nonverbal behaviors as signs of engagement during face-to-face interaction. We aim to build engaging Socially Interactive Agents, SIAs, that can adapt their behaviors during interaction. With an adaptive behavior generation model, we drive SIAs' upper face and head movements in real-time. We evaluate this platform through a scenario for Social Skills Training, SST.

INTRODUCTION

People use verbal and nonverbal behaviors to communicate with others. They adapt their behaviors to the other interlocutors to indicate their engagement in the conversation. This adaptation ability, which strengthens the bond between interlocutors, is important in human-agent interaction. In this demonstration, we propose a virtual agent system with adaptive real-time behavior generation for upper face and head movements, which can provide face-to-face multimodal interaction 1 . As an example of an application system, we show automatic social skills training using the system. Social skills training (SST) is a validated rehabilitation program used in psychiatric hospitals or job training center [START_REF] Bellack | Social Skills Training for Schizophrenia: A Step-by-Step Guide[END_REF]. It is geared toward persons suffering stress related to social anxiety. According to Bellack's definition, there are four basic social skills to be acquired to manage everyday activities: paying attention to an interlocutor's speech (LISTEN), conveying positive feelings (TELL), requesting something from an interlocutor (ASK), and refusing a request (DECLINE). SST involves offering these persons to act out scenarios related to these situations. We propose a virtual agent system for SST, which generates real-time adaptive behavior and renders SST evaluation and feedback.

SYSTEM SETUP

Figure 1 shows our system setup. A human participant sits in front of a screen displaying a close-up of a virtual agent (mainly its head and face). For behavior generation, the system captures the user's voice with a microphone and the user's face (head movement, gaze, and facial expressions) with a 1080p RGB webcam. We also use a speakerphone, a device that serves as both speaker and microphone, for the user's speech recognition and the agent's speech synthesis. To record the interaction, we use a microphone-embedded webcam with 1080p resolution. Two computers, with 2.4GHz Intel Core i9 mounted with NVIDIA Quadro RTX 4000 and 64GB RAM, are used to run the system. The first computer runs the Greta platform [START_REF] Niewiadomski | Greta: an interactive expressive ECA system[END_REF], an open-source virtual agent platform with an embodied conversational agent which can communicate verbally and nonverbally in real-time. The speech of the agent is rendered using the CereProc speech synthesizer. The second computer runs the ASAP model [START_REF] Woo | ASAP: Endowing Adaptation Capability to Agent in Human-Agent Interaction[END_REF] generating adaptive agent's behavior in real-time, along with the user capturing toolkits of OpenFace (facial feature extraction) and openSMILE (prosodic feature extraction). We also implement the SST evaluation system on the first computer, which uses OpenFace, OpenPose (body points extraction), Praat (prosodic feature extraction) for feature extractions (for more details, see [START_REF] Saga | Automatic evaluation-feedback system for automated social skills training[END_REF]). The computers communicate with each other via the OSC (Open Sound Control) communication protocol.

The behavior generation performs in real-time for a single synchronized system loop (acoustic and visual features extraction, and behavior generation) within the 0.04𝑠𝑒𝑐 (time of a frame). Approximately 7𝐺𝐵 RAM is required to run the system.

REAL-TIME ADAPTIVE BEHAVIOR GENERATION

To increase the user's engagement, real-time adaptive agent behavior is generated with the ASAP model [START_REF] Woo | ASAP: Endowing Adaptation Capability to Agent in Human-Agent Interaction[END_REF] by constantly adapting to the user's behaviors. It models the interpersonal relationship of multimodal signals with the self-attention pruning technique to give the agent the reciprocal adaptation capability. It receives previous visual (eye movements, head rotations, six upper face Action Units (AUs) [START_REF] Ekman | Measuring facial movement[END_REF] of AU1, AU2, AU4, AU5, AU6, and AU7, and that of the smile AU12) and audio (fundamental frequency, loudness, voicing probability, and 13 Mel-frequency Cepstral Coefficient (MFCC)) features as input. We used features extracted with OpenFace and openSMILE from both the human user and the agent. The ASAP model generates synchronized agent's adaptive behaviors (outputting facial AUs and head/gaze movements) for every frame (at each time-step) at 25𝑓 𝑝𝑠.

INTERACTION MANAGEMENT

The system controls dialogue turns with a rule-based management mechanism, which enables smooth turn-taking. The system recognizes the ending of the user's speech by detecting the silence through a speech recognition module. The user's utterance is not taken into account for the dialogue management during the agent's speech.

The dialogue is managed by the Flipper [START_REF] Jelte Van Waterschoot | Flipper 2.0: A pragmatic dialogue engine for embodied conversational agents[END_REF] engine. The user's utterance text obtained by Google ASR2 is passed to Flipper via ActiveMQ. The system selects predefined response utterances depending on keywords extracted from the user's utterance. The agent's adaptive behavior is generated with the ASAP model [START_REF] Woo | ASAP: Endowing Adaptation Capability to Agent in Human-Agent Interaction[END_REF] while Greta's internal behavior realizer module computes the agent's lip movement.

APPLICATION: SOCIAL SKILLS TRAINING SYSTEM

A basic human-human SST starts with ice breaking and briefly introduces the SST goal corresponding to each training target skill to maximize the training effect. Then, the participant acts in role-play situations with the trainer. After that, the trainer gives feedback on the role-play toward further improvement. They may repeat the role-play feedback loop several times for better training effects. We replace this process with a fully-automated system.

Each session ends with evaluation feedback. It is based on Saga's system [START_REF] Saga | Automatic evaluation-feedback system for automated social skills training[END_REF], comprised of evaluation and feedback modules with small modifications. The evaluation module estimates component scores ranging from one to five on the following three aspects: eye contact, facial expression, and vocal variation. For the estimation, we used random forest models based on multimodal features (average voice intensity, F0 frequency, smile, head poses, nodding, facial action units, and gestures. See [START_REF] Saga | Automatic evaluation-feedback system for automated social skills training[END_REF] for more details). The feedback module selects a set of pre-defined sentences to reflect users' nonverbal behaviors during the interaction.

CONCLUSION

We propose a virtual agent system that can interact with human users in real-time. The agent adapts its behavior to that of the user. We demonstrated the flexible integration ability of our system by showcasing its use with the SST scenario.

Demo video link: https://youtu.be/O_i1PrnV-_o

https://cloud.google.com/speech-to-text

ACKNOWLEDGMENTS

Funding was provided by the JST Core Research for Evolutionary Science and Technology, the Agence Nationale de la Recherche (ANR-JST CREST, TAPAS project, Grant No. JPMJCR19A5 for JST-CREST, ANR-19-JSTS-0001 for ANR).