A Construction of Logic-Constrained Functions with Respect to Awareness

Abstract

A logic-constrained function is motivated by modelling the behaviour of the electronic device (like a mobile phone) with respect to evocation caused by awareness. This paper presents an analysis to develop a logic-constrained function system. We firstly have the contradiction removal procedure for a proof system which is expected with negation as failure rule (as denoting unawareness) to derive the constraint (supposedly as awareness) with reference to the (abstract) functions like λ-terms. Though the system deriving constraints can be the logic programming system (Alferes,J.J. et al.) of coherence principle, a limited reasoning (with negation as failure) is treated in this paper to cope with inconsistency (contradiction) caused by classical negation, in terms of contradiction removal facility. We then have a description of the logic-constrained function. As a logic-constrained function, we have an outlook on a literal-constrained term, an extended λ-term, where the literal may be derivable from a proof system. The term conversions are defined such that a system originating from awareness may have abstract function applications, based on the literal-constrained term.

Introduction

As a ubiquitous system, we can assume the electronic device (like a mobile phone) in place of the PC in distributed environments through internets or wireless communications. (i) The device is expected to hold functional and objective knowledge abstractly. (ii) The device as a resource is bounded to be left alone until it is evoked and of use. The evocation of the device can be supported by constraint awareness of (a set of) states (as in [ 11 ]) which some predicate (with or without classical negation) may denote. That is, the evocation may be interpreted to be realized by an awareness of states (i.e., of a predicate). (iii) As long as we are concerned with awareness of a predicate for such a set of states, it is implementable as derivability from a proof system. (iv) In a proof system, negation as failure is applicable to unawareness, owing to derivability of the designated predicate. (Note that the closed world assumption is broader than negation as failure with reference to unawareness.)

Therefore we have an illustrative structure on logical awareness as in Table 1.

Derivability basis

A proof system ⇒

Evocation

Awareness ⇒

Device

Function construction

We then have technical problems: (1) Function constructions constrained by predicates (constructions of logic-constrained function) are to be modelled for the mobile phone evoked by awareness of a state set. (2) If we regard awareness as caused by derivability from a proof system, paraconsistency should be denied. If a complementary pair of predicates with and without negation is derivable, one of them must be removed.

Regarding the problems, abstract functions have been deeply studied in the λ-calculus such that there were many compact textbooks among which we can see the one ([ 9 ]). From knowledge views on function applications, an analysis of the function (application) constrained by logic concerning awareness is also a problem. For the function to conceive logical awareness, the logic-constrained function may be constructed, where the logical formula (which constrains functions) is often interpreted as: procedure or process ([ 12 ]) and state set ([ 11 ]) possibly inducing space and/or time notions, such that the logical formula can be concerned with awareness of some agent. In this paper, the notion of the state set is adopted. The denotation of a state set is described by a predicate (with or without classical negation) which may be derived (deduced) from a proof system. As regards derivability, negation as failure in computational logic ([ 12 ]), the inference rule “ p ⇒ ∼ p (or denoted as not p)” has been well studied. Unawareness may be defined in terms of negation as failure.

Motivated by the above problems, this paper is to analyze the logicconstrained function construction, where: (a) the logic programming system derives the literals with and without classical negation, by means of reasoning containing negation as failure, and (b) a logic-constrained function is defined by means of a combination of λ-terms with the logical formulae.

Regarding the logic programming system, the negative literals are as significant as positive ones, with reference to the closed world assumption, the default and/or negation as failure rules ([ 2, 17 ]). As an analysis, we need the negation as failure to denote unawareness with a contradiction-free reasoning. As before pointed out for the second problem, a complementary pair of literals with and without classical negation causes a contradiction even with respect to awareness. That is, the contradiction is not allowed for logic-constrained function: the contradiction is to be removed from awareness view such that reasoning to remove contradiction must be restricted. Concerning the logic-constrained function, the established λ-calculus is fundamental and may be extended to the one where the (λ-)term constrained by logical formulae is definable. This paper focuses on the definable terms generally denoting the logic-constrained functions, where the logic-constrained function is a λ-term with respect to awareness expressed by a logical formula. The awareness is regarded as caused by derivability from a proof system, while negation as failure for derivability supposedly denotes unawareness.

The paper of the analysis for logic-constrained functions is organized for the problem as motivations described here. In Section 2, the logic programming system is reviewed from the propositional logic version, where an idea of the contradiction removal is presented. Section 3 presents a contradiction removal procedure and its soundness is shown. In Section 4, we have an outlook on an extended λ-term with the literal (possibly containing classical negation) and its conversions. Section 5 gives comments regarding logic-constraints on the λ-term. 2

Logical Expressions

We now review the terminologies in propositional logic programming, as a proof system to possibly derive literals with and without classical negation. Negation as failure is to denote an unawareness, while contradiction caused by a pair of derivable literals (awareness) with and without classical negation must be removed by a limited reasoning.

(1) A set of symbols to stand for propositions is assumed. (2) Two kinds of negation sign are taken: the classical negation “¬” and the negation as failure “∼”. (3) A literal l is either an atom a, or a classical negation ¬a of an atom a.

An atom is an expression consisting of a symbol to denote a proposition.

Classical negation vs. negation as failure

The class of extended logic programs in the propositional logic is treated, where two kinds of negation may be contained. As a theory for the literalconstrained term which would be mentioned later, an extended logic program (ELP, for short) is a set of clauses of the form

l ← l1, . . . , lm, ∼ lm+1, . . . , ∼ ln (0 ≤ m ≤ n), where l and li are literals, and “∼” stands for the negation as failure (NAF, for short). The literal ∼ l is called a negation-as-failure literal. The literal l of the clause is said to be its head, and the literal sequence l1, . . . , lm, ∼ lm+1, . . . , ∼ ln is its body. The classical negation ¬l means (i) ¬a if l = a, and (ii) a if l = ¬a, for an atom a. The pair of literals a and ¬a is said to be complementary.

The expressions L, L1, . . . , Lm, . . . , M , M1, . . . , Mn, . . . are reserved to denote literals or negation-as-failure literals. The expressions α, α1, . . . , αm, . . . , β, β1, . . . , βn, . . . are reserved to denote sequences of literals or negation-as-failure literals.

A goal is an expression of the form ← l1, . . . , lm, ∼ lm+1, . . . , ∼ ln (0 ≤ m ≤ n), where li are literals. The goal of the form ← ∼ m1, . . . , ∼ mq (q ≥ 0) is said to be a negative goal. The negative goal is the empty clause, denoted by , if it contains no literal. For the ELPs, we must note a well established paraconsistent reasoning (which is regarded as a proof procedure to possibly derive literals) equipped with coherence principle ([ 1 ]): “For any objective literal ¬l, if ¬l is entailed by the semantics, then ∼ l is also entailed.” In the paper, a proof procedure with coherence principle is given, while some condition for the program to be consistent is shown.

We have an outlook on SLD resolution and negation as failure, where we can see [ 12, 17 ] among so many papers.

SLD resolution applied to goals is a rule to derive

← L1, . . . , Li−1, M1, . . . , Mn, Li+1, . . . , Lm from a goal ← L1, . . . , Li−1, l, Li+1, . . . , Lm and a clause l ← M1, . . . , Mn in the given ELP. That is, a literal l of a goal may be replaced by the body M1, . . . , Mn of a clause l ← M1, . . . , Mn, whose head is just the literal l.

Negation as failure is a rule to infer a negation-as-failure literal ∼ l, when the literal l is not derived by some proof procedure. We refine negation as failure in relation to SLD resolution such that the succeeding and failing (derivations) of a goal (with reference to a given ELP) are defined recursively as follows: (i) The goal ← l succeeds if ← l is reduced to

SLD resolutions. (ii) The goal ← l fails if one of following conditions holds: by applying finitely many (a) there is no clause whose head is the literal l. (b) there are goals ← α1, L1, β1, . . . , ← αn, Ln, βn (n ≥ 1), derived by SLD resolutions for the goal ← l such that all the goals ← L1, . . . , ← Ln fail.

(c) the goal ← ¬l succeeds. (iii) The goal ← ∼ l succeeds if the goal ← l fails. (iv) The goal ← ∼ l fails if the goal ← l succeeds.

Note the sense that if the goal ← l may succeed, then we may be aware of l.

Contradiction removal

Compared with the method of [ 1 ] involving the coherence principle, we have a different method of removing contradictory succeeding derivations of both the goal ← a and the goal ← ¬a. If both goals may succeed, contradictory awareness of a and ¬a is made, which should be escaped.

Now assume a propositional ELP

Q = {r ← q, ¬q; q ← ∼ p; p ← ∼ q; ¬q ←}.

For the goal ← r, we have the derivation by SLD resolution: A goal ← r is reduced to a goal ← q, ¬q, as illustrated below.

← r

| ← q, ¬q

(with a clause r ← q, ¬q) The goal ← ¬q can succeed with the clause ¬q ←, where it is reduced to the goal as shown below.

(with a clause ¬q ←) It follows that the goal ← q, ¬q is reduced to the goal ← q, while the goal ← q cannot succeed, for contradiction removal, after the success of the goal ← ¬q.

Alternatively, if we have a derivation of the goal ← q to , whose details is omitted, the goal ← q, ¬q is reduced to the goal ← ¬q, which is to be suspended. Here we can see that the goal ← r cannot succeed. Finally the following requirements are implemented.

(i) At most one of goals ← q and ← ¬q is permitted to succeed. (By means of some memory for the succeeding derivation to eliminate contradictions, the contradiction-free derivation is automated.) (ii) If the goal ← q succeeds, then the goal ← ¬q can be regarded as failing. 3

Reasoning Procedure

For reasoning to be apart from paraconsistency, we have two sets to be kept, which are to be transformed through succeeding and failing derivations: (i) the set of literals to remove contradictory succeeding derivations (ii) the set of negation-as-failure literals The former set (i) is expressed by Σ, Σ1, . . . , and the second one (ii) is by Δ, Δ1, . . . . Given an ELP P , the predicate sucP (G; Σ1; Δ1; Σ2; Δ2) is derived, when a goal G succeeds with the assumed sets Σ1 and Δ1, to acquire the sets Σ2 and Δ2. The predicate f ailP (G; Σ1; Δ1; Σ2; Δ2) is derived, when a goal G fails with the assumed sets Σ1 and Δ1, to acquire the sets Σ2 and Δ2. Following the derivations as above, we have the rules. Intuitively the succeeding derivation expresses some awareness, while the failing derivation detects unawareness, in relation to negation-as-failure rules.

We assume an ELP P and have the relational representations of succeeding and failing derivations, where the relations sucP and f ailP are defined simultaneously by recursion to be the least set satisfying the following closure. Because the relations demonstrate the implementation as procedural methods for the given ELP, they can be regarded as providing behaviours such that the abstraction of the representation is more general than those in [ 19 ]. The subscript P for the ELP P may be omitted if it is clear in the context.

(0) sucP ( ; Σ; Δ; Σ; Δ) for any Σ and Δ. (1) sucP (← L1, . . . , Li−1, M1, . . . , Mm, Li+1, . . . , Ln; Σ1 ∪ {l}; Δ1; Σ2; Δ2) for ¬l ∈ Σ1 and (l ← M1, . . . , Mm) ∈ P ⇒ sucP (← L1, . . . , Li−1, l, Li+1, . . . , Ln; Σ1; Δ1; Σ2; Δ2). (2) sucP (← L1, . . . , Li−1, Li+1, . . . , Ln; Σ1; Δ1; Σ2; Δ2) and ∼ l ∈ Δ1 ⇒ sucP (← L1, . . . , Li−1, ∼ l, Li+1, . . . , Ln; Σ1; Δ1; Σ2; Δ2). (3) sucP (← L1, . . . , Li−1, Li+1, . . . , Ln; Σ2; Δ2; Σ2; Δ2) and f ailP (← l; Σ1; Δ1 ∪ {∼ l}; Σ2; Δ2) for ∼ l ∈ Δ1 ⇒ sucP (← L1, . . . , Li−1, ∼ l, Li+1, . . . , Ln; Σ1; Δ1; Σ2; Δ2). (4) There is no clause in P , which contains l in the head ⇒

f ailP (← L1, . . . , Li−1, l, Li+1, . . . , Ln; Σ; Δ; Σ; Δ) for any Σ and Δ. (5) For any clause l ← M1j , . . . , Mnjj ∈ P (1 ≤ j ≤ k) of all the clauses which contain l in the head, f ailP (← L1, . . . , Li−1, M1j , . . . , Mnjj , Li+1, . . . , Ln; Σj ; Δj ; Σj+1; Δj+1) ⇒ f ailP (← L1, . . . , Li−1, l, Li+1, . . . , Ln; Σ1; Δ1; Σk+1; Δk+1). (6) sucP (← ¬l; Σ1; Δ1; Σ2; Δ2) ⇒ f ailP (← l; Σ1; Δ1; Σ2; Δ2). (7) f ailP (← L1, . . . , Li−1, Li+1, . . . , Ln; Σ1; Δ1; Σ2; Δ2) and ∼ l ∈ Δ1 ⇒ f ailP (← L1, . . . , Li−1, ∼ l, Li+1, . . . , Ln; Σ1; Δ1; Σ2; Δ2). (8) sucP (← l; Σ1; Δ1; Σ2; Δ2) for ∼ l ∈ Δ1 ⇒

f ailP (← L1, . . . , Li−1, ∼ l, Li+1, . . . , Ln; Σ1; Δ1; Σ2; Δ2).

We can see the characteristics of the relational representations: (a) If we have the relation sucP (G; ∅; ∅; Σ; Δ) for a goal G, the whole interpreter for the logic program can detect corresponding derivations. The literals of the goal G in the relation sucP are regarded as made aware of, while if the goal G is included in the relation f ailP then the literals of the goal is concerned with unawareness. (b) In the relation sucP (G; ∅; ∅; Σ; Δ), the set Δ contains the extraction of negation-as-failure literals. (c) By the set Σ of the relation sucP (G; ∅; ∅; Σ; Δ), we can trace the literals used for SLD resolution.

We see an illustration.

Example. Take a simple ELP P = {p ←, ¬p ←}.

(i) Clearly we have the empty clause clause p ← such that from a goal ← p with a given (ii) Similarly we have sucP (← ¬p; ∅; ∅; {¬p}; ∅). However, we cannot have sucP (← p; ∅; ∅; {p}; ∅).

sucP (← ¬p; {p}; ∅; {¬p}; ∅), after that we have got sucP (← p; ∅; ∅; {p}; ∅), as in the case of (i). (iii) After we have got sucP (← p; ∅; ∅; {p}; ∅) which is concerned with awareness of the literal p, the inference rule gives

f ailP (← ¬p; ∅; ∅; {p}; ∅), which detects unawareness of the literal ¬p.

In the following sense, the relation sucP , which may involve the effect of the relation f ailP , is sound. This is paraphrased to the sense of consistency that if a goal ← l succeeds, then ∼ l cannot be included in the set of negations-failure literals. It also contains an interpretation that awareness reasoned by the relation sucP is consistent with unawareness detected by the relation f ailP . The proof is made. Here we see its outline.

Definition 3.1 For a set Σ, we define the set Σ˜ to be {∼ ¬l | l ∈ Σ}. Theorem 3.2 Assume that sucP (← l; Σ1; Δ1; Σ2; Δ2) such that Σ1 = Δ1 = ∅. Then ∼ l ∈ Δ2∪ Σ˜2.

Proof (Outline) (1) By the definition of the relation sucP , ¬l ∈ Σ2. It follows that ∼ l ∈Σ˜2. (2) On the contrary to the assumption that ∼ l ∈ Δ2, suppose that ∼ l ∈ Δ2. Then, by the construction of the set Δ2, it follows that

f ailP (← l; Σ1; Δ1; Σ2; Δ2) for some sets Σ1, Δ1, Σ2, Δ2 such that l ∈ Δ1 ⊆ Δ2 ⊆ Δ2. There are the following cases to support this relation f ailP . (i) In case that sucP (← ¬l; Σ1; Δ1; Σ2; Δ2), this contradicts the first assumption that sucP (← l; Σ1; Δ1; Σ2; Δ2). (ii) In case that there is no clause whose head is l for the relation f ailP , this contradicts the first assumption that sucP (← l; Σ1; Δ1; Σ2; Δ2) such that there is some clause whose head is l. (iii) In case that f ailP (← ∼ m1, . . . , ∼ mn; Σ1; Δ1; Σ2; Δ2) for some sets Σ1, Δ1, Σ2, Δ2, which may be caused for some negative goal ← ∼ m1, . . . , ∼ mn ← ∼ m1, . . . , ∼ mn, derivable from the goal ← l, it is concluded that n = 0. Otherwise, the negative goal ← ∼ m1, . . . , ∼ mn is and it contradicts the relation f ailP . For the negative goal there is some literal mi ∈ Δ1 (1 ≤ i ≤ n) such that sucP (← mi; Σ1; Δ1; Σ2; Δ2), because of the relation f ailP . On the assumption that ∼ mi ∈ Δ2, we repeat the same discussion. We finally reach the case that: f ailP (← ∼ mf1 , . . . , ∼ mfn; Σf1 ; Δf1 ; Σf2 ; Δ2 ) f for some sets Σf1 , Δf2 , Σf2 , Δf2 , but there is no literal ∼ mif such that ∼ mif ∈ Δf1. This causes the case that ← ∼ mf f1 , .f. . , ∼f mfn = , which contradicts that f ailP (← ∼ mf1 , . . . , ∼ mfn; Σ1 ; Δ2 ; Σ2 ; Δf2 ). This concludes the proof.

Literal-Constrained Term

We here have the form: a constrained literal followed by a (function) term, where (a) the literal is derivable from some proof system like the logic programming system such that the literal may be interpreted as awareness (of an agent), and (b) the function term is held (by an agent) under the awareness of the literal, such that the form may be regarded as denoting a behaviour of an agent.

Syntax

An extended term from the original is shown below, where a logicconstraint may be made by a literal. If we prefer to the ELP, which derives literals, then the derivable literals may be constraints.

Definition 4.1 On the assumption of a proof system (say, Γ), a literalconstrained term (term, for short) is recursively defined as follows: (i) If x is a variable, then x is a term. (ii) If M , N are terms, then (M N ) is a term. (iii) If x is a variable and M a term, then (λx.M ) is a term. (iv) If p is a literal and M a term, then p < M > is a term.

Semantics

By the term p < M > with some system Γ (which may possibly be the ELP in the previous section), we mean that: • If p is derivable from Γ, then the term M is supported. • Unless p is derivable from Γ, then the term M is not supported.

When the ELP may be taken as a proof system Γ, the contradiction removal procedure is significant, because p < M > and ¬p < M > cannot be coherent.

Illustration

Even(x) = if x = 0 then true else if x = 1 then f alse else Odd(x − 1) Odd(x) = if x = 0 then f alse

Assume the following functional program. else if x = 1 then true else Even(x − 1) As a standard way, by means of a fixed point operator:

Let Y = λf.(λx.f (x x))(λx.f (x x)), Let evenf n = λg.λn.(if n = 0 then true else if n = 1 then f alse else g (− n 1)) Let oddf n = λf.λm.(if m = 0 then f alse else if m = 1 then true else f (− m 1)) Let even = Y (evenf n oddf n)

Let odd = Y (oddf n evenf n)

The terms “evenf n” and “oddf n” may be included in the expressions such as:

p < evenf n > and q < oddf n >, where the literals may denote awareness, which acknowledges the application of p < evenf n > to q < oddf n > for the usual term (evenf n oddf n) to even, and vice versa for the term (oddf n evenf n) to odd.

Condition and conversion

By the expression p −→ q, we mean that if p is derivable from Γ, then q is derivable from Γ.

In addition to the standard α, β, and η conversions, the following two conversions are to be presented: (γ1) (p < M > q < N >) p −→ q

q < (M N ) > (γ2) (λx.p < M >) p < λx.M >

Assume the program. f (x) = if x = 0 then 1 else x × f (x − 1)

Let f actorial = Y f actorialf n,

Let f actorialf n = λf.λx.(((iszero x) 1) (times x (f (−x 1)))), where the λ-term ((B X1) X2) can denote the conditional sentence if B then X1 else X2. If we have the fixed point operator p < Y >, the if-part q < (iszero 0) 1 >, and the else-part

r < T imes x (f (− x 1)) > such that p −→ q and q −→ r, then

r < Y f actorialf n > = r < f actorial >.

The relation ⇒∗ denotes a reflexive and transitive closure based on α, β, η, γ1 and γ2 conversions.

Church-Rosser theorem

Because (a) the calculus for terms constructed by using only (i), (ii) and (iii) conceives the Church-Rosser Theorem, and (b) α, β and η conversions are commutative with γ1 and γ2 conversion applications, we may see that the term constructed by Definition 4.1 is transformed to a normal form (which any conversion except α cannot be applied to) uniquely up to α conversion, with respect to the relation ⇒∗, if the term has one. It is stated as: Theorem 4.2 If the term M has a normal form, it is unique up to α conversion.

Proof (Outline) Applications of γ1 and γ2 may be sound with respect to the transformation to the normal form by the following senses:

Assume two terms M and N whose normal forms are Mnormal and Nnormal, respectively. For any terms M1 and N1 such that

M ⇒∗ M1 ⇒∗ Mnormal, and N ⇒∗ N1 ⇒∗ Nnormal, 12 with respect to γ1 conversion, and λx.p < M >

∗ p < M >⇒ p < M1 > λx.p < M1 > p < λx.M1 > p < λx.Mnormal > with respect to γ2 conversion such that we intuitively see the induction for the proof. Q.E.D.

If we adopt the ELP P as a formal system (Γ as above), whether p −→ q can be determined by reasoning that on condition that we have sucP (← p; ∅; ∅; Σ; Δ), we then have sucP (← q; Σ; Δ; Σ ; Δ ) for Δ ⊆ Δ and Σ ⊆ Σ . 5

Concluding Remarks

The problem of treatments for the logic-constrained function is related to the backgrounds: (i) Logic and database views are fundamental to analyze knowledge structure ([ 14, 17 ]), to understand dynamic structure with reference to knowledge ([ 15, 16 ]). (ii) Process algebra deals with sequence structure of communications (evaluations) ([ 10, 13 ]) even for distributed systems ([ 5 ]). (iii) The logic programming system (in computational logic) contains the notion of negatives such that both classical negation (in the literal regarding awareness) and negation as failure (regarding unawareness) are combined for more powerful representations ([ 1 ]).

For a literal-constrained term, the literal should be derivable from an indicated proof system. If derivability is concerned with awareness, the term (as a function application) is regarded as originating from awareness with constraint. In this paper, the logic programming system with a contradiction removal procedure is presented, not allowed to be paraconsistent.

As regards awareness in terms of derivability, we can also have the formal systems: hybrid logic (with modality and nomination) (as in [ 3 ]), and action logic (as in [ 8 ]).

With reference to actions like those of [ 15, 16 ], analyses of whether or not we can apply them to the literal-constrained term are needed.

As the proof system itself, we summarize some points on specific expressiveness of the ELP. (1) This paper presents an abstract representation of reasoning for its application to the reasoning of contradiction removal regarding derivability vs. awareness, independent of abduction reasoning as in [ 4, 6 ]. (2) The backgrounds of soundness of succeeding and failing derivations may be closely related to model theory, following [ 1, 19 ]. (3) The notion of exceptions for each literal to be constrained by is implementable in the derivations we present, while we may apply weak negation to it as in [20]. (4) There is a problem of whether or not a non-grounded version of the literals (for awareness constraints) may be built in the proof system to derive literals for constraints. A non-grounded version of negation as failure is relevant to the discussions as in [ 17, 18 ].

References

[1] Alferes , J.J. , Dam´asio, C.V. and Pereira , L.M., A logic programming system for nonmonotonic reasoning , J. of Automated Reasoning , 14 , pp. 93 - 147 , 1995 .

[2] Besnard , P. , An Introduction to Default Logic, Springer-Verlag, 1989 .

[3] Brauner , T. , Natural deduction for hybrid logic , JLC , 14 , 3 , pp. 329 - 353 , 2004 .

[4] Brogi , A. , Lamma , P. , Mancarella , P. and Mello , P. , A unifying view for logic programming with non-monotonic reasoning , Theoretical Computer Science , 184 , 1 - 2 , pp. 1 - 59 , 1997 .

[5] Bruns , G. , Distributed Systems Analysis with CCS , Prentice-Hall , 1996 .

[6] Dung , P.M., An argumentation-theoretic foundation for logic programming , J. of Logic Programming , 22 , pp. 151 - 177 , 1995 .

[7] Gelfond , M. and Lifschitz , V. , The stable model semantics for logic programs , Proc. of 5th ICLP , pp. 1070 - 1080 , 1988 .

[8] Giordano , L. , Martelli , A. and Schwind , C. , Ramification and causality in a modal action logic , JLC , 10 , 5 , pp. 625 - 662 , 2000 .

[9] Gordon , M.J.C. , Programming Language Theory and its Implementation , Prentice Hall, 1988 .

[10] Hoare , C.A.R. , Communicating Sequential Processes , Prentice-Hall, 1985 .

[11] Kucera , A. and Esparza , J., A logical viewpoint on process-algebra , J. of Logic and Computation , 13 , 6 , pp. 863 - 880 , 2003 .

[12] Lloyd , J.W. , Foundations of Logic Programming, 2nd, Extended Edition , Springer-Verlag, 1993 .

[13] Milner , R. , Communication and Concurrency , Prentice-Hall, 1989 .

[14] Minker , J . (ed.), Foundations of Deductive Databases and Logic Programming , Morgan Kaufmann Publishers, Inc., 1987 .

[15] Mosses , P.M. , Action Semantics , Cambridge University, 1992 .

[16] Reiter , R. , Knowledge in Action, The MIT Press, 2001 .

[17] Shepherdson , J.C. , Negation in Logic Programming , in: Minker, J . (ed.), Foundations of Deductive Databases and Logic Programming , pp. 19 - 88 , 1987 .

[18] Yamasaki , S. and Kurose , Y. , Soundness of abductive proof procedure with respect to constraint for non-ground abducibles , Theoretical Computer Science , 206 , pp. 257 - 281 , 1998 .

[19] Yamasaki , S. and Kurose , Y. , A sound and complete procedure for a general logic program in non-floundering derivations with respect to the 3-valued stable model semantics , Theoretical Computer Science , 266 , pp. 489 - 512 , 2001 .