The paper describes an approach to the construction of a resolution-type technique basing on a certain generalization of the resolution notion of a clause. This generalization called a conjunctive clause (c-clause) leads to a possibility to introduce two di erent inference rules and determine two c-clause calculi oriented to refutation search in rstorder classical logic both with and without equality. Using the connection of these calculi with Robinson's clash-resolution method, a simple way for the proving of their soundness and completeness is given. Analogs of some of the well-known resolution strategies for the calculi are suggested. Besides, the treatment of Maslov's inverse method in the resolution terms is given. This research can be used in (e-)learning systems for the intelligent testing of knowledge of trainees learning a mathematical subject.
This paper is devoted to the description of special calculi intended for the
establishing of the unsatis ability of a formula F of a certain form or a set S of
such formulas in rst-order classical logic maybe with equality. The calculi relate
to the class of refutation-search methods based on the ideas rstly presented in
Robinsin's paper [
After the appearance of the resolution method, the main e orts of automated
theorem-proving community were concentrated on its development in the
direction of the construction of its di erent modi cations and strategies oriented to
increasing the e ciency of deduction search. All such attempts based on the use
of a clause being a well-formed expression of the resolution method leaving aside
the possibility of building e cient methods using modi cations of the notion of a
clause, to which this paper is devoted. Besides, the problem of the interpretation
of the Maslov inverse method [
Our calculi completely are determined by their (resolution-type) inference rules. The deducibility of a special expression in such a calculus is equivalent to the unsatis ability of F or S. At that, is called a sound calculus, if the deducibility of implies the unsatis ability of F or S; is called a complete calculus, if the unsatis ability of F or S implies the deducibility of .
If we put certain restrictions on inferences of in a calculus , these restrictions are said to determine a strategy for proof search in .
All the above-said takes place for the clash-resolution method [
Let us stop on the way of the construction of an initial set of clauses for a
formula F (or a set S of such formulas) being investigated on unsatis ability.
First of all, we can consider that F is a closed formula. Further, let us suppose
that F already is presented in Skolem functional form (for satis ability), all
the quanti ers of which are omitted. Then, under the condition that all its
variables implicitly are bound by the universal quanti er, the following question
is reasonable: Can we refrain from the obligatory presentation F (or S) as a set
of clauses and develop a technique similar to the resolution one? Research in this
direction is described in what follows. At that, note that the papers [
We usually give references to the original papers, which laid the foundations
for the research in a particular direction, although for the modern description of
most of them, one can turn to [
First-order classical logic with functional symbols and equality is considered.
The notions of terms, atomic formula, and formulas are assumed to be known. A formula being the result of renaming of variables in a formula F is called a variant of F . A literal is an atomic formula or its negation. For a literal L of the form :A, its complementary L~ is A. If L is an atomic formula A, then its complementary L~ is :A.
As it was said above, we restrict ourselves by the consideration of only closed formulas F presented in Skolem functional form for satis ability by means of the elimination of positive quanti ers. That is, F may be considered as a formula of the form 8x1 : : : 8xm G(x1; ; xm), where x1; ; xm all the variables of F , and G(x1; ; xm) a quanti er-free formula. I. e. it can be assumed that in the case of reasoning on satis ability, one has to deal with only quanti er-free formulas, all variables of which implicitly are universally bound.
We can reduce G(x1; ; xm) to a formula D1 ^ : : : ^ Dn, where Di is a formula presented in disjunctive normal form (DNF). As a result, we can make investigation of the set fD1; : : : ; Dng on unsatis ability instead of making the appropriate investigation of G(x1; ; xm). This leads to the following notions.
If L1; : : : ; Lm are literals, then the expression L1 ^: : :^Lm (m 1) is called a conjunct. An expression of the form C1 _: : :_Cn, where C1; : : : ; Cn are conjuncts, is called a conjunctive clause, or a c-clause (n 0).
A c-clause not containing any conjunct (that is, if n = 0) is called an empty clause (or empty c-clause) and denoted by .
In what follows, any conjunct is considered to be the set of its literals and
any c-clause { the set of its conjuncts. Thus, in the case when any conjunct of
a c-clause contains exactly one literal, this c-clause can be considered as a usual
clause (see, for example, [
The introduced de nitions allow us to use all the semantic notions of rstorder classical logic for c-clauses and sets of c-clauses under the assumption that every variable in any c-clause is universally bound. The empty clause is considered to be an unsatis able formula.
Our main purpose is to prove that the inferring of in our calculi is equivalent to the unsatis ability of an initial set of c-clauses.
An inference from an initial set S of c-clauses in a calculi under consideration is a sequence D1; : : : ; Dn, where every Di (i = 1; : : : ; n) is either a variant of an c-clause from S or a variant of a conclusion of a rule applied to some of the c-clauses preceding Di. Therefore, our calculi uniquely are identi ed by their inference rules. That is why the names of rules will serve as unique names of the calculi under consideration. The deducibility of a c-clause C from a set S of c-clauses in a calculus is denoted by S ` C.
The resolution method rst was published in [
Let us give some necessary notations.
A substitution, , is a nite mapping from variables to terms that has the form = fx1 7! t1; : : : ; xn 7! tng, where variables x1; : : : ; xn are pairwise di erent and for any i (1 i n), the term ti is distinct from xi.
A substitution is called a variant substitution if t1, : : :, tn from are only variables that are pairwise di erent. In this case, the inverse (one-one) correspondence 1 exists and presents itself a (variant) substitution.
For an expression Ex and a substitution , the result of the application of to the expression of Ex is understood in the usual sense; it is denoted by Ex .
The composition of substitutions (as mappings) and is denoted by . It has the property that for any expression Ex, Ex ( ) = (Ex ) .
For any set of expressions, denotes the set obtained by the application of to each expression in . If is a set of (at least two) expressions and a singleton, then is called a uni er of . If 1; : : : ; n (n 1) are sets of expressions and for a substitution , the set i is a singleton (i = 1; : : : ; n), then is called a simultaneous uni er of 1; : : : ; n.
It is known (see, for example, [
Obviously, we can consider that any mgsu has the idempotence property that means that = . This fact will often be used in what follows implicitly.
Robinson's latent clash-resolution rule (RR). Let clauses C0; C1; : : : ; Cq (q 1) with mutually distinct variables be of the forms C00 _ L1;1 : : : _ L1;r1 : : : _ Lq;1 _ : : : _ Lq;rq , C10 _ E1;1 _ : : : _ E1;p1 , : : :, Cq0 _ Eq;1 _ : : : _ Eq;pq respectively, where C00; C10; : : : ; Cq0 are clauses and L1; : : : ; Lq; E1;1; : : : Eq;pq literals. Suppose that there exists the mgsu
of the sets fL~1;1;: : : ;L~1;r1 ; E1;1;: : : ; E1;p1 g, : : :, fL~q;1;: : : ; L~q;rq ; Eq;1;: : : ; Eq;pq g. Then the clause C00 _ C10 _ : : : _ Cq0 is said to be deducible from C0; C1; : : : ; Cq by the rule RR.
The RR-rule with two clauses as its premises will be denoted by RR2.
The paper [
Robinson's Proposition. An initial set S of clauses is unsatis able if and only if the empty clause is inferred in the RR-calculus. 3
Below, we introduce two resolution-type rules in order to de ne two speci c cclause calculi. These calculi have a number of similar properties. That is why their proofs are detailed only for one of them. As to the other calculus, the corresponding proofs for it can be obtained in the same way. 3.1
Let us start with the consideration of the calculus that is based on the analog of Robinson's rule RR.
Clash-resolution (CR). Let c-clauses D0; D1; : : : ; Dq (q 1) pairwise without common variables be of the forms D00 _ K1;1 _ : : : _ K1;r1 _ : : : _ Kq;1 _ : : : _ Kq;rq , D10 _ M1;1 _ : : : _ M1;p1 , : : :, Dq0 _ Mq;1 _ : : : _ Mq;pq respectively, where D00; : : : ; Dq0 are c-clauses and K1;1; : : : ; Kq;rg ; M1;1; : : : Mq;pq conjuncts. Suppose that K1;1; : : : ; Kq;rq contain literals L1;1; : : : ; Lq;rq respectively and for every j = 1; : : : ; q, Mj;1;: : :Mj;pj contain literals Ej;1;: : :Ej;pj respectively such that there exists the mgsu
of the sets fL~1;1;: : : ;L~1;r1 ; E1;1;: : : ; E1;p1 g, : : :, fL~q;1;: : : ; L~q;rq ; Eq;1;: : : ; Eq;pq g. Then the c-clause D00 _ D10 _ : : : _ Dq0 is said to be inferred from the nucleus D0 and electrons D1; : : : ; Dq by the CRrule. Besides, the q-tuple hD0; D1; : : : ; Dqi is called a CR-clash and D00 _ D10 _ : : : _ Dq0 its CR-resolvent.
Remark. If D0; D1; : : : ; Dq are only clauses, the de nitions of CR and RR are coincides, which gives a simple way for proving some results relating to CR.
Proof. Since we implicitly consider every variable in any c-clause to be bound by the universal quanti er, obviously it is enough to prove that a CR-resolvent is the logical conclusion of its premises only in the propositional case. For this, it is enough to check the validity of the propositional formula:
((D00 _ (L~1;1 ^ K10;1) _ : : : _ (L~1;1 ^ K10;r1 ) _ : : : _ (L~q;1 ^ Kq0 ;1) _ : : : _ (L~q;1 ^ Kq0 ;rq )) ^ (D10 _ (L1;1 ^ M10;1) _ : : : _ (L1;1 ^ M10;p1 )) ^ : : : ^ (Dq0 _ (Lq;1 ^ Mq0;1) _ : : : _ (Lq;1 ^ Mq0;pq ))) (D00 _ D10 : : : _ Dq0), where is the implication symbol, which can be made by applying induction on q. QED.
Let a c-clause D distinguished from be of the form K1 _ : : : _ Kn. Then (D) is the set fL1 _ : : : _ Ln : L1 occurs in K1; : : : ; Ln occurs in Kng.
For , we suppose that ( ) contains and only it.
If S is a set of c-clauses, then (S) denotes the set SD2S (D).
It is obvious that for any non-empty set S of c-clauses, (S) is a nite nonempty set and contains only clauses. Moreover, considering D as a formula, we can produce (D) my means of applying the following propositional tautology: A _ (B ^ C) (A _ B) ^ (A _ C), where is the logical equivalence symbol. Therefore, a set S is unsatis able if and only if (S) is an unsatis able set.
Remark. According to the previous remark, we conclude that Robinson's clash-resolution technique is used when we are interested in the establishing of the deducibility of from (S) in the CR-calculus. Thus, for any nite set S of c-clauses, it is true that S is unsatis able if and only if (S) `CR . Lemma 1. Let D0; D1; : : : ; Dq be c-clauses and A0; A1; : : : ; Aq clauses such that A0 2 (D0); A1 2 (D1); : : : ; Aq 2 (Dq). If for A0; A1; : : : ; Aq, there is the CRclash hA0; A1; : : : ; Aqi with A0 as a nucleus and A1; : : : ; Aq as electrons and A is its CR-resolvent, then there exists the CR-clash hD0; D1; : : : ; Dqi with D0 as a nucleus, D1; : : : ; Dq as electrons, and D as its CR-resolvent such that A 2 (D). Proof. Let us consider A0; A1; : : : ; Aq from the lemma conditions. Let they be of the form: B0 _ L1;1 _ : : : _ L1;r1 _ : : : _ Lq;1 _ : : : _ Lq;rq , B1 _ E1;1 _ : : : _ E1;p1 , : : :, Bq _ Lq;1 _ : : : _Lq;pq respectively, where B0; : : : ; Bq are clauses and L1;1; : : : ; Lq;rq ; E1;1; : : : Eq;pq literals such that there exists the mgsu of the sets fL~1;1, : : :, L~1;r1 , E1;1, : : :, E1;p1 g, : : :, fL~q;1, : : :, L~q;rq , Eq;1, : : :, Eq;pq g. Then the clause B0 _ B1 _ : : : _ Bn is a CR-resolvent of the above-given CR-clash.
Since A0 2 (D0); D0 can be presented in the form D00 _ K1;1 _ : : : _ K1;r1 _ : : : _ Kq;1 _ : : : _ Kq;rq , where D00 is a c-clause and K1;1; : : : ; Kq;rg conjuncts such that B0 2 (D00) and K1;1; : : : ; Kq;rg contain literals L1;1; : : : ; Lq;rq respectively.
Making reasoning in the similar way, we obtain that D1, : : :, Dq can be presented in the form D10 _ M1;1 _ : : : _ M1;p1 , : : :, Dq0 _ Mq;1 _ : : : _ Mq;pq respectively, where D10, : : :, Dq0 are c-clauses and M1;1; : : : Mq;pq conjuncts such that B1 2 (D10), : : : ; Bq 2 (Dq0) and M1;1; : : :, Mq;pq contain E1;1; : : : Eq;pq .
In accordance with the de nition of CR, this means that D0; D1; : : : ; Dq form a clash with D0 as a nucleus and D1; : : : ; Dq as electrons. For this CR-clash, D00 _ D10 _ : : : _ Dq0 is its CR-resolvent. Obviously, B0 _ B1 _ : : : _ Bn 2 (D00 _ D10 _ : : : _ Dq0 ). QED.
Proposition 2. Let S be a set of c-clauses and B10, : : :, Bn0 an inference of from (S) in the RR-calculus. Then there exists an inference B1, : : :, Bn of from S in the CR-calculus such that for every j (j = 1; : : : ; n) Bj0 2 (Bj ) and if Bj0 is a variant of a CR-resolvent of the CR-clash hBi0r , : : :, Bi01 i with Bi0r as its nucleus, then Bj is a variant of a CR-resolvent of the CR-clash hBir , : : :, Bi1 i with Bir as its nucleus (i1 < : : : < ir < j).
Proof. Let B10, : : :, Bn0 be an inference of from (S) in the RR-calculus. It is an inference of from (S) in the CR-calculus
For each i = 1; : : : ; n, assign a c-clause Bi to a clause Bi0 in the following way. j = 1. The de nition of an inference implies that B10 is a variant of a clause C 2 (S). That is there exists a variant substitution such that B10 is C . Hence, we can select such a c-clause D in S that C 2 (D). Take D as B1. Obviously, B10 2 (B1).
Suppose that j > 1 and we have c-clauses B1 : : :, Bj 1 that pairwise have no common variables and satisfy the conditions: B10 2 (B1), : : :, Bj0 1 2 (Bj 1). Two cases are possible.
(1) Bj0 is a variant of a clause C 2 (S). Proceeding in the same manner as in the case of j = 1, we easily achieve the necessary renaming some of the variables of D in order the result Bj has no common variables with B1, : : :, Bj 1.
(2) Bi0 is a variant of a CR-resolvent C of a CR-clash hBi0r , : : :, Bi01 i with Bi0r as its nucleus (i1 < : : : < ir). Accordantly to Lemma 1, we can construct the CR-clash hBir , : : :, Bi1 i with Bir as its nucleus and D as its CR-resolvent, for which C 2 (D).
Let be a variant substitution such that Bi0r is C . Obviously, we can select a variant B of D not having common variables with B1, : : :, Bj 1 and satisfying the condition Bj0 2 B. Denote this B by Bj .
Let us consider B1; : : : ; Bn. Since Bn0 is and ( ) contains only , Bn is the empty clause . Thus, accordingly to the construction of B1; : : : ; Bn, this sequence is an inference of satisfying the conclusion of the proposition. QED.
Now, it is easy to obtain the soundness and completeness of the CR-calculus. Theorem 1 (Soundness and completeness of CR-calculus). A set S of c-clauses is unsatis able if and only if S `CR .
Proof. The soundness of CR is provided by Prop. 1.
Completeness. If S is an unsatis able set of c-clauses, then (S) is an unsatis able set of clauses. The calculus RR is complete (Robinson's proposition). Hence, (S) `RR . Thus, S `CR on the basis of Prop. 2. QED.
Let us consider an example of a deduction in the CR-calculus. Note that all the examples in the paper are given only for propositional case since the resolution-type technique under consideration uses the usual uni cation. Example 1. Let U denote the following set of c-clauses: f(A ^ :A) _ (B ^ C) _ (E ^ L), :B _ :C, :E _ :Lg, where A; B; C; E, and L are atomic formulas. The (minimal) inference of from U in CR is as follows: 1. (A ^ :A) _ (B ^ C) _ (E ^ L) (2 U ), 2. (A ^ :A) _ (B ^ C) _ (E ^ L) (2 U ), 3. (B ^ C) _ (E ^ L) (by CR from (1) as a nucleus and (2) as an electron), 4. (B ^ C) _ (E ^ L) 5. :B _ :C 6. E ^ L 7. E ^ L 8. :E _ :L 9.
(a variant of (3)), (2 U ), (by CR from (5) as a nucleus and (3) and (4) as electrons), (a variant of (6)), (2 U ), (by CR from (8) as a nucleus and (6) and (7) as electrons).
Therefore, the set U is unsatis able. 3.2
Maslov's inverse method (denoted by MIM here) and Robinson's resolution
method (the calculus of clauses in our terminology) appeared approximately
at the same time: MIM { in 1964 [
After their appearance, the problem of the interpretation of MIM in the
resolution terms has arisen. This problem has attracted the attention of a number
of researchers in inference search (see, for example, [
In [
Inverse resolution (IR). Let c-clauses D0; D1; : : : ; Dq (q 1) pairwise without common variables be of the forms D00 _ K1 _ : : : _ Kq, D10 _ N11;1 _ : : : _ N11;p1;1 _ : : : _ N1r;11 _ : : : _ N1r;1p1;r1 , : : :, Dq0 _ Nq1;1 _ : : : _ Nq1;pq;1 _ : : : _ Nqr;q1 _ : : : _ Nqr;qpn;rn respectively, where D00; : : : ; Dq0 are c-clauses and K1; : : : ; Kq; N11;1; : : : ; Nqr;qpn;rn conjuncts. Suppose that for every j (1 j q), Kj contains literals Lj;1; : : : ; Lj;rj and Nj1;1; : : : ; Nj1;pj;1 ; : : : ; Njr;j1; : : : ; Njr;jpj;rj contain literals Ej1;1; : : : ;Ej1;pj;1 ; : : : ; Ejr;j1; : : : ; Ejr;jpj;rj respectively such that there exists the mgsu
of the sets fL~1;1; E11;1; : : : ; E11;p1;1 g; : : : ; fL~1;r1 ; E1r;11; : : : ; E1r;1p1;r1 g; : : : ; fL~q;1; Eq1;1; : : : ; Eq1;pq;1 g; : : : ; fL~q;rq ; Eqr;q1;: : : ; Eqr;qpq;rq g. Then the c-clause D00 _ D10 _ : : : _ Dq0 is said to be inferred from the nucleus D0 and electrons D1; : : : ; Dq by the IR-rule. Besides, the q-tuple hD0; D1; : : : ; Dqi is called its IR-clash and D00 _ D10 _ : : : _ Dq0 its IR-resolvent.
Having the IR-rule, we can speak about the IR-calculus.
1 In 1989, V. Lifschitz independently introducing the notion of a c-clause under the
name of a super-clause improved such interpretation [
The comparative analysis of IR and CR shows that the only di erence between them is in the ways of the selection of cutting literals for their applications. The following statement contains a more detailed explanation of this observation. Lemma 2. If hD0, D1, : : :, Dqi is a CR-clash with D0 an its nucleus and D1; : : :, Dq as its electrons, then for any its CR-resolvent D, it is possible to construct an IR-clash with D0 as its nucleus and certain variants of D1, : : :, Dq as its electrons such that for its some IR-resolvent D0 and a substitution , D = D0 . Proof. If hD0, D1, : : :, Dqi is the CR-clash from the de nition of CR-rule, then the c-clauses D0, D1, : : :, Dq can be presented as D00 _ K1;1 _ : : : _ K1;r1 _ : : : _ Kq;1 _ : : : _ Kq;rq , D10 _ M1;1 _ : : : _ M1;p1 , : : :, Dq0 _ Mq;1 _ : : : _ Mq;pq respectively, where D00; : : : ; Dq0 are c-clauses and K1;1; : : : ; Kq;rg ; M1;1; : : : Mq;pq conjuncts and moreover for literals L1;1; : : : ; Lq;rq , Ej;1; : : :Ej;pj from K1;1; : : : ; Kq;rg , M1;1; : : : Mq;pq respectively, there exists the mgsu of the sets 1 = fL~1;1;: : : ;L~1;r1 ; E1;1;: : : ; E1;p1 g, : : :, q = fL~q;1;: : : ; L~q;rq ; Eq;1;: : : ; Eq;pq g such that D = D00 _ D10 _ : : : _ Dq0 .
Let us take such variant substitutions 1;1, : : :, 1;r1 ,: : :, q;1,: : :, q;rq that D1 1;1,: : :, D1 1;r1 , : : :, Dq q;1 : : : Dq q;rq have no common variables with D0 and each other. Considering 1;11, : : :, q;rq 1 as mapping graphs, construct the set 1;11 [ : : : [ q;1rq . Obviously, it is a (variant) substitution. Let us denote it by and the c-clause Dj0 j;k _ Mj;1 j;k _ : : : _ Mj;pj j;k by Djk.
Let us consider D11, : : :, D1r1 , : : :, Dq1, : : :, Dqrq . Accordantly to their de nition and the de nition of , we have that Djk is the same as Djk j;k1 and, therefore, it is the same as Dj (j = 1; : : : ; q; k = 1; : : : ; rj ). Thus, we can select literals E11;1; : : : ;E11;p1 ; : : : ; E1r;11; : : : ; E1r;1p1 , : : :, Eq1;1; : : : ;Eq1;pq ; : : : ; Eqr;q1; : : : ; Eqr;qpq in M1;1 1;1; : : :, M1;p1 1;1, : : :, M1;1 1;r1 ; : : :, M1;p1 1;r1 , : : :, Mq;1 q;1; : : :, Mq;pq q;1, : : :, Mq;1 q;rq ; : : :, Mq;pq q;rq respectively, such that Eik;j i;k1 = Eik;j = Ei;j (i = 1; : : : ; q; j = 1; : : : ; pq; k = 1; : : : ; rq).
Considering and as mapping graphs, we conclude that = [ is a substitution. Because is the mgsu of the sets 1; : : : ; q, the de nition of and the idempotence of imply that is a simultaneous uni er of the sets of literals fL~1;1 E11;1; : : : ;E11;p1 g; : : : ; fL~1;r1 E1r;11; : : : ; E1r;1p1 g, : : :, fL~q;1 Eq1;1; : : : ;Eq1;pq g; : : :, fL~q;rq Eqr;q1; : : : ; Ejr;qpq g. Therefore, there exists the mgsu of these sets, for which = , where is a substitution.
As a result, we have that D0, D11, : : :, D1r1 , : : :, D1q, : : :, Dqrq can form the IR-clash with D0 as its nucleus and D11, : : :, D1r1 , : : :, D1q, : : :, Dqrq as its electrons that produces the IR-resolvent D0 = D00 _ D10 ( 1;1 ) _ : : : _ D10 ( 1;r1 ) _ : : : _ Dq0 ( q;1 ) _ : : : _ Dq0 ( q;rq ).
Since = and = [ , it is obvious that D0 = D. QED.
This result permits to \simulate" any inference in CR by an inference in IR. Proposition 3. Let S be a set of c-clauses and B1, : : :, Bn an inference of from S in the CR-calculus. Then there exists an inference B10, : : :, Bm0 of from S in the IR-calculus (m n) such that if Bj is a variant of a CR-resolvent of an CR-clash with Br as its nucleus, then for some j0 and r0 (j0 j; r0 r), Bj0 0 is a variant of an IR-resolvent of the corresponding IR-clash with Br00 as its nucleus; moreover, Bj = Bj0 0 for some substitution .
Proof. As in the case of the CR-rule, it is enough to establish the validity of the following formula, \extracted" from the de nition of IR-rule:
Theorem 2 (Soundness and completeness of IR-calculus). A set S of c-clauses is unsatis able if and only if S `IR .
Proof. The soundness is provided by Prop. 4.
Completeness. If S is unsatis able set, then S `IR by Theorem 1. By Prop. 3, any inference of from S in CR can be transformed into an inference of from S but already in the IR-calculus, that is S `IR . QED.
Example 2. Let us consider the set U from Example 1 and construct the (minimal) inference of from U in IR is as follows: 1. (A ^ :A) _ (B ^ C) _ (E ^ L) (2 U ), 2. (A ^ :A) _ (B ^ C) _ (E ^ L) (2 U ), 3. (B ^ C) _ (E ^ L) (by IR from (1) ac a nucleus and (2) as an electron), 4. :B _ :C (2 U ), 5. :E _ :L (2 U ), 6. (by IR from (3) as a nucleus and (4) and (5) as electrons).
We have again proved the unsatis ability of U .
Draw your attention to the fact that this inference in IR is shorter than the inference in CR from Example 1. This situation is more or less standard for these calculi (see the section containing a comparison of CR and IR). 4
The CR- and IR-calculi admit equality handling based on a modi cation of the
paramodulation rule that was proposed in [
We are needed in the following notions that provide us with a possibility to reduce the establishing of the validity of the rst-order statement with equality to the search of the refutation of a certain set of c-clauses.
Let S be a set of c-clauses. Then S' denotes the set of equality axioms for S
in the form of clauses, in which x; y; z; x0; : : : ; xp are variables (see, for example,
[
A set S of c-clauses is called equationally unsatis able if and only if the set S [ S' is unsatis able.
Thus, in the case when we have deals with S requiring equality handling,
we must establish the equationally unsatis ability of the set S, which can be
achieved by deducing the empty clause from S [ S'. But such approach leads
to the extreme large growth of the searching space. For the optimization of such
growth, we use a modi cation of the paramodulation rule [
Paramodulation rule PP. Let we have two c-clauses D and D0 _ (K ^ s ' t), where D0 is a c-clause and K conjunct (possibly, empty). If there exists mgsu of the set of terms fs; ug, where u is a term occurring in D at a selected position, then the c-clause D0 _ (D )[t ] is said to be inferred from these c-clauses by the rule P P , where (D )[t ] denotes the result of replacing in D the term u being at the selected position by t . At that, the ordered pair h D, D0 _ (K ^ s ' t) i is called a PP-clash (w.r.t. s ' t) with the P P -paramodulant D0 _ (D )[t ], nucleus D, and electron D0 _(K ^s ' t).
The set Sf of functionally re exive axioms for a set S of c-clauses consists of all the clauses of the form f (x1; : : : ; xp) ' f (x1; : : : ; xp), where f is a p-arity function symbol occurring in S.
Adding P P to the CR- and IR-calculi, we get the calculi CR+PP and IR+PP intended for inference search in rst-order classical logic with equality.
Remark. If in the above-given de nition, P P is applied to only clauses, we
have the usual paramodulation rule from [
Because of the completeness of the inference system \negative hyper-resolution
+ paramodulation" (see, for example, [
Robinson-Wos's Proposition. A set S of c-clauses is equationally unsatisable if and only if (S) [ fx = xg [ Sf `RR+P .
Taking into account the well-known result [
Now, we have all the necessary for obtaining the results about the completeness of the calculi CR+PP and IR+PP.
First of all, the following analog of Lemma 1 for the P P -rule is obvious. Lemma 3. Let D and D0 _ (K ^ s ' t) are c-clauses from the de nition of P P . If for C 2 (D) and C0 2 (D0), there exists the P P -clash hC, C0 _ s ' ti w.r.t. s ' t with a P P -paramodulant A, then there exists the P P -clash hD, D0 _ (K ^ s ' t)i w.r.t. s ' t with such a P P -paramodulant B that A 2 (B).
Using this lemma and Prop. 2 and 3, it is easy to obtain the following result. Proposition 5. Let S be a set of c-clauses and B10, : : :, Bn0 an inference of from (S) [ fx = xg [ Sf in the calculus RR+P. Then there exists an inference B1, : : :, Bn of from S [ fx = xg [ Sf in the calculus CR+PP (IR+PP) such that: (1) if Bj0 is a variant of a resolvent of an RR-clash with Br0 as its nucleus, then for some j0 and r0, Bj0 is a variant of a resolvent of the corresponding CR-clash (IR-clash) with Br0 as its nucleus and, additionally, Br0 2 (Br0 ) for some substitution ; (2) if Bj0 is a variant of a paramodulant of a P P -clash with Br0 as its nucleus, then for some j0 and r0, Bj0 is a variant of a paramodulant of the P P -clash with Br0 as its nucleus and Br0 2 (Br0 ) for some substitution .
This proposition, in fact, guarantees the completeness of the paramodulation extensions of the CR- and IR-calculi as well as their methods and strategies, some of which are given in the next section. Note that the soundness of such extensions is provided by Prop. 1 and 4 and the obvious fact that P P -paramodulant is a logical conclusion of the conjunction of all the c-clauses from fN; Eg [ fN; Eg', where N is a nucleus and E an electron of a P P -rule application. Theorem 3 (Soundness and completeness of CR+PP and IR+PP). A set S of c-clauses is equationally unsatis able if and only if S [ fx = xg `IR+P P (S [ fx = xg `CR+P P ). Moreover, CR (IR) can be the only binary rule. Proof. The soundness of CR+PP and IR+PP is provided by the remark in the preceding paragraph. Completeness takes place for CR+PP and IR+PP due to Corollary and Prop. 5. The completeness of CR+PP with the binary CR-rule is obvious. For proving the completeness of IR+PP with the binary IR-rule, it is enough to note that any binary application of CR can be \decomposed" into r1 binary applications of IR (see the proof of Lemma 2 for the binary case). QED. 5
Prop. 5 gives a simple way for transferring most part of the methods and
strategies taking place for the usual clash-resolution (RR) to the ones for the CR- and
IR-calculi for classical logic both with and without equality. For the
demonstration of how it is possible to do, let us consider the usual liner resolution and
positive and negative hyper-resolutions in their wording from [
Note that they are given for logic with equality. To obtain them for the case without equality, it is enough to delete all parts concerning the P P -rule in the de nitions and wordings of the theorems given below. Also note that their soundness is provided by the soundness of the rules CR, IR, and P P . That is why a soundness proof is absent in corresponding theorems.
Linear strategy for CR2+PP and IR2+PP. It permits to apply CR2 (IR2) or P P to the pair of c-clauses when beginning with the second rule application in an inference, any its c-clause is either a CR2-resolvent (IR2-resolvent) or P P -paramodulant of the previous application of the rule CR2 (IR2) or P P , and the other c-clause is a variant of either a c-clause from an initial set S of c-clauses or a c-clause that was deduced earlier.
Theorem 4 (Soundness and completeness of linear strategy for CR2+PP and IR2+PP). A set S of c-clauses is equationally unsatis able if and only if there exists an inference of from S [ fx = xg [ Sf satisfying to the linear strategy for CR2+PP (IR2+PP).
Proof. Completeness takes place due to the completeness of the usual linear
resolution with paramodulation [
Positive and negative hyper-resolution for CR2+PP (IR2+PP). An atomic formula is called a positive literal. A literal of the form :A, where A is an atomic formula, is a negative one.
A c-clause is called a positive (negative) if each its conjunct contains at least one positive (negative) literal. Note that there are c-clauses being positive and negative at the same time, for example, :A ^ A.
A CR- or IR-clash hD0; D1; : : : ; Dqi with D0 as a nucleus and D1; : : : ; Dq as electrons is called positive (negative), if D1; : : : ; Dq are positive (negative) c-clauses and the cut literals Lj;k in the de nitions of CR or IR respectively are negative (positive).
For logic without equality, positive (negative) hyper-resolution strategy for CR and IR permits constructing inferences containing only the positive (negative) hyper-resolution clashes with positive (negative) CR- or IR-resolvents.
In the case of logic with equality, we additionally permit to apply the P P -rule only to positive nucleus and electron; moreover, a literal containing the selected occurrence of the term u (see the de nition of P P -rule) must be positive. Theorem 5 (Soundness and completeness of positive and negative hyper-resolutions with P P -rule). A set S of c-clauses is equationally unsatis able if and only if there exists an inference of from S [ fx = xg [ Sf satisfying to the positive and negative hyper-resolution with CR- (IR-) and P P -rules.
Proof. Completeness. Since there exists an inference of from (S)[fx = xg[Sf
satisfying to the usual positive (negative) hyper-resolution and
paramodulation (see [
Remark. In Theorems 9 and 10, the adding of functionally re exive axioms
to the set S is the necessary condition for completeness. Examples demonstrating
this for clauses (when CR, IR, and RR are coincided) can be found in [
Below, we give the description of MIM in the form of a special strategy for IR.
Maslov's inverse method deals with so-called favorable assortments. In this connection, we consider MIM as a calculus of favorable assortments that has two inference rule: A and B. The A rule determines an initial set of favorable assortments, while the B rule produces new favorable assortments from the already deduced ones. That is why we treat assortments as clauses and favorable assortments as favorable clauses being produced by the and rules (see below).
If C is a conjunct L1 ^ : : : ^ Lr, where L1; : : : ; Lr are literals, then C~ denotes the clause L~1 _ : : : _ L~r.
Rule . Let S be a set of c-clauses and Sd = fC~ : C is a conjunct from a c-clause belonging to Sg. If S = fC : C = C0 _ C00 , where C0, C00 2 Sd and C0 and C00 contain literals L and L0 respectively such that there exists the mgsu of fL~; L0gg, then any clause from S is called a f avorable one deduced from S by the -rule.
Obviously, S is a nite set if S is the same. Besides, each its (favorable) clause contains both a literal and its complementary. That is why S is a unsatis able set of c-clauses if and only if the set S [ S is unsatis able.
Rule . Let S be a set of c-clauses, D 2 S, D consists of q conjuncts, and C1, : : :, Cq be favorable clauses. If the IR-rule can be applied to D as a nucleus and C1, : : :, Cq as electrons, than the IR-resolvent of this application is called a f avorable clause that is deducible from D, C1, : : :, Cq by the -rule.
Note that the requirement that the number of conjuncts in D ids equal to q leads to the fact that any IR-resolvent of -rule is a clause.
In these terms, MIM presents itself the following strategy for IR-calculus called a MIM-strategy: First of all, we produce all the possible favorable clauses applying the -rule; then, we apply only the -rule attempting to deduce .
The soundness of the MIM-strategy provides the soundness of IR-rule and
the above-given remark about S [ S . As to completeness, the proof of it is
omitted here; we simply give the rewording of the main result for MIM from [
This result seams unexpected because of the requirement that D from the de nition of the -rule must consist of exact q conjuncts. This apparent contradiction is explained by the fact that when using the MIM-strategy, we construct S containing clauses, the usage of which in an application of the -rule can be considered as a \latent" way for reducing the number of electrons.
The below-given example demonstrates some of the features of inferences satisfying to the MIM-strategy.
Example 3. It is easy to see that for U from Example 1, U d = f:A _ A; :B _ :C, :E _ :L; B; C; E; Lg. As a result, U = f:A _ A _ :A _ A; :B _ :C _ B; :B _ :C _ C; :E _ :L _ E; :E _ :L _ Lg. We have the following MIM-inference: 1. (A ^ :A) _ (B ^ C) _ (E ^ L) 2. :B _ :C 3. :E _ :L 4. :A _ A _ :A _ A
We have proved the unsatis ability of U at the 3rd time. 7
One can see that the obtained results on the CR- and IR-calculi \echo" each other. In this connection, it is interesting to know is there any advantages of one of them over the other? Moreover that Prop. 3 states that any inference of in CR can be simulated by an inference of in IR with the same number of rule applications. This section contains an answer on this question when comparison is made w.r.t. inferences being minimal on the number of rule applications.
By ( ; ; S), denote the number all the c-clauses in an inference of a c-clause C from a set S in a calculus that are deduced by di erent rule applications. The inference is minimal on the number of rule applications if for any other inference 0 of a variant of C from S in , the inequality ( ; ; S) ( ; 0; S) holds.
Let denote an inference of from S in CR. Using Prop. 3, it is easy to construct an inference of from S in IR such that (IR; ; S) (CR; ; S). Thus, in the case when min and min denotes the minimal inferences on the introduced characteristic, we have that (CR; min; S) (IR; min; S) 0.
Let us make an attempt to nd an upper bound for this di erence restricting us by the case when an initial set S contains only c-clauses without variables.
Let us consider an application of IR-rule to a nucleus c-clause D0 and electron clauses D1, : : : ; Dn (n n) with an IR-resolvent D. Its attentive analysis demonstrates that this (n + 1)-arity application can be slitted into n binary applications of CR-rule in the following way: rst we make a binary application of CR to D0 and D1, then to an obtained CR-resolvent and D2, and so on. That is we can split any n + 1-arity IR-application into n binary CR-applications in such a way that for the result C of such CR-rule applications, C will contain all or some of conjuncts belonging to D.
This observation leads to the following upper bound for the di erence given above: (CR; min; S) (IR; min; S) P(mi 2), where mi is the arity of the ith CR-rule application in min and the sum is taken over all of mi.
To demonstrate that this upper bound is achieved, let us take the sets Sn = f(L1 ^ E1) _ : : : _ (Ln ^ En), (A1;1 ^ B1;1) _ : : : _ (A1;m1 ^ B1;m1 ) _ L~1 _ (2 S), (2 S), (2 S), (2 S), (2 S), j b A~n;mn _ B~n;mn _ L~n _ E~n (2 S), d (L1 ^ E1) _ : : : _ (Ln ^ En) (2 S), j L1 _ E~1 (by IR from the 1st-block c-clauses with the 1st c-clause as a nucleus), ~ j : : : b Ln _ E~n (by IR from the nst-block c-clauses with the 1st c-clause as a nucleus), ~
(by IR from the (n+1)st block c-clauses with the 1st c-clause as a nucleus).
Using the ideas from [
Now, let us convert into an inference of from Sn, but already in the CR-calculus in the following way:
For each i (i = 1; : : : ; n), let us replace the c-clause L~i _ E~i by the sequence of c-clauses (Ai;2 ^ Bi;2) _ : : : _ (Ai;mi ^ Bi;mi ) _ L~i _ E~i, : : :, (Ai;mi ^ Bi;mi ) _ L~i _ E~i, L~i _ E~i that along with the all c-clauses form the i th block is an inference of L~i _ E~i in CR. Replace the empty clause by the sequence (L2 ^ E2) _ : : : _ (Ln ^ En), : : :, : : : (Ln ^ En), , being an inference of in CR since (L2 ^ E2) _ : : : _ (Ln ^ En) is deduced from (L1 ^ E1) _ (L2 ^ E2) _ : : : _ (Ln ^ En) and (L1 ^ E1) by the CR-rule, : : :, (Ln ^ En) is deduced from (Ln 1 ^ En 1) _ : : : _ (Ln ^ En) and (Ln 1 ^ En 1) by the CR-rule, is deduced from (Ln ^ En) and (Ln ^ En) by CR.
We have that is an inference of from Sn in CR, for which (CR; ; Sn) = (Pn
i=1 mi) + (n + 1). Again using the ideas from [
Finally, we get (CR; ; Sn) (IR; ; Sn) = (n 1) + Pin=1(mi 1), that is the upper bound is reachable. 8
The paper does not touch any practical aspects and is purely theoretical. Nevertheless, the author considers that it may be useful for researchers involved in the implementation of intelligent systems, in particular, e-learning systems requiring tools for proof search in classical logic at least for the following reasons.
The research demonstrates that the transition to c-clauses being the generalization of the widely-used resolution notion as a clause gave the possibility to construct the calculi possessing di erent properties in general and not worsening such an important characteristic as the minimum number of rule applications in comparison with the usual resolution methods. Although now it is di cult to say that the \behavior" of provers based on these calculi will be better than the \behavior" of the well-know resolution provers such as Vampire or Prover 9, we may expect that more detailed analysis of the proposed approach will lead to the further improvement of the traditional resolution technique. From this point of view, MIM seems to be a more attractive method, possessing a number of positive features not mentioned in the paper and requiring a separate study.