Radu Iosif

Cristina Serban

A Complete Cyclic Proof System for Inductive Entailments in First Order Logic

. We show the proof system to be sound, in general, and complete, under certain semantic restrictions involving the set of constraints in the inductive system. Moreover, we investigate the computational complexity of checking these restrictions, when the function symbols in the logic are given the canonical Herbrand interpretation.

Introduction

Inductive definitions play an important role in computing, being an essential component of programming languages, databases, automated reasoning and program verification systems. The main advantage of using inductive definitions is the ability of reasoning about sets of logical objects, by means of recursion. The semantics of these definitions is described in terms of least fixed points of higher-order functions on assignments mapping predicates to sets of models. A natural problem is the entailment, that asks whether the least solution of one predicate is included in the least solution of another. Examples of entailments are language inclusion between finite-state (tree) automata, context-free grammars or verification conditions generated by shape analysis tools using specifications of recursive data structures as contracts of program correctness.

The principle of infinite descent, stated by Fermat [START_REF] Bussey | Fermat's method of infinite descent[END_REF], has become an important tool for reasoning about entailments between inductively defined predicates. In a nutshell, a proof by infinite descent is a particular proof by contradiction, in which we assume the existence of a counterexample from a wellfounded domain and show the existence of a strictly smaller counterexample for the same entailment problem. By repeating this step, we obtain an infinite descending chain of counterexamples, which is impossible when the domain of counterexamples is well-founded.

A cyclic proof [START_REF] Brotherston | Sequent Calculus Proof Systems for Inductive Definitions[END_REF] is a finite derivation tree in which certain leaves (buds) are connected to internal nodes (companions) via backlinks, such that on every infinite path obtained by following backlinks there are infinitely many progress points ensuring that no counterexample can be propagated along that path ad infinitum. Together with the local soundness of each proof rule (if all premises are true, the conclusion is true), this so-called global trace condition [START_REF] Brotherston | Cyclic proofs for first-order logic with inductive definitions[END_REF][START_REF] Brotherston | Sequent calculi for induction and infinite descent[END_REF] ensures the soundness of a cyclic proof.

In particular, cyclic proofs reason about inductive definitions by deriving the inductive invariants on-the-fly, as opposed to classical proofs by induction, in which these invariants have to be provided. Moreover, cyclic proofs are shown to be strictly more general than inductive proofs: all proofs by induction can be written as cyclic proofs (with cut) [START_REF] Brotherston | Sequent calculi for induction and infinite descent[END_REF], whereas there are statements provable using cyclic proof that cannot be proved using induction [START_REF] Berardi | Classical system of Martin-Löf's inductive definitions is not equivalent to cyclic proof system[END_REF]. Despite these interesting features, cyclic proofs face several problems, e.g.:

• Practical applications within automated reasoning systems are met with the inherent complexity of checking the global trace condition, which requires time exponential in the size of the derivation tree, unless certain structural restrictions are used. A typical restriction is that the companion of a bud must also be an ancestor, which can be checked in time logarithmic in the size of the proof. Additionally, it is possible to check the soundness of a cyclic proof by checking inclusion of weighted automata [START_REF] Rowe | Realizability in cyclic proof: Extracting ordering information for infinite descent[END_REF]. • The boundaries of completeness (for which systems of inductive definitions does a valid entailment query have a proof?) are not entirely understood. In [START_REF] Brotherston | Sequent Calculus Proof Systems for Inductive Definitions[END_REF][START_REF] Brotherston | Sequent calculi for induction and infinite descent[END_REF], cut-free completeness is shown for the system LKID ω , in which one allows infinite recursive proofs, that cannot be folded into finite cyclic proofs. It is thus an interesting open problem which inductive systems admit complete (finite) cyclic proofs. Besides implying the decidability of entailments1 , a complete proof system gives a way of certifying the correctness of a certain theorem prover implementation, by producing machine-checkable proofs of the validity of queries [START_REF] Stump | SMT proof checking using a logical framework[END_REF]. The relation between cyclic proof systems and automata is long-standing, one of the main results being a complete proof system for the modal µ-calculus, proposed by Walukiewicz [START_REF] Walukiewicz | Completeness of Kozen's axiomatisation of the propositional mu-calculus[END_REF]. In a similar vein, the proof system presented in this paper stems from the observation that language inclusion of tree automata can be proved using an infinite descent argument. Given tree automata A and B, we assume the existence of a tree t ∈ L(A) \ L(B), where L(A) [L(B)] denotes the language of A [B], and prove the existence of strictly smaller tree t ∈ L(A) \ L(B), in the subtree order. Since the subtree order is well-founded, there is no such tree to start with and thus L(A) ⊆ L(B). Moreover, the search space built by antichain-based algorithms for language inclusion between tree automata [START_REF] Holík | Efficient inclusion checking on explicit and semi-symbolic tree automata[END_REF] can roughly be viewed as a cyclic sequent calculus proof. Because tree automata over finite alphabets have a decidable inclusion problem, these problems are further shown to have complete cyclic proof systems.

The contributions of this paper are two-fold:

1. We provide a proof system for entailments between inductive predicates defined using a system of mutually recursive definitions, written using quantifier-free first-order logic. We show that the system is sound, using a local constraint on the (reversed) path between a bud and its companion in the derivation. Completeness is subject to three decidable conditions on the set of ground constraints that occur in the system of definitions. Moreover, we make proof generation effective by providing suitable strategies that limit the possibilities of applying the inference rules and guide the search towards finding a proof or a counterexample. 2. We investigate the computational complexity of checking whether a given system complies with the semantic restrictions required to ensure its completeness. An implementation can effectively check these conditions and issue a warning indicating the source of incompleteness of the proof system, for a given entailment problem. Our proof system is a typical example of the unfold-and-match method that is used in state-of-the-art tools for reasoning about inductively defined recursive data structures [11]. Our main contribution in this area is the study of the completeness problem and an attempt to defining a class of inductive definitions for which unfold-and-match paradigms are complete, when infinite descent is used to ensure termination. As a by-product, we obtain a language inclusion algorithm for tree automata, that in addition to answering yes/no, issues proof certificates and counterexamples.

The method presented here is general enough so that it can be adapted to other types of logic. We provide a prototype implementation of this semi-algorithm [START_REF] Iosif | An entailment checker for separation logic with inductive definitions[END_REF], that uses a slightly modified variant of the inference rules for proving entailments between inductive predicates in Separation Logic [START_REF] Reynolds | Separation logic: A logic for shared mutable data structures[END_REF].

Preliminaries

We adopt the classical terminology of first-order logic over a countable signature Σ consisting of function symbols f (x 1 , . . . , x n ), where #( f ) = n denotes the arity of f . A constant c is a function symbol of arity zero. We assume the existence of a boolean sort with constants ⊥ and for false and true, respectively. A predicate p(x 1 , . . . , x n ) is a function symbol of the boolean sort.

Let Var be a countably infinite set of variables. For a term t, we denote by FV(t) the set of variables in t. For a formula φ, we denote by FV(φ) the set of variables not occurring under the scope of a quantifier and write φ(x) for FV(φ) ⊆ x. The same notation applies to sets F of formulae, where FV(F)

def = φ∈F FV(φ).
Given sets of variables x and y, a substitution θ : x → T Σ (y) is a function mapping variables to terms and let xθ def = {θ(x) | x ∈ x} be the image of x via θ. A substitution θ is flat if Varθ ⊆ Var, i.e. each variable is mapped to a variable. For a formula φ(x), we denote by φθ the formula obtained by replacing each occurrence of x ∈ x with the term θ(x), and lift this notation to sets as

Fθ def = {φθ | φ ∈ F}.
A structure is a tuple (U, I , ν), where U is a universe, I is an interpretation that maps each function symbol f into a total function f I : U #( f ) → U and ν is a partial mapping of variables into elements of U. For a tuple of variables x = (x 1 , . . . , x n ), we write ν(x) for (ν(x 1 ), . . . , ν(x n )). A distinguished class of structures are the Herbrand structures (T Σ , H , ν), where H maps each function symbol f into the function f H carrying any tuple of terms t 1 , . . . ,t #( f ) into the term f (t 1 , . . . ,t #( f ) ).

The semantics of first-order logic is given by the |= relation between structures and formulae. For When U and I are understood, we write ν |= φ instead of (U, I , ν) |= φ. A formula φ is satisfiable if and only if (U, I , ν) |= φ for some structure, called a model. We say that φ entails ψ, written φ |= ψ if and only if every model of φ is also a model of ψ.

Inductive Definitions

Let Pred ⊆ Σ be a finite set of predicates, whose interpretations are given by a set of rules. Formally, a rule is a pair ({φ(x, x 1 , . . . , x n ), q 1 (x 1 ), . . . , q n (x n )}, p(x)), where x, x 1 , . . . , x n are pairwise disjoint sets of variables, φ is a formula, called the constraint, p(x) is a predicate atom called the goal and q 1 (x 1 ), . . . , q n (x n ) are predicate atoms called subgoals. The variables in x are called goal variables, whereas those in n i=1 x i are called subgoal variables. A system of inductive definitions (system, for short) S is a finite set of rules, such that for each ρ ∈ S, the constraint of ρ is a satisfiable conjunctive quantifier-free formula2 . W.l.o.g, we assume that each goal with a predicate symbol p has the same tuple goal variables and that each predicate symbol p ∈ Pred occurs within the goal of at least one rule in S. As a shorthand, we write p(x) := S R 1 | . . . | R n , when (R 1 , p(x)), . . . , (R n , p(x)) are all the rules with goal p(x) in S.

Given a universe U and an interpretation I , an assignment X maps each predicate p ∈ Pred to a set X (p) ⊆ U #(p) . Given a rule (R, p(x)) ∈ S, where R = {φ, q 1 (x 1 ), . . . , q n (x n )}, we extend the assignment to the body of the rule as X (R)

def = {ν | (U, I , ν) |= φ and ∀i ∈ [1, m] . ν(x i ) ∈ X (q i )}.
Then we define the function F S on assignments, such that, for each assignment X and each predicate p ∈ Pred, we have:

(F S (X )) (p) = n i=1 {ν(x) | ν ∈ X (R i )}, where p(x) := S R 1 | . . . | R n .
A solution of S is an assignment X such that F S (X ) ⊆ X , where inclusion between assignments is defined pointwise. It can easily be shown that the set of assignments, together with the ⊆ relation, forms a complete lattice, since any powerset equipped with the subset relation is a complete lattice. Because F S is monotone 3 , the assignment µS def = {X | F S (X ) ⊆ X } is the least fixpoint of F S and the least solution of S, where intersection of assignments is again defined pointwise.

Example 1. Consider the system S neo [3,

(n) = s i (c) | i ≥ 0 , µS neo (e) = s 2i (c) | i ≥ 0 and µS neo (o) = s 2i+1 (c) | i ≥ 0 , i.e.
n, e and o are sets of terms corresponding to the unary encodings of natural, even and odd numbers, respectively. Furthermore, the F S functions are provably continuous 4 , thus µS = i≥1 F i S ( / 0), where / 0 is the assignment mapping each predicate to the empty set and

F i S is the i-th iteration of F S , i.e. F 1 S def = F S and
F i S def = F i-1 S • F S , for all i > 1.
Continuity of F S allows us to compute the sequence of under-approximants of µS by iterating over natural numbers, instead of ordinals. For a predicate p and a tuple of values v = (v 1 , . . . , v #(p) ) ∈ U #(p) , we denote by sn(p, v) ∈ N the least number j > 0 such that v ∈ j i=1 F i S ( / 0)(p), or 0 if there is no such j. This value is called a stage number in the following.

In this paper, we are concerned with the following entailment problem: given an inductive system S and predicates p, q 1 , . . . , q n having the same arity, is it true that µS(p) ⊆ n i=1 µS(q i )? We denote valid entailments by p |= S q 1 , . . . , q n . For instance, considering the system S neo from Example 1, we have n |= S neo e, o, whereas n |= S neo e and n |= S neo o.

We close this section by showing that the entailment problem is undecidable, in particular, when restricted to Herbrand structures, with universe T Σ and interpretation of function symbols H .

Theorem 1. The entailment problem on Herbrand structures is undecidable.

Proof. The proof is by reduction from the inclusion problem for context-free languages, a known undecidable problem [START_REF] Sipser | Introduction to the Theory of Computation[END_REF]Theorem 5.10]. Let G = Ξ, Σ, ∆ be a context-free grammar, where Ξ is the set of nonterminals, Σ is the alphabet of terminals, and ∆ is a set of productions (X, w) ∈ Ξ × (Ξ ∪ Σ) * . For a nonterminal X ∈ Ξ, we denote by L X (G) ⊆ Σ * the language produced by G starting with X as axiom.

The problem "given X,Y ∈ Ξ, does L X (G) ⊆ L Y (G)?" is undecidable. Given a context-free grammar G = Ξ, Σ, ∆ , we define a system S G as follows:

• each nonterminal X ∈ Ξ corresponds to a predicate X(x, y),

• each alphabet symbol a ∈ Σ corresponds to a unary function symbol a and a word w = a 1 . . . a n ∈ Σ * is encoded by the context (i.e. the term with a hole) w = a 1 (. . . a n (.)),

• each grammar rule (X, u 1 X 1 . . . u n X n u n+1 ) ∈ ∆ corresponds to a rule:

{φ(x, y, x 1 , y 1 , . . . , x n , y n ), X 1 (x 1 , y 1 ), . . . , X n (x n , y n )} , X(x, y) of S G , where φ ≡ x ≈ u 1 (x 1 ) ∧ n-1 i=1 y i ≈ u i+1 (x i+1 ) ∧ y n ≈ u n+1 (y) .
In particular, a rule (ε, X) ∈ ∆ maps into a rule {x ≈ y} , X(x, y) of S G . We must check that, for any nonterminals X,Y ∈ Ξ, we have L X (G) ⊆ L Y (G) if and only if X |= S G Y . This is proved using the following invariant:

∀w ∈ Σ * . (∀t . [x ← w(t), y ← t] ∈ µS G (X)) ⇔ w ∈ L X (G)
where [x ← t, y ← u] denotes the valuation mapping x to t and y to u.

Cyclic Proofs for Inductive Predicate Entailments

The previous negative result (Theorem 1) motivates the search for classes of inductive definitions with decidable entailment problems. Since inductive definitions that encode context-free grammars cannot have decidable entailments, an obvious workaround is to consider systems that define regular languages. In this respect, trees are arguably the most general type of structure for which the notion of regularity (recognizability by finite-state automata) is well understood 5 .

For this reason, the developments in this section are inspired by a state-of-the-art language inclusion algorithm for top-down tree automata [START_REF] Holík | Efficient inclusion checking on explicit and semi-symbolic tree automata[END_REF], briefly explained next. Our method for developing a proof system (set of inference rule schemata) for the entailment problem is to losely mimic the actions of the algorithm and the order in which they apply. However, we go beyond just proving inclusion of tree automata. Our proof system is sound and can be used with any entailment problem as defined above. Moreover, we characterize the class of inductive systems for which valid entailments do have finite proofs built using a strategy we provide.

Tree Automata Inclusion as Cyclic Proof Search

We assume basic knowledge of tree automata [START_REF] Comon | Tree automata techniques and applications[END_REF] and consider top-down nondeterministic finite tree automata (NFTA), whose actions are described by transition rules q f -→ (q 1 , . . . , q n ), meaning that if the automaton is in state q and the input is a ground term f (t 1 , . . . ,t n ), then it moves simultaneously on each t i changing its state to q i , for all i ∈ [n]. A ground term is accepted by an automaton A in state q if each constant subterm (leaf) can be eventually read by a rule of the form q a -→ (). The language of a state q in A, denoted L(A,q), is the set of ground terms accepted by A starting with q.

An NFTA can be naturally viewed as an inductive system, where predicates represent states and predicate rules are obtained directly from transition rules, as follows. For instance, the transition rule q f -→ (q 1 , . . . , q n ) can be written as ({x ≈ f (x 1 , . . . , x n ), q 1 (x 1 ), . . . , q n (x n )}, q(x)), where variables range over ground terms and the function symbols are interpreted in the Herbrand sense. If S A is the inductive system corresponding to A, then L(A,q) = µS A (q) for any state (predicate) q and the language inclusion problem L(A, p) ⊆ n i=1 L(A,q i ) is equivalent to the entailment p |= S A q 1 , . . . , q n . Since language inclusion is decidable for NFTA 6 , we leverage from an existing algorithm for this problem by Holík et al. [START_REF] Holík | Efficient inclusion checking on explicit and semi-symbolic tree automata[END_REF] to build a complete set of inference rules and derive a proof search technique. This algorithm searches for counterexamples of the inclusion problem L(A, p) ⊆ k i=1 L(A,q i ) by enumerating pairs (r, {s 1 , . . . , s m }), where r is a state that can be reached via a sequence of transitions from p, and {s 1 , . . . , s m } are all the states that can be reached via a sequence of transitions with the same function symbols, from q 1 , . . . , q k , respectively. A counterexample is found when the algorithm encounters a pair (r, {s 1 , . . . , s m }) such that there exists a rule r a → (), but no rule s i a → ()

for any i ∈ [1, m].
Example 2. Consider the tree automaton A, consisting of the transition rules:

p f - → (p 1 , p 2 ) q f - → (q 1 , q 2 ) q f - → (q 2 , q 1 ) p 1 g - → (p 1 ) p 1 a - → () q 1 g - → (q 1 ) q 1 a - → () p 2 g - → (p 2 ) p 2 b - → () q 2 g - → (q 2 ) q 2 b - → () It is not hard to see that L(A, p) = { f (g n (a), g m (b)) | n ≥ 0, m ≥ 0} and L(A,q) = { f (g n (a), g m (b)) | n ≥ 0, m ≥ 0} ∪ { f (g n (b), g m (a)) | n ≥ 0, m ≥ 0}.
To check L(A, p) ⊆ L(A,q), we start with (p, {q}).

An execution of the top-down inclusion algorithm is pictured below:

(p, {q})

((p 1 , p 2 ), {(q 1 , q 2 ), (q 2 , q 1 )}) (p 1 , {q 1 , q 2 }) (p 1 , {q 1 }) (p 2 , {q 2 }) (p 2 , {q 2 , q 1 }) ((), {()}) (p 1 , {q 1 , q 2 }) ((), {()}) (p 1 , {q 1 }) ((), {()}) (p 2 , {q 2 }) ((), {()}) (p 2 , {q 2 , q 1 }) f a g a g b g b g
The algorithm performs two types of moves: transitions and split actions. The arrows labeled by symbols f , g, a and b are transitions, for instance the arrow labeled by f takes p into the tuple (p 1 , p 2 ) by the transition p f -→ (p 1 , p 2 ) and {q} into the set of tuples {(q 1 , q 2 ), (q 2 , q 1 )}, by the transitions q f -→ (q 1 , q 2 ) and q f -→ (q 2 , q 1 ). However, the pair ((p 1 , p 2 ), {(q 1 , q 2 ), (q 2 , q 1 )}) is problematic because it asserts that L(A, p 1 ) × L(A, p 2 ) ⊆ L(A,q 1 ) × L(A,q 2 ) ∪ L(A,q 2 ) × L(A,q 1 ). Using several properties of the Cartesian product [9, Theorem 1] there are multiple ways to split this proof obligation into several simpler conjunctive subgoals. If at least one split move leads to a proof, then the inital proof obligation holds. The split move used above simultaneously considers (p 1 , {q 1 , q 2 }), (p 1 , {q 1 }), (p 2 , {q 2 }) and (p 2 , {q 2 , q 1 }), together asserting that L(A, p 1 ) ⊆ L(A,q 1 ) and L(A, p 2 ) ⊆ L(A,q 2 ). The other

options are: (1) (p 1 , {q 1 , q 2 }) (p 1 , {q 1 }), (p 1 , {q 2 }), and (p 2 , {q 2 , q 1 }); (2) (p 1 , {q 1 , q 2 }), (p 2 , {q 1 }), (p 1 , {q 2 }), and (p 2 , {q 2 , q 1 }); (3) (p 1 , {q 1 , q 2 }), (p 2 , {q 1 }), (p 2 , {q 2
}), and (p 2 , {q 2 , q 1 }). The algorithm does not expand nodes (p, S) with p ∈ S, for which inclusion holds trivially, or having a predecessor (p, S ) with S ⊆ S (enclosed in dashed boxes), since any counterexample that can be found from (p, S) could have been discovered from (p, S ).

Inference Rules and Proof Search

We now describe the set of inference rules using a Gentzen-style sequent calculus. We denote sequents as Γ ∆, where Γ and ∆ are sets of formulae, called antecedent [Γ] and consequent

[∆]. (R) Γ 1 ∆ 1 . . . Γ n ∆ n Γ ∆ side conditions . . . . C Γ p ∆ p
The commas in the sequents are read as set union and we avoid the enclosing brackets when writing down sequents. A sequent of the form p(x 0 ) q 1 (x 1 ), . . . , q n (x n ), where p, q 1 , . . . , q n are predicate symbols is said to be basic.

An inference rule r has #r ≥ 0 premises Γ i ∆ i , for i = 1, . . . , #r and a conclusion Γ ∆. A rule with no premises is called an axiom and we write for its empty premiss list. Additionally, certain inference rules may have a pivot Γ p ∆ p , which is always a sequent preceding the conclusion on the path from the root to itself. The path between the pivot and the conclusion of a rule is subject to a pivot constraint C, formally defined below.

For conciseness of presentation, we define inference rule schemata R, that are possibly infinite sets of inference rules sharing the same pattern. Without entering formal details, we assume that checking whether a given inference rule instance belongs to a given schema is straightforward and that there are finitely many instances of a certain schema for a given pivot and consequent. Definition 1. A derivation is a possibly infinite tree D = (V, v 0 , S, R, P), where V is a set of vertices, v 0 ∈ V is the root node, and for each vertex v ∈ V , S(v) is a sequent, R(v) is an inference rule schema and, if v = v 0 , then P(v) is the parent of v. In particular, for each v ∈ V \ {v 0 }, S(v) is a premiss of an instance of R(P(v)), whose conclusion is S(P(v)). A proof is a finite derivation, such that each leaf is the conclusion of an axiom.

This definition strays from the classical definition of cyclic proofs, viewed as graphs, rather than trees [START_REF] Brotherston | Cyclic proofs for first-order logic with inductive definitions[END_REF][START_REF] Brotherston | Sequent Calculus Proof Systems for Inductive Definitions[END_REF]. Below we recover the graph structure of a proof, by explicitly introducing backlinks:

Definition 2. Given a derivation D = (V, v 0 , S, R, P), a backlink is a pair (u, v) with u, v ∈ V such that u is the conclusion of the instance of R(u) and v is its pivot. A trace is a sequence of vertices τ = v 1 , v 2 , . . . such that, for all i ≥ 2, either v i-1 = P(v i ) or (v i-1 , v i ) is a backlink. A path of τ is any finite subsequence π = v i , . . . , v j such that i < j and v k-1 = P(v k ), for all k ∈ [i + 1, j]. If, moreover, (v j , v i ) is a backlink, then π is a direct path.
Backlinks generalize the relation between buds and companions in [START_REF] Brotherston | Cyclic proofs for first-order logic with inductive definitions[END_REF][START_REF] Brotherston | Sequent Calculus Proof Systems for Inductive Definitions[END_REF]. For a backlink (u, v), we call u a bud and v its companion, when u has no direct successors in the derivation tree. For now, the only rules introducing backlinks are axioms, hence all pivots will be companions. However we prefer to distinguish pivots from companions, for further extensions of the system with rules that may have a pivot without being axioms. Observe, moreover, that we require companions to always be ancestors of buds in the derivation. As shown in [START_REF] Brotherston | Sequent Calculus Proof Systems for Inductive Definitions[END_REF], this is not a restriction, because any cyclic proof can be transformed into an equivalent cyclic proof with this property 7 .

To define pivot constraints formally, for a path π = v 1 , . . . , v k with k ≥ 2, we denote by R(π) the sequence R(v 1 ), . . . , R(v k-1 ) of inference rule schemata that are applied on π. The pivot constraint C of a rule schema R is a set of finite sequences of rule schemata, such that, if π is the direct path from the pivot of (the instance of) r to its conclusion, then R(π) ∈ C.

Given a system of inductive definitions S and a set of predicates p, q 1 , . . . , q k ∈ Pred of equal arities, a set of inference rule schemata R is (i) sound if, for any proof D = (V, v 0 , S, R, P) using the inference rules of R , with S(v 0 ) = p(x) q 1 (x), . . . , q n (x), we have p |= S q 1 , . . . , q n , and (ii) complete if p |= S q 1 , . . . , q n implies the existence of a proof D = (V, v 0 , s, r, p) using the inference rules of R , where S(v 0 ) = p(x) q 1 (x), . . . , q n (x). The following general result will be used next, in the proof of soundness for our particular set of inference rules.

Proposition 1. Any infinite trace of a proof D contains infinitely many direct paths. A strategy is a set S of sequences of inference rule schemata. A sequence σ is a prefix of S if there exists another sequence τ such that στ ∈ S. A derivation D [proof] is an S-derivation [S-proof] if R(π) is a prefix of S, for each path π of D.

Algorithm 1 Proof search semi-algorithm.

data structure: Node(Seq, CList, Parent, Rule), where:

• Seq is the sequent that labels the node,

• CList is the list of children nodes,

• Parent is the link to the parent of the node,

• Rule is the inference rule with consequent Seq. input:

• a system of inductive definitions S,

• a sequent p(x) q 1 (x), . . . , q n (x),

• a set R of inference rule schemata and a strategy S output: a proof D = (V, v 0 , S, R, P) such that S(v 0 ) = p(x) q 1 (x), . . . , q n (x)

1: Root ← Node(p(x) q 1 (x), . . . , q n (x), [], nil, nil) 2: WorkList ← {Root} 3: while WorkList = / 0 do 4:
remove N from WorkList and match it with Node(Γ ∆, CList, P, R)

5:
let π be the path between Root and N 6:

let R N ⊆ R be the inference rule schemata applicable on N.Seq and π 7:

let R 0 N ⊆ R N be the subset of R N with empty premiss lists

8: if R(π) • R is a valid prefix of S for some R ∈ R 0 N then 9:
N.Rule ← R 10:

mark N as closed 11:

if N not closed and R(π

) • R is a valid prefix of S for some R ∈ R N \ R 0 N then 12:
let r be an instance of R such that N.Seq is the consequent of r 13:

for each premiss Γ ∆ of r do append N to N.CList if N.CList is empty then mark N as closed Given an input sequent p(x) q 1 (x), . . . , q n (x), a set R of inference rules and a strategy S, the generic proof search semi-algorithm (1) uses a worklist iteration to build a derivation of p(x) q 1 (x), . . . , q n (x). When a sequent is removed from the worklist, it chooses (non-deterministically) an inference rule and an instance whose consequent matches the current sequent, if one exists. To enhance the chance of termination, the nodes matching an axiom are considered eagerly (line 8). Since we assumed that the only rules introducing backlinks are axioms, the treatment of axioms takes also care of the coverage of buds by companions. It is not difficult to show that, if an S-proof of the input sequent p(x) q 1 (x), . . . , q n (x) exists, then semi-algorithm (1) will output that proof.

Proof Rules for Entailment

The inference rules for proving entailments between inductively defined predicates are essentially of one of the three types: unfolding (U), reduction (R) and split (S). In addition, we consider two axiom schemata, one for sequents that are valid no matter how the predicates are interpreted (AX) and another one for infinite descent (ID). We call URS and URSID the sets of inference rule schemata introduced below, without and with the (ID) rule, respectively. A sequent Γ ∆ stands for the (proof obligation of the) entailment Γ |= ∃ y∈FV(∆)\FV(Γ) y . ∆. For a compact presentation of the rules, we omit the existential quantifiers. Moreover, we write (Γ i ∆ i ) n i=1 for Γ 1 ∆ 1 . . . Γ n ∆ n . Throughout the section we assume a system S of inductive definitions.

The inference rules (LU) and (RU) unfold a predicate atom p(x) occurring in the antecedent or the consequent of a sequent Γ ∆, respectively. By unfolding, we essentially mean the replacement of p(x) with the bodies of the rules of its inductive definition p(x)

:= S R 1 (x, y 1 ) | . . . | R n (x, y n ): (LU) (R i (x, y i ), Γ \ p(x) ∆) n i=1 Γ ∆ p(x)∈Γ y 1 ,...,y n fresh variables (RU) Γ R 1 (x, y 1 ), . . . , R n (x, y n ), ∆ \ p(x) Γ ∆ p(x)∈∆ y 1 ,..

.,y n fresh variables

Observe that the left unfolding yields a set of premises, one for each R i , whereas the only premiss of the right unfolding is obtained by replacing p(x) in the consequent of the conclusion with a set of conjunctions R i , in which the subgoal variables of each R i are fresh. The inference rules (RD) eliminate the constraints from both the antecedent and consequent of the conclusion. The existentially quantified variables from the consequent are eliminated using a finite subset of the set Sk(φ,

ψ i ) def = {θ : y i → T Σ (x, x 1 , . . . , x n ) | φ |= ψθ} of
substitutions, mapping the existentially quantified variables of ψ i (x, y i ) to Skolem terms over the free variables of φ(x, x 1 , . . . , x n ). These terms witness the entailments between the constraints of the antecedent and those of the consequent.

(RD) p 1 (x 1 ), . . . , p n (x n ) {Q j θ | θ ∈ S j } i j=1 φ(x, x 1 , . . . , x n ), p 1 (x 1 ), . . . , p n (x n ) {ψ j (x, y j ) ∧ Q j (y j )} k j=1 ( k j=1 y j ) ∩ (x ∪ i=1 x i )= / 0 φ|= i j=1 ∃ y∈y j y . ψ j φ |= k j=i+1 ∃ y∈y j y . ψ j S j ⊆Sk(φ,ψ j ),∀ j∈[1,i] (∧R) (Γ p i (x) ∧ Q , ∆) n i=1 Γ p 1 (x) ∧ . . . ∧ p n (x) ∧ Q , ∆
Because (RD) can create conjunctions of predicate atoms with the same arguments, every application of (RD) will be followed by a cleanup of the premiss consequents, using a right introduction rule (∧R).

To understand the relation between proofs and tree automata language inclusion checking, we view a pair (p, {q 1 , . . . , q n }) in the top-down antichain algorithm (Example 2) as a sequent p(x) q 1 (x), . . . , q n (x). In the algorithm of Example 2, the (LU), (RU) and (RD) rules are combined in a single transition move. This is natural because the transition rules of tree automata are controlled uniquely by the function symbols labeling the root of the current input term. Since function symbols can only be compared via equality, the constraints within the predicate rules of a tree automata match unambiguously. For instance, we have x ≈ f (x 1 , x 2 ) |= ∃y 1 ∃y 2 . x ≈ g(y 1 , y 2 ) if and only if f and g are the same function symbol, in which case the only substitution witnessing the validity of the entailment is θ(x i ) = y i , for i = 1, 2. However, when considering generic first-order constraints, matching amounts to discovering non-trivial substitutions that prove an entailment between existentially quantified formulae in the logic in which the constraints are written. Moreover, the matching step implemented by the (RD) rule is crucial for proving completeness of the set of inference rules, by generalizing from the simple case of tree automata constraints and discovering general properties of the set of constraints that allow matching to be complete ( §5.1).

Next, the splitting rules (SP) generalize the split moves of the inclusion algorithm (Example 2) by breaking a sequent p 1 (x 1 ), . . . ,

p n (x n ) Q 1 (x 1 , . . . , x n ), . . . , Q n (x 1 , . . . , x n ) into basic sequents. (SP) p ī j (x) {q ī j (x) | ∈ [k], f j (Q ) = ī j } n k j=1 p 1 (x 1 ), . . . , p n (x n ) Q 1 (x 1 , . . . , x n ), . . . , Q k (x 1 , . . . , x n ) ∀i, j∈[1,n] . x i ∩x j = / 0, ī∈[1,n] n k Q i = n j=1 q i j (x j ),Q i = q i 1 ,...,q i n F (Q 1 ,...,Q k )={ f 1 ,..., f n k } Given tuples {Q 1 , . . . , Q k } consisting of n ≥ 1 predicate atoms each, a choice function f maps each Q i into an index f (Q i ) ∈ [1, n]
corresponding to a position in the tuple. We denote by

F (Q 1 , . . . , Q k ) the set of choice functions, of cardinality n k ≤ n ||Pred|| n . Given a tuple ī ∈ [1, n] n k , associating a value in [1, n] to each choice function f ∈ F (Q 1 , . . . , Q k ),
there exists an application of (SP) generating n k premises with antecedent p ī j (x), j ∈ [1, n k ] and consequent consisting of all predicate atoms q ī j (x), ∈ [1, k] obtained from predicates at position ī j in the tuples Q which are mapped to ī j by f j .

Finally, we introduce two axiom schemata. First, the rules (AX) close the current branch of the proof if the sequent can be proved using a decision procedure for the underlying constraint logic, which treats the predicates as uninterpreted boolean functions. For the tree automata language inclusion algorithm, this rule is similar to encountering a pair (p, S), with p ∈ S.

(AX) Γ ∆ Γ|=∃ y∈FV(∆)\FV(Γ) y . ∆ (ID) Γθ ∆ θ θ flat injective substitution ∆⊆∆ . . . . URSID * •LU•URSID *
Γ ∆ Second, the infinite descent rules (ID) are the only rules to introduce backlinks, from the conclusion Γθ ∆ θ to a predecessor (pivot) vertex labeled with Γ ∆. The pivot condition URSID * • LU • URSID * requires that a vertex labeled with a rule (LU) occurs on the direct path between the pivot and the conclusion. As we explain next, this condition suffices to guarantee soundness of URSID.

We recall that the inclusion algorithm of Example 2 stops expanding a branch in the search tree whenever it has discovered a pair (p, S ) that has a predecessor (p, S), with S ⊆ S . In analogy, the (ID) rules close the current branch of the derivation, when the last sequent Γθ ∆ θ has a predecessor Γ ∆ with ∆ ⊆ ∆ , modulo a substitution θ. For technical reasons, related to the soundness of URSID, we consider only flat injective such substitutions, when applying (ID).

Example 3. Consider the system S A , corresponding to the tree automaton from Example 2:

p(x) := S A x ≈ f (x 1 , x 2 ), p 1 (x 1 ), p 2 (x 2 ) q(x) := S A x ≈ f (x 1 , x 2 ), q 1 (x 1 ), q 2 (x 2 ) p 1 (x) := S A x ≈ g(x 1 ), p 1 (x 1 ) | x ≈ a | x ≈ f (x 1 , x 2 ), q 2 (x 1 ), q 1 (x 2 ) p 2 (x) := S A x ≈ g(x 1 ), p 2 (x 1 ) | x ≈ b q 1 (x) := S A x ≈ g(x 1 ), q 1 (x 1 ) | x ≈ a q 2 (x) := S A x ≈ g(x 1 ), q 2 (x 1 ) | x ≈ b
Part of the proof for p(x) q(x) is shown below. Note the similarities with the algorithm of Example 2, whose transition moves correspond to subtrees of the proof rooted in an (LU) node whose children are successively labeled with (RU) or (RD).

p(x) q(x) x ≈ f (x 1 , x 2 ), p 1 (x 1 ), p 2 (x 2 ) q(x) x ≈ f (x 1 , x 2 ), p 1 (x 1 ), p 2 (x 2 ) x ≈ f (y 1 , y 2 ) ∧ q 1 (y 1 ) ∧ q 2 (y 2 ), x ≈ f (y 1 , y 2 ) ∧ q 2 (y 1 ) ∧ q 1 (y 2 ) p 1 (x 1 ), p 2 (x 2 ) q 1 (x 1 ) ∧ q 2 (x 2 ), q 2 (x 1 ) ∧ q 1 (x 2 ) [ †] p 1 (x) q 1 (x), q 2 (x) p 1 (x) q 1 (x) p 2 (x) q 2 (x) p 2 (x) q 2 (x), q 1 (x) LU RU RD SP [ †] p 1 (x) q 1 (x), q 2 (x) ( * )
x ≈ a q 1 (x), q 2 (x)

x ≈ a x ≈ a, q 2 (x), x ≈ g(y 1 ) ∧ q 1 (y 1 )

x ≈ g(x 1 ), p 1 (x 1 ) q 1 (x), q 2 (x)

x ≈ g(x 1 ), p 1 (x 1 ) x ≈ a, q 2 (x), x ≈ g(y 1 ) ∧ q 1 (y 1 )

x ≈ g(x 1 ), p 1 (x 1 ) x ≈ a, x ≈ b, x ≈ g(y 1 ) ∧ q 1 (y 1 ), x ≈ g(y 1 ) ∧ q 2 (y 1 )

p 1 (x 1 ) q 1 (x 1 ), q 2 (x 1 ) ( * ) LU RU AX RU RU RD ID
The split move of the algorithm corresponds to the single node labeled (SP), whose consequent consists of conjunctions of Q 1 = (q 1 , q 2 ) and Q 2 = (q 2 , q 1 ). The set of choice functions is

F (Q 1 , Q 2 ) = { f 1 = {(Q 1 , 1), (Q 2 , 1)}, f 2 = {(Q 1 , 1), (Q 2 , 2)}, f 3 = {(Q 1 , 2), (Q 2 , 1)}, f 4 = {(Q 1 , 2), (Q 2 , 2)}}. Out of the 16 index choice tuples for F (Q 1 , Q 2 ), only (1, 1, 1, 2), (1, 1, 2, 2), (1, 2, 1, 2) and (1, 2, 2, 2)
are relevant. To obtain the above proof, we chose ī = (1, 1, 2, 2). We mark with ( * ) the pivot required for the application of the (ID) rule above. Observe that the pivot constraint is satisfied because the pivot is the conclusion of a (LU) rule.

Soundness of URSID

We establish soundness of the URSID set of inference rules, by first proving the local soundness of URS. More precisely, for every rule that is an instance of a rule schema R ∈ URS, the validity of all premises implies the validity of the conclusion. For technical reasons that will become clear in a moment, Lemma 1 below proves the equivalent contrapositive statement.

Let S be a fixed system, U a universe and I an interpretation, throughout this section. For a formula φ and an assignment X , that maps each predicate symbol p occurring in φ to a set X (p) ⊆ U #(p) , we denote by [[φ]] X the set of valuations ν of FV(φ), such that (U, I , ν) |= φ, when each predicate atom p(x) is true if and only if ν(x) ∈ X (p). For conciseness, we omit the formal definition. Moreover, given a set F consisting of predicate atoms q 1 (x 1 ), . . . , q n (x n ) and several other formulae, not containing predicate atoms, for a valuation ν of FV(F), we denote by M (F, ν) the multiset of stage numbers sn(q 1 , ν(x 1 )), . . . , sn(q n , ν(x n )) ∈ N. It is easy to see that the antecedent of any sequent Γ ∆ that occurs in a URS derivation consists only of predicate atoms and constraints, thus M (Γ, ν) is defined, for each valuation ν of FV(Γ). Before giving the local soundness result (Lemma 1), we briefly recall the definition of the Manna-Dershowitz multiset order for natural numbers: Definition 3 ( [START_REF] Dershowitz | Proving termination with multiset orderings[END_REF]). Given multisets M, N ⊆ N, we write N ≤ † M if and only if either M = N, or there exists a non-empty finite multiset X ⊆ M and a (possibly empty) multiset Y , where for all y ∈ Y there exists x ∈ X such that y < x and N = (M \ X) ∪Y .

It is known that the ≤ † order is well-founded, since ≤ is well-founded on N [START_REF] Dershowitz | Proving termination with multiset orderings[END_REF].

Lemma 1. For each instance of an inference rule schema R ∈ URS, with conclusion Γ ∆ and premises (Γ i ∆ i ) n i=1 and for each valuation

ν of FV(Γ) such that ν ∈ [[ Γ]] µS \ [[∃ y∈FV(∆)\FV(Γ) y . ∆]] µS , there exists a valuation ν i ∈ [[ Γ i ]] µS \ [[∃ y∈FV(∆ i )\FV(Γ i ) y . ∆ i ]] µS such that M (Γ, ν) ≥ † M (Γ i , ν i ), for some i ∈ [1, n]. Moreover, if R = LU then M (Γ, ν) > † M (Γ i , ν i ).
We introduce a relation between valuations and write ν ν if and only if ν is a countermodel of the conclusion of an inference rule and ν is the countermodel of one of its premises, whose existence is asserted by Lemma 1.

To tackle the soundness of URSID, we must show that a countermodel cannot be indefinitely propagated along an infinite trace through the proof, going via backlinks. A first technical point that must be addressed is the extension of the relation to the backlinks introduced by the (ID) inference rules. Let Γ ∆ be the conclusion and Γ ∆ be the pivot of an (ID) rule. Now suppose that ν ∈ [[ Γ]] µS \ [[∃ y∈FV(∆)\FV(Γ) y . ∆]] µS is a countermodel valuation of the conclusion. By the side condition, we have Γ = Γ θ and ∆ = ∆ θ, for a set ∆ ⊆ ∆ , where θ is a flat and injective substitution. Since the restriction of θ to the set FV(Γ θ) ∪ FV(∆ θ) is bijective, it has an inverse and ν

• θ -1 is a countermodel for Γ ∆ , i.e. ν • θ -1 ∈ [[ Γ ]] µS \ [[∃ y∈FV(∆ )\FV(Γ ) y . ∆ ]] µS 8 . Moreover, because θ is flat, we have M (Γ, ν) = M (Γ , ν • θ).
Now suppose, for a contradiction, that there exists a proof D = (V, v 0 , S, R, P) for an invalid sequent S(v 0 ) = Γ 0 ∆ 0 . Then we can build an infinite trace τ = u 0 , u 1 , . . . through D, and a sequence of valuations ν 0 ν 1 . . ., such that ν i is a countermodel for S(v i ) = Γ i ∆ i , for all i ≥ 0. Moreover, by Lemma 1 and the extended definition of for backlinks, we have that M (Γ i , ν i ) ≥ † M (Γ i+1 , ν i+1 ), for all i ≥ 0. But, by Proposition 1, τ must contain an infinite number of direct paths. Since, by the pivot condition of (ID), any direct path has at least one application of (LU), by the second point of Lemma 1, we obtain an infinitely decreasing sequence of multisets M (Γ j 1 , ν j 1 ) > † M (Γ j 2 , ν j 2 ) > † . . ., where j 1 < j 2 < . . ., thus contradicting the well-foundedness of ≥ † . Hence there is no countermodel to start with and the entailment Γ 0 |= ∃ y∈FV(∆ 0 )\FV(Γ 0 ) y . ∆ 0 must hold.

Theorem 2. For any URSID proof D = (V, v 0 , S, R, P), such that S(v 0 ) = Γ ∆, the entailment Γ |= ∃ y∈FV(∆)\FV(Γ) y . ∆ holds.

Relative Completeness of URSID

As previously discussed, the undecidability of the entailment problem (Theorem 1) excludes the possibility of having a complete set of inference rules in which every valid entailment has a finite proof. In this section, we identify a class of inductive definition systems for which URSID is complete and the entailment problem is decidable. Unlike with most decidable fragments of first (second) order logic, we do not impose syntactic restrictions on the form of the inductive definitions in the system. Rather, we give three conditions that must be satisfied by all quantifier-free constraints in the inductive rules. Moreover, we tackle the decidability of these conditions in the Herbrand interpretation of first-order logic and give several complexity upper bounds for the problem of checking whether a given system complies with them. Before giving the completeness proof under these restrictions, we suggest a stronger but easy-to-check syntactic criterion.

Restricting the Set of Constraints

The following definitions introduce sufficient conditions that ensure completeness of URSID. Effectively checking these conditions for a given inductive system is subject to the existence of a decision procedure for the ∃ * ∀ * fragment of the logic in which the constraints are written, i.e. the set of prenex normal form sentences of the form ∃x 1 . . . ∃x n ∀y 1 . . . ∀y m . φ, where φ is a quantifier-free boolean combination of equality and interpreted predicate atoms. For first-order logic with the Herbrand interpretation, this problem, known as disunification, has been shown decidable in [START_REF] Comon | Equational problems and disunification[END_REF], with tighter complexity bounds given in [START_REF] Pichler | On the complexity of equational problems in cnf[END_REF]. In the rest of this section, we assume a fixed universe U and interpretation I .

The first restriction requires that, given any models for the subgoals of an inductive rule, it must be possible to find an all-encompassing model that also satisfies the constraint of the rule. This restriction We give an upper bound for the complexity of the problem whether a given inductive system has the fvi property, in the Herbrand interpretation of constraints. It is unclear, for now, whether this bound can be tightened, because the exact complexity of the satisfiability of equational problems is unknown 12 . Lemma 3. The problem "given an inductive system S, does S have the fvi property?" is in NEXPTIME in the Herbrand interpretation. If there exists a constant K > 0, independent of the input, such that for each constraint φ(x, x 1 , . . . , x n ), with goal variables x and subgoal variables n i=1 x i , respectively, we have ||x i || ≤ K, then the problem is in NP.

The third and last condition required for the completeness of URSID is also related to the elimination of constraints from sequents. Intuitively, we do not allow two constraints to overlap, having at least one model in common, without one entailing the other. Definition 6. An inductive system S is non-overlapping if and only if, for any two constraints φ(x, x 1 , . . . , x n ) and ψ(x, y 1 , . . . , y m ) in S, with goal variables x and subgoal variables n i=1 x i and m j=1 y j respectively, φ ∧ ψ is satisfiable only if φ |= ∃y 1 . . . ∃y m . ψ.

For a non-overlapping system, if φ(x, x 1 , . . . , x n )∧ψ(x, y 1 , . . . , y m ) is a satisfiable conjunction of constraints, then the formulae ∃x 1 . . . ∃x n . φ and ∃y 1 . . . y m . ψ are equivalent. It unclear, for now, whether this condition can be lifted by considering, e.g. disjoint conjunctive minterms consisting of constraints and their negations. This is mainly because introducing negative constraints might affect the nonfiltering property of the system (Definition 4). Lemma 4. The problem "given a first order inductive system S, is S non-overlapping?" is in NP in the Herbrand interpretation.

Example 6. The S A inductive system from Example 3 is non-overlapping. Consider, for instance, the constraints x ≈ f (x 1 , x 2 ) and x ≈ f (y 1 , y 2 ). Then x ≈ f (x 1 , x 2 ) ∧ x ≈ f (y 1 , y 2 ) is satisfiable and x ≈ f (x 1 , x 2 ) |= ∃y 1 ∃y 2 . x ≈ f (y 1 , y 2 ) holds. However, if we take the constraints x ≈ f (x 1 , x 2 ) and x ≈ g(y 1 ), then x ≈ f (x 1 , x 2 ) ∧ x ≈ g(y 1 ) is unsatisfiable.

A Syntactic Completeness Criterion

The three conditions above (Definitions 4, 5, 6) are of technical nature and meant for machine rather than human checking. That is, given a particular instance of the entailment problem, we show the existence of algorithms that answer yes/no to the question whether URSID is complete for that particular instance -in case of a negative answer, the proof search semi-algorithm 1 is not bound to terminate. However, it is desirable to also have a stronger but easy-to-check criterion. The following definition introduces such a criterion, and the next lemma proves that every inductive defnition system that complies with it has a decidable entailment problem.

Given terms t and u, a substitution θ is a unifier for t and u if and only if t = uθ. Observe that the relation "t and u have a unifier" is a preorder but not an equivalence. We assume, in the rest of this section, the Herbrand interpretation of function symbols. Definition 7. An inductive definition system S is said to be rooted if and only if each constraint is of the form x∈x x ≈ t x , where x are the goal variables, each t x is a term using subgoal variables only and, moreover, for any two terms t x and u x that occur in different constraints φ(x, x 1 , . . . , x n ) and ψ(x, y 1 , . . . , y m ), with subgoal variables n i=1 x i and m j=1 y m , respectively, if t x and u x have a unifier θ, then for each j ∈ [1, m] there exists i ∈ [1, n] such that (FV(u) ∩ y j )θ = FV(t) ∩ x i .

Observe that rooted systems are strictly more expressive than the inductive definitions of tree automata. For instance, the rooted system from Example 3 defines non-regular sets of terms.

z 1 ≈ a, z 1 ≈ a ∧ z 2 ≈ a, z 2 ≈ b z 1 ≈ f (u 1 ) ∧ z 2 ≈ f (u 2 ) ∧ o(u 1 , u 2 ), o(z 2 , z 1 ) z 1 ≈ f (v 1 ), z 2 ≈ f (v 2 ), n(v 1 , v 2 ) e(z 1 , z 2 ), o(z 2 , z 1 ) z 1 ≈ f (v 1 ), z 1 ≈ a ∧ z 2 ≈ b, z 2 ≈ f (v 2 ), z 1 ≈ f (w 1 ) ∧ z 2 ≈ f (w 2 ) ∧ o(w 1 , w 2 ), n(v 1 , v 2 ) z 2 ≈ f (w 1 ) ∧ z 1 ≈ f (w 2 ) ∧ e(w 1 , w 2 ) [ †] n(v 1 , v 2 ) e(v 2 , v 1 ), o(v 1 , v 2 )
. . . The derivation rooted in the ( †) is a symmetric copy of the derivation rooted in the ( √ ) node and ending with ( †). As usual, we mark the conclusion of (ID) and its companion with ( * ). The pivot constraint is satisfied because the pivot is the conclusion of an (LU) rule.

The following shows that rooted systems always non-filtering, non-overlapping and have the fvi property. As shown in the next section, this provides a sufficient completeness criterion and, moreover, an argument for the decidability of the entailment problem within this class of systems. Proposition 2. Any rooted system is non-filtering, non-overlapping and has the fvi property.

Completeness of URSID

We prove that URSID is complete for entailments between predicates in inductive systems that are nonfiltering, non-overlapping and have the fvi property ( §5.1). A derivation is said to be maximal if it cannot be extended by an application of an inference rule, and irreducible if it cannot be rewritten into a smaller derivation of the same sequent by an (ID) application. Note that the proof search semi-algorithm (1) generates only irreducible derivations, because (ID) is always applied before any other inference rules.

A derivation D is structured if, on each path of D, between any two consecutive applications of (LU) there exists an application of (RD). Intuitively, unstructured derivations constitute poor candidates for proofs. For instance, a derivation consisting only of applications of (LU) rules will only grow the size of

  a quantifier-free formula φ, we write (U, I , ν) |= φ when the formula obtained from φ by replacing each function symbol f by f I and each variable x by ν(x) is logically equivalent to . The interpretation of quantifiers is standard: (U, I , ν) |= ∃x . φ if and only if (U, I , ν[x ← u]) |= φ for some value u ∈ U, where ν[x ← u] is the valuation that assigns x to u and behaves like ν elsewhere.

7

  Such proofs are said to be in cycle normal form [3, Definition 6.2.1].

14 :N

 14 ← Node(Γ ∆ , [], N, nil) 15:

Example 7 . 1 )

 71 Consider the system S r below:n(x 1 , x 2 ) := S r x 1 ≈ a ∧ x 2 ≈ b | x 1 ≈ f (y 1 ) ∧ x 2 ≈ f (y 2 ), n(y 2 , y 1 ) m(x) := S r x ≈ g(y 1 , y 2 ), n(y 1 , y 2 ) e(x 1 , x 2 ) := S r x 1 ≈ a ∧ x 2 ≈ b | x 1 ≈ f (y 1 ) ∧ x 2 ≈ f (y 2 ), o(y 1 , y 2 ) o(x 1 , x 2 ) := S r x 1 ≈ f (y 1 ) ∧ x 2 ≈ f (y 2 ), e(y 1 , y 2 ) p(x) := S r x ≈ g(y 1 , y 2 ), e(y 1 , y 2 ) | x ≈ g(y 1 , y 2 ), o(y 2 , yIt is easy to see that S r is rooted and, moreover, that µS r (m) = µS r (p) = g( f 2n (a),f 2n (b)) | n ≥ 0 ∪ g( f 2n+1 (b), f 2n+1 (a)) | n ≥ 0 ,which is not a regular tree language. Below we sketch a URSID proof for the sequent m(x) p(x):m(x) p(x) x ≈ g(z 1 , z 2 ), n(z 1 , z 2 ) p(x) x ≈ g(z 1 , z 2 ), n(z 1 , z 2 ) x ≈ g(y 1 , y 2 ) ∧ e(y 1 , y 2 ), x ≈ g(y 1 , y 2 ) ∧ o(y 2 , y 1 ) [ √ ] n(z 1 , z 2 ) e(z1 , z 2 ), o(z 2 , z 1 ) ( * ) z 1 ≈ a, z 2 ≈ b e(z 1 , z 2 ), o(z 2 , z 1 )

n(v 1 ,

 1 v 2 ) e(v 1 , v 2 ), o(v 1 , v 2 ) ( * )

  Terms are defined recursively: any constant or variable is a term and f (t 1 , . . . ,t #( f ) ) is a term if t 1 , . . . ,t #( f ) are terms. We write T Σ (x) for the set of terms with function symbols in Σ and variables in x. A ground term is a term without variables and T Σ denotes the set of ground terms (we drop the subscript when it is clear from the context). An atom is either an equality t 1 ≈ t 2 , or a predicate atom p(t 1 , . . . ,t #(p) ), where t 1 ,t 2 , . . . ,t #(p) are terms. A formula is a quantified boolean combination of atoms. The size of a formula is the number of symbols needed to write it down.

Assuming a countable vocabulary and a complete finite proof system, since any entailment has either a countermodel or a proof, one could decide its validity by alternating the search for a countermodel with that of a proof.

A rule with a false constraint is removed and ({φ 1 ∨ . . . ∨ φ n , Q } , p(x)) is replaced by ({φ 1 , Q } , p(x)), . . . , ({φ n , Q } , p(x)).

See [15, Theorem 1.3.2].

See[START_REF] Serban | Automated Reasoning in Separation Logic with Inductive Definitions[END_REF] Theorem 1.3.4].

Several definitions of graph automata exist but none has a decidable inclusion problem.

See, e.g. [6, Corollary 1.7.9].

R.Iosif and C. Serban

Because (U, I , ν) |= φ ⇐⇒ (U, I , ν • θ -1 ) |= φθ, for an arbitrary formula φ and a bijective substitution θ.

Converting a formula into CNF requires exponential time at most, thus NEXPTIME is an upper bound.

Conclusions and Future Work

We present a cyclic proof system for entailments between inductively defined predicates written using first-order logic, based on Fermat's principle of Infinite Descent. The soundness of this principle is coined by a semantic restriction on the constraints of the inductive system, that asks that models generated by unfoldings decrease in a well-founded domain. On the other hand, completeness is applicable under three additional semantic restrictions on the set of constraints. In general, all these restrictions are decidable, with computational complexities that depend on the logical fragment in which the constraints of the inductive system are written.

is necessary because lifting it leads, in general, to the undecidability of the entailment problem, as it is the case for tree automata with equality and disequality constraints 9 . Definition 4. A system of inductive definitions S is non-filtering if and only if, for every rule ({φ(x, x 1 , . . . , x n ), q 1 (x 1 ), . . . , q n (x n )}, p(x)) ∈ S, for all i ∈ [1, n] and all v i ∈ µS(q i ), there exists a valuation ν, such that ν(x i ) = v i and (U, I , ν) |= φ.

Unfortunately, this condition is undecidable for Herbrand models, as showed by the following: Lemma 2. The problem "given an inductive system S, is S non-filtering?" is undecidable in the Herbrand interpretation.

This negative result suggests adopting a stronger condition. Namely, we require that, for each rule ({φ(x, x 1 , . . . , x n ), q 1 (x 1 ), . . . , q n (x n )}, p(x)), the formula ∀x 1 . . . ∀x n ∃x . φ(x, x 1 , . . . , x n ) is valid, or equivalently, that ∃x 1 . . . ∃x n ∀x . ¬φ(x, x 1 , . . . , x n ) is unsatisfiable. Because each constraint φ is a conjunction of equalities s ≈ t and disequalities ¬(s ≈ t) between terms, ¬φ is a disjunction of equalities and disequalities, trivially in conjunctive normal form. Since the satisfiability of the formulae ∃x∀y . φ(x, y), with φ in conjunctive normal form, is NP-complete 10 , the above validity problem is in co-NP.

Example 4. The S A system from Example 3 is non-filtering. If, for instance, the rules for p were changed to p(x) :

, then S A would become filtering, as all the subgoals models for which the values of x 1 and x 2 differ would be rejected by the new predicate rule.

The second restriction guarantees that all constraints can be eliminated from a sequent, by instantiating the free variables of the consequent, that do not occur in the antecedent, using finitely many substitutions that map onto the subgoal variables from the antecedent. Given a sequent such as, e.g. φ(x, x 1 , . . . , x n ), p 1 (x 1 ), . . . , p n (x n ) ∃y 1 . . . ∃y m . ψ(x, y 1 , . . . , y m ) ∧ q 1 (y 1 ) ∧ . . . ∧ q m (y m ) if the entailment φ |= ∃y 1 . . . ∃y m . ψ is valid, the (RD) inference rule replaces it with a finite number of sequents p 1 (x 1 ), . . . , p n (x n ) {q 1 (y 1 θ) ∧ . . . ∧ q m (y m θ) | θ ∈ S}, where φ |= ψθ, for each substitution θ.

This elimination of constraints from sequents is generally sound, but incomplete. The above entailment is valid if φ(x, x 1 , . . . , x n ) |= ψ (x, x 1 , . . . , x m ), where ψ is obtained from ψ by replacing each y ∈ y 1 ∪ . . . ∪ y m with a Skolem function symbol f y (x, x 1 , . . . , x n ) not occurring in φ or ψ 11 . A complete inference rule would have to consider all possible interpretations of these Skolem witnesses. This is impossible in general, as their definitions are not bound to any particular form.

To ensure completeness of URSID, we require that these functions are defined as flat substitutions ranging over x ∪ n i=1 x i . This condition ensures that there are finitely many possible interpretations of these Skolem witnesses. Definition 5. A system of inductive definitions S has the finite instantiation property if and only if, for any two constraints φ(x, x 1 , . . . , x n ) and ψ(x, y 1 , . . . , y m ) from S, with goal variables x and subgoal variables n i=1 x i and m j=1 y j , respectively, the set Sk(φ, ψ)

Moreover, S has the finite variable instantiation (fvi) property iff for all j ∈ [1, m] there exists i ∈ [1, n] such that y j θ = x i , for each θ ∈ Sk(φ, ψ).

Example 5. The S A inductive system from Example 3 has the fvi property. Take, for instance, the constraints φ ≡ x ≈ f (x 1 , x 2 ) and ψ ≡ x ≈ f (y 1 , y 2 ). The entailment φ |= ∃y 1 ∃y 2 . ψ is witnessed by a single substitution θ with θ(x 1 ) = y 1 and θ(x 2 ) = y 2 , which means that Sk(φ, ψ) = {θ}. the left-hand sides of the sequents, without making progress towards or a countermodel. Observe that each subtree of a structured derivation is also structured. We denote by D(Γ ∆) the set of irreducible, maximal and structured derivations D = (V, v 0 , S, R, P) whose root nodes are labeled by S(v 0 ) = Γ ∆.

Lemma 5. If S has the fvi property, then the following hold:

1. any irreducible and structured derivation is finite, and 2. for any sequent Γ ∆, the set D(Γ ∆) is finite.

Next, we prove an invariant on the shape of the sequents occurring in a proof of a basic sequent. Definition 8. A set F = {φ 1 , . . . , φ n , q 1 (x 1 ), . . . , q m (x m )} is tree-shaped if and only if φ 1 , . . . , φ n are constraints, q 1 (x 1 ), . . . q m (x m ) are predicate atoms, and there exist trees t 1 , . . . ,t k such that:

• each node labeled with a constraint φ i (y, y 1 , . . . , y n ) in some tree t , ∈ [1, k] has exactly n children and for all j ∈ [1, n], the j-th child is labeled either (i) with a constraint whose goal variables are y j , or (ii) with a predicate atom q k (y j ), and • a predicate atom q i (x i ) may only be a leaf in a tree t j , for some j ∈ [1, k].

Tree-shaped sets can be uniquely represented by trees labeled with formulae, thus we use sets of trees instead of sets of formulae interchangeably. Lemma 6. Given an inductive system S and the predicate atoms p(x), q 1 (x), . . . , q n (x), in every sequent Γ ∆ such that p(x) q 1 (x), . . . , q n (x) ; Γ ∆, Γ is a tree-shaped set and ∆ consists of finite conjunctions of tree-shaped sets.

The following lemma characterizes the cases in which the root of a derivation is labeled by an invalid sequent, from which a countermodel can be extracted. This is crucial in establishing our completeness result (Theorem 3). We write Γ ∆ ; Γ ∆ iff Γ ∆ occurs in a derivation from D(Γ ∆).

Lemma 7. Given a non-filtering and non-overlapping inductive definition system S with the fvi property, the predicate atoms p(x), q 1 (x), . . . , q n (x), and a sequent Γ ∆ such that p(x) q 1 (x), . . . , q n (x) ; Γ ∆, if every derivation D ∈ D(Γ ∆) contains a leaf labeled with sequent with empty consequent, then there exists a valuation ν ∈

The following theorem proves that URSID is complete and provides a proof search strategy.

Theorem 3. Given a non-filtering, non-overlapping inductive system S with the fvi property, let p, q 1 , . . . , q n be predicates symbols occurring in S. Then the entailment p |= S q 1 , . . . , q n holds only if the sequent p(x) q 1 (x), . . . , q n (x) has an S-proof with the set of inference rules URSID, where S is defined by the regular expression (LU

Proof. Since S is non-filtering and non-overlapping, and moreover, it has the fvi property and also p |= S q 1 , . . . , q n , by Lemma 7, there exists a finite maximal, structured and irreducible derivation D ∈ D(p(x) q 1 (x), . . . , q n (x)) which does not contain a leaf labeled by a sequent with empty consequent. But then, no node in D is labeled by a sequent with empty consequent, because all descendants of such a node must have empty consequents as well.

We first show that this derivation is actually a proof (i.e. all its leaves are labeled with ). Suppose there exists a leaf that is not labeled with . This means that the leaf is labeled by a sequent Γ ∆, where ∆ = / 0. Let π be the path in D leading to this leaf. Since D is a maximal derivation, π cannot be extended any further by the application of an inference rule. Assume that the last inference rule applied on π belongs to the schema R and its parent is labeled by Γ ∆ . Since p(x) q 1 (x), . . . , q n (x) ; Γ ∆ , by Lemma 6, Γ is a tree-shaped set and ∆ is a set of conjunctions of tree-shaped sets. Also, R cannot be (AX) or (ID), because then the leaf would be labeled by . We do a case split based on R:

1. (LU) Then Γ ∆ is of the form R, Γ \ r(y) ∆ , where (R, r(y)) ∈ S is an inductive rule. If ∆ contains at least one predicate atom, we can still apply (RU), which contradicts the fact that D is maximal. Otherwise, because ∆ = / 0 consists of conjunctions of tree-shaped sets and does not contain any predicate atoms, it must be the case that ∆ contains only non-trivial conjunctions, obtained from previous applications of (RU) or (RD). We distinguish the following cases:

• Γ \ r(y) = / 0. Then we can apply (RD) to the sequent R ∆ and extend D, a contradiction.

is the first occurrence of a rule (LU) then it must be the case that Γ \ r(y) = / 0, which contradicts our assumption. Then there must have been a previous application of (LU) on π, and, because D is structured, (RD) must have been applied between them. Therefore, since Γ is tree-shaped, Γ \ r(x) can only contain predicates, because the constraints introduced by (LU) are always eliminated by (RD). Then we can apply (LU) and extend D, a contradiction.

(RU)

, where r(y) is a predicate atom and r(y

r(y) contains at least one predicate, we can apply (RU) and extend D, contradiction. Otherwise, because ∆ = / 0 consists of conjunctions over tree-shaped sets and it does not contain any predicates, then it must be the case that ∆ contains only non-trivial conjunctions, obtained from previous applications of (RU) or (RD). We distinguish the cases:

• Γ contains a predicate atom. Then we can apply (LU) and extend D, contradiction.

• Γ does not contain predicate atoms. Because Γ is tree-shaped and D is structured, Γ can only contain a constraint with no subgoal variables. Then we can apply (RD) and extend D, contradiction.

(RD)

Then Γ ∆ is of the form r 1 (y 1 ), . . . , r m (y m ) Q 1 (y 1 , . . . , y m ), . . . , Q k (y 1 , . . . , y m ) and we can apply (LU) -or even (∧R), (RU) or (SP) if possible -to Γ ∆, which means that we can still extend π, leading to a contradiction.

(∧R)

Γ ∆ is of the form Γ r(y) ∧ Q , ∆ . Since we only apply (∧R) as cleanup after (RD), Γ only contains predicate atoms and Q is a conjunction of predicate atoms. Then we can continue to apply (∧R) if r(y) ∧ Q or any member of ∆ contains some conjunction s 1 (z) ∧ . . . ∧ s k (z), or apply (LU), (RU), or (SP), leading to a contradiction. 5. (SP) Then Γ ∆ is of the form r(y) s 1 (y), . . . , s m (y) and we can apply (LU) or (RU) to Γ ∆, which means that we can still extend π and leads to a contradiction. We will now show that the sequence of inference rules fired on each maximal path in D is captured by the strategy S. Let π be an arbitrary maximal path in D. Since D is a maximal derivation, π cannot be extended any further by the application of an inference rule. W.l.o.g. we assume that the first application of (LU) is not immediately preceded by an application of (RU) -otherwise, one can obtain the same sequent by first applying (LU) before any (RU). The proof goes by induction on the number N ≥ 1 of basic sequents that occur on π. If N = 1, then the only basic sequent p(x) q 1 (x), . . . , q n (x) occurs on the first position of π. In this case (SP) is never applied on π, because its premiss is also basic sequent, contradicting with N = 1. We distinguish two cases:

1. If (LU) is not applied on π, the only possibility is to apply AX ∈ S to p(x) q 1 (x), . . . , q n (x), thus ending the path. Otherwise, (LU) is enabled, which contradicts the maximality of π. 2. Else, since (LU) is applied on π, then it must be applied in the beginning, because only (LU) and (RU) are applicable on p(x) q 1 (x), . . . , q n (x) and we assumed that no instance of (RU) immediately precedes (LU). Assume that the first rule applied on π is:

(LU) Γ ∆ p(x) q 1 (x), . . . , q n (x) Then (Γ , p(x)) ∈ S is an inductive rule and (LU) cannot be applied again without applying (RD) first, due to the assumption that D is structured. Since ∆ = {q 1 (x), . . . , q n (x)}, we can now apply (RU). Because (SP) is never applied on π, either (AX) or (RD) can be applied next. In the first case, we obtain R(π) ∈ LU • RU • AX ∈ S. In the second case, if n = 1 in the premiss of (RD), since S has the fvi property, we obtain that the premiss of (RD) is a basic sequent, contradicting our assumption. Then it must be the case that n > 1, and now (RD) is not applicable any longer, because the number of predicate atoms will always be bigger than the number of subgoal variables in the constraint from the antecedent. The only possibilities for continuation are then (AX), (ID), (∧R), (LU) and (RU). However, (∧R) is applicable only a finite number of times, equal to the number of conjunctions of predicate atoms with the same arguments from the consequent, (RU) can also only be applied a finite number of times, equal to the number of singleton predicate atoms from the antecedent, and (LU) is applicable at most once, because (RD) is no longer applicable. In both cases, π is not maximal, because (LU) is enabled. Then the only possibility is to end the path by (AX) or (ID), obtaining LU

where ρ starts with the second occurrence of a basic sequent in π. As before, the first occurrence is the initial sequent p(x) q 1 (x), . . . , q n (x). Then the inference rule applied on the last vertex of τ is either (SP) or (RD). In the latter case, the sequent's antecedent consists of a single predicate atom. In the former case, there is an application of (RD) optionally followed by several applications of (∧R) preceding the last vertex of τ, and consider now the conclusion of the last application of (RD) on a vertex in τ. As argued before, the antecedent of this conclusion is a predicate rule of S with goal r(y), introduced by a previous application of (LU). Since, between the premiss of this (LU) instance and the conclusion of (RD), the antecedent of the sequents is unchanged, the only possibility is that (RU) has been used between them, thus R(π) ∈ LU • RU * • RD • ∧R * • SP? • R(ρ). By the inductive hypothesis, we have R(ρ) ∈ S, thus R(π) ∈ (LU • RU * • RD • ∧R * • SP?) • S ⊆ S, as required.

The proof search semi-algorithm (1) only explores irreducible derivations. If executed with the strategy S from Theorem 3, these derivations are also structured. By Lemma 5 (1), irreducible and structured derivations are finite, thus every execution of the semi-algorithm is guaranteed to terminate. If, moreover, the input inductive system S is ranked, non-filtering, non-overlapping and has the fvi property, then URSID is complete and semi-algorithm (1) is a decision procedure for the entailment problems of S.