Towards a Substitution Tree Based Index for Higher-order Resolution Theorem Provers Tomer Libal Alexander Steen Inria Saclay Freie Universität Berlin Palaiseau, France Berlin, Germany tomer.libal@inria.fr a.steen@fu-berlin.de Abstract One of the reasons that forward search methods, like resolution, are efficient in practice is their ability to utilize many optimization tech- niques. One such technique is subsumption and one way of utilizing subsumption efficiently is by indexing terms using substitution trees. In this paper we describe an attempt to extend such indexes for the use of higher-order resolution theorem provers. Our attempt tries to handle two difficulties which arise when extending the indexes to higher-order. The first difficulty is the need for higher-order anti-unification. The second difficulty is the closure of clauses under associativity and com- mutativity. We present some techniques which attempt to solve these two problems. 1 Introduction Term indexing is a popular technique for speeding up computations to a broad variety of tools in computational logic, ranging from resolution based theorem provers [17] to interpreters of programming languages such as Prolog. A key aspect for optimizing such tools is to use sophisticated methods for redundancy elimination. One such method for clause-based indexes is subsumption. Forward subsumption allows to discard clauses which are less general than clauses already processed, whereas backward subsumption allows to remove stored clauses if a more general one is encountered. The idea behind both is that using more general clauses drastically reduces the search space while still being enough for completing certain tasks [9]. Due to the importance of subsumption in practical applications, there is a variety of indexing techniques that support efficient subsumption queries. We refer the reader to the survey about term indexing by Ramakrishnan et al. [16]. In a similar way to tools for first-order logic, higher-order logic tools can benefit also from term indexing for efficient subsumption. Unfortunately, higher-order matching, which is a required technique for determining subsumption, is much more complex than its first-order counter part [21]. We only know of few approaches to higher-order term indexing: Theiß and Benzmüller designed a term index [22] for the LEO-II higher-order resolution theorem prover [3]. However, their approach focuses on efficient low-level term (traversal) operations such as β-normalization and occur-checks. Additionally, term sharing is employed in order to reduce space consumption and for allowing constant-time equality checks between α-equivalent terms. The closest to our approach is the higher-order term indexing technique by Pientka [14]. Both approaches are based on substitution trees [6] and on propagating to the leaves those components of the indexed terms for Copyright c by the paper’s authors. Copying permitted for private and academic purposes. In: P. Fontaine, S. Schulz, J. Urban (eds.): Proceedings of the 5th Workshop on Practical Aspects of Automated Reasoning (PAAR 2016), Coimbra, Portugal, 02-07-2016, published at http://ceur-ws.org 82 which there is no efficient unification algorithm. One difference is the assumed term representation: In order to efficiently manage more complex type systems, such as dependent types, Pientka has chosen to represent terms using Contextual Modal Type Theory [12]. This technique allows for an elegant treatment of dependent types but requires a specially designed unification procedure [15]. Our use of the standard simple type theory [4] allows us to use type-independent unification algorithms [2]. Another difference is the technique chosen for propagating the non-pattern content: While we use an efficient algorithm for computing the pattern generalization of two non-pattern terms [2] (also made possible by our choice of term representation), Pientka’s technique is based on a normalizing pre-processing step [15] which computes the non-pattern content as additional constraints and might incur an additional cost. A somewhat less crucial difference is the treatment of associativity and commutativity (AC). Since unification algorithms which incorporate this theory do not exist for higher-order logic, we deal with the problem by integrating the treatment of AC into the operations of the index. Pientka’s index primary target are not terms in clausal form and therefore, this problem is not treated there. It should not be too complex, though, to integrate the ideas presented in this paper in Pientka’s index in order to achieve the same AC treatment. Obvious other differences include the state of the art of Pientka’s index, its implementation within the Twelf system [13], and the experimental results which are included and its rigorous representation. Our index is yet to be implemented and experimented with and we are still to provide fully rigorous presentation. Nevertheless, we believe that our approach might be more suitable for indexing higher-order terms in general higher-order theorem provers. This claim is, of course, to be justified by the implementation and experimentation of both indexing techniques within Leo-III [24]. In this paper we hence present a higher-order indexing technique for the theorem prover Leo-III which is also based on substitution trees. The differences just discussed and especially the treatment of non-pattern terms might suggest that forward and backward subsumption operations can be efficiently handled by our approach. The main difficulty which arises when trying to store clauses in an index is that the index must be closed under the AC properties of clauses. In addition, when computing subsumed clauses, the number of literals in the clause is not as important as the fact that each literal in the subsuming clauses must generalize a literal in the subsumed one. As long as we only treat unit clauses, no special treatment is required and the technique presented in [7] can be safely extended to deal with higher-order terms. When dealing with multi-literal clauses, though, one has to compensate between optimizing the size of the index and optimizing the operations over the index. As can be seen in [23], one cannot avoid an expensive backtracking search. We suggest a different approach which is supposed to take advantage on searching the index in parallel. In order to achieve that, we plan to store each literal independently in the index and on subsumption calls, to retrieve and compare the literals in parallel. Due to the fact that Leo-III is based on a multi-agent architecture [20], we hope that such an approach would be efficient in practice. Since we are using substitution trees, we are still faced with the problem of using the costly higher-order unification and anti-unification procedures. In the presented work we somehow avoid this problem by using a variant of higher-order anti-unification [2] which computes pattern [11] substitutions. The use of this algorithm will allow us to maintain a substitution tree all of whose inner nodes are pattern substitutions, on which unification and anti-unification are efficient. The definitions and properties of our index are still being investigated and some of them are not yet formally proved. Nevertheless, we hope that the arguments and examples will convince the reader about the potential of our approach for the indexing of arbitrary higher-order clauses and for the support of the forward and backward subsumption functions over this index. In the next section we present the necessary definitions required for understanding this paper as well as the basic ideas of substitution trees and higher-order anti-unification. Following this section is the main part of the paper, in which we introduce our notion of higher-order substitution trees and define the insert, delete, retrieve and subsumption functions. We close our paper with a conclusion which also describes potential future work. 2 Preliminaries In this section we present the logical language that is used throughout the paper. The language is a version of Church’s simple theory of types [4] with an η-conversion rule as presented in [1] and with implicit α-conversions. Unless stated otherwise, all terms are implicitly converted into β-normal and η-expanded form. Let T0 be a set of basic types, then the set of types T is generated by T := T0 | T → T. Let C be a signature of function symbols and let V be a countably infinite set of variable symbols. In our definitions and examples the symbols u, w, x, y, z, W, X, Y, Z ∈ V, and f, g, h, k, a, b, c ∈ C are used. We sometimes use subscripts and 83 superscripts as well. The set Termα of terms of type α is generated by Termα := f α | xα | (λxβ .Termγ ) | (Termβ→α Termβ ) where f ∈ C, x ∈ V and α ∈ T (in the abstraction, α = β → γ). Applications throughout the paper will be associated to the left. We will sometimes omit brackets when the meaning is clear. We will also normally omit typing information when it is not crucial for the correctness of the results. τ (tα ) = α refers to the type of a term. The set Term denotes the set of all terms. positions are defined as usual. We denote the subterm of t at position p by t|p . Bound and free variables are defined as usual. Given a term t, we denote by hd(t) its head symbol. Substitutions and their composition (◦) are defined as usual, namely (σ ◦ θ)(X) = θ(σ(X)). The domain and codomain of a substitution σ are denoted by dom(σ) and codom(σ). The image of σ is the set of all variables in codom(σ). We denote by σ|W the substitution obtained from substitution σ by restricting its domain to variables in W . We denote by σ[X 7→ t] the substitution obtained from σ by mapping X to t, where X might already exist in the domain of σ. The join of two substitutions σ and θ is denoted σ • θ (cf. [7]). We extend the application of substitutions to terms in the usual way and denote it by postfix notation. Variable capture is avoided by implicitly renaming variables to fresh names upon binding. A substitution σ is more general than a substitution θ, denoted σ ≤ θ, if there is a substitution δ such that σ ◦ δ = θ. Similarly, a substitution σ is the most specific generalization of substitutions τ and θ if σ ≤ τ , σ ≤ θ and there is no other substitution δ fulfilling these properties such that δ > σ. A substitution σ matches a substitution τ if there is a substitution δ such that δ ◦ τ = σ. A complete set of matchers between substitutions σ and τ is a set A of substitutions such that A contains all the matching substitutions between σ and τ . A substitution σ is a renaming substitution if codom(σ) ⊆ V and |codom(σ)| = |dom(σ)|. The predicate rename(σ) is true iff σ is a renaming substitution. We denote the inverse of a renaming substitution σ by inverse(σ). 2.1 Substitution Trees This section describes substitution trees based on those defined in [6]. In order to optimize some functions on trees, the definition in [6] uses normalized terms and substitutions. As we will see, we will insert the literals of a clause independently into the index and therefore, if we normalize them as suggested in [6] the relationship between the free variables among the different literals will be lost. The main differences, therefore, between our presentation and that in [6] is that we will avoid normalizing terms and substitutions and in addition, allow terms to be of arbitrary order. Definition 1 (Substitution Trees). A substitution tree is defined inductively and is either the empty tree  or the tuple (σ, Π) where σ is a substitution and Π is a set of substitution trees such that 1. each node in the tree is either a leaf node (σ, ∅) or an inner node (σ, Π) with |Π| ≥ 2. 2. for every branch (σ1 , Π1 ), . . . , (σn , Πn ) in a non-empty tree we have dom(σi ) ∩ (dom(σ1 ) ∪ . . . ∪ dom(σi−1 )) = ∅ for all 0 < i ≤ n. 2.2 Higher-order Anti-unification Anti-unification denotes the problem of finding a generalization t of two given terms t1 and t2 , i.e. a term t such that there exist substitutions σ1 , σ2 such that tσ1 = t1 and tσ2 = t2 . A key algorithm for the procedures which are described in the remainder of this paper is the higher-order anti-unification algorithm of Baumgartner et al. [2]. This algorithm differs from most higher-order unification and anti-unification procedures not only by being applicable to arbitrary (simply typed) higher-order terms, but also by efficiently computing very specific generalizations. By very specific generalization (in contrast to the most specific one) we here mean the most specific higher- order pattern which generalizes two arbitrary higher-order terms. This pattern, however, might not be the most specific generalization of these two higher-order terms. Higher-order patterns are restricted forms of higher-order terms for which it is known that efficient unification algorithms exist [11]. Details about the higher-order pattern fragment or even the above anti-unification algorithm are not crucial for understanding this paper and are therefore omitted. It is important to note that since only most specific pattern generalizations are found, the size of the index described in this paper is not optimal. We will explain this point in more detail later. The anti-unification algorithm of Baumgartner et al. is subsequently denoted by msg∗ . 84 Definition 2 (Algorithm msg∗ [2]). The algorithm msg∗ takes two arbitrary higher-order terms t1 and t2 as input and returns a higher-order pattern s and substitutions σ1 and σ2 such that 1. sσ1 = t1 and sσ2 = t2 , and 2. there is no other higher-order pattern s0 fulfilling the above property such that there is a non-trivial substi- tution δ where sδ = s0 . Baumgartner et al. showed that the algorithm msg∗ computes a unique solution (up to renaming of free variables) and takes cubic time [2]. In this paper we are interested in a variant of this algorithm which computes substitutions, rather than terms and which is defined as follows: Definition 3 (Most specific pattern generalizing substitution). Given substitutions θ1 and θ2 , the substitution σ is the most specific pattern generalizing substitution if there are substitutions τ1 and τ2 such that codom(σ) contains only higher-order patterns, σ ◦ τ1 = θ1 , σ ◦ τ2 = θ2 and there is no substitution σ 0 > σ fulfilling these properties. An algorithm for computing the most specific pattern generalizing substitution, denoted msg, can be defined on top of msg∗ . Definition 4 (The algorithm msg). The algorithm msg takes two substitutions θ1 , θ2 as input and returns a triple (σ, τ1 , τ2 ) with σ, τ1 , τ2 as in Def. 3. To that end, let dom(θ1 )∪dom(θ2 ) = {x1 , . . . , xn }. Let (f (s1 , . . . , sn ), τ1 , τ2 ) = msg∗ (f (θ1 (x1 ), . . . , θ1 (xn )), f (θ2 (x1 ), . . . , θ2 (xn ))) where f is a new function symbol of arity n. Finally, set σ := {x1 7→ s1 , . . . , xn 7→ sn }. Claim 5. Let θ1 , θ2 be two substitutions and let (σ, τ1 , τ2 ) = msg(θ1 , θ2 ). Then σ is a most specific pattern generalizing substitution of θ1 and θ2 . Also, σ is unique up to renaming of free variables. The algorithm msg takes cubic time, hence can be used to efficiently build up a substitution tree index (cf. next section). 3 Substitution Trees for Higher-order Clauses In this section we will describe some modifications to first-order substitution trees which will allow us to extend them to higher-order terms. The most obvious obstacle in extending the trees to higher-order terms is the fact that substitution trees de- pend on procedures for unification, anti-unification and matching. These procedures, while being both relatively efficient and unitary in classical first-order logic [10], are highly complex in higher-order logics and do not possess unique solutions any more [8, 19]. Another obstacle is the fact that since we are targeting resolution theorem provers, the terms we are going to store, retrieve, delete and check for subsumption are not mere syntactic terms but clauses with are closed under AC. In the first-order case, one can use dedicated unification algorithms which, although not unitary any more [5], are still feasible. In the higher-order case, due to the complex nature of even the syntactic unification procedure, one needs to find another approach. Our solution to the first problem is to relax a core property of substitution trees and allow also non least general generalizations as substitutions in the nodes of the trees. Towards this end, we employ the anti-unification algorithm from section 2.2. The use of this algorithm will render our trees less optimal as nodes may now contain more general substitutions than necessary and therefore one child may be more general than another child of a node. On the other hand, the algorithm is only cubic in time complexity and is unitary. Our approach to the second problem is to handle the AC properties of clauses not on the anti-unification or matching level, but to encode their treatment into the retrieval, insertion, deletion and subsumption functions. We obtain this by regarding each literal of a clause as an independent higher-order term and, in addition, assigning labels that are identical for all literals of the same clause. Classical substitution trees depend on the anti-unification algorithm for treating associativity and commuta- tivity as well as other properties required by subsumption, such as one clause being a sub-clause of the other. If such an anti-unification algorithm for higher-order term can be found, a simple extension to the trees in section 2.1 can be defined which enjoys the same definitions for insert, delete and retrieval as defined in [6]. This exten- sion will also preserve the property of substitution trees that the index does not contain variants of substitutions already stored and the deletion function removes all variants of some input substitution. 85 x0 7→ x1 x1 7→ = x2 x3 x1 7→ a (b u1 ) u2 x1 7→ u1 u2 x1 7→ ¬ x2 (3) (4) x2 7→ a (b u) x2 7→ a (b u1 ) u2 x2 7→ u3 u2 x2 7→ a (b u3 ) u2 x3 7→ u x3 7→ u1 u2 (3) (4) (1) (2) Figure 1: An example of a substitution tree Since it is not clear if such an anti-unification procedure can be practical, we choose a different approach which will greatly change the form of the substitution trees. Our treatment of subsumption requires the substitution trees to contain all inserted literals, including those which are variants of already stored ones. Similarly, delete will only remove certain substitutions and not all variants of an input substitution. In addition, we will have all stored substitutions be associated with a set of labels which denotes the clause they are part of. In this way we can insert and retrieve the literals independently for a given clause. We will now give the refined definition of higher-order substitution trees. Definition 6 (Higher-order Substitution Trees). A higher-order substitution tree is the triple (σ, Π, L) where σ is a substitution, Π is a set of substitution trees and L is a set of labels such that the following properties hold: • if L = ∅, then Π is not empty. • if Π is not empty, then σ is a pattern substitution. From now on we will refer to higher-order substitution trees just as substitution trees. The above definition makes retrieval in the tree much more efficient as the traversal of the tree will always use the algorithm msg and not less efficient algorithms. Our trees will always have a root node {x0 7→ x1 } and will therefore never be empty. This is done in order to simplify the insertion operation as the root node will always be more general than any inserted term. Example 7. We use as running example, the manipulation of the index as done by Leo-III [24] when running on a variant of Cantor’s surjective theorem. The first six clauses which are inserted are the following (where α and β are types, α := ι → β and β := ι → o): (1) = (aα (bβ→ι uβ )) uβ (2) = (aα (bβ→ι uβ1 ) uι2 ) (uβ1 uι2 ) (3) ¬ (uβ3 uι2 ) ∨ (aα (bβ→ι uβ1 ) uι2 ) (4) (uβ1 uι2 ) ∨ ¬ (aα (bβ→ι uβ3 ) uι2 ) (5) (aα (bβ→ι uβ1 ) uι2 ) ∨ ¬ (aα (bβ→ι uβ3 ) uι2 ) (6) (uβ1 uι2 ) ∨ ¬ (uβ3 uι2 ) Here, ∨ denotes the union of single literals. Note that clause (5) is subsumed by both clauses (3) and (4) and that clause (6) subsumes clauses (3), (4) and (5). We will use this clause set to demonstrate the insert, retrieval and delete operations of the higher-order substitution trees. Fig. 1 displays the higher-order substitution tree after the insertion of the first four clauses. The above example demonstrates why our trees are not optimized as for example, one of the children of node x0 7→ x1 , the node x1 7→ a (b u1 ) u2 is less general than the child x1 7→ u1 u2 . Also, it demonstrates the problem of using arbitrary higher-order terms in the inner nodes of the tree as there are many possible substitutions which generalizes x1 7→ u1 u2 to x1 7→ a (b u1 ) u2 , but only one most specific pattern generalization, x0 7→ x1 . In our trees, each branch from the root of the tree to a leaf corresponds to a literal of some clause. Since we will need to know the actual substitutions at these leaves, we introduce the notation of composed substitutions: 86 x0 7→ x1 x0 7→ x1 x1 7→ f(y) Π0 x1 7→ f(x2 ) Π0 x0 7→ x1 (2) y7→ a x2 7→ b x2 7→ a Π x1 7→ f(a) (1) (2) (1) (1) (a) Variant insertion (b) Compatible insertion (c) Non-compatible (or empty) insertion Figure 2: Cases of inserting a substitution into the index from Ex. 10. Definition 8 (Composed Substitutions). Given a substitution tree T = (σ, Π, L) and let τ be a substitution at a leaf of T such that the nodes on the branch from the root of T to τ are (σ1 , . . . , σn ). Then, the composed substitution for τ , denoted comp-sub(τ ), is given by comp-sub(τ ) = σ1 • . . . • σn . For example, in Fig. 1, consider the leftmost leaf labeled (1). Here, the composed substitution is given by {x0 7→ x1 } • {x1 7→ = x2 x3 } • {x2 7→ a (b u), x3 7→ u} = {x0 7→ = a (b u) u}. Note that, in the context of substitution trees, σ • θ equals σ ◦ θ|dom(σ) if σ and θ are substitutions on a path from the root node to a leaf where θ occurs directly below (i.e. as a child node of) σ. 3.1 Insertion We will define now how to insert new elements into the tree. The definition is similar to the insertion function defined in [6]. One difference is the use of msg for both finding variants and computing generalizations as well as adding labels to the leaves of the tree. An even more important difference is that since we store clauses and not terms, we must also store in the tree variants of existing nodes. Given a clause labeled by l for insertion, we insert each literal t of the clause separately. In the following algorithm, we insert to the tree the substitution τ = {x0 7→ t}. Definition 9 (Insertion Function insert). Let (σ, Π, L) be a substitution tree, τ a substitution to be inserted and l the clause label of this substitution. Compute the following set A = {(θi , δi1 , δi2 ) | (σi , Πi , Li ) ∈ Π, (θi , δi1 , δi2 ) = msg(σi , τ )}. Then, insert((σ, Π, L), τ, l) = (σ, Π0 , L) where: • (Variant) if there exists (θi , δi1 , δi2 ) ∈ A such that δi1 is a renaming, then Π0 = Π \ {(σi , Πi , Li )} ∪ {insert((σi , Πi , Li ), inverse(δi1 ) ◦ δi2 , l)}. • (Compatible) otherwise, if there exists (θi , δi1 , δi2 ) ∈ A such that codom(θi ) contains non-variable terms, then Π0 = Π \ {(σi , Πi , Li )} ∪ {(θi , {(δi1 , Πi , Li ), (δi2 , ∅, {l})})}. • (Non compatible or empty) otherwise, let (θ, δ 1 , δ 2 ) = msg(σ, τ ) and Π0 = Π ∪ {(δ 2 , ∅, {l})}. Example 10. Assume we want to insert the substitution τ = {x0 7→ f (a)} for clause (1) into the tree ({x0 7→ x1 }, Π). • if Π = ∅, then we get the tree in Fig. 2c where Π is empty. • if Π = {({x1 7→ f (y)}, ∅, {(2)})} ∪ Π0 , then we have a variant node since msg({x1 7→ f (y)}, τ ) = ({x1 7→ f (y)}, id, {y 7→ a}) and we get the tree in Fig. 2a. • if there is no variant but Π = {({x1 7→ f (b)}, ∅, {(2)})}∪Π0 , then we have a compatible node since msg({x1 7→ f (b)}, τ ) = ({x1 7→ f (x2 )}, {x2 7→ b}, {x2 7→ a}) and codom({x1 7→ f (x2 )}) contains non variable symbols and we get the tree in Fig. 2b. • if there is also no compatible child, we get the tree in Fig. 2c. The way we insert substitutions into the tree preserves the tree being a substitution tree. Claim 11. If T is a higher-order substitution tree and τ a substitution, then insert(T, τ, l) is also a higher-order substitution tree. 87 x0 7→ x1 x1 7→ = x2 x3 x0 7→ x1 x2 7→ a (b u) x2 7→ a (b u1 ) u2 x1 7→ = (a (b u)) u x3 7→ u x3 7→ u1 u2 (1) (1) (2) (a) Inserting clause (1) (b) Inserting clause (2) Figure 3: Insertion of clauses (1) and (2) to the index from Ex. 12 x0 7→ x1 x1 7→ = x2 x3 x1 7→ a (b u1 ) u2 x1 7→ ¬ (u3 u2 ) (3) (3) x2 7→ a (b u) x2 7→ a (b u1 ) u2 x3 7→ u x3 7→ u1 u2 (1) (2) Figure 4: Insertion of clause (3) from Ex. 12 The above property will make retrieval in the tree much more efficient as the traversal of the tree will always use the algorithm msg and not less efficient algorithms. We show next how to insert the clauses of our running example. Example 12. Figures 3, 4 and 1 show the state of the index after consecutive insertion of clauses (1) and (2), (3), and (4), respectively. Note that, in the above tree, it can be seen why the tree is not optimal when using msg. Although the nodes having a (b u1 ) u2 are instances of u1 u2 , the tree does not capture it and creates two separate nodes. This happens because u1 u2 is not in the pattern fragment. 3.2 Deletion While the insert function defined in the previous section did not differ much from the definition in [6], our definition of the deletion function is completely different. Deletion in first-order substitution trees serves as a logical operation and can be used to perform some limited backward subsumption. Since we store the literals of a clause independently in the tree, we need more information before we can decide if a substitution can be deleted. We will therefore define the deletion function as an optimization function which will remove from the index certain labels of clauses. Since such a deletion can leave some leaves of the tree without labels, we need to recursively optimize the tree by removing and merging nodes. The formal definition of the deletion function del is given by: Definition 13 (Deletion Function del). Given a substitution tree T = (σ, Π, L) and a clause to be removed labeled by l, the function del(T, l) is defined as follows: • Let Π0 = T 0 ∈Π del(T 0 , l). S • if σ = {x0 7→ x1 } (root) return (σ, Π0 , L \ {l}). • else if Π0 = ∅ and L = {l}, then return . 88 • else if Π0 = {(σ 0 , Π00 , L00 )} and |L \ {l}| = 0, then return (σ ◦ σ 0 , Π00 , L00 ). • else return (σ, Π0 , L \ {l}). Example 14. After deleting clauses (3) and (4) from the tree in Fig. 1, the result is the tree in Fig. 3b. 3.3 Retrieval Retrieval in substitution trees is used in order to retrieve all substitutions with a specific relation to some input substitution. Since we are interested in forward and backward subsumption, the relations we are interested in are for the input substitution to be less and more general than the substitutions in the tree, respectively. In order to support associativity and commutativity of clauses, our substitution trees use a non-standard indexing mechanism where each literal is being stored independently from the other literals of the clause. This will prompt us, for each subsumption call, to try to retrieve all substitutions in the tree with a specific relation to all literals of an input clause. Since all retrieve calls can be done in parallel, Leo-III, with its multi-agent architecture, can take advantage on this approach to the associativity and commutativity of higher-order clauses. It should be noted that since we consider the literals of a clause separately, but a subsumption check requires a common substitution to be applicable to the clause, we need to gather, in addition to the labels, all substitutions that denote the relationship between the literals in the index and the literals of the input clause. One property of higher-order terms cannot be avoided. In order to retrieve substitutions, a matching algorithm between two arbitrary higher-order substitutions must be used. We have avoided its use when inserting elements by using the anti-unification algorithm from Sec. 2.2. This algorithm will also allow us to traverse the tree when retrieving substitutions and reach a possible matching node according to the definition of substitution trees. The last action of the retrieval operation, the actual matching of a node with the input substitution, requires a stronger algorithm than msg. For this operation we will use a standard higher-order matching algorithm. Since the call to this algorithm is performed at most once for each stored substitution and since incomplete higher-order matching algorithms can perform very well in practice, we hope that this step will not impair much the efficiency of the trees. The use of incomplete algorithms is not essential here as a failure to match two substitutions when checking for subsumption might only increase the size of the substitution tree. In the following, we will assume being given a (possibly incomplete) matching algorithm. Such an algorithm can be, for example, based on Huet’s pre-unification procedure [8] with bounds on the depth of terms. Definition 15 (Matching Algorithm match). Given two substitutions σ and τ , then match(σ, τ ) = M where M is a complete set of matchers between σ and τ . We now describe the two supported retrieve calls, which will both return a set of labels corresponding to an input substitution. Each label will be associated to a set of substitutions. The first of such functions returns all labels of substitutions which are more general than the input argument. Intuitively, this function traverses the tree and uses msg for checking if the input substitution is a variant of the respective node. A formal definition is given by Definition 16 (Retrieval Function g-retrieve). Given a substitution tree T = (σ, Π, L) and a substitution τ , g-retrieve(T, τ, τ 0 ) returns a set of labels associated with substitutions, defined inductively as follows (τ 0 = τ at the initial call, but it may change during traversal): • if Π = ∅ and M = match(τ, comp-sub(σ)) such that M is not empty, then return (L, M ). • otherwise, return {(L, match(τ, comp-sub(σ))}∪ {g-retrieve((σ 0 , Π0 , L0 ), τ, δ2 ) | (σ 0 , Π0 , L0 ) ∈ Π, msg(σ 0 , τ 0 ) = (θ, δ1 , δ2 ), rename(δ1 )}∪ {g-retrieve((σ 0 , ∅, L0 ), τ, ) | (σ 0 , ∅, L0 ) ∈ Π}. Example 17. Let the substitution tree T be that from Fig. 1 and let τ = {x0 7→ (a (b u1 ) u2 )}. The execution of g-retrieve(T, τ ) proceeds as follows: • apply msg on all children of the root in order to find either a variant or a leaf, and obtain the two inner nodes ({x1 7→ (a (b u1 ) u2 )}, ∅, {(3)}) and ({x1 7→ (u1 u2 )}, ∅, {(4)}). • recursively apply g-retrieve on the two leaves. 89 • now apply match on the two composite substitutions {x0 7→ (a (b u1 ) u2 )} and {x0 7→ (u1 u2 )}, in order to obtain the two sets {δ1 = {u1 7→ u1 , u2 7→ u2 }} and {δ2 = {u1 7→ λz.(a (b u1 ) u2 )}, . . .}. • for each leaf, since the result is not empty, the function returns the sets {((3), {δ1 })} and {((4), {δ2 , . . .})}. Note that the set of matchers can contain more than one element and even be infinite. We hope to optimize this function in the future. Claim 18. The set returned by g-retrieve((σ, Π, L), τ ) contains all the labels of substitutions θ which are stored in (σ, Π, L) and which are more general than τ . In addition, if a substitution δ is associated with the label of θ, then δ ◦ θ = τ . The second retrieval function returns all substitutions which are less general than the input substitution. The tree is still traversed using the function msg but this time we will not be able to use msg to check if σ is a variant of τ . This is due to the fact that we used msg to check if τ is a variant of σ by checking if δ1 is a renaming substitution for msg(σ, τ ) = (θ, δ1 , δ2 ). This worked as both σ and θ are pattern substitutions. If we try to check whether σ is a variant of τ , since τ might not be a pattern substitution, δ2 might not be a renaming substitution even if it is a variant. On the other hand, if σ is a variant of τ , then all the nodes in the subtrees of σ are variants of τ , so we need to use match only when we reach a node of which τ is not a variant and stop there. We first introduce an utility function which gathers all literals on the leaves of a tree. Definition 19 (Gathering of labels). Given a substitution tree T = (σ, Π, L) and a substitution τ , gather(T, τ ) = (L, match(comp-sub(σ), τ )) ∪ {gather(T 0 , τ ) | T 0 ∈ Π}. Example 20. The application of gather(T, τ ) where T is the last child of the root in Fig. 1 and τ = {x0 7→ (u1 u2 )} proceeds as follows: • since there are no labels in the node, it proceed recursively on the two children. • the application on the first child returns {((3), A)}, where A = {u1 7→ λz.¬(u3 u2 ), . . .} is the result of match on the composite function {x0 7→ ¬(u3 u2 )} and τ . • the application on the second child returns {((4), A)}, where A = {{u1 7→ λz.¬(a (b u3 ) u2 )}, . . .} is the result of match on the composite function {x0 7→ ¬(a (b u3 ) u2 )} and τ . • return the union of these two sets. Definition 21 (Retrieval Function i-retrieve). Given a substitution tree T = (σ, Π, L) and a substitution τ , i-retrieve(T, τ, τ 0 ) returns a set of labels associated with substitutions, defined inductively as follows (τ 0 = τ at the initial call, but it may change during traversal): • if msg(σ, τ 0 ) = (θ, δ1 , δ2 ) such that either δ1 is not a renaming or δ2 is a renaming, and match(comp-sub(σ), τ ) = M such that M is not empty, then return (L, M ) ∪ {gather(T, τ ) | T ∈ Π}. • otherwise, if δ1 is a renaming, return {i-retrieve(T 0 , τ, δ2 ) | (T 0 ) ∈ Π}. • otherwise, return ∅. Example 22. Let the substitution tree T be the one from Fig. 1 and τ be the substitution {x0 7→ (u1 u2 )}. The function i-retrieve(T, τ ) proceeds as follows: • we first calculate msg({x0 7→ x1 }, τ ) = (x0 7→ x1 , id, {x1 7→ (u1 u2 )}). • since id is a renaming, we recursively apply i-retrieve on all nodes. • for all children, the first case of i-retrieve now holds and we start gathering all the labels in the tree. For brevity, we give the example only for the last node: • as mentioned, the first case now holds for this node as msg({x1 7→ ¬x2 }, {x1 7→ (u1 u2 )}) = ({x1 7→ x3 }, {x3 7→ ¬x2 }, {x3 7→ (u1 u2 )}) and therefore δ1 is not a renaming. On the other hand, match({x0 7→ ¬x2 }, {x0 7→ (u1 u2 )}) = {{u1 7→ λz.¬x2 }, . . .} is not empty. 90 • gather all labels on this node, as shown in Ex. 20. Claim 23. The set returned by i-retrieve((σ, Π, L), τ ) contains all the labels of substitutions which are stored in (σ, Π, L) and which are less general than τ . In addition, if a substitution δ is associated with the label of θ, then δ ◦ τ = θ. We now show how the checks for forward and backward subsumptions of clauses can be implemented using g-retrieve and i-retrieve. 3.3.1 Forward Subsumption Forward subsumption checks if an input clause is subsumed by a clause in the index. In case the clause is subsumed, no change to the index is made and the input clause is not inserted into the index. Definition 24 (Subsumption). A clause c is subsumed by a clause d if |c| ≤ |d| and there is a substitution σ such that for each literal l of d there is a literal l0 of c such that lσ = l0 . Here, |c| denotes the number of literals in c. Our way of treating associativity and commutativity means that for each literal of the input clause we gather all more general literals in the index with their associated substitution sets. These sets contains all substitutions which independently match the literals in the tree to the literals of the input clause. In order to detect that the input clause is subsumed by the index, we need to show two things. We first need to show that for all the literals of a clause, a more general literal is returned by the index. In addition, we need to show that for each such literal is associated a ”compatible” substitution. Two substitutions are ”compatible” if they agree on all variables in the intersection of their domains. This requirement means that if d is a clause in the index that subsumes the input clause c, then if each of the literals of d subsumes a literal of c with a ”compatible” substitution, then there is indeed a substitution σ such that each of the literals of d subsumes a literal of c with σ. It should be noted that the above technique is based on set subsumption, in contrast to multiset subsumption which is commonly used. A main reason for preferring multisets over sets, is to prevent cases where a clause is being subsumed by a larger clause, which is possible according to the above definition and leads to an incomplete search procedure. In order to restrict such cases, we will only allow subsumption of clasues which are not smaller than the subsuming clauses. We will now give the formal definition of forward subsumption. Definition 25 (Forward Subsumption fsum). Let T be a substitution tree and c = l1 ∨ . . . ∨ ln a clause. Let A = {g-retrieve(T, {x0 7→ li } | 0 < i ≤ n}. The function fsum(T, c) returns true if there are in A the labels (l, M1 ), . . . , (l, Mk ) such that k = |l| is the number of literals of clause l, k ≤ n, and for each two sets Mi and Mj for 0 < i < j ≤ k, there are substitutions σi ∈ Mi and σj ∈ Mj such that σi (x) = σj (x) for all x ∈ dom(σi ) ∩ dom(σj ). Example 26. We will follow the computation of fsum(T, c) where T is the substitution tree of Fig. 1 and c is clause (5) from Ex. 7. • We first compute the set A which is the union of g-retrieve(T, {x0 7→ (a (b u1 ) u2 )}) and g-retrieve(T, {x0 7→ ¬(a (b u3 ) u2 )}). • the first set was already computed in Ex. 17 and resulted in {((3), {{u1 7→ u1 , u2 7→ u2 }}), ((4), {{u1 7→ λz.(a (b u1 ) u2 )}, . . .})}. • the second set is computed in a similar way and results in {((4), {{u3 7→ u3 , u2 7→ u2 }}), ((3), {{u3 7→ λz.(a (b u3 ) u2 )}, . . .})}. • since the size of both (3) and (4) is 2 and the number of occurrences of the labels of each is 2, we are just left with checking if the matching substitutions are compatible, which is easily verified since their domains are disjoint. • we return that (5) is subsumed by the index (by both (3) and (4)). Claim 27. If fsum(T, c) returns true, then there is a clause d indexed by T such that c is subsumed by d. 91 x0 7→ x1 x1 7→ = x2 x3 x1 7→ u1 u2 x1 7→ ¬ (u3 u2 ) (6) (6) x2 7→ a (b u) x2 7→ a (b u1 ) u2 x3 7→ u x3 7→ u1 u2 (1) (2) Figure 5: The final substitution tree 3.3.2 Backward Subsumption Similarly to the way we treated forward subsumption, we can also define backward subsumption. When we detect that the index contains clauses which are subsumed by an input clause, we will need to modify the index in order to delete these clauses. In order to detect all clauses in the index which are subsumed by the input clause, we need to show that the sets returned for each literal of the input clause contain the labels of the subsumed clauses and that the substitution sets associated with the same labels across sets contain ”compatible” substitutions. Definition 28 (Backward Subsumption bsum). Let T be a substitution tree and c = l1 ∨ . . . ∨ ln a clause. Let Ai = i-retrieve(T, {x0 7→ li } for all 0 < i ≤ n. Label l ∈ bsum(T, c) if n ≤ |l| and (l, Mi ) ∈ Ai for all 0 < i ≤ n such that for each two sets Mi and Mj for 0 < i < j ≤ n, there are substitutions σi ∈ Mi and σj ∈ Mj such that σi (x) = σj (x) for all x ∈ dom(σi ) ∩ dom(σj ). Example 29. We will follow the computation of bsum(T, c) where T is the substitution tree of Fig. 1 and c is clause (6) from Ex. 7. • We first compute the sets A1 = i-retrieve(T, {x0 7→ (u1 u2 )}) and A2 = i-retrieve(T, {x0 7→ ¬(u3 u2 )}). • the set A1 was already computed in Ex. 22 and results in {((1), {{u1 7→ λz. = (a (b u))u}, . . .}), ((2), {{u1 7→ λz. = (a (b u1 ) u2 )(u1 u2 )}, . . .}), ((3), {{u1 7→ λz.(a (b u1 ) u2 )}, . . .}), ((4), {{u1 7→ λz.(u1 u2 ))}, . . .}), ((3), {{u1 7→ λz.¬(u3 u2 )}, . . .}), ((4), {{u1 7→ λz.¬(a (b u3 ) u2 )}, . . .})}. • the set A2 can be computed in a similar way and results in {((3), {{u3 7→ λz.(u3 u2 )}, . . .}), ((4), {{u3 7→ λz.(a (b u3 ) u2 )}}), . . .}. • we notice that only the labels (3) and (4) occur in both sets A1 and A2 and that each of the substitutions from A2 can be matched with two substitutions in A1 . • both options are compatible, the first option means that each literals of clause (6) subsumes a different literal of clauses (3) and (4) while the second option means that they subsumes the same literal in these clauses. • we conclude that they are both redundant. • the resulted tree after their removal was computed in Ex. 14. Claim 30. If l ∈ bsum(T, c) and the clause d is labeled by l, then d is subsumed by c. Example 31. The result of inserting clause (6) to the substitution tree from the previous example can be seen in Fig. 5. 92 4 Conclusion and Future Work In this work, we have presented an indexing data structure for higher-order clause subsumption based on substi- tution trees. We make use of an efficient higher-order pattern anti-unification algorithm for calculting meaningful generalizations of two arbitrary higher-order terms. The proposed indexing method is rather limited as is does not support subsumption testing modulo associativity and commutativity which is, of course, essential for general clause subsumption. However, even the limited approach admits effective subsumption queries in certain cases. Additionally, improvements for including such AC aspects are sketched. While the index is not size-optimal in general, we believe that the approach performs quite good in practice, especially when combined with further, orthogonal indexing techniques that could be used as a pre-test. One suitable candidate is a higher-order variant of feature vector indexing [18]. The substitution tree index as described here is planned for implementation in the Leo-III prover [24]. We hope that due to Leo-III’s agent-based architecture [20], independent agents can traverse the substitution tree index in parallel. The index is mainly devised for employment in resolution-based provers, but it seems possible to generalize the approach to non-clausal-based deduction procedures. For further work we need to investigate means of suitably enhancing msg to handle AC properties and other subsumption properties. Also, the matching algorithm could be improved such that it returns minimal complete sets of substitutions which can then be used for the subsumption procedure. At the current state of the index data structure, the inserted substitutions are not normalized. This is essentially a shortcoming that originates from the way we relate the matching substitutions of different literals of the same clause to each other. This results, however, in a substitution tree that contains occurrences of substitutions which are equivalent up to free variables renaming. To overcome this shortcoming, we need to find a way of keeping the substitutions normalized while still being able to relate the matchers of different literals. Acknowledgements Work of the first author was funded by the ERC Advanced Grant ProofCert. The second author has been supported by the DFG under grant BE 2501/11-1 (Leo-III). We thank the reviewers for the very valuable feedback they provided. References [1] Hendrik Pieter Barendregt. The Lambda Calculus – Its Syntax and Semantics, volume 103 of Studies in Logic and the Foundations of Mathematics. North-Holland, 1984. [2] Alexander Baumgartner, Temur Kutsia, Jordi Levy, and Mateu Villaret. A variant of higher-order anti- unification. In Leibniz International Proceedings in Informatics (LIPPICS): 24th International Conference on Rewriting Techniques and Applications (RTA 2013): RTA 2013: June 24-26 2013: Eindhoven, The Netherlands, vol. 21, p. 113-127. Dagstuhl Publishing, 2013. [3] Christoph Benzmüller, Lawrence C. Paulson, Nik Sultana, and Frank Theiß. The Higher-Order Prover LEO-II. Journal of Automated Reasoning, 55(4):389–404, 2015. [4] Alonzo Church. A formulation of the simple theory of types. J. Symb. Log., 5(2):56–68, 1940. [5] François Fages. Associative-commutative unification. Journal of Symbolic Computation, 3(3):257–275, 1987. [6] Peter Graf. Substitution tree indexing. In Rewriting Techniques and Applications, pages 117–131. Springer, 1995. [7] Peter Graf and Christoph Meyer. Advanced indexing operations on substitution trees. In CADE, volume 1104 of Lecture Notes in Computer Science, pages 553–567. Springer, 1996. [8] Gérard P. Huet. A unification algorithm for typed lambda-calculus. Theor. Comput. Sci., 1(1):27–57, 1975. [9] A. Leitsch. The Resolution Calculus. EATCS Monographson Theoretical Computer Science. Springer, 1997. [10] Alberto Martelli and Ugo Montanari. An efficient unification algorithm. ACM Trans. Program. Lang. Syst., 4(2):258–282, April 1982. 93 [11] Dale Miller. Unification of simply typed lambda-terms as logic programming. In 8th International Logic Programming Conference, pages 255–269. MIT Press, 1991. [12] Aleksandar Nanevski, Frank Pfenning, and Brigitte Pientka. Contextual modal type theory. Under consid- eration for publication in the ACM Transactions on Computation Logic, 2005. [13] Frank Pfenning and Carsten Schürmann. System description: Twelfa meta-logical framework for deductive systems. In Automated DeductionCADE-16, pages 202–206. Springer, 1999. [14] Brigitte Pientka. Higher-order term indexing using substitution trees. ACM Transactions on Computational Logic (TOCL), 11(1):6, 2009. [15] Brigitte Pientka and Frank Pfenning. Optimizing higher-order pattern unification. In Automated Deduction– CADE-19, pages 473–487. Springer, 2003. [16] I. V. Ramakrishnan, R. C. Sekar, and Andrei Voronkov. Term indexing. In John Alan Robinson and Andrei Voronkov, editors, Handbook of Automated Reasoning (in 2 volumes), pages 1853–1964. Elsevier and MIT Press, 2001. [17] John Alan Robinson. A machine-oriented logic based on the resolution principle. J. ACM, 12(1):23–41, 1965. [18] Stephan Schulz. Simple and efficient clause subsumption with feature vector indexing. In Automated Reasoning and Mathematics, volume 7788 of Lecture Notes in Computer Science, pages 45–67. Springer, 2013. [19] Wayne Snyder and Jean H. Gallier. Higher-order unification revisited: Complete sets of transformations. J. Symb. Comput., 8(1/2):101–140, 1989. [20] Alexander Steen, Max Wisniewski, and Christoph Benzmüller. Agent-Based HOL Reasoning. In The 5th International Congress on Mathematical Software (ICMS 2016), volume 9725 of LNCS, Berlin, Germany, 2016. Springer. To appear in 2016. [21] Colin Stirling. Decidability of higher-order matching. Logical Methods in Computer Science, 5(3), 2009. [22] Frank Theiss and Christoph Benzmüller. Term indexing for the LEO-II prover. In IWIL-6 workshop at LPAR 2006: The 6th International Workshop on the Implementation of Logics, Pnom Penh, Cambodia, 2006. [23] Andrei Voronkov. Implementing bottom-up procedures with code trees: a case study of forward subsump- tion. Technical report, 1995. [24] Max Wisnieski, Alexander Steen, and Christoph Benzmüller. The Leo-III project. In Alexander Bolotov and Manfred Kerber, editors, Joint Automated Reasoning Workshop and Deduktionstreffen, page 38, 2014. 94