Simon Cruanes

Superposition with Structural Induction

. Lemmas obtained by generalization or theory exploration can be introduced during search, used, and proved, all in the same search space. We describe an implementation and present some promising results.

Introduction

Superposition-based theorem provers and SMT (Satisfiability Modulo Theory) solvers have considerably improved automation in some proof assistants thanks to hammers [START_REF] Paulson | Three years of experience with Sledgehammer, a practical link between automatic and interactive theorem provers[END_REF][START_REF] Kaliszyk | Learning-assisted automated reasoning with Flyspeck[END_REF]. However, because these proof assistants provide inductive datatypes, many theorems are out of reach of the automated provers, which are not able to perform inductive reasoning. Such theorems include basic properties of Peano arithmetic, reasoning about data structures such as lists and trees, manipulating syntax trees (which are often represented as a recursive datatype), etc.

Most state of the art theorem provers for first-order logic with equality are based on superposition [START_REF] Schulz | E -a brainiac theorem prover[END_REF][START_REF] Riazanov | Vampire 1.1 (system description)[END_REF][START_REF] Weidenbach | System Description: SPASS Version 3.0[END_REF][START_REF] Bachmair | On Restrictions of Ordered Paramodulation with Simplification[END_REF]. However, they often lack support for types or (inductive) datatypes. Vampire [START_REF] Riazanov | Vampire 1.1 (system description)[END_REF] has recently gained some support for datatypes [START_REF] Kovács | Coming to terms with quantified reasoning[END_REF] but does not perform induction yet.

Automatic inductive provers do exist [START_REF] Kaufmann | ACL2: An industrial strength version of Nqthm[END_REF][START_REF] Biundo | The Karlsruhe induction theorem proving system[END_REF][START_REF] Stratulat | A unified view of induction reasoning for first-order logic[END_REF] but they are usually not complete (nor very efficient) on the classical first-order logic problems hammers rely on. INKA [START_REF] Biundo | The Karlsruhe induction theorem proving system[END_REF] was based on resolution, but not superposition. A recent extension to CVC4 [START_REF] Reynolds | Induction for SMT solvers[END_REF] equips it with inductive reasoning, but so far no major superpositionbased theorem prover has inductive capabilities. Kersani and Peltier modified Prover9 to handle induction [START_REF] Kersani | Combining superposition and induction: A practical realization[END_REF], but only for natural numbers; it is unclear how their technique could be extended to arbitrary datatypes. Otter-λ [START_REF] Beeson | Otter-lambda, a Theorem-prover with Untyped Lambda-unification[END_REF] can use its (incomplete) higher-order unification algorithm to apply explicitly the induction principle, but it does not try to introduce any lemma nor does it handle defined functions or datatypes efficiently. Another superposition prover able to prove some inductive properties is Pirate [15, unpublished], but in its architecture each inductive property is solved in a separate saturation loop; it resembles more an inductive prover that would use a superposition prover for discharging subgoals.

In this work we propose a new architecture that permits a seamless integration of multiple induction attempts into the deduction process of a superposition prover. All the proof attempts are performed in the same saturation loop [START_REF] Schulz | E -a brainiac theorem prover[END_REF]. This has several advantages. First, if the problem does not actually need induction, a regular first-order proof can be obtained as usual. Second, once a particular inductive goal has been proved, it is considered as a normal first-order formula. This means it can participate in all the usual inference and simplification rules and contribute to the rest of the proof. Third, efforts are allocated to the various inductive proof attempts using the same clause selection heuristics that drive the first-order prover. This means the same elaborate heuristics can be reused for inductive proofs.

Our approach relies on a variant of superposition with polymorphic types, recursive functions, and inductive datatypes, as well as support for AVATAR [START_REF] Voronkov | AVATAR: the architecture for first-order theorem provers[END_REF] for reasoning by case (Sect. 3). Regular splitting without backtracking [START_REF] Riazanov | Splitting Without Backtracking[END_REF] could be used instead of AVATAR, but is less convenient and efficient. This richer variant of superposition treats defined functions efficiently. The prover can handle problems expressed in TIP [START_REF] Claessen | TIP: Tons of Inductive Problems[END_REF] ("Thousands of Inductive Problems"). It encodes the non-first-order constructs of TIP, such as pattern matching, during a preprocessing step.

On top of this extension of superposition, we introduce a new rule to instantiate the structural induction schema and prove a property by induction (Sect. 4). Pursuing several inductive goals simultaneously is made possibly by introducing a cut rule on top of AVATAR (Sect. 5). The properties to prove by induction come from several sources: the input goal, explicit lemmas requested by the user, or subgoals needed in already ongoing proofs (Sect. 6). The numerous heuristics for guessing relevant lemmas that have been developed for decades [START_REF] Kaufmann | ACL2: An industrial strength version of Nqthm[END_REF][START_REF] Bundy | Rippling: A heuristic for guiding inductive proofs[END_REF][START_REF] Boyer | A Computational Logic Handbook[END_REF][START_REF] Kapur | Lemma discovery in automating induction[END_REF][START_REF] Aubin | Strategies for mechanizing structural induction[END_REF] can be adapted to our framework. We also present a simple way to filter out invalid potential lemmas (Sect. 7).

To show the practical feasibility of the approach, we implemented the extensions of superposition and the inductive reasoning rules in Zipperposition, a modular prover (Sect. 8). Comparisons with CVC4 on the TIP benchmarks show that the implementation is reasonably competitive, and suggest that an implementation in E or Vampire could lead to excellent results.

Basic Definitions

We define some notions and notations that will be useful for the rest of the paper. An atomic type is a type constructor applied to 0 or more atomic types. A (polymorphic) type has the form Πα 1 . . . α n . (τ 1 , . . . , τ k ) → τ where the α i 's are type variables and each τ i is an atomic type. By s, t, u, v we denote terms, generated from variables x, y, z and function symbols f, g, h. By t we denote a finite (possibly empty) sequence of terms. A term is ground if it contains no variable. Given a term t and a position p, we write t| p for the subterm of t at p. We write t u if t is a (strict) subterm of u, i.e. if there is a non-empty position p such that t = u| p . A substitution is a mapping σ from variables to terms such that the set of variables dom(σ) def = {x | x = xσ} is finite. We always implicitly restrict ourselves to well-typed terms, substitutions, etc.

A literal is an equation s t or disequation s t. Note that is a logical symbol, whereas = denotes syntactic equality. A proposition p is implicitly represented by p . A clause is a disjunction of literals, denoted by C or D. The empty clause is the empty disjunction, equivalent to ⊥ (false). We sometimes view clauses as multisets of literals. Ground literals and clauses are defined in the obvious way.

We reuse some concepts from AVATAR [START_REF] Voronkov | AVATAR: the architecture for first-order theorem provers[END_REF]. A boolean mapping • is an injective mapping from clauses (and more generally, in our case, of formulas) into the propositional literals of a SAT solver. A clause with assertion, or Aclause, is a pair of a clause C and conjunction of boolean literals Γ , called the trail, and noted C ← Γ . It holds in an interpretation if either C holds, or Γ does not hold. We write for boolean conjunction and ⊕ for exclusive disjunction.

An inductive (data)type is defined by a set of constructors, at least one of which is non-recursive -we ignore mutually recursive datatypes, which can be encoded into a single datatype. A term t is purely inductive if every subterm of t whose type is inductive, has the form c(t We seek to establish the satisfiability of formulas in standard models. To achieve this, we will instantiate the induction schema over the inductive types. The induction schema for an inductive type τ is a second order formula parameterized by a variable P : τ → bool, but we instantiate it into a first-order formula that will be (dis)proved by superposition.

Example 1 (Natural Numbers). The type of natural numbers, nat, is a classic inductive type whose constructors are {0, s}. Its inductive values are all the natural numbers {0, s(0), . . . , s k (0), . . .}. The induction schema is ∀P : nat → bool. P (0) ∧ (∀n : nat. P (n) ⇒ P (s(n))) ⇒ ∀n. P (n).

Example 2 (Lists). The type of polymorphic lists is list(α). Its constructors are [ ] and (::) : α × list(α) → list(α). The purely inductive values of type list(τ ) are finite lists of purely inductive values of type τ . The induction schema on lists is ∀α. ∀P : list(α) → bool. P ([ ]) ∧ (∀x : α l : list(α). P (l) ⇒ P (x :: l)) ⇒ ∀l. P (l)

Superposition with Recursive Functions and Datatypes

Before considering induction, we need the theorem prover to be able to handle problems that contain defined functions and datatypes. In addition, input prob-lems can contain constructs that are outside of the realm of first-order terms, such as pattern matching and boolean conditionals ("if-then-else"). The solution we propose is multifold: (i) add some additional inference rules and simplification rules for datatypes; (ii) a notion of rewriting that does not rely on the term ordering; this is used to properly encode recursive functions; (iii) a preprocessing algorithm that removes non-first-order constructs by introducing newly defined functions and use them to encode the terms.

We adopt the notations and inference system of superposition from E [START_REF] Schulz | E -a brainiac theorem prover[END_REF] and AVATAR [START_REF] Voronkov | AVATAR: the architecture for first-order theorem provers[END_REF], and recall the following notions: an inference rule (noted with a single bar) infers the bottom clause(s) from the top clause(s); a simplification rule (with a double bar) replaces the top clause(s) with the bottom ones.

Recursive Functions and Rewriting

Superposition relies on a term ordering for orienting equations. This usually works well for first-order logic. However, recursive functions (on datatypes) are difficult to orient properly with such term orderings. Often, a rule ∀x. f (t) u defining f will be oriented right-to-left because u will contain several occurrences of variables, be heavier (in KBO), etc. whereas we would like it to be oriented in the more natural left-to-right direction.

To unfold recursive functions efficiently, we translate them into rewrite rules. By construction, the left-hand side of the rewrite rules that define f is of the form f (t 1 , . . . , t n ) where the t i are generated from variables and constructors. Rules are also non-overlapping, ensuring that the resulting rewrite system is confluent: at most one rule will apply to any tuple of arguments. Rewriting is done left-to-right, regardless of the term ordering. This strategy is not complete in general,1 but it guarantees that unfolding a function definition acts as an efficient simplification step. Recursive predicates are defined analogously, using rules of the form l C i (rewriting a positive literal into a set of clauses) and ¬l i C i (rewriting a negative literal into a set of clauses). This sort of rewriting is known as deduction modulo [START_REF] Dowek | Theorem Proving Modulo[END_REF] and, in our context, can be expressed as polarized resolution [START_REF] Burel | Embedding Deduction Modulo into a Prover[END_REF].

Having a well-delimited set of rules that define a function also enables the notion of argument position, defined below. This notion is useful because it provides some insight on which arguments influence the control flow of the function, and which ones are just carried around passively or serve as accumulators. In particular, it is pointless to try to perform induction on a passive argument, because the constructors at such positions cannot be eliminated.

Definition 1 (Argument Positions). Given a function f with k arguments, defined by rules

f (t 1,1 , . . . , t 1,k ) u 1 , . . . , f (t n,1 , . . . , t n,k ) u n
we say that each i, for 1 ≤ i ≤ k, is an argument position of f . An argument position i is passive if every occurrence of f in (u j ) n j=1 has t i,j as i th argument; in other words, if f always calls itself with the same i th argument. A non-passive argument position i is an accumulator if every (t i,j ) n j=1 is a variable; it is primary otherwise. Intuitively, a primary position is one that the function might examine for determining whether to recurse or not. x, qrev(x :: y, z) qrev(y, x :: z): the first position is primary, the second is an accumulator.

Preprocessing the Input

Our prover can parse problems expressed in TIP [START_REF] Claessen | TIP: Tons of Inductive Problems[END_REF], an extension of SMT-LIB [START_REF] Barrett | The Satisfiability Modulo Theories Library (SMT-LIB)[END_REF] with recursive functions, polymorphism, and datatypes. However, many constructs in this language have no straightforward equivalent in a superposition prover, in which there are only clauses and first-order terms. These constructs are pattern matching, conditionals ("if-then-else"), lambda abstractions, and let-bindings; let-bindings are expanded, conditionals and pattern matches are either named, or become toplevel case distinction as a set of rewrite rules. Again, the rewrite rules generated by our encoding are terminating and confluent; they are also orthogonal to the other rewrite rules because their head symbol is a fresh constant. We show a few examples of encodings in Figure 1.

Inference Rules for Constructors

We consider the algebra of freely generated datatypes, such as Peano numbers, lists, or binary trees. This fragment is general enough to express many classic types and data structures, yet it is reasonably simple. Other theories such as rational arithmetic can also be used (e.g. using Hierarchic superposition [START_REF] Baumgartner | Hierarchic superposition with weak abstraction[END_REF]) but no induction will be performed on variables of these types.

Even without considering induction, datatypes need dedicated inference rules to account for acyclicity; other properties such as injectivity can be accounted for by adding either rules or axioms. Some SMT solvers have decision procedures for datatypes [START_REF] Reynolds | A decision procedure for (co)datatypes in SMT solvers[END_REF][START_REF] Barrett | An abstract decision procedure for satisfiability in the theory of inductive data types[END_REF][START_REF] De Moura | Z3: An efficient SMT solver[END_REF]. Similar work exists for superposition [START_REF] Kovács | Coming to terms with quantified reasoning[END_REF][START_REF] Wand | Automatic Induction inside Superposition[END_REF][START_REF] Horbach | Superposition for fixed domains[END_REF]. We use a small set of rules, as presented in Figure 2. In the rules, c and c are distinct inductive constructors (e.g., the empty list [ ], the successor symbol, etc.). The positive version of Acyclicity rule can also be used as a simplification when the unifier σ is trivial. These rules are sound with respect to standard models, but do not, by themselves, ensure completeness without induction.

Proving Formulas by Induction

Let us first look at a single proof by induction before we consider how to integrate such proofs in the superposition machinery (Sect. 5). An inductive goal is a closed ∀x. leq(z, x) ∀x. leq(s(x), z) ⊥ ∀x y. leq(s(x), s(y)) leq(x, y)

(define-fun pred ((x Nat)) Nat (match x (case z z) (case (s x2) x2))) (define-fun-rec fact ((x Nat)) Nat (let ((one (s z))) (if (leq x one) one (mult x (fact (pred x))))) pred(z) z ∀x. pred(s(x)) x ∀x. fact(x) f(x, leq(x, s(z))) ∀x. f(x, ) s(z) ∀x. f(x, ⊥)
mult(x, f(pred(x), leq(pred(x), s(z))) where f is fresh

(declare-fun g (Nat Nat) Nat) (define-fun h ((x Nat) (y Nat)) Bool (let ((g2 (lambda ((x Nat)) (g y (s x))))) (=> (= x y) (= (g2 x) (g2 y))))) ∀x y. h(x, y) x y ⇒ f2(y, x) f2(y, y) ∀y z. f2(y, z) g(y, s(z))
where f2 is fresh Fig. 1: Encoding a few expressions and definitions formula ∀x 1 . . . x n y 1 . . . y m . j C j where the variables x i have inductive types and each C j is a clause. To try and prove such a goal, we instantiate the structural induction schema over a non-empty subset of x into a first-order formula F , and try to refute ¬F by the usual process of Skolemizing variables, reducing ¬F to conjunctive normal form (CNF), and performing inferences until ⊥ is deduced. We can instantiate the induction schema for a goal ∀x 1 , . . . , x k . G on the variables x 1 , x 2 , . . . , x k (k ≥ 1) by instantiating it on x 1 first (taking P (x) = ∀x 2 . . . x k . G), obtaining F , and then by applying the induction principle on x 2 , . . . , x k to every occurrence of P in F .

Instantiating the Induction Schema

Before we explain how to instantiate the induction schema over a given set of variables, we must first define the notions of inductive Skolem constant and coverset.

Definition 2 (Coverset [START_REF] Zhang | A mechanizable induction principle for equational specifications[END_REF]). A coverset for an inductive type τ is a set of terms built from inductive constructors and variables x 1 , . . . , x n such that each Definition 4 (Ground Coverset). A ground coverset κ(i) for an inductive Skolem constant i is a set of ground terms obtained by replacing all variables in a coverset with fresh Skolem constants, such that t∈κ(i) i t holds in any model. The elements of κ(i) represent all the possible "shapes" of i in any model. If t, i : τ and there is some t ∈ κ(i) such that t t , we write sub(t, i). We define κ ↓ (i) = {t ∈ κ(i) | ∃t t. sub(t , i)} -the set of recursive cases. To prove an inductive goal F def = ∀x 1 . . . x n y 1 . . . y m . i C i by induction over variables x 1 , . . . , x n , we start by skolemizing each x i with i i and each y j with c j . Then, we map each inductive Skolem constant i i to a ground cover set κ(i i ). Our objective is to refute the following set of clauses:

c(t) c (t ) ∨ D Disjointness+ D c(t) c (t ) ∨ D Disjointness- c(t1, . . . , tn) c(t 1 , . . . , t m ) ∨ D Injectivity n i=1 (ti t i ∨ D) t C[u] ∨ D tσ = uσ Acyclicity+ Dσ t C[t] ∨ D Acyclicity- where C[ ] is a non-trivial constructor context
t1∈κ(i1),...,tn∈κ(in) cnf(¬ i C i [x → t, y → c)] ← n j=1 i j t j ∪ u1∈κ ↓ (i1),...,un∈κ ↓ (in) i ∀y. C i [x → u] ← n j=1,sub(ti,ui) i j t j ∪ n j=1 t∈κ(ij ) i j t
The first set of clauses comes from the negation of our goal, after skolemization and case split (using a coverset to examine the possible shapes of these Skolem constants (i j ) j ). The second set comes from inductive hypothesis: to prove ⊥ from ¬( i C i )[x → n 0 ], in the case n 0 s(n 1 ), we need the hypothesis ( i C i )[x → n 1 ]. The third set of boolean formulas, sent to the SAT solver, forces each Skolem constant to be equal to exactly one member of its ground coverset. We recall that • turns a literal or clause into a propositional atom.

Example 6 (Associativity of +). Let F def = ∀x y z : nat. x + (y + z) (x + y) + z. To prove F , we perform induction on {x}, with Skolem symbols {x 0 , y 0 , z 0 } and ground coverset κ(x 0 ) = {0, s(x 1 )}. The resulting clauses are: 0 + (y 0 + z 0 ) (0 + y 0 ) + z 0 ← x 0 0 s(x 1 ) + (y 0 + z 0 ) (s(x 1 ) + y 0 ) + z 0 ← x 0 s(x 1 ) ∀y z.

x 1 + (y + z) (x 1 + y) + z ← x 0 s(x 1 ) x 0 0 ⊕ x 0 s(x 1 )
Now, superposition (and AVATAR) can prove ⊥ from these clauses:

1 induction(F ).base 0 + (y 0 + z 0 ) (0 + y 0 ) + z 0 ← x 0 0 2 def(+) 0 + x x 3 rewrite(1,2) y 0 + z 0 y 0 + z 0 ← x 0 0 4 eq-res(3) ⊥ ← x 0 0 5 avatar(4) ¬ x 0 0 6 induction(F ).hyp ∀y z. x 1 + (y + z) (x 1 + y) + z ← x 0 s(x 1 ) 7 induction(F ).rec s(x 1 ) + (y 0 + z 0 ) (s(x 1 ) + y 0 ) + z 0 ← x 0 s(x 1 ) 8 def(+) s(x) + y s(x + y) 9 rewrite [START_REF] Bachmair | On Restrictions of Ordered Paramodulation with Simplification[END_REF][START_REF] Kovács | Coming to terms with quantified reasoning[END_REF] s(x 1 + (y 0 + z 0 )) s((x 1 + y 0 ) + z 0 ) ← x 0 s(x 1 ) 10 sup [START_REF] Weidenbach | System Description: SPASS Version 3.0[END_REF][START_REF] Kaufmann | ACL2: An industrial strength version of Nqthm[END_REF] s(x 1 + (y 0 + z 0 )) s(x 1 + (y 0 + z 0 )) ← x 0 s(x 1 ) 11 eq-res [START_REF] Biundo | The Karlsruhe induction theorem proving system[END_REF] ⊥ ← x 0 s(x 1 ) 12 avatar(11) ¬ x 0 s(x 1 )

13 induction(F ).case-split x 0 0 x 0 s(x 1 ) 14 res [START_REF] Riazanov | Vampire 1.1 (system description)[END_REF][START_REF] Reynolds | Induction for SMT solvers[END_REF][START_REF] Kersani | Combining superposition and induction: A practical realization[END_REF] ⊥

The last inference is done by the SAT solver after the addition of the boolean constraints ¬ x 0 0 and ¬ x 0 s(x 1 ) , establishing unsatisfiability.

Example 7 (Transitivity of ≤). Let

F def = ∀x y z : nat. x ≤ y ∧ y ≤ z ⇒ x ≤ z,
where ≤ is defined by the rules {∀x. 0 ≤ x, ∀x. ¬(s(x) ≤ 0), ∀x y. x ≤ y ⇐⇒ s(x) ≤ s(y)}. To prove F , we perform induction on {x, y, z}, with Skolem symbols {x 0 , y 0 , z 0 } and ground coversets κ(x 0 ) = {0, s(x 1 )}, κ(y 0 ) = {0, s(y 1 )}, κ(z 0 ) = {0, s(z 1 )}. We obtain the following set of clauses, which is first-order refutable:

0 ≤ 0 ← x0 0 y 0 0 0 ≤ 0 ← y 0 0 z0 0 s(x1) ≤ 0 ← x0 s(x1) y 0 0 s(x1) ≤ s(y 1 ) ← x0 s(x1)
y 0 s(y 1 ) s(y 1 ) ≤ 0 ← y 0 s(y 1 ) z0 0 s(y 1 ) ≤ s(z1) ← y 0 s(y 1 ) z0 s(z1)

¬(0 ≤ 0) ← x0 0 z0 0 ¬(s(x1) ≤ 0) ← x0 s(x1) z0 0 ¬(s(x1) ≤ s(z1)) ← x0 s(x1) z0 s(z1) ¬(0 ≤ s(z1)) ← x0 0 z0 s(z1) ¬(x1 ≤ y 1 ) ∨ ¬(y 1 ≤ z1) ∨ (x1 ≤ z1) ← x0 s(x1) y 0 s(y 1 ) z0 s(z1) x0 0 x0 s(x1) y 0 0 y 0 s(y 1 ) z0 0 z0 s(z1)
Remark 1. Using AVATAR for keeping track of case splits allows an inductive lemma, once proved, to become a normal axiom and participate in other proofs using the following simplifications:

C ← Γ a AvatarSimp+ C ← Γ C ← Γ ¬a AvatarSimp-
if the SAT-solver has proved a (propagated at level 0)

Selecting the Induction Variables

We have seen how to prove an inductive goal by induction over a set of variables. But how do we know which variables to choose? Going back to the case of Example 6 (associativity of addition), there are three variables, but only the leftmost one will lead to a successful induction.

The relevant notion here is that of primary positions under functions (Definition 1). Here we draw inspiration from Aubin's work [START_REF] Aubin | Strategies for mechanizing structural induction[END_REF]. The heuristic is that if a variable appears in at least one primary occurrence, it is a candidate for induction. Let G def = ∀x y. i C i be an inductive goal, with variables x having an inductive type. A primary occurrence in G is a position p in some clause C i such that (i) C i | p does not occur directly under a constructor, and (ii) every non-empty prefix of p occurs either below a constructor, an uninterpreted symbol, or under a primary argument position of a defined function or predicate. Intuitively, a subterm (such as a variable on which we might do induction) is a primary occurrence in G if replacing this subterm by a constructor-headed term has a chance of making G reducible by some rewrite rule. In Example 6, the goal is ∀x y z : nat. x + (y + z) (x + y) + z. Of all three variables, only x appears in primary occurrences. Now consider Example 7, where the goal is ∀x y z : nat. x ≤ y ∧ y ≤ z ⇒ x ≤ z. All variables occur in primary positions, because both positions of ≤ are primary. However, simply replacing x with a constructor-headed term will not always suffice to reduce the (ground) goal negation; indeed s(x 1 ) ≤ y 0 and ¬(s(x 1 ) ≤ z 0 ) cannot be reduced. Therefore, we extend Aubin's heuristic [START_REF] Aubin | Strategies for mechanizing structural induction[END_REF]. If two variables in primary positions in the goal G occur immediately under the same defined symbol, both at primary argument positions, then we perform induction on both of them simultaneously. For Example 7 that means that we perform induction over {x, y, z}, which succeeds.

Performing Several Inductive Proofs with AVATAR

In practice, we need to carry out several proofs by induction. It is necessary when such a proof depends on other properties that are themselves proved by induction. One such case is nested induction: to prove ∀x y. x + y y + x, the lemmas ∀x. x + 0 x and ∀x y. x + s(y) s(x + y) are required. We wish to carry out all these proofs within a single saturation loop of the superposition prover, to reuse the existing algorithms and main loop. Fortunately, AVATAR makes it easy to introduce several lemmas and interleaving their proof with the main saturation process. Given a (candidate) lemma F (a closed first-order formula), the clauses

{C ← lemma F | C ∈ cnf(F )} ∪ {D ← ¬ lemma F | D ∈ cnf(¬F )}
are added to the saturation set. This corresponds to a boolean split over F ∨ ¬F , where the choice between F and ¬F is represented by the boolean valuation of the propositional literal lemma F .

Definition 5 (Lemma Introduction).

The introduction rule of a lemma F , where F is a first-order formula, is the following inference rule:

Lemma C∈cnf(F ) C ← lemma F ∧ D∈cnf(¬F ) D ← ¬ lemma F Theorem 1.
The inference rule Lemma is sound.

Proof. Lemma is similar to an AVATAR boolean split on F ∨ ¬F using the boolean F (F , being closed, is either valid or unsatisfiable). Since ¬F def = ¬ F , we obtain the trivial constraint F ¬ F and the "A-formulas" F ← F and ¬F ← ¬ F that can then be reduced to CNF. In essence, Lemma is using an adaptation of AVATAR splitting to formulas of the form F ∨ ¬F where F is closed.

In a part of the search space, inference with A-clauses of the form C ← F will correspond to using the lemma F , assuming it has been proved; in another part, inferences with A-clauses of the form D ← ¬ F will possibly lead to (conditional) proofs of F by reaching clauses of the form ⊥ ← ¬ F Γ (proof of F under assumptions ¬Γ ).

Remark 2 (Fairness and Lemmas). Using Lemma on a non-theorem formula F does not prevent an unsatisfiable combined state from being reached. The proof of each lemma is interleaved with the rest of the saturation process. Thanks to this, it is possible to introduce several (candidate) lemmas even if they are not all true or provable. However, it might take a longer time to find a solution, because of the larger search space.

Finding Subgoals and Lemmas by Generalization

In this section, we examine several ways of guessing new inductive goals that are likely to help existing proof attempts progress. There is a large amount of literature dedicated to lemma guessing, either by generalizing a subgoal [START_REF] Kaufmann | ACL2: An industrial strength version of Nqthm[END_REF][START_REF] Wand | Automatic Induction inside Superposition[END_REF][START_REF] Kapur | Lemma discovery in automating induction[END_REF][START_REF] Aubin | Strategies for mechanizing structural induction[END_REF] or by exploring an equational theory systematically to find formulas that seem to hold based on testing [START_REF] Reynolds | Induction for SMT solvers[END_REF][START_REF] Claessen | Hipspec: Automating inductive proofs of program properties[END_REF]. In this paper we present simple, relatively straightforward techniques that already yield good results; more sophisticated heuristics can be added on top.

Even though lemmas can either be proved on the fly by introducing a cut, or provided as axioms in the input file, they will be used in the same way in both cases. A subgoal is never generalized and replaced by a lemma; rather, we introduce a lemma which, if proved, will solve the subgoal by regular superposition.

Proving Subgoals by Induction

A superposition prover starts by reducing the input problem in CNF, in our case with some additional transformations (Sect. 3.2). A clause C containing at least one inductive Skolem constant can be negated, the constants replaced by fresh variables, resulting in an inductive goal that can be tested and then proved.

Similarly, during the course of saturation with some induction attempts, clauses of the form C ← ¬ lemma G Γ (where G is an inductive goal) are clauses that need to be reduced to ⊥ if G is to be proved. Again, if C contains at least one inductive Skolem constant, we can negate it, replace constants by variables, and assess the resulting goal.

More precisely, to prove a goal i C i by generalizing inductive Skolem constants i 1 , . . . , i n (n ≥ 1) occurring in the clauses C i : (i) we replace each i j by a fresh variable x j ; (ii) we negate every literal in the C i and swap conjunctions and disjunctions; (iii) we redistribute conjunction over disjunction to get back to a CNF. Clauses in the result are quantified over {x j } j and a subset of i freevars(C i ). This generalization technique also applies to the original goal after it has been negated and reduced to CNF during preprocessing. It makes it possible to prove inductively goals that are not in CNF.

A subtlety here is that if an induction variable j is a sub-case of some other constant (j ∈ κ ↓ (i)), there exist induction hypotheses (in other clauses) that might be needed for nested induction. In this case we also try the inductive goal where j is not replaced by a fresh variable, and run both proof attempts simultaneously. 2

Generalizing subgoals

An inductive goal G might not be provable by induction directly. For example, doing induction on x to prove ∀x. x + (x + x) (x + x) + x will not succeed: in the recursive case x 0 = s(x 1 ), the clauses are x 1 + (x 1 + x 1 ) (x 1 + x 1 ) + x 1 s(x 1 ) + (s(x 1 ) + s(x 1 )) (s(x 1 ) + s(x 1 )) + s(x 1 ) but even after reduction, the hypothesis cannot rewrite the negative clause in any way because of successor symbols that appeared at passive positions. Following, once more, Aubin [START_REF] Aubin | Strategies for mechanizing structural induction[END_REF], we generalize the primary occurrences of a variable in a goal if it occurs at least twice in primary positions, and at least once in passive positions. In this way, doing inference on the primary occurrences will have better chances of succeeding. This generalization is only performed if the generalized goal still passes tests successfully (see Sect. 7).

Similarly, if a non-variable, non constructor-headed term occurs at least twice in primary positions, and is neither a variable nor constructor-headed, we can generalize it the same way.

Heuristics for guessing relevant lemmas from a goal have been developed for decades [START_REF] Kaufmann | ACL2: An industrial strength version of Nqthm[END_REF][START_REF] Bundy | Rippling: A heuristic for guiding inductive proofs[END_REF][START_REF] Boyer | A Computational Logic Handbook[END_REF][START_REF] Kapur | Lemma discovery in automating induction[END_REF][START_REF] Aubin | Strategies for mechanizing structural induction[END_REF] and can be adapted to our framework. For those that require to examine both the current subgoal and the induction hypothesis, more bookkeeping would be needed, because these objects live in the unstructured set of clauses, rather than in a sequent.

Remark 3. Speculating lemmas can be detrimental to the search space, by introducing many new clauses and performing arbitrary cuts. Therefore, the application of this rule must be heuristically restricted. In our implementation, we forbid deeply nested applications of generalization (beyond a small, user definable limit). Developing more advanced heuristics is however necessary.

7 Testing Conjectures before trying to prove them Heuristics, as useful as they are, can mislead a solver into trying to prove inductive goals that are not valid. Attempting to prove an invalid goal with likely lead to a non-terminating superposition saturation on its own, draining memory and CPU resources away from the main proof effort. It pays to perform some limited amount of computation to try and rule out invalid goals.

To test a goal G def = ∀x. i C i , we do a limited number of saturation step, starting from {C i } i . Clauses from the main saturation loop can be used in inferences, emulating a set-of-support strategy. If ⊥ can be derived, the goal is invalid and can be discarded. Many inductive goals, in practice, use computable (recursive) functions. Testing tools such as (Lazy) SmallCheck [START_REF] Runciman | Smallcheck and lazy smallcheck: automatic exhaustive testing for small values[END_REF] and QuickCheck [START_REF] Claessen | QuickCheck: a lightweight tool for random testing of Haskell programs[END_REF] are popular options for these properties; in our case, we use narrowing [START_REF] Lindblad | Property directed generation of first-order test data[END_REF] because it is readily adapted to rewriting-based functions: the resulting rules are listed in Figure 3. In addition, not all goals contain only computable functions -some functions or predicates might only occur in axioms, not definitions -so we also need to perform the usual superposition inferences.

This mechanism for ruling out invalid goals works quite well in practice, even with a relatively small number of saturation steps. The limit on saturation steps Fig. 4: Experiments on TIP benchmarks tains 15,853 first-order problems.5 CVC4, again, performs quite well; Prover9 is included as a base reference, and E (version 1.9) is one of the best first-order provers. This benchmark shows that Zipperposition keeps good performance on first-order problems.

It is interesting to note that CVC4 is very versatile, and can play on many boards, including first-order logic and inductive theorem proving, in addition to more traditional SMT abilities such as ground reasoning with theories such as arithmetic. We hope that superposition provers will also extend their domain of competency to tackle more expressive logics. Having diverse techniques for automated theorem proving means that portfolio approaches will work well, and will benefit from complementary strengths of the solvers.

Conclusion

In this work, we show a practical integration of inductive reasoning into a superposition prover. Such a combination is desirable because many problems fall outside of either fragment: they might not be purely equational (or Horn), as usually assumed by inductive provers, and yet they might require some inductive reasoning. We introduce a simple inference rule for adding multiple cuts during proof search. Inductive proofs are interleaved with the normal first-order proof search, thanks to AVATAR and this new inference rule.

We also present some techniques for generating inductive subgoals during the proof search, based on Aubin's work [START_REF] Aubin | Strategies for mechanizing structural induction[END_REF]; other generalization heuristics, including the ones that rely on theory exploration [START_REF] Claessen | Hipspec: Automating inductive proofs of program properties[END_REF], are compatible with our approach. User-provided lemmas can also be tried and used during proof search, without compromising soundness if they are actually invalid.

Our approach should be relatively straightforward to port to existing state of the art superposition provers. The unsophisticated implementation we describe performs reasonably well on the IsaPlanner and TIP benchmarks. With the addition of more powerful generalization techniques, this suggests that superpositionbased first-order provers can become competitive with existing induction provers. In particular, Vampire already supports inductive datatypes and AVATAR split- Fig. 5: Results on the first-order fragment of TPTP ting, and performed very well in SMT-COMP 2016, suggesting superposition is ready to be applied outside of pure first-order logic.

Example 3 .

 3 (a) + with the definition 0 + x x, s(x) + y s(x + y): the first argument is primary and the second one, passive. (b) ≤ defined by (0 ≤ x) , (s(x) ≤ 0) ⊥, (s(x) ≤ s(y)) (x ≤ y): both positions are primary. (c) qrev with the rules qrev([ ], x)

  original encoded (declare-datatype Nat ((z) (s Nat))) (define-fun-rec leq ((x Nat)(y Nat)) Bool (match x (case z true) (case (s x2) (match y (case z false) (case (s y2) (leq x2 y2))))))

Fig. 2 :

 2 Fig. 2: Inference rules to deal with inductive constructors

Example 4 .Example 5 .

 45 The coversets of the type nat from Example 1 are of the form {0, s(0), . . . , s k (0), s k+1 (x)} for some k ≥ 0. The coversets of the type list(τ ) from Example 2 are of the form {[ ], x 1 :: [ ], . . . , x 1 :: . . . :: x m :: y} where m > 0, x 1 , . . . , x m : τ , and y : list(τ ).

  1 , . . . , t n ) where c is a constructor symbol. A constructor context C[ ] is a term built from constructors, function symbols of non-inductive type, and a unique occurrence of ; applying the context to a term t, written C[t], means replacing the occurrence of by t. C[t] is only defined if it is well typed. A Herbrand model is standard if (i) it satisfies the axioms of datatypes: exhaustiveness and disjointness of constructors; (ii) every (ground) term is equal to some purely inductive term; (iii) equivalence classes of inductive types are acyclic, i.e. for every non-trivial constructor context C[ ], t C[t] is true in the model.

It might even induce rewriting loops in some cases where the term ordering used by superposition and the rewrite system are not compatible. In our experience this does not seem to happen often.

Our framework allows attempting to prove several distinct inductive goals to solve a single subgoal.

CVC4 1.5-prerelease r6317, see http://cvc4.cs.stanford.edu/web/

commit 187b71af8d920d0634b2b8b34c4ac4834b2f6a94 at https://github.com/ tip-org/benchmarks.

experiments on TPTP were run on a 2.20 GHz Intel Xeon CPU with 30 s timeout and a memory limit of 2 GB.

Acknowledgments The author would like to thank Jasmin Blanchette, Gilles Dowek, Guillaume Burel, Pascal Fontaine, and reviewers of previous versions of this paper (one of them, in particular, for pointing out a lot of related works and limitations in several occasions).

is a trade-off between the usefulness of detecting invalid conjectures, and the time spent on each candidate lemma.

Implementation and Experiments

To evaluate our approach, we implemented it in a superposition prover, Zipperposition [35, chapter 3]. The prover is implemented in OCaml, available at https://github.com/c-cube/zipperposition under a permissive BSD license. Thanks to its modular architecture, many extensions of superposition have been added to it, including (as of version 1.2) integer linear arithmetic [35, chapter 4], first-class boolean terms [START_REF] Kotelnikov | The Vampire and the FOOL[END_REF], rewrite rules (used for evaluating recursive functions), a simpler version of AVATAR [START_REF] Voronkov | AVATAR: the architecture for first-order theorem provers[END_REF], basic support for AC symbols [START_REF] Schulz | E -a brainiac theorem prover[END_REF], and the inductive reasoning described in this paper. This allows the prover to solve such problems as ∀(p : α → bool) (l : list(α)). length(l) ≥ length(filter(p, l)) by using a combination of arithmetic, booleans, and induction. The prover can parse its own native format, TPTP [START_REF] Sutcliffe | The TPTP Problem Library and Associated Infrastructure: The FOF and CNF Parts, v3.5.0[END_REF], and TIP [START_REF] Claessen | TIP: Tons of Inductive Problems[END_REF].

In Figure 4, we compare Zipperposition with two variations of CVC4 3 on TIP benchmarks. 4 The first one, CVC4, corresponds to cvc4 --lang smt --quant-ind to perform goal-directed induction [START_REF] Reynolds | Induction for SMT solvers[END_REF]; the second one, CVC4-gen, has the additional flag --conjecture-gen to generate lemmas by theory exploration, like Hipspec [START_REF] Claessen | Hipspec: Automating inductive proofs of program properties[END_REF]. We use https://github.com/tip-org/tools/ to convert TIP problems into SMT-LIB by removing pattern matching (which is not supported by CVC4). The classical set of IsaPlanner benchmarks [START_REF] Johansson | Conjecture Synthesis for Inductive Theories[END_REF] are included as a subset of TIP benchmarks. Solvers are given 30 s for each problem, which is a reasonable amount of time a user might wait for automatic provers in a proof assistant. The results are encouraging, since Zipperposition relies on quite simple generalization techniques.

However, our initial aim was to extend superposition provers to do induction, while retaining their efficiency in first-order reasoning. Figure 5 shows a comparison of Zipperposition with some other provers, on TPTP 6.1, which con-


{ "@context":["http://www.w3.org/ns/csvw", {"@language": "en"}], "url": "trees.csv", "dc:title": "Trees", "dc:license": { "@id": "http://.../../cc-by/"}, "dc:modified": {"@value": "2010-12-31", "@type": "xsd:date"}, "tableSchema": { "columns": [ { "name": "ID", "titles": ["ID", "Identifier"], "datatype":"string", "required": true }, { "name": "Street", "titles": "On Street", "dc:description": "…", "datatype": "string" }, ... ], "primaryKey": "ID", "aboutUrl": "#id-{ID}" }} <http://unice.fr/staff/7> rdf:type ex:Teacher. <http://unice.fr/staff/7> foaf:name "Catherine". <http://unice.fr/staff/8> rdf:type ex:Teacher. <http://unice.fr/staff/8> foaf:name "Olivier". http://www.w3.org/TR/r2rml/ Franck MICHEL <http://example.org/member/106> foaf:mbox "john@foo.com". <http://example.org/member/106> foaf:mbox "john@example.org". Mapping of a NoSQL DBs to RDF with xR2RML { "id": 106, "firstname": "John", "emails": [ "john@foo.com", "john@example.

  LOD Cloud: 10K datasets, 150B Statements Linking Open Data cloud diagram 2017. A. Abele, J.P. McCrae, P. Buitelaar, A. Jentzsch and R. Cyganiak. http://lod-cloud.net/ On the Web In RDF Under open licences Interlinked Publishing legacy data in RDF raises tricky of heterogeneous data into RDF Choose vocabularies to represent RDF data Access the RDF data produced The key importance of metadata Agenda Describe the translation of heterogeneous data into RDF Choose vocabularies to represent RDF data Access the

  <#MapMbox> xrr:logicalSource [ xrr:query "db.people.find({'emails':{$ne: null}})" ]; rr:subjectMap [ rr:template "http://example.org/member/{$.id}" ]; rr:predicateObjectMap [ rr:predicate foaf:mbox; rr:objectMap [ xrr:reference "$.emails.*"; rr:termType rr:Literal ] ].

  org" ] } xR2RML Describe the translation of heterogeneous data into RDF Choose vocabularies to represent RDF data Access the RDF data produced The key importance of metadata Agenda Franck MICHEL Custom Mapping: reuse existing vocabularies Large variety of existing vocabularies But may be difficult to find the appropriate one Partial coverage of the domain Granularity: too high (cumbersome), too low (useless) Different points of view Frequently, a mixed approach is used Describe the translation of heterogeneous data into RDF Choose vocabularies to represent RDF data Access the , dates, license, version, reference articles Access Format, structure, location (dwld), query method Meaning What do the data represent? What concepts, entities, semantics? Interpretation Units (cm or inches, left/right)… Provenance Acquired with which equipment, parameters, protocols? Derived from which dataset? With which processing? Dataset-level or entity-level provenance Statistics Number of triples per property of class, links to other datasets… … Franck MICHEL Several works normalize metadata descritpions and how to use metadata  CSVW: CSV on the Web  DCAT: Data Catalog Vocabulary DCAT extensions, application profiles W3C Dataset Exchange Working Group  VoID: Vocabulary of Interlinked Datasets  HCLS: Health Care & Life Sciences Dataset Profile  …

  ://www.w3.org/2013/csvw/ Franck MICHEL

	Direct Mapping of a RDB to RDF
	<PEOPLE/ID=7> rdf:type	<PEOPLE> .
	<PEOPLE/ID=7> <PEOPLE#FNAME> "Catherine" .
	<PEOPLE/ID=7> <PEOPLE#WROTE> <BOOK/ID=22> .
	<PEOPLE/ID=8> rdf:type	<People> .
	<PEOPLE/ID=8> <PEOPLE#FNAME> "Olivier" .

https<PEOPLE/ID=8> <PEOPLE#WROTE> <BOOK/ID=22> .

Table : PEOPLE

 :

	Custom Mapping of a RDB to with R2RML
	Table: PEOPLE
	ID ID	FNAME FNAME	WROTE (FK BOOK/ID) WROTE (FK BOOK/ID)
	7 7	Catherine Catherine	22 22
	8 8	Olivier Olivier	22 22
	… …	… …	… …
			Existing vocabularies
	Franck MICHEL

https://www.w3.org/TR/2012/REC-rdb-direct-mapping-20120927/ Franck MICHEL Custom Mapping of a RDB to RDF <http://unice.fr/staff/7> rdf:type ex:Teacher. <http://unice.fr/staff/7> foaf:name "Catherine". <http://unice.fr/staff/7> dc:contributor <http://unice.fr/book/22>. <http://unice.fr/staff/8> rdf:type ex:Teacher. <http://unice.fr/staff/8> foaf:name "Olivier". <http://unice.fr/staff/8> dc:contributor <http://unice.fr/book/22>. <#MapPeople> rr:logicalTable [ rr:tableName "PEOPLE" ]; rr:subjectMap [ rr:template "http://unice.fr/staff/{ID}"; rr:class ex:Teacher; ]; rr:predicateObjectMap [ rr:predicate foaf:name; rr:objectMap [ rr:column "FNAME" ]; ].