«Abstract. In this paper we deﬁne a new clausal class, called BU, which can be decided by hyperresolution with splitting. We also consider the ...»
A New Clausal Class Decidable by
Lilia Georgieva1,2, Ullrich Hustadt3, Renate A. Schmidt1,2
Department of Computer Science, University of Manchester, UK
Max-Planck-Institut f¨r Informatik, Saarbr¨cken, Germany
Department of Computer Science, University of Liverpool, UK
Abstract. In this paper we deﬁne a new clausal class, called BU, which
can be decided by hyperresolution with splitting. We also consider the model generation problem for BU and show that hyperresolution plus splitting can also be used as a Herbrand model generation procedure for BU and, furthermore, that the addition of a local minimality test allows us to generate only minimal Herbrand models for clause sets in BU. In addition, we investigate the relationship of BU to other solvable classes.
1 Introduction In recent work [13, 14] we have considered the fragment GF1− of ﬁrst-order logic which was introduced by Lutz, Sattler, and Tobies . GF1− is a restriction of the guarded fragment which incorporates a variety of modal and description logics via standard or non-standard translations, and can be seen as a generalisa- tion of these logics. In contrast to the guarded fragment , GF1− allows for the development of a space-eﬃcient decision procedure. Under the assumption that either (i) there is a bound on the arity of predicate symbols in GF1− formulae, or (ii) that each subformula of a GF1− formula has a bounded number of free variables, the satisﬁability problem of GF1− is PSPACE-complete , while under identical assumptions the satisﬁability problem of the guarded fragment is EXPTIME-complete . Thus, GF1− has the same complexity as the modal and description logics it generalises.
In  we have shown that hyperresolution plus splitting provides a decision procedure for GF1−. One of the interesting features of GF1− is that it is one of the few solvable classes where, during the deduction by the resolution decision procedure, derived clauses can contain terms of greater depth than the clauses in the initial set of clauses. In  we have shown that a modiﬁcation of the main procedure of a standard saturation based theorem prover with splitting can pro- vide a polynomial space decision procedure for GF1−. We also describe several solutions to the problem of generating minimal Herbrand models for GF1−.
We thank the referees for helpful comments and suggestions. The work is supported by research grants GR/M36700 and GR/R92035 from the EPSRC, UK.
1 In [13, 14] we have used structural transformation (or deﬁnitional form transformation, cf. e.g. [3, 18]), to transform GF1− formulae into clausal form. While it is straightforward to give a schematic characterisation of the resulting sets of clauses, it is much more diﬃcult to state the conditions which an arbitrary set of clauses needs to satisfy so that it shares most or all the properties of the clauses sets we obtain from the deﬁnitional form transformation of GF1− formulae.
In this paper we deﬁne a new clausal class BU which generalises the set of all clause sets we can obtain from GF1− via the deﬁnitional form transformation.
BU is deﬁned such that hyperresolution plus splitting is still a decision procedure.
Since hyperresolution is implemented in many state-of-the-art theorem provers, e.g. Otter, SPASS, and Vampire, this gives a practical decision procedure for the class. We also show that if an input clause set from BU is not refuted, an adequate representation of a model and of a minimal model of the clausal class can be extracted from the information produced by the prover.
A main motivation for studying classes like GF1− and BU is that a variety of expressive modal and description logics can be embedded into them. Expressive modal and description logics have found applications in such varied areas as, for example, veriﬁcation, program analysis, knowledge representation, deductive data bases and the semantic web. However, there are a number of alternative solvable classes for which the same is true. We will discuss the relationship of BU to some of these alternative classes.
The paper is organised as follows. Section 2 deﬁnes the notation used, some basic concepts and a hyperresolution calculus with splitting. The clausal class BU is deﬁned in Section 3, and the relationship of BU to other solvable classes is discussed in Section 4. The applicability of the hyperresolution calculus as a decision procedure for the class, model building by hyperresolution and in particular, minimal model building are investigated in Sections 5 and 6. The ﬁnal section is the Conclusion.
2 Fundamentals and hyperresolution
Notation. The notational convention is as follows. We use the symbols x, y, z for ﬁrst-order variables, s, t, u for terms, a, b for constants, f, g, h for functions, P, Q for predicate symbols, A for atoms, L for literals, C for clauses, ϕ, φ, ψ, for formulae, and N for sets of clauses.
An over-line indicates a sequence. An i-sequence is a sequence with i elements.
If s and t are two sequences of terms and X is a set of terms, then the notation s ⊆ t (s ⊆ X) means that every term in s also occurs in t (X). By deﬁnition, s = t (s = X) iﬀ s ⊆ t and t ⊆ s (s ⊆ X and every term in X occurs in s). The union of the terms in s and t is denoted by s ∪ t. Given a sequence s of terms, fs (ui ) denotes a sequence of terms of the form f1 (u1 ),..., fk (uk ), where ui ⊆ s for every 1 ≤ i ≤ k.
Terms, literals, clauses and orderings. The term depth dp(t) of a term t, is inductively deﬁned as follows. (i) If t is a variable or a constant, then dp(t) = 1.
2 (ii) If t = f (t1,..., tn ), then dp(t) = 1 + max dp(ti ) | 1 ≤ i ≤ n. The term depth of a literal is deﬁned by the maximal term depth of its arguments, and the term depth of a clause is deﬁned by the maximal term-depth of all literals in it.
A literal is an atomic formula A (a positive literal) or the negation ¬A of an atomic formula A (a negative literal). We regard a clause as a multiset of literals and consider two clauses C and D to be identical if C can be obtained from D by variable renaming. A multiset over a set L is a mapping C from L to the natural numbers. We write L ∈ C if C(L) 0 for a literal L. We use ⊥ to denote the empty clause. A positive (negative) clause contains only positive (negative) literals. The positive (negative) part of a clause is the subclause of all positive (negative) literals. A split component of a clause C ∨ D is a subclause C such that C and D do not have any variables in common, i.e. are variable disjoint. A maximally split (or variable indecomposable) clause cannot be partitioned (or split) into subclauses which do not share variables.
A clause C is said to be range restricted iﬀ the set of variables in the positive part of C is a subset of the set of variables of the negative part of C. A clause set is range restricted iﬀ it contains only range restricted clauses. This means that a positive clause is range restricted only if it is a ground clause.
A strict partial ordering on a set L (i.e. an irreﬂexive and transitive relation) can be extended to an ordering mul on (ﬁnite) multisets over L as follows:
C mul D if (i) C = D and (ii) whenever D(x) C(x) then C(y) D(y), for some y x. mul is called the multiset extension of.
Given an ordering on literals we deﬁne a maximal literal in a clause in the standard way: A literal L in a clause C is maximal in C, if there is no literal L in C, for which L L. A literal L is strictly maximal in C if it is the only maximal literal in C.
A term, an atom, a literal or a clause is called functional if it contains a constant or a function symbol, and non-functional, otherwise.
3 A derivation in Rhyp from a set of clauses N is a ﬁnitely branching, ordered tree T with root N and nodes which are sets of clauses. The tree is constructed by applications of the expansion rules to the leaves. We assume that no hyperresolution or factoring inference is computed twice on the same branch of the derivation. Any path N (= N0 ), N1,... in a derivation T is called a closed branch in T iﬀ the clause set j≥0 Nj contains the empty clause, otherwise it is called an open branch. We call a branch B in a derivation tree complete (with respect to Rhyp ) iﬀ no new successor nodes can be added to the endpoint of B by Rhyp, otherwise it is called an incomplete branch. A derivation T is a refutation iﬀ every path N (= N0 ), N1,... in it is a closed branch, otherwise it is called an open derivation.
In general, the calculus Rhyp can be enhanced with standard simpliﬁcation rules such as tautology deletion and subsumption deletion, in fact, it can be enhanced by any simpliﬁcation rules which are compatible with a general notion of redundancy [4, 5]. A set N of clauses is saturated up to redundancy with respect to a particular reﬁnement of resolution if the conclusion of every inference from non-redundant premises in N is either contained in N, or else is redundant in N.
A derivation T from N is called fair if for any path N (= N0 ), N1,... in T, with limit N∞ = j≥0 k≥j Nk, it is the case that each clause C which can be deduced from non-redundant premises in N∞ is contained in some Nj. Intuitively, fairness means that no non-redundant inferences are delayed indeﬁnitely. For a ﬁnite complete branch N (= N0 ), N1,... Nn, the limit N∞ is equal to Nn.
Theorem 1 (). Let T be a fair Rhyp derivation from a set N of clauses.
Then: (i) If N (= N0 ), N1,... is a path with limit N∞, then N∞ is saturated (up to redundancy). (ii) N is satisﬁable if and only if there exists a path in T with limit N∞ such that N∞ is satisﬁable. (iii) N is unsatisﬁable if and only if for every path N (= N0 ), N1,... the clause set j≥0 Nj contains the empty clause.
The clausal class BU3
The language of BU is that of ﬁrst-order clausal logic. Additionally, each predicate symbol P is uniquely associated with a pair (i, j) of non-negative integers, such that if the arity of P is n then i + j = n. The pair is called the grouping of the predicate symbol. Sometimes the grouping (i, j) of a predicate symbol P will be made explicit by writing P (i,j). The notion of grouping is extended to literals in the following way. A literal L is said to satisfy the grouping condition with respect to the sequences x and s, if L = (¬)P (i,j) (x, s) or L = (¬)P (j,i) (s, x), where x is an i-sequence of variables, and s is either a j-sequence of variables disjoint from x or a j-sequence of terms of the form f (z) where z ⊆ x, and x is non-empty. Repetitions of variables and terms in any of the sequences are allowed.
Furthermore, an acyclic relation d, called an acyclic dependency relation, is deﬁned over the predicate symbols. Let + be the transitive closure of d. Then d + d is an ordering on predicate symbols. This ordering extends to atoms, literals 4 and clauses by the following deﬁnitions. Given two literals L1 = (¬)P1 (s) and L2 = (¬)P2 (t), L1 D L2 iﬀ P1 + P2. The multiset extension of the ordering d D, also denoted by D, deﬁnes an ordering on ground clauses. The acyclicity of d implies that D is also acyclic.
Given a ﬁnite signature Σ such that (i) any predicate symbol has a unique grouping, and (ii) there is an acyclic dependency relationship d on the predicate symbols in Σ, we deﬁne the class BU of clausal sets over Σ as follows.
A clausal set N belongs to BU if any clause C in N satisﬁes one of the three conditions below as well as the following. If C is a non-ground and non-positive clause then C is required to contain a strictly D -maximal literal, which is negative and non-functional. This literal is called the main literal of the clause.
The predicate symbol P of the main literal must either have the grouping (0, i) or (i, 0), where i is the arity of P.
Condition 1: C is a non-positive, non-ground and non-functional clause and the following is true.
(a) The union of the variables of the negative part can be partitioned into two disjoint subsets X and Y, at least one of which is non-empty.
(b) For every literal L in C, either the variables of L are (i) subsets of X, or (ii) subsets of Y, or (iii) there are non-empty sequences x, y, such that x ⊆ X, y ⊆ Y and L satisﬁes the grouping condition with respect to x and y.
(c) Either the main literal contains all the variables of the clause, or it contains all the variables from one of the sets X and Y, and there is a negative literal L whose arguments satisfy (b.iii) and which contains all the variables from Y if the main literal contains all the variables from X, or all the variables from X if the main literal contains all the variables from Y.
Condition 2: C is a non-positive and non-ground functional clause and the following is true.
(a) The main literal of C contains all the variables of C.
(b) Every other literal L in C satisﬁes the grouping condition with respect to two disjoint sequences of variables x and y, or with respect to two sequences x and fx (ui ), where x is a sequence of variables and fx (ui ) is a sequence of terms fi (ui ) such that ui ⊆ x.
Condition 3: C is a positive ground unit clause, its arguments are constants and its predicate symbol has grouping (0, i) or (i, 0).
Consider the following clauses.
1. ¬P (x, y) ∨ ¬Q(x) ∨ ¬R(x, x, y, z) 5. ¬P (x, y) ∨ Q(x, x, y, f (x, y))
2. ¬P (x, y, z) ∨ ¬Q(y, x) ∨ R(x, x, y, z) 6. ¬P (x, y) ∨ Q(x, x, y, g(y))
3. ¬P (x, y) ∨ ¬Q(y, z) ∨ ¬R(x, x, y, z) 7. ¬P (x, y) ∨ Q(x, x, g(y), y)
4. ¬P (x, y) ∨ ¬Q(y, z) ∨ ¬R(x, y, z, x) 8. ¬P (x) ∨ P (f (x)) It follows from the deﬁnition of BU that all non-positive clauses must contain a covering negative literal which contains all the variables of the clause. This negative literal can be the main literal, or it is a literal satisfying Condition 1.(b.iii).
5 In the latter case the clause must contain another negative literal which is the main literal. In Clause 1 the literal ¬R(x, x, y, z) is the covering negative literal.