One of the reasons that forward search methods, like resolution, are e cient in practice is their ability to utilize many optimization techniques. One such technique is subsumption and one way of utilizing subsumption e ciently 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 di culties which arise when extending the indexes to higher-order. The rst di culty is the need for higher-order anti-uni cation. The second di culty is the closure of clauses under associativity and commutativity. We present some techniques which attempt to solve these two problems.
Copyright c by the paper's authors. Copying permitted for private and academic purposes. which there is no e cient uni cation algorithm. One di erence is the assumed term representation: In order to e ciently 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 uni cation procedure [15]. Our use of the standard simple type theory [4] allows us to use type-independent uni cation algorithms [2]. Another di erence is the technique chosen for propagating the non-pattern content: While we use an e cient 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 di erence is the treatment of associativity and commutativity (AC). Since uni cation 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 di erences 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 justi ed 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 di erences just discussed and especially the treatment of non-pattern terms might suggest that forward and backward subsumption operations can be e ciently handled by our approach.
The main di culty 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 di erent 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 e cient in practice.
Since we are using substitution trees, we are still faced with the problem of using the costly higher-order uni cation and anti-uni cation procedures. In the presented work we somehow avoid this problem by using a variant of higher-order anti-uni cation [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 uni cation and anti-uni cation are e cient.
The de nitions 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 de nitions required for understanding this paper as well as the basic ideas of substitution trees and higher-order anti-uni cation. Following this section is the main part of the paper, in which we introduce our notion of higher-order substitution trees and de ne the insert, delete, retrieve and subsumption functions. We close our paper with a conclusion which also describes potential future work. 2
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 j T ! T. Let C be a signature of function symbols and let V be a countably in nite set of variable symbols. In our de nitions and examples the symbols u; w; x; y; z; W; X; Y; Z 2 V, and f; g; h; k; a; b; c 2 C are used. We sometimes use subscripts and superscripts as well. The set Term of terms of type is generated by Term := f j x j ( x :Term ) j (Term ! Term ) where f 2 C; x 2 V and 2 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 de ned as usual. We denote the subterm of t at position p by tjp. Bound and free variables are de ned as usual. Given a term t, we denote by hd(t) its head symbol.
Substitutions and their composition ( ) are de ned 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 jW 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 post x 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 speci c generalization of substitutions and if , and there is no other substitution ful lling 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 jcodom( )j = jdom( )j. The predicate rename( ) is true i 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 de ned in [6]. In order to optimize some functions on trees, the de nition 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 di erent literals will be lost. The main di erences, 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.
De nition 1 (Substitution Trees). A substitution tree is de ned inductively and is either the empty tree the tuple ( ; ) where is a substitution and is a set of substitution trees such that or
2.
dom( i) \ (dom(
Higher-order Anti-uni cation Anti-uni cation denotes the problem of nding 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-uni cation algorithm of Baumgartner et al. [2]. This algorithm di ers from most higher-order uni cation and anti-uni cation procedures not only by being applicable to arbitrary (simply typed) higher-order terms, but also by e ciently computing very speci c generalizations.
By very speci c generalization (in contrast to the most speci c one) we here mean the most speci c higherorder pattern which generalizes two arbitrary higher-order terms. This pattern, however, might not be the most speci c generalization of these two higher-order terms. Higher-order patterns are restricted forms of higher-order terms for which it is known that e cient uni cation algorithms exist [11].
Details about the higher-order pattern fragment or even the above anti-uni cation algorithm are not crucial for understanding this paper and are therefore omitted. It is important to note that since only most speci c 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-uni cation algorithm of Baumgartner et al. is subsequently denoted by msg .
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 de ned as follows: De nition 3 (Most speci c pattern generalizing substitution). Given substitutions 1 and 2, the substitution is the most speci c 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 > ful lling these properties.
An algorithm for computing the most speci c pattern generalizing substitution, denoted msg, can be de ned on top of msg .
( ; 1; 2) with ; 1; 2 as in Def. 3. To that end, let dom(
Claim 5. Let 1; 2 be two substitutions and let ( ; 1; 2) = msg( 1; 2). Then is a most speci c 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 e ciently build up a substitution tree index (cf. next section). 3
In this section we will describe some modi cations to rst-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 depend on procedures for uni cation, anti-uni cation and matching. These procedures, while being both relatively e cient and unitary in classical rst-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 rst-order case, one can use dedicated uni cation 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 uni cation procedure, one needs to nd another approach.
Our solution to the rst 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-uni cation 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-uni cation 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-uni cation algorithm for treating associativity and
commutativity as well as other properties required by subsumption, such as one clause being a sub-clause of the other. If
such an anti-uni cation algorithm for higher-order term can be found, a simple extension to the trees in section
2.1 can be de ned which enjoys the same de nitions for insert, delete and retrieval as de ned in [6]. This
extension 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.
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 rst six clauses which are inserted are the following (where
and are types, := ! and := ! o):
(
that clause (
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 speci c 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 :
x17! f(y)
(
For example, in Fig. 1, consider the leftmost leaf labeled (
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 = fx0 7! tg.
De nition 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 = f( i; i1; i2) j ( i; i; Li) 2 ; ( i; i1; i2) = msg( i; )g. Then, insert(( ; ; L); ; l) = ( ; 0; L) where: (Variant) if there exists ( i; i1; i2) 2 A such that i1 is a renaming, then finsert(( i; i; Li); inverse( i1) i2; l)g. 0 = n f( i; i; Li)g [ (Compatible) otherwise, if there exists ( i; i1; i2) 2 A such that codom( i) contains non-variable terms, then 0 = n f( i; i; Li)g [ f( i; f( i1; i; Li); ( i2; ;; flg)g)g. (Non compatible or empty) otherwise, let ( ; 1; 2) = msg( ; ) and 0 = [ f( 2; ;; flg)g.
Example 10. Assume we want to insert the substitution
x1g; ).
= fx0 7! f (a)g for clause (
is empty.
if = f(fx1 7! f (y)g; ;; f(
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 substitution tree.
a substitution, then insert(T; ; l) is also a higher-order
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 de ned in the previous section did not di er much from the de nition in [6], our de nition of the deletion function is completely di erent. Deletion in rst-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 de ne 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 de nition of the deletion function del is given by: De nition 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 de ned as follows:
Let 0 = ST 02
del(T 0; l). if
= fx0 7! x1g (root) return ( ; 0; L n flg). else if 0 = ; and L = flg, then return . else if 0 = f( 0; 00; L00)g and jL n flgj = 0, then return ( 0; 00; L00).
else return ( ; 0; L n flg).
Retrieval in substitution trees is used in order to retrieve all substitutions with a speci c 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 speci c 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-uni cation 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 de nition 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 e ciency 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-uni cation procedure [8] with bounds on the depth of terms.
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 rst 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 de nition is given by De nition 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, de ned 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 f(L; match( ; comp-sub( ))g[ fg-retrieve(( 0; 0; L0); ; 2) j ( 0; 0; L0) 2 fg-retrieve(( 0; ;; L0); ; ) j ( 0; ;; L0) 2 g.
; msg( 0; 0) = ( ; 1; 2); rename(
for each leaf, since the result is not empty, the function returns the sets f((
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 rst introduce an utility function which gathers all literals on the leaves of a tree.
De nition 19 (Gathering of labels). Given a substitution tree T = ( ; ; L) and a substitution , gather(T; ) = (L; match(comp-sub( ); )) [ fgather(T 0; ) j T 0 2 g.
Example 20. The application of gather(T; ) where T is the last child of the root in Fig. 1 and
(u1 u2)g proceeds as follows:
= fx0 7!
since there are no labels in the node, it proceed recursively on the two children.
the application on the rst child returns f((
return the union of these two sets.
De nition 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, de ned 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 ) [ fgather(T; ) j T 2 g. otherwise, if 1 is a renaming, return fi-retrieve(T 0; ; 2) j (T 0) 2 g.
otherwise, return ;.
function i-retrieve(T; ) proceeds as follows: be the substitution fx0 7! (u1 u2)g. The we rst calculate msg(fx0 7! x1g; ) = (x0 7! x1; id; fx1 7! (u1 u2)g). since id is a renaming, we recursively apply i-retrieve on all nodes.
for all children, the rst case of i-retrieve now holds and we start gathering all the labels in the tree.
as mentioned, the rst case now holds for this node as msg(fx1 7! :x2g; fx1 7! (u1 u2)g) = (fx1 7! x3g; fx3 7! :x2g; fx3 7! (u1 u2)g) and therefore 1 is not a renaming. On the other hand, match(fx0 7! :x2g; fx0 7! (u1 u2)g) = ffu1 7! z::x2g; : : :g is not empty. gather all labels on this node, as shown in Ex. 20.
We now show how the checks for forward and backward subsumptions of clauses can be implemented using g-retrieve and i-retrieve. 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.
such that for each literal l of d there is a literal l0 of c such that l = l0. Here, jcj 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 rst 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 de nition 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 de nition of forward subsumption.
De nition 25 (Forward Subsumption fsum). Let T be a substitution tree and c = l1 _ : : : _ ln a clause. Let A = fg-retrieve(T; fx0 7! lig j 0 < i ng. The function fsum(T; c) returns true if there are in A the labels (l; M1); : : : ; (l; Mk) such that k = jlj 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 2 Mi and j 2 Mj such that i(x) = j (x) for all x 2 dom( i) \ dom( j ).
We rst compute the set A which is the union of g-retrieve(T; fx0 7!
g-retrieve(T; fx0 7! :(a (b u3) u2)g).
(a (b u1) u2)g) and
the rst set was already computed in Ex. 17 and resulted in f((
we return that (
Claim 27. If fsum(T; c) returns true, then there is a clause d indexed by T such that c is subsumed by d. Similarly to the way we treated forward subsumption, we can also de ne 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. De nition 28 (Backward Subsumption bsum). Let T be a substitution tree and c = l1 _ : : : _ ln a clause. Let Ai = i-retrieve(T; fx0 7! lig for all 0 < i n. Label l 2 bsum(T; c) if n jlj and (l; Mi) 2 Ai for all 0 < i n such that for each two sets Mi and Mj for 0 < i < j n, there are substitutions i 2 Mi and j 2 Mj such that i(x) = j(x) for all x 2 dom( i) \ dom( j).
We rst compute the sets A1 = i-retrieve(T; fx0 7! (u1 u2)g) and
A2 = i-retrieve(T; fx0 7! :(u3 u2)g).
the set A1 was already computed in Ex. 22 and results in f((
z: = (a (b u1) u2)(u1 u2)g; : : :g);
((
the resulted tree after their removal was computed in Ex. 14.
In this work, we have presented an indexing data structure for higher-order clause subsumption based on substitution trees. We make use of an e cient higher-order pattern anti-uni cation 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 e ective 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 di erent 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 nd a way of keeping the substitutions normalized while still being able to relate the matchers of di erent literals.
Acknowledgements Work of the rst 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.