Äîêóìåíò âçÿò èç êýøà ïîèñêîâîé ìàøèíû. Àäðåñ îðèãèíàëüíîãî äîêóìåíòà : http://www.cplire.ru/Lab144/ciclops07.pdf Äàòà èçìåíåíèÿ: Mon Sep 24 14:53:34 2007 Äàòà èíäåêñèðîâàíèÿ: Mon Oct 1 20:23:11 2012 Êîäèðîâêà: Ïîèñêîâûå ñëîâà: àöîáñ áôìáîôéþåóëáñ áîïíáìéñ

Op erational Approach to the Mo dified Reasoning, Based on the Concept of Rep eated Proving and Logical Actors
Alexei A. Morozov
Institute of Radio Engineering and Electronics RAS Mokhovaya 11, Moscow, Russia, 125009 morozov@cplire.ru http://www.cplire.ru/Lab144/

Abstract. The message of this paper is the following: there is one more basic principle of operational semantics of logic programming (besides backtracking, recursion, etc.) that gives a solution of challenging problem of combining strict declarative semantics of logic languages with the dynamic behavior (that includes destructive assignment operations and interaction with dynamic environment). We have developed this principle, named repeated proving, in the Actor Prolog logic language. In this paper the repeated proving principle is explained with the help of an operational semantics (abstract machine) for sequential logic programs enhanced with logical actors. The problems of soundness and completeness of the control strategy are considered.

Intro duction
We address the problem of ensuring strict declarative semantics of logic languages operating in dynamic environment [1,2,3,4]. Our approach reminds of so-called perturbation model of constraint-based languages. In the perturbation model, unlike the standard (refinement) one, at the beginning of execution cycle variables have specific associated values satisfying the constraints. The value of one or more variables is perturbed by some outside influence, such as an edit request from the user, and the task of the prover is to adjust the values of the variables in such a way as to satisfy the constraints again [5,6]. The problem is closely related to the problem of ensuring the declarative semantics of the destructive assignment operation in logic languages. One can consider the updates in the outer world as a kind of destructive assignment that violates the soundness of the logic program. In this article, this problem is solved using the principle of repeated proving of sub-goals. In section 1, the ideas of repeated proving and logical actors are set forth. In section 2, a special notation is introduced along with the architecture of an abstract machine implementing a sequential control strategy of logic programs enhanced with logical actors. In section 3, transition diagrams of the abstract machine are defined. In section 4, the problems of soundness and completeness of the operational semantics are discussed.


2

Alexei A. Morozov

1

The Idea of Rep eated Proving and Logical Actors

Let us consider a logic program written in pure Prolog that has a classical model-theoretic semantics. The idea of repeated proving consists in dividing the AND-tree of the logic program into separate branches (sub-goals to be proved) called logical actors (1 ,. . . ,n on the Fig. 1) that should have the following operational properties:
V3
1 3

V

1

V V
4 4

2

V
2

5

5

Fig. 1. The idea of repeated proving of sub-goals.

1. Common variables (V1 ,. . . ,Vm ) are the single channel of data exchange between the actors. 2. Proving of separate actors can be fulfilled independently in arbitrary order. 3. One can cancel the results of proving of some actors without logic program backtracking while keeping all other sub-goals of the program. After canceling results of proving of an actor, its proving is to be repeated. Thus, one can implement a modification of reasoning. The results and consecution of reasoning itself can be partially modified in the process and after the logical inference. This makes possible to eliminate contradictions between the results of logical reasoning and new information income from outer world. The best example of application of the idea is implementation of long-lived Web agents. Let us imagine a Web agent written in logic language. The purpose of the agent is to make a logical inference on the basis of several remote data sources and to check some assertions about the remote resources. Let us imagine also that the agent is long-lived, i.e., it operates during a period of time that is longer than the period of information update. Thus the agent should react on any modification of remote resources and inform the user about the current state of the assertions to be checked. The problem is that one cannot repeat execution of the logic program from the beginning with any change in the outer world -- the repeat of the whole process of data collection performed during the long period of time is inefficient and, in some cases, technically impossible. Therefore one must change some branches of logic inference that depend on the modified data and keep all other branches unchanged. This is the case of modification of reasoning and the challenge is to provide soundness and (if possible) completeness of logical reasoning under the modification.


The Concept of Repeated Proving and Logical Actors

3

Another area that is recognized as a prospective application of the perturbation model of constrain-based languages is graphic user interface management [ 6]. We have successfully applied the logical actors approach for both the logical programming of Web agents [7,8] and visual user interface management [9]. An additional issue of our research is development of logic ob ject-oriented model of asynchronous concurrent computations based on the logical actors approach [10]. In the following sections a conservative extension of standard control strategy of (sequential) Prolog is developed that implements the repeated proving of logical actors.

2

The Architecture of Abstract Machine

Let us consider an abstract machine that implements a sequential control strategy for logic programs enhanced with logical actors. The input language of this machine is the Horn subset of first order logic formulas enhanced with special means implementing logical actors. The abstract machine implements the following general principles: 1. The standard control strategy (depth-first left-to-right search) is a part of the control strategy implemented by the abstract machine. 2. The AND-tree of logic program is to be divided into separate logical actors, i.e., any pending sub-goal of the program is a logical actor or a part of a logical actor. 3. Any logical actor obtains its own (local) substantiation (local values of common variables). 4. The results of proving of logical actor can be cancelled. 5. The logical actor can be proved once again after the canceling of results of its previous proving. 6. The states of logical actors are restored during the backtracking. Thus, the abstract machine implements the standard control strategy exactly if there is only one logical actor in the program (i.e., all the branches of the ANDtree belong to the same actor). Each logical actor A of the program has its own (local) values of variables. Actor A unifies its values with the values that belong to other actors in the following cases only: 1. The local values are compared in the course of successful termination of proving of actor A. 2. The local values are compared when actor A executes the ':=' built-in predicate (this predicate will be considered later). During the comparison of values that belong to different actors, abstract machine can cancel results of proving of some actors to provide consistency between remaining actors of the program (to provide existence of the most general unifier for all the values of all the actors of the program that remain uncancelled). After that the abstract machine tries to prove the cancelled actors once again.


4

Alexei A. Morozov

Let us name the operation of canceling of results of proving of the actor as neutralization of actor. Thus, the proving of actor A includes the following main stages (see Fig. 2).

Autonomous proving of the actor Interaction with other actors of the program Neutralization Repeated proving of Checking consistency of some actors neutralized actors between the actors

Fig. 2. The stages of execution of logical actor. There are three possible states of the actor: 1. Let us name an actor active if the proving of this actor is performing at this moment and is not ended yet. 2. The actor that was successfully proved (and was not neutralized yet) is named proven. 3. The actor is named neutral if the proving of this actor was cancelled and the repeated proving of it was not started yet. Neutralization of active actors is prohibited (see the formal rules of selecting actors for neutralization in section 3). Thus, sometimes the contradictions between the actors of the program cannot be eliminated with the help of actor neutralization. In this case standard backtracking occurs in the program, that returns actor A to the stage of autonomous proving. In the case if the abstract machine successfully eliminates contradictions between the actors with the help of neutralization of some set N A of actors, repeated proving of all the neutral actors occurs. If proving of all neutral actors terminates with success (or set N A is empty), the proving of actor A terminates with success. In another case backtracking occurs in the logic program, that returns actor A to the stage of autonomous proving. Thus, a failure of the repeated proving of any actor of the N A set will backtrack the program. Let us introduce some special notions to define the control strategy formally: ­ The state of abstract machine is a set of actors: = {A1 , A2 , . . . , An } , where Ai , i = 1 . . . n, are the actors of the program. ­ Actor Ai is a branch of AND-tree created as a result of execution of so-called actor cal l of a predicate @m(t1 , . . . , tk ): Ai = , m ( t 1 , . . . , t k ) , R ,


The Concept of Repeated Proving and Logical Actors

5

where is an (unique) name of actor; m(t1 , . . . , tk ) is an atomic formula that corresponds to given actor; R is a list named the results of proving of the actor. ­ The result of proving of an actor is information obtained during the proving of the actor: instantiations of variables, backtrack points, etc.: E = , F , where is the name of actor that has invoked the proving under consideration; F is a stack of so-called failure continuations that is used for implementation of backtracking. ­ The failure continuation is a stack containing sub-goals to be proved during investigation of one branch of OR-tree: C = G, , N , B , where G is a list of sub-goals; is an instantiation of variables used during investigation of the branch of the OR-tree under consideration; N is a list of actor names that were neutralized during investigation of given branch of the OR-tree; B is a list of actor names that were created during investigation of this branch. ­ The Subgoal can be a usual predicate call m(t1 , . . . , tk ), an actor predicate call @m(t1 , . . . , tk ), compositions of sub-goals S1 and S2 , S1 or S2 , etc. A special notation (@-language) necessary for definition of abstract machine states is given in tables 1, 2. The semantics of formulas of kind . {GL = S : G, S ubst = } is the following: there is an actor in the state of abstract machine, that has the following properties: 1. The GL cell situated on the top of the stack of failure continuations that is situated on the top of the stack of results of proving of the actor has value S : G (a list). 2. The S ubst cell situated on the top of the stack of failure continuations that is situated on the top of the stack of results of proving of the actor has value . In a similar manner, a formula of kind . = , M , R has the following semantics: there is an actor in state of abstract machine. The value of this actor is equal to , M , R . One can use given formulas in the following sense: "The state, such that there is an actor that has the following properties. . . ". We will use also formulas of the following kind in the transition diagrams: = : {GL : = G}. The semantics of these formulas is "The state of abstract machine differs from the state in that a new value G was assigned to the GL cell that is situated on the top of the stack of failure continuations that is situated on the top of the stack of results of proving of the actor."


6

Alexei A. Morozov

Table 1. The table of basic symbols of the @-language.
Notion Constant Variable Functor Term Atomic formula Name of actor Symb ol C onst V ar F un T er m Atom N ame Definition Typical elements a, b, c X, Y , Z f

Sub-goal

S ubg oal

Pro cedure P rocedur e Definition of proce- P rocedur es dures

C onst; V ar ; t, v , u f (t1 , . . . , tk ), k 1 m (t1 , . . . , t k ), k 0 M , , , . . . ; ; , where and are special names true; f ail; M ; @M ; S1 and S2 ; S1 or S2 ; del([1 , . . . , n ]); back ([1 , . . . , n ]); S wait( ); redo( ); neutraliz e({1 , . . . , n }); restart({1 , . . . , n }) M: - S P Function Atom S ubg oal D

Table 2. Definition of the @-language.
Notion Symb ol Definition {A1 , A 2 , . . . , A n }, n 1 Typical elements

State of abstract ma- S tate chine Actor Actor List of results of prov- RL ing Results of one proving Result Stack of failure continuations Failure continuation List of sub-goals (named also success continuation) Substitution List of names of neutral actors List of names of created actors FL C ont GL

, M , R A nil; E : R, is a list with head E R and rest R. , F ; neutral E where neutral is a special symb ol nil; F C:F G, , N , B nil; success; f ailure; S : G C G

S ubst N eutr B uilt

, , . . . ; ( is the empty substitution) [ 1 , . . . , n ] N [ 1 , . . . , n ] B


The Concept of Repeated Proving and Logical Actors

7

A logic program is defined as a set D of procedures1 (see designations of the @-language in table 1) and an initial state of the program: 0 ( ) = , m(t1 , . . . , tk ), , m(t1 , . . . , tk ) : nil, , [ ], [ ] : nil : nil , target actor hereafter) that is active in the actor situated in outer world (the external under consideration. All the actors except state of the abstract machine:

where is the name of an actor (the state, and is dummy name of an actor) that has invoked the program for the actor are proven2 in the 0

: 0 . {N ame = } : is prov en( 0 , ) The abstract machine can reach one of two final states: 1. The success state: S U C C E S S . {C ont = success, , N , B }, where is the target actor introduced in the 0 initial state. 2. The failure state: F AI LU RE . {F L = f ailure, , [ ], [ ] : nil}. Note, that the success and the failure states are alternative in accordance with given definitions. Deadlocks never occur in the abstract machine.

3

Transition System

The transition system of abstract machine is defined with the help of set of transition schemas and set of labels (let us denote the typical label by l). Let us consider the main stages of the proving of logical actor (Fig. 2). 3.1 Autonomous Proving of Actor

Execution of logic program is performed in accordance with the standard control strategy (depth-first left-to-right search) on this stage of proving of the actor. This strategy is implemented with the help of the transition schemas: T rue, Rec, Loc1 , S eq , and Alt. Some auxiliary schemas implement creation, deletion, and modification of logical actors during the proving. T rue -- elimination of the true sub-goal during the execution of actor . ---- . {GL = true : G} - - - - . {GL : = G} The semantics of this transition schema is the following one: "If current state of abstract machine is such that an actor exists and current list of sub-goals of this actor GL = true : G, then state can be transformed into new one. In new state of abstract machine current list of sub-goals of actor is modified:
1

T rue,

2

Let us do not use different procedures with the same functor (name and arity) of heading M to simplify the presentation. The is prov en predicate is defined in section 3.2.


8

Alexei A. Morozov

GL : = G. All other attributes of actor and all other actors of the abstract machine will not changed during the transformation." Rec -- a call of predicate m during the execution of actor . The rename : P P function implements renaming of variables of given procedure in the standard manner. The mg u : (M1 , M2 ) function computes the most general unifier of terms M1 , M2 (iff the unifier exists). . {GL = m(t1 , . . . , tk ) : G, S ubst = } P D : rename(P ) = (m(u1 , . . . , uk ): - S ) = mg u(m(t1 , . . . , tk ), m(u1 , . . . , uk )) = : {GL : = S : G, S ubst : = } where Rec, is the label of transition scheme under consideration. The statements over the line determine the conditions when the Rec schema can be performed. The statements under the line explain what is the difference between old state and new state that can be obtained with the help of the Rec transition schema. Loc1 -- backtracking of given actor . The `-' function designates the difference between lists: L - L = L , if L = [1 , . . . , n ] and L = [1 , . . . , n |L ]. The `+' function designates concatenation of lists. . {F L = S : G, , N , B : ( G , , N , B : F )} , S = f ail (S = m(t1 , . . . , tk ) ¬ P D : rename(P ) = (M : - S ) = mg u(m(t1 , . . . , tk ), M )) = : {F L : = back (N + B ) : (del(B ) : G ) , , N , B : F } , N =N -N , B =B-B Loc2 -- recognition of necessity to transmit backtracking from actor to the actor that has invoked current proving of actor . . {F L = S : G, , N , B : nil} , S = f ail (S = m(t1 , . . . , tk ) ¬ P D : rename(P ) = (M : - S ) = mg u(m(t1 , . . . , tk ), M )) = : {F L : = back (N + B ) : (del(B ) : f ailure) , , [ ], [ ] : nil}
Loc2 ,

-- - - - - -

Rec,

---- ---

Loc1 ,

Glo -- transmission of backtracking from actor to actor . . {Result = . {S ubg oal = = : {GL
Glo, ,

---- ---

---- ----

, f ailure, , [ ], [ ] : nil } wait()} : = f ail : nil}


The Concept of Repeated Proving and Logical Actors

9

B ack0 -- termination of process of recovering the states of actors during backtracking of the program. . {GL = back ([ ]) : G} - - - - - . {GL : = G} - - - - B ack1 -- recovery of the active or the proven state of actor during backtracking of actor . . {GL = back ([ |B List]) : G } . {RL = , G , , N , B : F : R } = : {GL : = back (N + B + B List) : (del(B ) : G )} , {RL : = R } ----- -----
B ack1 ,, B ack0 ,

B ack2 -- recovery of the neutral state of actor during backtracking of . . {GL = back ([ |B List]) : G } . {RL = neutral : R } = : {GL : = back (B List) : G } , {RL : = R } ----- -----
B ack2 ,,

Del0 -- termination of deletion of actors during backtracking of actor . . {GL = del([ ]) : G} - - - - . {GL : = G} --- Del1 -- deletion of actor during backtracking of actor . The `/' function designates deletion of actor: 1 / = 2 , such that { , M , R } 2 = 1 , 1 = 2 . . {S ubg oal = del([ |DList])} = ( : {S ubg oal : = del(DList)}) / -- - - - - - - -
Del1 ,, Del0 ,

S eq -- execution of conjunction of sub-goals of actor . . {GL = (S1 and S2 ) : G} - - - - . {GL : = S1 : (S2 : G)} - - - Alt -- execution of disjunction of sub-goals of actor . . {F L = (S1 or S2 ) : G, , N , B : F }
Alt, S eq ,

--- --- . {F L : = S1 : G, , N , B : ( S2 : G, , N , B : F )} N ew1 -- execution of actor predicate call @m during execution of actor . The code auxiliary function is used for preparation of arguments of actor predicate call. This function (see Fig. 3) provides transfer of maximal quantity of information about the values of the arguments of predicate into the actor


10

Alexei A. Morozov

to be created. The code function transfers the values of the instantiated variables and copies the variables that are unbound. The copy auxiliary function copies the values of variables. The new v ariable function creates new variables. The is v ariable function checks if the argument is an (unbound) variable. The not exists(, ) expression means , M , F . / . {F L = @m(t1 , . . . , tk ) : G, , N , B : F } not exists(, ) P D : rename(P ) = (m(u1 , . . . , uk ): - S ) ([v1 , . . . , vk ] , ) : = code([t1 , . . . , tk ] , ) = mg u(m(v1 , . . . , vk ), m(u1 , . . . , uk )) F L : = wait( ) : G, , N , [ |B ] = : : ( redo( ) : G, , N , [ |B ] : F ) { , m(v1 , . . . , vk ), , S : nil, , [ ], [ ] : nil : nil } -- - - - -----
N ew1 ,,

code : [{ti }, ] [{ti }, ] , i = 1 . . . n : = ; do i = 1 . . . n if ti = f ({uj }), j = 1 . . . k [{vj }, ] : = code({uj }, ); ti : = f ({vj }); : = elsif is v ariable(ti ) if is v ariable(ti ) ti : = ti else [ti , ] : = copy (ti , ); := fi else ti : = ti fi od

copy : [t, ] [t , ] if t = f ({uj }), j = 1 . . . k : = ; do j = 1 . . . k if is v ariable(uj ) uj : = new v ariable(); : = uj = uj else uj , : = copy (uj , ) f i; := od; t : = f ( { uj } ) , j = 1 . . . k else t : = t ; : = fi

Fig. 3. Definitions of coding and copying functions. N ew2 -- recognition of that an actor predicate @m call cannot be performed during the execution of actor . . {S ubg oal = @m(t1 , . . . , tk ), S ubst = ¬ P D : rename(P ) = (m(u1 , . . . , uk ): - S ) ([v1 , . . . , vk ] , ) : = code([t1 , . . . , tk ] = mg u(m(v1 , . . . , vk ), m(u1 , . . . , = : {GL : = f ail : nil} ---- ----
N ew2 ,

} , ) uk ))


The Concept of Repeated Proving and Logical Actors

11

Redo1 -- backtracking of the actor during backtracking of actor . . {F L = redo( ) : G , , N , B : F } . RL = , G , , N , B : C : F : R F L : = wait( ) : G , , N , B = : , : ( redo( ) : G , , N , B : F ) RL : = , f ail : nil, , N , B : C : F ----- ----- Redo2 -- recognition of that backtracking of actor cannot be performed during execution of actor . . {S ubg oal = redo( )} . {RL = , C : nil : R } = : {GL : = f ail : nil} ----- -----
Redo2 ,, Redo1 ,,



:R



3.2

Interaction of Logical Actors

The abstract machine implements the following operations on this stage: 1. The comparison of substitutions that correspond to various actors of the program. 2. Neutralization of some actors. 3. Repeated proving of neutral actors. C heck1 -- checking if the actors of the program are consistent (during termination of proving of actor ). Let us introduce some additional notions: ­ is neutral(, ) = . {Result = neutral};
def def def

­ is activ e(, ) = ¬is neutral(, ) . {GL = success};

­ is prov en(, ) = ¬is neutral(, ) . {GL = success}; ­ S U B S T (, ) is substitution , . {S ubst = }, or empty substitution , if is neutral(, );
def n

­ does exist(, ) = , M , R ­ (, {1 , . . . , n }) =
i=1

;

S U B S T (, i ) -- is a set of substitution assign-

ments corresponding to all the actors 1 , . . . , n in state . Definition 1. Set S of substitution assignments is conflicting one, if there are two subsets 1 and 2 and a variable X such that: 1. 1 and 2 are substitutions. 2. These substitutions gives values V1 and V2 to the X variable, that have no most general unifier.


12

Alexei A. Morozov

inconsistent(S ) = 1 S 2 S X : ¬ mg u(X 1 , X 2 ). Definition 2. consistent(S ) = ¬inconsistent(S ) -- is a consistent set of substitution assignments. Definition 3. A set of names N A of actors to be neutralized and proved repeated ly may be neutraliz ed(, N A) : 1. N A : does exist(, ) is prov en(, ); 2. N A : set of actors {i } , i = 1, . . . , k : does exist(, i ) : inconsistent( ({1 , . . . , k , })) consistent( ({1 , . . . , k })); 3. A set of substitution equations of actors of any subset of that has no common elements with the N A set should be consistent one. The condition (2) excludes any unnecessary neutralization of actors that are irrelevant to the contradictions that should be eliminated. . {GL = nil} N A : may be neutraliz ed(, N A) = : {GL : = neutraliz e(N A) : (restart(N A) : success)} ----- ----
C heck1 , def

def

C heck2 -- recognition of impossibility to eliminate contradictions between the actors with the help of neutralization of some actors (during termination of proving of actor ). . {GL = nil} ¬ N A : may be neutraliz ed(, N A) = : {GL : = f ail : nil} ----- ----
C heck2 ,

N eut0 -- termination of neutralization of actors (during termination of proving of actor ). . {GL = neutraliz e() : G} - - - - - . {GL : = G} - - - - N eut1 -- neutralization of actor during execution of actor : . {C ont . {RL = = : / = neutraliz e({ } N A ) : G, , N , B } , N A R} {C ont : = neutraliz e(N A ) : G, , [ |N ], B } , {RL : = neutral : R}
N eut0 ,

----- -----

N eut1 ,,

S ucc -- termination of proving of actor with success. . {GL = restart() : G} - - - - . {GL : = G} ---
S ucc,


The Concept of Repeated Proving and Logical Actors

13

C all -- invocation of repeated proving of actor during execution of . . {F L = restart({ } RA ) : G, , N , B : F } . = , m(v1 , . . . , vk ), R F L : = wait( ) : (restart(RA ) : G) = : : ( redo( ) : (restart(RA ) : G) , , [ {RL : = , m(v1 , . . . , vk ) : nil, , [ ], [ ] -- - - - - - - -
C all,,

, RA / , , [ |N ], B |N ], B : F ) : nil : R} ,

Note that the C heck1 , the N eut1 , and the C all schemas make abstract machine nondeterministic one. C on -- resumption of proving of actor after termination of proving of actor that was invoked by actor . . {GL = success} . {GL = wait() : G} = : {GL : = G} Note that defined abstract machine provides a possibility for modeling destructive assignment of variables with the help of logical actors. For instance, the X := Y build-in predicate is implemented in the Actor Prolog language, that invokes the interaction between the actors of the program. The operational semantics of the ':=' predicate is straightforward one: 1. The predicate tries to unify the X and the Y terms. 2. If the most general unifier exists, the interaction of actors of the program is performed in accordance with the rules described above. 3. If neutralization and repeated proving of actors provides consistency between the actors of the program, the execution of the ':=' predicate terminates with success. In another case backtracking occurs in the program. The model-theoretic semantics of this predicate is exactly the same as the semantics of the usual equality '=' in pure Prolog and the operational semantics of the '=' predicate is a special case of the ':=' predicate operational semantics. - - - - -- - - -
C on, ,

4

Op erational Semantics

The operational semantics of sequential logic program enhanced with logical actors is a map O that pro jects definition of procedures D and an initial state of program 0 , 0 . = , m(t1 , . . . , tk ), R , into the set of finite and infinite chains of states obtained with the help of transition schemas defined above. Definition 4. Operational semantics O:
l l l

O [D , ] =

0 def

1 2 n S 0 - 1 - . . . - n

U CCESS

- 1 - . . . - 0 - 1 - . . . .
l1 l2

0

l1

l2

ln

F n AI LU RE




14

Alexei A. Morozov

Note that the model-theoretic semantics of defined @-language strictly corresponds to the model-theoretic semantics of pure Prolog without negation. Definition 5. An initial set of actor constraints is a set of logical statements that corresponds to al l the proven actors of initial state 0 : I nit =
def i

Mi for al l i , Mi , Ri 0 , such that is prov en( 0 , i ).

Prop osition 1 (on soundness of the op erational semantics). The operational semantics O is sound, i.e., the success final state of the program can be obtained only if union of procedure definitions D with the negation of conjunction of initial set I nit and goal statement m(t1 , . . . , tk ) is unsatisfiable: 0 -
SU CCESS

(D {¬ (I nit m(t1 , . . . , tk ))} |= ) .

Prop osition 2 (on completeness of the op erational semantics). The success final state of the program wil l be obtained if a substitution exists, such that D |= (I nit m(t1 , . . . , tk )) , and no infinite computations arise: 0 -
SU CCESS

.

Thus, the program can fall into an infinite computation even if a success branch is present in the AND-OR tree, like the standard sequential Prolog. Nevertheless the additional operation of neutralization of actors cannot provoke looping of the program, because the neutralization of active actors is prohibited in schema C heck1 . The practical use of the control strategy under consideration requires that the abstract machine stops after the obtaining of the first success final state despite the fact that the abstract machine can implement the exhaustive search until all existed answers are computed or an infinite computation occurs. This restriction corresponds to the perturbation model of constraint-based languages, i.e., the problem to be solved by the abstract machine is to fit given system of constraints to new information income from outer world only. After that, the abstract machine will wait for a new outside influence.

Conclusion
The logical actors concept gives an alternative to the nonmonotonic approach in logic programming. It forms a basis for solving the problem of ensuring soundness and completeness of the destructive assignment operation as well as strict classical model-theoretic semantics of logic programs operating in dynamic environment (such as graphical user interface and Internet). The repeated proving of sub-goals allows to modify the logical reasoning during the execution of a logic program. Following the principle of modifiable


The Concept of Repeated Proving and Logical Actors

15

reasoning, we have developed concurrent ob ject-oriented logic language Actor Prolog that ensures soundness of logic programs operating under conditions of permanent altering and updating of input information [ 11,8,12]. The ideas stated in this paper are approved by practical experiments with visual logic programming and Web agent logic programming [7]. The author is grateful to Prof. Yu.V. Obukhov, Dr. A.F. Polupanov, Dr. A.N. Kruglov, and Dr. S.V. Remizov (IRE RAS) for help and support in implementing the pro ject, to Acad. Yu.I. Zhuravlev and Prof. V.A. Zakharov (Moscow State University) for fruitful discussions of the problem. This work was supported by RFBR, pro ject no. 06-07-89302.

References
1. Chesnevar, C.I., Maguitman, A.G., Loui, R.P.: Logical models of argument. ACM Computing Surveys 32(4) (2000) 337­383 2. Alferes, J., Pereira, L.: Logic programming updating -- a guided approach. In Kakas, A., Sadri, F., eds.: Computational Logic: From Logic Programming into the Future -- Essays in honour of Robert Kowalski. Volume 2. Springer (2002) 382­412 3. Dix, J., Furbach, U., Niemelae, I.: Nonmonotonic reasoning: Towards efficient calculi and implementations. In Voronkov, Robinson, eds.: Handbook of Automated Reasoning. Volume 2. Elsevier (2001) 1121­1234 4. Eiter, T., Fink, M., Sabbatini, G., Tompits, H.: Using methods of declarative logic programming for intelligent information agents. Theory and Practice of Logic Programming 2(6) (2002) 645­709 5. Rossi, F.: Constraint (Logic) Programming: A Survey on Research and Applications. In: New Trends in Constraints: Joint ERCIM/Compulog Net Workshop, Paphos, Cyprus, October 1999. Selected Papers. Volume 1865 of LNAI., Springer (1999) 40­74 6. Sannella, M., Maloney, J., Freeman-Benson, B., Borning, A.: Multi-way versus one-way constraints in user interfaces: Experience with the DeltaBlue algorithm. Software -- Practice and Experience 23(5) (1993) 529­566 7. Morozov, A.: Development and application of logical actors mathematical apparatus for logic programming of Web agents. In Palamidessi, C., ed.: ICLP 2003. LNCS 2916, Springer (2003) 494­495 8. Morozov, A., Obukhov, Y.: An approach to logic programming of intelligent agents for searching and recognizing information on the Internet. Pattern Recognition and Image Analysis 11(3) (2001) 570­582 Available at: http://www.cplire.ru/Lab144/pria570m.pdf. 9. Morozov, A.: Visual logic programming based on the SADT diagrams. In Dahl, V., Niemela, I., eds.: ICLP 2007. LNCS 4670, Springer (2007) 436­437 10. Morozov, A.: Logic ob ject-oriented model of asynchronous concurrent computations. Pattern Recognition and Image Analysis 13(4) (2003) 640­649 Available at: http://www.cplire.ru/Lab144/pria640.pdf. 11. Morozov, A.: Actor Prolog: an ob ject-oriented language with the classical declarative semantics. In Sagonas, K., Tarau, P., eds.: Proc. of the IDL'99 Int. Workshop, Paris, France (1999) 39­53 Available at: http://www.cplire.ru/Lab144/paris.pdf. 12. Morozov, A.: Getting Started in Actor Prolog. IRE RAS (2002) Available at: http://www.cplire.ru/Lab144/start/.