Resolution in a New Modal Logic

1. INTRODUCTION

In the real world, the situation is often encountered where a postulate can be many-valued rather than two-valued. However, the many­ valued logic is too complex to be applied to predicate calculus in artificial intelligence.

There are some other interesting logics such as a modal logic, tense logic or fuzzy logic. The modal logic [2], [3] had its effective beginning with work of C.L. Lewis[3] some sixty years ago, and is known as the logic of necessity and possibility. The tense logic [4], [6] deals with statements containing tensed verbs or explicit temporal references, and is logically similar to the modal logic. In these logics, the mode and tense are represented by two monadic symbols, and a postu­ late can be two-valued; true or false.

The present paper proposes a new logic which falls under the heading of the ordinal modal logic in a wide sense.. The proposed logic deals with . statements which contain adverbs or verbs representing manner such as possibility, uncertainty and causality. Monadic operators called manner operators are introduced to express such manner. A postulate in the logic can be four-valued; for example, true, possibly true, possibly false, or false. That is, a value T or F is assigned to each atomic formula in a well-formed formula(wff), but a value T, T*, F*, or F is assigned to the wff as described in the following sections. Consequently, we call the new logic the multi­ binary logic or manner logic(ML). The manner logic can represent more complicated statements than the ordinal predicate logic, since it is essentially a four-valued logic.

Thus we are interested in the application of the ML to solve intellectual difficult problems. As is well known, the resolution principle due to Robinson[7], [8], [9] is a simple but extremely useful technique for mechanical theorem proving. It is difficult, however, to apply the Robinson's resolution principle to the ML, because clauses contain manner operators. To circumvent this diffi­ culty, additional clauses which are valid are used in a refutation process. The present paper considers some fundamental properties of the ML, and gives a new rule of inference for mechanical theorem proving.

2. FUNDAMENTAL PROPERTIES

This section is devoted to consideration of fundamental properties of the ML. We shall introduce the symbol "*" with intention of interpreting it as a manner operator, which is placed on the shoulder of well-formed formulas. Suppose a proposition P is interpreted as "She is beautiful". Then P* is "She is possibly beautiful", "She will ·be beautiful", or "She seems to be beautiful" or "She is very beautiful", in the sense of the modal, tense or fuzzy logic, respectively.

The symbols such as P, Q and R, that are used to denote propositions are called atoms. Definition 1 Well-formed formulas (wff) or formulas for short in the ML are defined recursively as follows:

1. An atom is a formula.

2. If G is a formula, then so are -c and G*.

3. If G and Hare formulas, then so are GVH, GII.H, G-+H.

4. All formulas are generated by applying the above rules.

In the ordinal logic, a well-formed formula can be either true or false. Here we represent "true" by T and "false" by F. Therefore, _,G is T when G is F, and is F when G is T. In the similar manner, G* is T* when G is T, and is F* when G is F. Consequently, a well-formed formula G can be T, T*, F* or F; that is, true, true in the sense of"*", false in the sense of "*", or false. For example, G is true, G is probably true, G is probably false, or G is false.

We begin by defining some logical symbols used here by means of Table 1. They are (negation), *(manner), v(disjunction), ~ (conjunction), and -.(implication). This table expresses the truth value of the statements. It is seen from Table 1 that the implication can be represented by a negation and disjunction as follows:

where X andY are wffs.

Some examples of statements containing manner operators are shown below. Let P and Q be propositional symbols interpreted as

P : She is young.

Q : She is beautiful.

Then the expression X~Y asserts as follows:

P-. Q If she is young, then she is beautiful.

P .. Q*: If she is young, then she be beautiful. seems to

P*~Q : If she seems to be young, is beautiful. then she

P* .. Q*: If she seems to be young, seems to be beautiful. then she

(P-4'Q)*: It seems that if she is young she is beautiful.

As shown in the above examples, more complex statements can be represented if manner operators are employed.

Now, we consider the fundamental properties of the ML. Let P, Q, and R be atoms, and X, Y, and Z be well-formed formulas. From the truth table, Table 1, we have the following laws:

Distributed laws

Complement laws

These laws arc the same as those in the ordinal logic, but the following laws are peculiar to the ML.

Using the laws (1)- (15), we have the logical equivalences as follows:

o P A ""P* "' P 1\ F* , ... P A P* = ... P A F*.

[Proof] The proof is obtained from Eq. (13).

o py,..p* = P VT*,

._.py P* = -P vT*.

[Proof] The proof is obtained from Eq. (13).

o "'Pi\P*vPA-P* = F*.

[Proof] The proof is obtained from Eqs. (16) and (17).

o (P v P*) A ( ... p., ..... p*) F*.

[Proof] The proof is obtained from Eqs. (16) and (17).

[Proof] The proof is obtained from Eqs. (14) and (15).

[Proof] The proof is obtained from Eqs. (14) and (15).

[Proof] The proof is obtained from Eqs. (14) and (15) .

[Proof] The proof is obtained from Eqs. (14) and (15).

[Proof] The proof is obtained from Eqs. (18) and (19).

[Proof] The proof is obtained from Eqs. (14) and (15).

Now, we will show that a formula Y can be represented in the conjunctive and/or disjunc­ tive normal form.

Definition 2. A formula Y is said to be in a conjunctive or disjunctive normal form if and only if Y has the form

where each of Y1, ... , Yn is a disjunction or conjunction of literals with and without manner operators, respectively.

Let P1, P2, ... , Pm, Ql, Q2, ... , Qn be atoms, and Y(Pl, P2, . . . , Pm, Qy, Q~, ... , QA) be an (m + n)adic formula. Then we have

v ........ .

The former is the disjunctive normal form and the latter is the conjunctive normal form. As mentioned before, Y( ......... ) can beT, T*, F* or F, and then T* and F* appear in Eqs. (26) and (27). Using Eqs.(l8) and (19), however, we can eliminate T* and F*. Therefore, any formula can be represented by using

- , * , V , and II ·

3. RESOLUTION TECHNIQUES

As is well known, the resolution principle is a useful technique for making deduction in the system of the first-order predicate calculus. Here we consider techniques based on the resolution principle for the ML system. Some important definitions of terminology are given as follows:

Definition 3 A formula G is said to be satis­ fiable or semi-satisfiable if and only if there exists an interpretation I such that Y is evaluated to Tor T*, respectively. In this case , we say I satisfies or semi-satisfies Y. Definition 4 A formula is said to be unsatis­ fiable or semi-unsatisfiable, if and only if it is F or F* under all its interpretation. A formula is said to be satisfiable or semi­ satisfiable if and only if it is not unsatis­ fiable or not semi-unsatisfiable, respectively. Definition 5 A formula G is said to be a logical consequence or semi-consequence of a given set of formulas S, if and only if every interpretation satisfying or semi-satisfying S also satisfies or semi-satisfies G, respec­ tively.

Definition 6 Given a formula G, a formula G obtained by removing all manner operators in G is said to be a reduced formula of G. Definition 7 Given a clause C, a clause C obtained by removing all manner operators in C is said to be a reduced clause of C. Definition 8 A clause which takes F or F* is said to be an empty or semi-empty clause, respectively.

Processes for showing the unsatisfiability or semi-unsatisfiability are called refutation processes. The following theorems give basic properties used for refutation processes. Theorem 1

The following clauses C1 and C2 are valid.

[Proof]

From Eq. (17), we have

which gives the proof .

Theorem 2

Given formulas Y1, ... , Yn and a formula G, G is a logical consequence or semi-consequ­ ence of Y1, ..· , Yn if and only if the formula (Y1 ~ ... II Yn11 "'G) is unsatisfiable or semi­ unsatisfiable, respectively.

[Proof]

• ( .,. ) Suppose G is a logical consequence or semi-consequence. In an interpretation I satisfying or semi-satisfying Y1, ... , Yn, G is T or T* and then Y 1 " .. . ,.. Y n 11- G is F or F*, respectively.
• ( +-) Suppose Y1 A ··· 11 Yn A ... G is unsatisfi­ able or semi-unsatisfiable. For any interpre­ tation I, if Y1 11 ··· 11 Yn is TorT*, then G must be T or T* in I. Therefore, G is a logical consequence or semi-consequence of Y1 · · .. · Yn.

Now, we consider the application of the resolution principle due to Robinson to the theorem proving in the ML.

The resolution principle is essentially an elegant technique to check whether a given set of clauses is unsatisfiable or semi­ unsatisfiable.

Consider the following set of clauses

The resolution technique is very similar to that of Robinson except that clauses may contain manner operators. In this case, the resolvent Q* (clause C4) is obtained by deleting the pair of literals P and - P from clauses C1 and C2:

from c1 and c2.

q.e.d.

However, we have no way to get the resolvent from clauses c 3 and c4. Thus, a new set of clauses s2 is introduced such that

Since Cs is a tautology from Theorem 1, S2 is equivalent to S1 from the point of view of refutation processes. Thus we have

Therefore, S2 is semi-unsatisfiable and so is S1. In the above example, however, if C3 · "'Q* is used instead of c 3, then we have the empty

clause as the resolvent of C3 and C4.

Here a question arises : In what case a set of clauses is semi-unsatisfiable ? As described before, a formula G is a logical semi-consequence of YJ, ... , Yn if a semi­ empty clause is obtained as a resolvent in a refutation process. This means, therefore, that G is true tn a sense of "*"· For example, consider the case where "G*" asserts "It possibly rains". If·a semi-empty clause is obtained, the proof is possibly true or the inference is possibly correct. That is, it is possibly true to conclude that it rains. On the other hand, the proof is true if an empty clause is obtained. The following sets of clauses are also semi-unsatisfiable and give the same results as above.

Now we will show some important properties of a resolvent in the following theorems.

Theorem 3

A resolvent of given two clauses c 1 and c2 is a logical consequence or semi-consequence of C1 and C2.

[Proof]

Let C1, C2 and C3 be denoted as follows: C1=XvC{, C2=-Xvc2, C3=CivC2. The proof will be made in the case (i) X= F, (ii) F*, (iii) T*, and (iv) T. Suppose there exists an interpretation I for which C1 and C2 are T or T*. In cases (i) arid (ii), C{ must be Tor T*, and thus C3 = r or T*. In cases (iii) and (iv), C2 must beT or T*, and thus C3 = T or T*. This gives the proof. q.e.d.

Theorem 4

Let S be an unsatisfiable or semi­ unsatisfiable set of clauses and S be a reduced set of S. If an empty clause is obtained from S by applying the resolution principle, then either an empty or semi-empty clause is obtained from S. [Proof]

Let C3 be a resolvent of reduced clauses cl and c2. If cl and C2can be resolved, then they must be indicated as follows: C1 = L" C{, and c2 = -L" C2, where L is a literal. Therefore, we have (i) C1 = X v C{, C2 =-X VCi, or (ii) C1 · PvC{, C2 = -P*vC2. It is clear that an empty clause is obtained as the resolvent in the case (ii) and that an empty or semi~empty clause is obtained in the case (i).

Fig. 1 illustrates an example of refuta­ tion graphs for a set of clauses as follows:

F*

-P*(x) v Q(y) -P*(x) v Q*(y) : unused clauses Q(y) 1/ ""Q*(y) 1/ F* : tautology

4. CONCLUDING REMARKS

We have. considered a new logic called the ML and derived its mathematical properties. Due to manner operators introduced here, the ML can express more complex statements than the ordinal logic . Since the ML can be considered an extension of the ordinal binary logic, its logical manipulation is quite simple, although it is a four-valued logic. Four values are true(T), true in the sense of"*" (T*), false in the sense of "*"(F*) and false (F) . Furthermore, we have developed some interesting applications of the ML to mechanical theorem proving in artificial intelligence. A refuta­ tion process for the ML system is similar to that of the ordinal propositional or predicate logic. The idea of semi-unsatisfiability is introduced in the refutation process. That is, a semi-empty clause is obtained as a resolvent if a set of clauses is semi-unsatisfiable. In the refutation process for mechanical theorem proving, therefore, the appearance of a semi­ empty clause means that the inference is not completely true but true in the sense of "*"· This is one of the advantages of our system.

Several directions seem to be interesting for furthering investigations .of the ML from both a mathematical and applicational point of view. The author believes that the ML system is quite useful for solving complex problems.