The Theorem Prover Using a Parallel Processing System

1. INTRODUCTIO~

An AND/OR graph is often used to solve problems. It abstractly expressed the concept of dividing one problem into several sub-problems which are independently solved. This makes it possible that the sub-problems are solved in a parallel process. In this paper, D-graph deduction is proposed, which is based on a reductio ad absurdum using D-graph (a kind of directed AND/OR graph). The D-graphs are corresponded to the predicate logic formulas which represent the axioms and the negation of the theorem proved.

If several sub-problems share the same variables in problem solving, then the way in which one problem is solved may affect the solution of the others. This prevents sub-problems from being solved independently. There is the same issue in the D-graph deduction. The use of micro -actors settles such an issue. The micro-actors are the modules which compose basic structure for the knowledge representation. They can be applied to search a D-graph, because the D-graph basically consists of OUT-AND arcs. It will be shown that the sub-problems are solved independ­ ently in a micro-actor system in which the micro -actors correspond to the nodes in the D-graph and the common variables.

2. D-GRAPH DEDUCTION

2.1 First Order Predicate Logic and D-graphs

The authors will propose a formal deduction method using a directed AND/OR graph, called D-graph deduction, which is based on a reductio ad absurdum argument for the first order logic using D-graphs. Nodes in the D-graph are corre­ sponded to the predicate symbols, theirnegation~ TN (which means true), and FN (which means false). A set of arcs indicates a clause (a predicate logical formula).

THE THEOREM PROVER USING A PARALLEL PROCESSING SYSTEM

* ** * Hitoshi Ogawa, Tadahiro Kitahashi and Kokichi Tanaka

• *Faculty of Engineering Science Osaka University Toyonaka, Osaka 560 JAPAN
• ** Toyohashi University of Technology Toyohashi, Aichi 440 JAPAN

[Definition 1] A label (a,a) is attached to arc (A,B) corresponding to the formula A(a) ~ B(a), as shown in Fig. l. a and a are the argu­ ments of the predicates A and B, respectively. Thus, a label to an arc is an ordered pair of variable vectors, whose components are the var­ iables and Skolem functions of predicates corre­ sponding to the start and the goal nodes.

Let Greek lower-case letters express the tuple of constants, variables and Skolem functions.

[Definition 2] (Rules for translating clauses to a D-graph)

1. Select a clause from a set of support, ,,~here the set of support is a non-empty subset K of the initial set S of clauses such that S- K is satisfiable. Let the clause be represented L 1 ( >. l ) v ... v Lh ( Ah) .

Nodes L 1 , ... , Lh in the D-graph are regarded as OUT-AND nodes concerning TN, and arcs (TN, L 1 ), ... , (TN, Lh) are grouped by a linking symbol. Attached to the arcs are the labels ( ,A 1 ), ... , ( ,Ah) (See Fig. 2 (a)).

1. Let L 1 (A 1 )v ... vLm(Am) be a clause which has more than one literal, excluding the clause chosen at (1). This clause can be translated as fo 11 ows:

The D-graph representing this formula consists of OUT-AND arcs and nodes conserning ,L as shown in Fig. 2 (b). The above operation must be performed for a 11 i ( i = 1 , . . . , m) .

(3) A unit clause L( >. ), which is not selected at (1), may be modified to .,L(>.) +False. L( >. ) is therefore represented as the D-graph illustrated in Fig. 2 (c).

1. L( >. ) and .,L(>.) are always inconsistent, so the clause set containing them is unsatis­ fiable. They are indicated by IN-AND arcs and nodes concerning FN, as shown in Fig. 2 (d).

2. 2 Completeness of D-graph Deduction

D-graph deduction is carried out by communi­ cating the state of a node to its successor and by referring to the labels. The following define the state of a node and its communica­ t i on rule, and the relation between a node and FN in the D-graph.

[Definition 3] Suppose e , with lable {a, B), denotes the arc from node A to node B, and that y represents the state of A. If there exists the most general unifier (m.g.u.) rr of a andy, the state y of A is said to satisfy the label condition and e is said to be abailable . Then the state of B is Brr. When the state y of A does not satisfy the label condition of e , nothing is conveyed to B, i .e., this is equiv­ alent to that saying arc e does not exist.

[Definition 4] (Achievability for a D-graph) Achievability is defined between any node and FN as fo 11 ows :

(1) If a node A is connected to FN by an arc (A, FN) which is not an IN-AND arc and is avail ab 1 e, then A ..X.. FN.

(2) Suppose that the set of arcs (A, N 1 ), . . . , (A, N ) forms an OUT-AND arcs concerning A. If m each of the arcs is available and N . ..X..FN (i J = 1 , ... , m) , then A ~ FN. (3) If there is a sequence of arcs (,A, N 1 ), (N 1 , N 2 ), ... , (Nn' A) (or (A, N 1 ), (N 1 , N 2 ), ... , (Nn, ,A)) and all arcs are available together with the most general unifier rr for the states of A and ,A, then A..X..FN (.,A~FN). If there are nodes M 1 , ... . , Mm which have an OUT-AND relation with ,A (A), FN must be achiev­ able from them and the state of Mi (i = 1, ... , m) applied must satisfy the label condition . (4) A~FN is only generated by applying the above rules.

The D-graph deduction is carried out to deter­ mine whether FN is achievable from TN in D-graph which represents the axioms and the negation of the theorem. The states of nodes and the labels of arcs are employed to deal with the arguments of the predicates. The complete­ ness of the 0-graph deduction is guarenteed by Theorem 1.

[Theorem 1] Let G be the D-graph representing a set of S of clauses. S is unsatisfiable if and only if TN~ FN in G.

3. PARALLEL PROCESSING SYSTEM

In this section, a parallel processing system is described to solve the problem using micro-actors. The micro-actors are the modules for the knowl ­ edge base. The mic~o-actor is compo~ed of a . script and an acqua1ntance. The scr1pt cons1sts of the pairs of the message pattern and the action corresponding to the pattern. The micro -actor has the acquaintance as a memory space to hold the data and the names of the other micro -actors it directly knows about. Since only message passing is the interactive method between the micro-actors, the action of a micro -actor never affects the other micro-actors. This enable us to construct a parallel processing system.

3.1 Node Micro-Actors and Variable Micro-Actors

We will define two kinds of micro-actors. One is a node micro-actor (NMA), which corresponds to a node in a D-graph. Scripts of NMAs are the same. That is, they have a program which sends messages to the other NMAs according to their acquaintances. An NMA stores the relation between the node indicated by the NMA and the other nodes, in ELIST in its acquaintance. An example of ELIST is as shown in Fig. 4 (a).

Another is a variable micro-actor (V~~). which corresponds to a common variable and is made under searching a graph. Since a micro-actor is independent of the other micro-actors except for message sending, a VMA is independent of the other VMAs and NMAs. However, several NMAs must be able to refer to one VMA. There are two kinds of actions of a VMA:

1. Add the sent data to the aquaintance.
2. Reply the data which have flag sent. The basic data of the acquaintance is in form of (F V), where F is a set of flags which are similar to sentence number, and V is a value. (When the value is not given, V is NIL.)

TN-ELIST = ((NIL P (x)) ~ P-ELIST = (((?x) Q (x) R (x))). Q-ELIST = (((A) FN NIL) ((B) FN NIL)).

R-ELIST = (((B) FN NIL) ((C) FN NIL)).

[Example 1] The D-graph illustrated in Fig. 3 is a part of D-graph representing the following clauses:

axioms: ,P(x)vQ(x)vR(x), ,Q(A), ,Q(B),

,R(B), ,R(C).

negation of theorem: P(x).

Where A, B and C are constants, and x is a var­ iable. Fig. 4 (b) shows a micro-actor system corresponding to the D-graph in Fig. 3. Fig. 4 (a) shows ELISTs in the micro-actors. Graph searching begins when TN sends the messages and is carried out by sending message from NMAs to NMAs. NMAs perform one of three operations: expansion (sending the messages to successors), merging (merging several messages into one) and partial refutation (which is similar to ancestor resolution). FN replies to its ancestor. When a NMA receives a reply, the NMA checks the consistency of it. So the result of the system does not depend on the order of replies the messages which are sent concurrently. The system is stopped when a reply is sent to TN. Sending message from NMAs to Nt-1As makes the coroutine control, while sending message from NMAs to VMAs makes the subroutine control.