In this paper, we study an efficient equality computation in connection tableaux, and give a new variant of Brand, Bachmair-Ganzinger-Voronkov and Paskevich's modification methods, where the symmetry elimination rule is never applied. As is well known, effective equality computing is very difficult in a top-down theorem proving framework such as connection tableaux, due to a strict restriction to re-writable terms. The modification method with ordering constraints is a wellknown remedy for top-down equality computation, and Paskevich adapted the method to connection tableaux. However the improved modification method still causes essentially redundant computation which originates in a symmetry elimination rule for equational clauses. The symmetry elimination may produce an exponential number of clauses from a given single clause, which inevitably causes a huge amount of redundant backtracking in connection tableaux. In this paper, we study a simple but effective remedy, that is, we abandon such symmetry elimination for clauses and instead introduce new equality inference rules into connection tableaux. These new inference rules have a possibility of achieving efficient equality computation, without losing the symmetry property of equality, which never cause redundant backtracking nor redundant contrapositive computation. We implemented the proposed methods in a sophisticated prover SOLAR which is originally designed to finding logical consequences, and show a preliminary experimental results for TPTP benchmark problems. This research is now in progress, thus the experimental results provided in this paper are tentative ones.
In this paper, we study an efficient equality computation in connection tableaux, and
give a variant of modification methods investigated by Brand [
1This research was partially supported by the Grant-in-Aid from The Ministry of Education, Science and Culture of Japan ((A) No.20240016) a=u1 b㻛 u1
C4 Order Violated !! b㻛 u3 a㻛 u3 a>b
㼠 x1㼠=x1 㱔 ={u1/u3, u3/b, …}
P 㼠
Q
x1㼠=x1 Succeed !!
As is well known, effective equality [
Let S1 be a set of clauses { ¬P , P ∨Q∨a ≈ b, b 6≈ a, ¬Q∨P }. The modification method transforms S1 into the following set of clauses with ordering constraints: C1 : ¬P C2 : (P ∨ Q ∨ a ≃ u1 ∨ b 6≃ u1) · (a ≻ u1 ∧ b C3 : (P ∨ Q ∨ b ≃ u2 ∨ a 6≃ u2) · (b ≻ u2 ∧ a C4 : (b 6≃ u3 ∨ a 6≃ u3) · (b u3 ∧ a u3) C5 : ¬Q ∨ P Ref : x ≃ x (Reflexivity Axiom) u1) u2) A clause with ordering constraints takes the form of D ·δ where D is an ordinary clause and δ is a conjunction of ordering constraints s ≻ t, s t or s = t. The ordering constraint δ of D · δ is expected to be satisfiable together with D. Notice that the above two clauses C2 and C3 are produced from the single clause P ∨ Q ∨ a ≈ b by symmetry elimination rule (more precisely, together with transitivity elimination rule). Figure 1 depicts two consecutive tableaux in a connection tableaux derivation, where we assume the ordering b ≻ a over constants. The left tableau fails to be closed because the goal a 6≃ u2 violates the ordering constraint a u3, where the variable u3 is substituted with b. The failure of derivation invokes backtracking, and eventually replaces the tableau clause C2 below the top clause C1 with the clause C3. The right tableau in Fig. 1 succeeded in being closed, and simultaneously satisfies the ordering constraints. Notice that there are identical subtableaux below the goal Q in both left and right tableaux. Unfortunately, none of well-known pruning methods, such as folding-up/Creduction or local failure caching, can prevent the redundant duplicated computation, because the clause C2 containing Q in the left tableau is replaced with C3 in the right tableau. Such a redundant computation essentially originates in the duplication of a given clause by symmetry elimination.
In this paper, we study a simple but effective remedy, that is, we abandon such
symmetry elimination of clauses, and instead introduce new equality inference rules into
connection tableaux. These new inference rules can achieve efficient equality
computation, without losing the symmetry property of equality, which never cause redundant
backtracking nor redundant contrapositive computation. Finally, we evaluate the
proposed method through experiments with TPTP benchmark problems. Paskevich [
We give some preliminaries according to Paskevich [
The equality predicate is denoted by the symbol ≈. We abbreviate the negation ¬(s ≈ t) as s 6≈ t. We consider equalities as unordered pairs of terms; that is, a ≈ b and b ≈ a stand for the same formula. As is well known, the equality is characterized by the congruence axioms E consisting of four axioms, i.e., reflexivity, symmetry, transitivity and monotonicity. The symbol ≃ will denote “pseudo-equality”, i.e., a binary predicate without any specific semantics. We utilize ≃ in order to replace the symbol ≈ when we transform a clause set into a logic without equality. The order of arguments becomes significant here: a ≃ b and b ≃ a denote different formulas. The expression s 6≃ t stands for ¬(s ≃ t).
We denote non-variable terms by nv, nv1 and nv2, and also arbitrary terms by l, r, s, t, u and v. Variables are denoted by x, y and z. Substitutions are denoted by σ and θ. The result applying a substitution σ to an expression E is denoted by Eσ. We write E[s] to indicate that a term s occurs in E, and also write E[t] to denote the expression obtained from E by replacing one occurrence of s with t.
We use an ordering constraint as defined in Bachmair et al. [
2A reduction ordering > is an ordering over terms such that: (1) > is well-founded; (2) for any terms s, t, u and any substitution θ, if s > t then u[sθ] > u[tθ] holds. Expansion (Exp):
S || Γ, ¬P (r), P (s) ⊥ · (r = s)
S || Γ, ¬P (r), Δ, P (s) ⊥ · (r = s)
S, (L1 ∨ · · · ∨ Lk) || Γ
L1 · · · Lk S || Γ, P (r), ¬P (s)
⊥ · (r = s) S || Γ, P (r), Δ, ¬P (s)
⊥ · (r = s)
Let S be a set of clauses. A constrained clause tableau for S is a finite tree T (See Fig. 1 as an example). Each node except for a root node is a pair L · γ where L is a literal and γ is a constraint. Any branch that contains the literal ⊥, which represents the false, is closed. A tableau is closed, whenever every branch in it is closed and the overall of constraints in it is satisfiable.
Each inference step grows some branch in the tableau by adding new leaves under the leaf of the branch in question. Initially, an inference starts from the single root node. Symbolically, we describe an inference rule as follows:
S || Γ
· · · L1 · γ1
Ln · γn
where S is an initial given set of clauses, Γ is the branch being augmented (with
constraints not mentioned), and (L1 · γ1), . . . , (Ln · γn) are the added nodes. Whenever
we choose some clause C in S to participate in the inference, we implicitly rename all
variable in C to some fresh variables. The standard connection tableau calculus [
Any clause tableau built by the rules of CT can be considered as a tree of inference steps. Every tableau of CT always starts with an expansion step; also that first expansion step can be followed only by another expansion, since connection step requires at least two literals in a branch. In a tableau, an expansion clause is the added clause in an expansion step.
Let T be a tableau of CT for a set S of clauses. We say that T is strongly connected whenever every strong connection step in a tableau follows an expansion step, and every expansion step except for the first (or top) one is followed by exactly one strong connection step. Moreover, T is said to be a refutation for S if T is strongly connected and closed.
Theorem 1 (Letz et.al [
Ordered paramodulation is a well-known efficient equality inference rule. It is well
known that top-down (or linear) deduction systems, including connection tableaux, are
difficult frameworks for efficient equality computation because of hard restriction of
redexes, i.e., subterms allowed to rewrite. For example, Snyder and Lynch [
Modification Method and Connection Tableaux
In this subsection, we firstly, show the modification method given by Bachmair, Ganzinger
and Voronkov [
Elimination of Congruence Axioms Given a set S of equational clauses, we apply three kinds of elimination rules and replace the equality predicate ≈ by the predicate ≃ to obtain a modified clause set S’, such that S’ is satisfiable iff S is equationally satisfiable. If R is a set of such elimination rules, we say a constrained clause is in R-normal form if no rule in R is applicable to it. We denote by R(S) the set of all R-normal forms of a clause in S.
We first show S-modification rules which replaces the equality symbol ≈ with the pseudo-equality ≃, and generates several clauses which can simulate computational effects of symmetry axiom.
• Positive S-modification:
s ≈ t ∨ C • Negative S-modification: nv 6≈ t ∨ C x 6≈ nv ∨ C
x 6≈ y ∨ C where θ is a substitution {x/y}.
⇒ s ≃ t ∨ C and t ≃ s ∨ C ⇒ ⇒ ⇒ nv 6≃ t ∨ C nv 6≃ x ∨ C Cθ Remark: Positive S-modification rule is quite problematic, because one equation is duplicated to two equations each of which has converse directions. We shall give a remedy for it in the next section.
Secondly we give M-modification rules which flatten clauses by abstracting subterms via introduction of new variables as follows:
P (. . . , nv, . . .) ∨ C ¬P (. . . , nv, . . .) ∨ C f (. . . , nv, . . .) ≃ t ∨ C f (. . . , nv, . . .) 6≃ t ∨ C s ≃ f (. . . , nv, . . .) ∨ C s 6≃ f (. . . , nv, . . .) ∨ C ⇒ ⇒ ⇒ ⇒ ⇒ ⇒ nv 6≃ z ∨ P (. . . , z, . . .) ∨ C nv 6≃ z ∨ ¬P (. . . , z, . . .) ∨ C nv 6≃ z ∨ f (. . . , z, . . .) ≃ t ∨ C nv 6≃ z ∨ f (. . . , z, . . .) 6≃ t ∨ C nv 6≃ z ∨ s ≃ f (. . . , z, . . .) ∨ C nv 6≃ z ∨ s 6≃ f (. . . , z, . . .) ∨ C where z is a new variable, called an abstraction variable.
The third one is T-modification rule for generating clauses which can simulate effects of transitivity axiom.
3Notice that CT≃ was introduced to prove the completeness of the lazy paramodulation calculus in [
SMT(S) || Γ, ¬P (r), P (s) ⊥ · (r = s) SMT(S) || Γ, nv 6≃ r, s ≃ t ⊥ · (nv = s ≻ t = r)
SMT(S) || Γ, ¬P (r), Δ, P (s)
⊥ · (r = s) SMT(S) || Γ, nv 6≃ r, Δ, s ≃ t ⊥ · (nv = s ≻ t = r)
Equality Resoution(ER) : SMT(S) || Γ, l 6≃ r
⊥ · (l = r) SMT(S) || Γ, P (r), ¬P (s)
⊥ · (r = s) SMT(S) || Γ, s ≃ t, nv 6≃ r
⊥ · (nv = s ≻ t = r) SMT(S) || Γ, P (r), Δ, ¬P (s)
⊥ · (r = s) SMT(S) || Γ, s ≃ t, Δ, nv 6≃ r
⊥ · (nv = s ≻ t = r) • Positive T-modification: • Negative T-modification: s ≃ nv ∨ C
s ≃ z ∨ nv 6≃ z ∨ C s 6≃ nv ∨ C
s 6≃ z ∨ nv 6≃ z ∨ C where z is a new variable, called a link variable.
Notice that if the term t in s ≃ t is a variable, then T-modification does nothing.
Let SMT(S) denote a set T(M(S(S))), i.e., the set of normal clauses obtained from S by consecutively applying S, M and T-modification. Notice that the size of SMT(S) is exponential to the one of S.
Theorem 2 (Bachmair et al. [
Bachmair et al. [
CEE(S) denote the set of clauses of SMT(S) with ordering constraints.
Theorem 3 (Bachmair et al. [
Connection Tableaux for Modification with Ordering Constraints
Paskevich [
Theorem 4 (Paskevich [
Connection Tableaux for Modification without S-Modification The size of SMT(S) is unfortunately exponential to the one of S, which is truly problematic and causes a huge amount of redundant computation. The positive S-modification, hence, should be abandoned. We alternatively introduce new inference rules for simulating the effects of symmetry axiom and construct a new connection tableau calculus CTwS (Connection Tableaux for modification Without S-modification). Definition 1 Let P-modification be a transformation rule of clauses, which just replaces the equality symbol ≈ with the pseudo symbol ≃ in positive equalities. We define nSMT(S) to be a a set of normal clauses obtained from S by just successively applying P-modification, negative S-modification, M-modification and negative T-modification.
Notice that the size of nSMT(S) is linear to the one of S because positive S-modification is never applied.
Once the positive S-modification is abandoned, no symmetry formula t ≃ s of an initial equality s ≃ t is generated in the modification process, which means that the succeeding positive T-modification is not accomplished either. Therefore, we need a mechanism compensating such a deficit of clause transformation. In this paper, we introduce new inference rules which can simulate not only positive S-modification but also positive T-modification for keeping transitivity properties of a positive equality.
We propose the following new rules, called symmetry and transitivity splitting rules, abbreviated as ST-splitting, which can simultaneously simulate the computational effects of symmetry and transitivity axioms.
Naive ST-Splitting Rule: nSMT(S) || Γ, s ≃ nv
s ≃ z nv 6≃ z nSMT(S) || Γ, nv ≃ t t ≃ z nv 6≃ z where nv is a non-variable term and x is a variable. introduced into a tableau by the expansion rule. Some of raw positive equalities s ≃ t are changed to ordinary equality literals by ST-splitting. Conversely ST-Splitting rule is restricted to apply only to a raw positive equality. Moreover, the strong connection rule for a negative equality is also restricted to apply only to raw positive equalities. Furthermore, we force every raw positive equality to be followed either by ST-Splitting or by new strong contraction rules shown below.
Given a literal L, we write [L] to denote a framed literal s ≃ t , called a raw positive literal if L is a positive equality s ≃ t; otherwise [L] denotes L itself. We modify the expansion rule into the one which produces a raw literal for a positive equality.
nSMT(S), (L1 ∨ · · · ∨ Lk) || Γ
[L1] · · · [Lk] ST-Splitting Rule should be changed to treat only raw positive literals.
ST-Splitting Rule: nSMT(S) || Γ, s ≃ nv
s ≃ z nv 6≃ z nSMT(S) || Γ, nv ≃ t t ≃ z nv 6≃ z The original form of strong connection for negative equality is no longer appropriate, because it cannot deal with raw positive equalities nor corporate with ST-splitting rule. The new calculus CTwS has to simulate all valid inferences involving the strong connection in CT≃ for SMT(S) in order to preserve completeness. Let C ∈ S be a clause s ≃ t ∨ K1 ∨ · · · ∨ Km. There are four possible clauses obtained by S-modification and T-modification from C with respect to s ≃ t:
DDDD4213 :::: st ≃≃ zz ∨∨ nnvvs22t ≃≃66≃≃ xxzz ∨∨∨∨ KKKK1111′′′′ ∨∨∨∨ ···· ···· ···· ∨∨∨∨ KKKKmmmm′′′′ iiiiffff ttss iiiissss aaaa vnvnaoaornrnii-a-avvbbaallrereiiaxaxbbllee tteerrmm nnvv22 where z is a fresh variable. All of these clauses have possibilities to be used as an expansion clause for the strong connection in CT≃. Next we consider new strong connection rules for CTwS in order to simulate these inferences in CT≃. a=b
ST-Left a=z
b㻛 z
C4 Order Violated !! b㻛 u3 a㻛 u3 a>b
㼠 x1㼠=x1 㱔 ={z/u3, u3/b, …} 䎀 P C6
b=z P 㼠
Q x1㼠=x1 Succeed !!
Firstly, we study a simulation of strong connection using the clause D1 in SMT(S). Consider an expansion inference for D1 in CT≃. If L is a negative equality nv1 6≃ r such that nv1 is non-variable and is unifiable with s, then the following strong connection is available in CT≃: (1) (2) On the other hand, if L is a positive equality u ≃ v such that u is unifiable with nv2, then we have the following strong connection in CT≃:
s ≃ z ⊥ · (nv1 = s ≻ z = r)
The above first inference (1) in CT≃ can be simulated in nSMT(S) with the new
expansion rule and ST-splitting for a raw equality s ≃ nv2 and the weak connection
rule as follows:
However, it is definitely better to use a sort of strong connection rule instead of the
weak connection, because a connection constraint for a tableau becomes much simpler
and more effective to drastically reduce the search space. We, hence, introduce a new
strong connection rule which can perform the above inference steps as an integrated
one-step inference in CTwS. The following is a naive form for directly simulating the
inference (1):
where nv1 and nv2 are non-variable terms. We can eliminate the link variable z
because z never occurs elsewhere in a tableau, and moreover we can add an ordering
constraint. The final form of the above rule is:
Remark: The above ordering constraint nv2 r is not explicitly used in the strong
connection in CT≃, as shown in the inference (1). Thus this additional constraint can
reduce the alternative choices of expansion rules, compared with CT≃. Recall the
term nv2 initially occurs as an argument of the equality s ≃ nv2 of the original clause
s ≃ nv2 ∨ K1 ∨ · · · ∨ Km in S. Thus we can say, CTwS directly uses full information
of the equality s ≃ nv2 for strong connection and thus expansion, while CT≃ just
uses this information indirectly through variable binding for a linked variable.4 This
difference is a rather important point because several state-of-arts top-down provers,
such as SETHEO [
Similarly, the above inference (2) can also be simulated in nSMT(S) with a raw positive equality s ≃ nv2 as follows:
u ≃ v
We can also eliminate the link variable z and add an additional ordering for s ≃ z without losing completeness. Finally, we obtain the following new rule: nSMT(S) || Γ, u ≃ v, s ≃ nv2 s ≃ z Notice that this rule superficially requires a positive raw literal s ≃ nv2 as a partner of strong connection of a positive literal u ≃ v.
Next we study a simulation of strong connection using the clause D2. Consider the following inference involving expansion and strong connection of D2 in CT≃. (3) where nv1 is a non-variable term. The above (3) can simply be simulated in nSMT(S) with the raw equality s ≃ x as follows:
Moreover, we have to investigate inferences using strong connections with the clauses D3 and D4 of SMT(S), and can derive additional three rules for nSMT(S) by similar discussions. Eventually, we obtain the following set of strong connection rules for nSMT(S): Strong Connection for Negative Equality in nSMT(S):
nSMT(S) || Γ, nv1 6≃ r, s ≃ nv2 where nv1 and nv2 denote non-variable terms, x is a variable.
We show a total view of the connection tableaux CTwS for nSMT(S) in Fig. 5. The following is the first main theorem of this paper: Theorem 5 The calculus CTwS is sound and complete. That is, S ∪ E is unsatisfiable iff there is a closed and strongly connected tableau in CTwS for nSMT(S). 3.3
Yet another Connection Tableaux for Modification In this section, we consider yet another connection tableaux, called CTwST, where the strong connection for positive equality is further improved with a more strict ordering constraint. As was shown in the previous subsection, one of the strong connection for a positive equality for nSMT(S) is:
nSMT(S) || Γ, s ≃ t, nv1 6≃ r ⊥ · (nv1 = s ≻ t = r)
nSMT(S) || Γ, s ≃ nv1 s ≃ z nv1 6≃ z nSMT(S) || Γ, nv1 ≃ t t ≃ z nv1 6≃ z
nSMT(S) || Γ, ¬P (r), P (s) ⊥ · (r = s)
nSMT(S) || Γ, nv1 6≃ r, s ≃ nv2
Equality Resolution (ER) nSMT(S) || Γ, l 6≃ r
⊥ · (l = r) Recall that T-modification splits a given negative equality l 6≃ r into the disjunction l 6≃ z ∨ r 6≃ z if r is not a variable. Thus, the literal l 6≃ z (or r 6≃ z) loses the information about the initial partner term r (or respectively, l). Thus the above strong connection rule cannot utilize full information provided by negative equalities in a clause set S which is initially given. As a remedy, we omit T-modification for negative equality literals as well, and instead give a set of new connection rules for preserving transitivity Definition 2 We define nSM(S) to be a a set of normal clauses obtained from S by just applying negative S-modification and M-modification.
The calculus CTwST differs from CTwS in the following points; firstly CTwST accepts nSM(S) as an input set of clauses, not nSMT(S); secondly we add a new expansion rule and T-splitting rules for treating a raw negative equality; thirdly we replace the strong connection SC-PosE-1 with new three rules with raw negative equalities. We modify the expansion rule to the one which produces raw literals both for positive and negative equalities. Given a literal L, we write [[L]] to denote the framed literal
L , called a raw literal if L is a positive equality s ≃ t or a negative equality s 6≃ t; otherwise [[L]] denotes L itself.
nSM(S), (L1 ∨ · · · ∨ Lk) || Γ
[[L1]] · · · [[Lk]] We add the following T-splitting rules in order to treating raw negative equalities, which naturally correspond with T-modification.
T-Splitting for Negative Equality for nSM(S):[-0.5ex] nSM(S) || Γ, s 6≃ nv1 s 6≃ z nv1 6≃ z nSM(S) || Γ, s 6≃ y s 6≃ y At last, we replace the rule SC-PosE-1 by the following three rules: Strong Connection for Positive Equality for nSM(S): nSM(S) || Γ, l ≃ r, nv1 6≃ nv2 nSM(S) || Γ, l ≃ r, s 6≃ nv2 ⊥ · (nv1 = l ≻ r) nv2 6≃ r · (nv2 r) s 6≃ r · (s r) ⊥ · (nv2 = l ≻ r) nSM(S) || Γ, l ≃ r, nv1 6≃ y
⊥ · (nv1 = l ≻ r = y) 4
Extended SOLAR and Experimental Evaluation
In this section, we show some tentative experimental results with SOLAR [
SOLAR
performance of SOLAR compared with state-of-the-art theorem provers Otter 3.0 [
Table 2 shows the performances of several kinds of equality computation methods
in connection tableaux.6 The first “Axioms” indicates a naive use of the congruence
axioms, and the second “M-mod” represents a method for using just M-modification
together with reflexivity, symmetry and transitivity axioms. Each row denoted by
“infer.” is the sum total of the numbers of inferences needed for equational problems
which can commonly be solved by all of CT≃, CTwS and CTwST. The upper half of
Table 2 shows the results obtained by using ordinary M-modification, while the lower
half is for the ones obtained by using a semi-optimized M-modification, given in [
We investigated Paskevich’s connection tableaux for equality computation, and pointed out that a naive use of S-modification is problematic. We proposed, as some remedies, improved connection tableau calculi for efficient equality computation. We also showed tentative experimental results of evaluating the proposed methods using SOLAR. This research is now in progress. For example, we are still studying a further 5TPTP library v.3.5.0 has 2,175 non-equational problems and 4,171 equational problems, where there are 863 unit equational problems.
6Throughout experiments, we used non-recursive Knuth-Bendix ordering given by Riazanov and
Voronkov [