A Fixed Point Representation of References

Abstract

This position paper is concerned with the reference in computer science. We have a formal representation of lazy references in contrast to eager and failure ones. The representation problem is motivated by static analysis in Web accessibility. A fixed point theory is adopted for such an analysis.

Introduction

To make analyses in Web usability or accessibility, we aim at capturing the link situation on the Web sites and referential relations among Web site pages. For an apperception of the link structure, this position paper deals with static analysis of relations of references which are concretized as Web site pages. The total reference structure is described by a fixed point of an associated mapping for the structure. As regards static analysis, several frameworks have been well established. Hybrid logic, which involves both state-dependent and modal operators, is a formal system with logical meanings of states and worlds ([1, 2]). Relations between the events are discussed through predicates in classical and modal logic ([3, 9]). The event as the cause-and-effect relationship is made clear from the view of rule-based system ([21]). Correlation between action and knowledge has also been studied ([14]). A mathematical behaviour of action is formulated in [13], while action may be captured by modal logic ([6]). The agent technology style is current as in [15], where algebraic approach to process originates from [8, 12] such that a logical viewpoint is given in the paper ([10]). A multi-agent is well designed in terms of modal logic ([7]).

In this position paper, based on the first-order logic (or the propositional logic) analysis approach ([5]), we see a mathematical aspect of reference structures relevant to Web site pages with fixed point theory. A Web site page recursively includes page references, where the page is itself a reference from other site pages. So far we see that there is a simple structure for some page A as a primary one: A primary reference A (recursively) includes references B1, . . . , Bn, where A may be referred to by others, and some of B1, . . . , Bn may not be available without any correct link. As regards how to make use of the references, we can think that: – To visit the (page) reference is regarded as eager. – Not to visit (but to see only the name of) the (page) reference is regarded as lazy.

– Non-available reference for visit is regarded as a failure.

Whether or not a (page) reference is visited is supposedly determined by the user (visitor). The primary reference (which the user now pays attention to and which includes other references in) is thus interpreted as: (i) eager if all the included references are eager. (ii) lazy if it never occurs as a primary one such that it is designated as lazy, or if it is a primary one where at least one included reference is not eager and other included references are eager or lazy. (iii) a failure if it is not available as a primary one, or if a primary reference with at least one included reference is a failure.

Note that the primary reference is interpreted as eager if it contains no reference. The classification of eager and lazy references for this case looks like the standard evaluation about call-by-value (eager) and call-by-name (lazy) modes of [17]. We then have a problem to see what set of lazy references is. The set of all considerable references is still finite, but it must be large enough to want to have a treatment to cover the case that the set may be countably infinite. A fixed point theory for the complete lattice is a technique as in [11, 18], to be incorporated into analysis and classification of eager and lazy reference sets, where the references are organized likely by recursive rule structures of the form: the reference including reference sequences. 2

Representation of References

In this paper, we consider recursive structures of references, which are given as a set of finite or countably infinite rules of the form A A1 . . . Al (l ≥ 0), where A, Ai are references. A is the head, while A1 . . . Al is the successor (sequence). We suppose in a set of rules that each head is followed by a unique successor.

Syntactically, we assume: (i) a set P of rules of the form A A1 . . . Al (l ≥ 0) where any two rules with the same head, A B1 . . . Bm and A C1 . . . Cn, have the same successor, and (ii) a set BP of all references occurring in the set P .

The interpretation of references is defined as eager, lazy and a failure: Assume a set P of rules. Given a set L, we have inferences to inductively define the predicates eager and lazyL which are mutually exclusive: (ir1) A

is in P eager(A) (ir2)

A A1 . . . Am is in P (m > 0) for all Ai (1 ≤ i ≤ m), eager(Ai) eager(A)

A does not occur in the head of any rule A is in L

lazyL(A) A A1 . . . Am is in P (m > 0) for all Aj (1 ≤ j ≤ m), eager(Aj) or lazyL(Aj ) for some Ak (1 ≤ k ≤ m), not eager(Ak)

lazyL(A)

Semantically, we say that: (i) If eager(A), the reference A is eager. (ii) If lazyL(A), the reference A is lazy. (iii) If neither eager(A) nor lazyL(A), the reference A is a failure. Example 1. Assume a set P containing: (i) A B, and (ii) B A C. Note that neither a rule A nor a rule A B, C can be included into the set P , as long as the rule A B (with the head A) is in P . What set of references may be lazy? To see it, we have exhaustive cases: ( 1 ) A, B, C are failures, unless there is some lazy reference. ( 2 ) C may be lazy, whether or not both of A and B are lazy. Neither A nor B can be lazy, if C still remains to be a failure. ( 3 ) For A and C to be lazy, all the A, B, C are lazy. Similarly for B and C to be lazy, all are lazy.

A mapping TP : 2BP → 2BP is defined to be

TP (I) = {A | ∃A

A1 . . . Al ∈ P. A1, . . . , Al ∈ I}.

Note that the mapping TP is similar to the mapping associated with a logic program ([11]), such that it collects eager references based on the set I of eager references. Such a mapping is often adopted. As easily seen, if I ⊆ J, then TP (I) ⊆ TP (J), that is, TP is monotone. In what follows, we have the notation: TPn(I) =

I (n = 0)

TP (TPn−1(I)) (n > 0) for a subset I ⊆ BP . The mapping TP is continuous: For any ω-chain I0 ⊆ I1 ⊆ I2 ⊆ . . . ,

∪k∈ω TP (Ik) = TP (∪k∈ω Ik).

Thus TP has the least fixed point, ∪n∈ω TPn(∅), which is denoted by lf p(TP ).

The following mapping looks like the one for logic programs with negation (as in [16, 19, 20]), but the present usage is not relevant to the treatment of negations in 3-valued logic. To capture the set of lazy references, we make use of the following mapping SP . With respect to a subset K ⊆ BP , P [K] = {A

A1 . . . Am | ∃A A1 . . . AmB1 . . . Bn ∈ P (m ≥ 0, n ≥ 0). B1, . . . , Bn ∈ K}.

Note that P [∅] = P . A mapping SP : 2BP → 2BP is defined to be

The set SP (K) denotes the collection of eager and lazy references based on the set K of lazy references. It follows that SP (∅) = lf p(TP [∅]) = lf p(TP ). When J ⊆ K, A ∈ TPi [J](∅) ⇒ A ∈ TPi [K](∅). It is because: (i) (basis) In case that i = 0, it trivially holds. (ii) (induction step) In case that i > 0:

A ∈ TPi [J](∅) ⇒ ∃A A1 . . . Am ∈ P [J ]. A1, . . . , Am ∈ TPi −[J1](∅) ⇒ ∃A B1 . . . Bn ∈ P [K] such that {B1, . . . , Bn} ⊆ {A1, . . . , Am} It follows that B1, . . . , Bn ∈ TPi −[J1](∅). By induction hypothesis, we can assume that B1, . . . , Bn ∈ TPi −[J1](∅) ⇒ B1, . . . , Bn ∈ TPi −[K1 ](∅). Therefore A ∈ TPi [K](∅).

This concludes that SP (J ) = ∪i∈ω TPi [J](∅) ⊆ ∪i∈ω TPi [K](∅) = SP (K). That is, the mapping SP is monotone. By monotonicity of SP , SP (Ji) ⊆ SP (∪i∈ω Ji) for any ω-chain J0 ⊆ J1 ⊆ J2 ⊆ . . .. Thus ∪i∈ω SP (Ji) ⊆ SP (∪i∈ω Ji). On the other hand, to show the opposite subset relation, we firstly assume that A ∈ SP (∪i∈ω Ji). Then:

A ∈ SP (∪i∈ω Ji)

j ⇒ ∃j ∈ ω. A ∈ TP [∪i∈ω Ji](∅)

j ⇒ ∃k ∈ ω. A ∈ TP [Jk](∅)

j ⇒ A ∈ ∪j∈ω TP [Jk](∅) = SP (Jk) Therefore SP (∪i∈ω Ji) ⊆ SP (Jk) for some k ∈ ω such that SP (∪i∈ω Ji) ⊆ ∪k∈ω SP (Jk). That is, SP is continuous. By means of the definition of SP (K) with respect to the mapping TP [K], SP (K) is the least fixed point of TP [K] such that we can see the following lemma.

Lemma 1. (1) For any A

A1 . . . Am ∈ P [K] (m ≥ 0), ( 2 ) For any A

A1 . . . Am ∈ P (m ≥ 0), ( 3 ) For any A

A1 . . . Am ∈ P (m > 0),

A1, . . . , Am ∈ SP (K) iff A ∈ SP (K).

A1, . . . , Am ∈ SP (K) ∪ K iff A ∈ SP (K).

A1, . . . , Am ∈ SP (K) ∪ K and there is at least one Ai 6∈ SP (∅) iff A ∈ SP (K) − SP (∅).

Proof. (1) For the rule A

A1 . . . Am ∈ P [K] (m ≥ 0): A ∈ SP (K) ⇔ A ∈ ∪i∈ω TPi [K](∅) ⇔ A1, . . . , Am ∈ ∪i∈ω TPi [K](∅) ⇔ A1, . . . , Am ∈ SP (K) ( 2 ) For the rule A A1 . . . Am ∈ P (m ≥ 0), we can derive a rule A B1 . . . Bn ∈ P [K] such that {B1 . . . Bn} ⊆ {A1 . . . Am}. The set {B1 . . . Bn} is obtained by removing each Ai of {A1 . . . Am} for Ai ∈ K. By means of ( 1 ), B1 . . . Bn ∈ SP (K) iff A ∈ SP (K). Thus

A1, . . . , Am ∈ SP (K) ∪ K iff A ∈ SP (K). ( 3 ) By means of ( 2 ), A1, . . . , Am ∈ SP (K) ∪ K (m ≥ 0) iff A ∈ SP (K). There is some Ai 6∈ S(∅) iff A 6∈ SP (∅), by ( 2 ) for the case that K = ∅. It follows that

A1, . . . , Am ∈ SP (K) ∪ K (m > 0) and there is at least one Ai 6∈ SP (∅) iff A ∈ SP (K) − SP (∅). 3

Lazy Reference Set Related to Fixed Point

In this section, we examine the set of lazy references.

Lemma 2. Assume the set P of rules. A reference A is in SP (∅) iff it is eager.

Proof. (1) Assume eager(A).

(i) If eager(A) by means of (ir1), then A is in P such that A ∈ SP (∅) (by

Lemma 1 ( 2 )). (ii) If eager(A) by means of (ir2), then a rule A A1 . . . Am is in P and for all Ai (1 ≤ i ≤ m), the predicates eager(Ai) are supposed. By induction hypothesis for eager(Ai) (1 ≤ i ≤ n), Ai ∈ SP (∅), such that by Lemma 1 ( 2 ), A ∈ SP (∅). This completes the induction. ( 2 ) Assume that A ∈ SP (∅). We prove it by induction on m for the rule A A1 . . . Am (m ≥ 0), with respect to A ∈ SP (∅). (i) If m = 0, that is, A is in P , then eager(A) (by the inference (ir1)). (ii) If m > 0 such that A A1 . . . Am is in P , by induction hypothesis of eager(Ai) (1 ≤ i ≤ m) for Ai ∈ SP (∅), we have eager(A) with the inference (ir2). This completes the induction.

Lemma 3. Assume the set P of rules. A reference A ∈ BP does not occur in the head of any rule iff A ∈ SP (BP ).

Proof. (i) Assume that the reference A occurs in the head of some rule such that there is a rule A A1 . . . Am in P (m ≥ 0). It follows that A is in P [BP ]. Thus A ∈ TP [BP ](∅) ⊆ SP (BP ). (ii) On the other hand, assume that A ∈ SP (BP ). Then A ∈ SP (BP ) = ∪i∈ω TPi [BP ](∅), which demonstrates that A occurs in the head of some rule.

For the lazy reference, we need the superset relation L ⊇ SP (L) − SP (∅) for a subset L ⊆ BP . By Lemma 2, a set of lazy references has no common reference with the set SP (∅) (the set of eager references). Assume a set M ⊆ SP (BP ) ⊆ SP (∅) such that M may be a set of references not occurring in the heads and be designated as lazy. We next investigate a fixed point of the equation L = (SP (L) − SP (∅)) ∪ M for some M ⊆ SP (BP ) by the following two theorems. Theorem 1. The set P of rules is supposedly given, where L ⊆ SP (∅). If L = {A | lazyL(A)},

L = (SP (L) − SP (∅)) ∪ M for some set M ⊆ SP (BP ).

Proof. If L = ∅, then the theorem trivially holds. Assume that L = {A | lazyL(A)} 6= ∅. Suppose lazyL(A) (A ∈ L by the assumption). We prove inductively that: – A ∈ L occurs in the head of some rule iff A ∈ SP (L) − SP (∅). – A ∈ L does not occur in the head of any rule iff A ∈ M for some M ⊆

SP (BP ).

We see that:

A occurs in the head of some rule ⇔ there is a rule A A1 . . . Am ∈ P (m > 0) such that ∃Ai. (Ai is not eager), and ∀Aj. (Aj is eager or lazy) ⇔ there is a rule A A1 . . . Am ∈ P (m > 0) such that:

∃Ai.(Ai 6∈ SP (∅)) and ∀Aj.(Aj ∈ SP (L) ∪ L) ⇔ A ∈ SP (L) − SP (∅)

(by Lemma 1 ( 3 )) A ∈ L does not occur in the head of any rule iff A ∈ SP (BP ) (Lemma 3) such that A ∈ M for some M ⊆ SP (BP ). This completes the proof.

Lemma 4. Assume a fixed point L of the equation L = (SP (L) − SP (∅)) ∪ M for some set M ⊆ SP (BP ). Then (i) L ⊆ SP (∅). (ii) SP (L) − SP (∅) ⊆ SP (SP (∅)). (iii) M ⊆ SP (SP (∅)).

Proof. (i) SP (L) − SP (∅) ⊆ SP (∅). M ⊆ SP (BP ) ⊆ SP (∅). It follows that L ⊆ SP (∅). (ii) By (i), applying the monotone mapping SP , SP (L) ⊆ SP (SP (∅)). Then SP (L) − SP (∅) ⊆ SP (SP (∅)). (iii) Since SP (SP (∅)) ⊆ SP (BP ) by monotonicity of the mapping of SP , SP (BP ) ⊆ SP (SP (∅)). On the assumption that M ⊆ SP (BP ), M ⊆ SP (SP (∅)).

In Lemma 4, we suppose that a set M is designated as lazy. Theorem 2. Assume that a set P of rules is given, such that L = (SP (L) − SP (∅)) ∪ M where M ⊆ SP (BP ). Then L = {A | lazyL(A)}.

Proof. If L = ∅, the theorem trivially holds. We now suppose that L 6= ∅. ( 1 ) Take any reference A ∈ L. We prove inductively with the following cases (i) and (ii) that lazyL(A). (It follows that L ⊆ {A | lazyL(A)}.) (i) Assume that A ∈ SP (L) − SP (∅) 6= ∅.

A ∈ SP (L) − SP (∅) ⇒ there is a rule A A1 . . . Am (m > 0) in P such that:

A1, . . . , Am ∈ SP (L) ∪ L and at least one Ai is not in SP (∅) (by Lemma 1 ( 3 )) ⇒ there is a rule A A1 . . . Am (m > 0) in P such that:

A1, . . . , Am are eager or lazy, and at least one Ai is not eager (by induction hypothesis) : Aj ∈ SP (L) − SP (∅) ⇒ Aj is lazy;

Aj ∈ SP (∅) ⇒ Aj is eager; Aj ∈ L − (SP (L) − SP (∅)) ⇒ Aj is lazy ⇒ A is lazy, that is, lazyL(A) (ii) Assume that A ∈ M ⊆ SP (BP ). By Lemma 3, A does not occur in the head of any rule. If A ∈ L, then lazyL(A).

By (i) and (ii), we conclude that L ⊆ {A | lazyL(A)}. ( 2 ) We next prove that if lazyL(A) then A ∈ L. (i) If A occurs in the head of some rule, then there is a rule A A1 . . . Am such that each Aj is eager or lazy (Aj ∈ SP (∅) ∪ L), and at least one Ai is not eager (Ai 6∈ SP (∅)). It follows that A ∈ SP (L) − SP (∅) ⊆ L. (ii) If A does not occur in the head of any rule, A ∈ L because of lazyL(A). As the conclusion of ( 2 ), L ⊇ {A | lazyL(A)}, by which we conclude that L = {A | lazyL(A)}, as well as the proof ( 1 ). This completes the proof.

By Theorems 1 and 2, we see that L is a fixed point of the equation:

L = (SP (L) − SP (∅)) ∪ M for some set M ⊆ SP (BP ) iff L = {A | lazyL(A)}. As is seen, there is a least fixed point of the equation. Note that M ⊆ SP (BP ) is not uniquely determined for the equation L = (SP (L) − SP (∅)) ∪ M . In the next section, instead of the equation L = (SP (L) − SP (∅)) ∪ M , we take a superset relation L ⊇ SP (L) − SP (∅) without such a set M . 4

Soundness and Completeness of Reference Laziness

We firstly have a soundness theorem of the predicate lazyL(A) (which states that A is lazy with the set L ⊆ SP (∅)), with respect to membership of A in L or in SP (L) − SP (∅) with some set L′, where

SP (L) − SP (∅) ⊆ SP (L′) − SP (∅) ⊆ L′ ⊆ SP (∅).

Theorem 3. Given a set P of rules, assume lazyL(A), where L ⊆ SP (∅). Then A ∈ L, or there is L′ such that A ∈ SP (L) − SP (∅) ⊆ SP (L′) − SP (∅) ⊆ L′ ⊆ SP (∅).

Proof. Assume that lazyL(A). ( 1 ) We prove inductively that A ∈ L, or A ∈ SP (L) − SP (∅) as follows: (i) If A doe not occur in the head of any rule, A must be in L because of the predicate lazyL(A). (ii) If A occurs in the head of some rule, then: there is a rule A A1 . . . Am ∈ P (m > 0) such that: ∃Ai. (Ai is not eager), and ∀Aj. (Aj is eager or lazy) ⇒ there is a rule A A1 . . . Am ∈ P (m > 0) such that:

∃Ai.(Ai 6∈ SP (∅)) and ∀Aj.(Aj ∈ SP (L) ∪ L) ⇒ A ∈ SP (L) − SP (∅) ( 2 ) Now we assume the case that lazyL(A) such that A ∈ SP (L) − SP (∅). With L0 = L and L1 = SP (L) − SP (∅), we have an ω-chain L1 ⊆ L2 ⊆ . . ., owing to monotonicity of SP ,

SP (L0) − SP (∅) = L1 SP (L0 ∪ L1) − SP (∅) = L2 . . . . . . . . . . . .

SP (∪i∈ω Li) − SP (∅) = ∪i≥1 Li where SP (∪i∈ω Li) = ∪i∈ω SP (Li) by continuity of SP . Take L′ = ∪i∈ω Li ⊇ ∪i≥1 Li. Then

A ∈ L1 ⊆ ∪i≥1 Li = SP (∪i∈ω Li) − SP (∅) = SP (L′) − SP (∅) ⊆ L′. Because Li ⊆ SP (∅) (i ∈ ω) by the construction of Li, L′ = ∪i∈ω Li ⊆ SP (∅). This completes the proof.

We next have a completeness theorem of the predicate lazyL(A) (which states that A is lazy with the set L ⊆ SP (∅)), with respect to membership of A in SP (L) − SP (∅), where

SP (L) − SP (∅) ⊆ L ⊆ SP (∅).

Theorem 4. Assume a set P of rules such that ∅ 6= SP (L) − SP (∅) ⊆ L for a set L ⊆ SP (∅). If A ∈ SP (L) − SP (∅), then lazyL(A).

Proof. Assume that A ∈ SP (L) − SP (∅). By Lemma 1 ( 3 ), there is a rule such that A1, . . . , Am ∈ SP (L) ∪ L and at least one Ai in in SP (∅). Because A1, . . . , Am are all in SP (L) ∪ L and at least one Ai is in SP (∅), we see the cases for each Aj : (i) Aj ∈ L (ii) Aj ∈ SP (∅) ⊆ SP (L) ⇒ eager(Aj ) (by Lemma 2) (iii) Aj ∈ SP (L) − SP (∅) ⊆ SP (L) ⇒ lazyL(Aj ) (by induction hypothesis for Aj ) If Ai is in SP (∅), then Ai is in L or lazyL(Ai) excluding the case (ii). By the inferences (ir3) and (ir4), we can conclude that lazyL(A). 5

Concluding Remarks

We have dealt with a finite or countably infinite set of rules, where the set of lazy references is represented by means of fixed point approach. Practically only a finite set is needed, where the theoretical considerations are available from static analysis views as in this paper. Given a set of P of rules with a set L of designated lazy references, we have soundness and completeness of reference laziness in the following sense: ( 1 ) (soundness) The predicate lazyL(A) (which states that the reference A is lazy with the set L ⊆ SP (∅)) is sound with respect to membership of A in L or in SP (L) − SP (∅), with some set L′ such that

SP (L) − SP (∅) ⊆ SP (L′) − SP (∅) ⊆ L′ ⊆ SP (∅). ( 2 ) (completeness) The predicate lazyL(A) (which states that A is lazy with the set L ⊆ SP (∅)) is complete with respect to membership of A in SP (L) − SP (∅), where

SP (L) − SP (∅) ⊆ L ⊆ SP (∅).

In addition to the soundness, the designation of lazy references may step by step construct some set L′ which is relative to the soundness of the predicate lazyL(A) with respect to membership of A in SP (L) − SP (∅).

The set of finite-failure references (the finite-failure set) may be defined. This is similar to finite failure of logic programming ([11]), however, a unique successor (which may be the empty) for each head may be allowable in this case.

We can define the finite-failure set F FP to be F FP = ∪d∈ω F F d , where: P F FP0 = {A ∈ BP | A does not occur in the head of any rule} − L, F FPd = {A ∈ BP | ∃A A1 . . . Am ∈ P, ∃Ai. Ai ∈ F FPd−1} − L (d > 0). When L = ∅, regarding the reference as a proposition with the propositional Horn logic, we have F FP = ∩i∈ω TPi (Bp) (where TPi stands for i-times applications to the set BP ).

If we allow the case that there are more than two rules with a head including different successors, which is prohibited in the set of rules of this paper, the rule set conceives the interpretation that the reference A is both eager and lazy. Even if such a case is involved, the properties as in the propositional Horn logic may be of use for the treatments of references. It may be a problem to see a relation between the lazy reference set and the set ∩i∈ωTPi (BP ). How we temporarily have a set L may affect some reasonable considerations about the relation.

References

1. Areces , C. and Blackburn , P. , Repairing the interpolation in quantified logic , Annals of Pure and Applied Logic , 123 , 287 - 299 , 2003 .

2. Brauner , T. , Natural deduction for hybrid logics , J. of Logic and Computation , 14 , 329 - 353 , 2004 .

3. Cervesato , I. , Chittaro , L. and Montanari , A. , A general modal framework for the event calculus and its skeptical and credulous variants , Proc. of 12th European Conference on Artificial Intelligence , pp. 12 - 16 , 1996 .

4. Dean , T. and Boddy , M. , Reasoning about partially ordered events , Artificial Intelligence , 36 , pp. 375 - 399 , 1988 .

5. Genesereth , M.R. and Nilsson , N.J. , Logical Foundations of Artificial Intelligence , Morgan Kaufmann, 1988 .

6. Giordano , L. , Martelli , A. and Schwind , C. , Ramification and causality in a modal action logic , J. of Logic and Computation , 10 , pp. 625 - 662 , 2000 .

7. Harpern , J.Y. and Lakemeyer ,G., Multi-agent only knowing , J. of Logic and Computation , 11 , pp. 41 - 70 , 2001 .

8. Hoare , C.A.R. , Communicating Sequential Processes , Prentice-Hall, 1985 .

9. Kowalski , R.A. , Database updates in the event calculus , J. of Logic Programming , 12 , 121 - 146 , 1992 .

10. Kucera , A. and Esparza , J., A logical viewpoint on process-algebraic quotients , J. of Logic and Computation , 13 , pp. 863 - 880 , 2003 .

11. Lloyd , J.W. , Foundations of Logic Programming , 2nd, Extended Edition , SpringerVerlag, 1993 .

12. Milner , R. , Communication and Concurrency , Prentice-Hall, 1989 .

13. Mosses , P.M. , Action Semantics , Cambridge University, 1992 .

14. Reiter , R. , Knowledge in Action, The MIT Press, 2001 .

15. Russell , S. and Norvig , P. , Artificial Intelligence-A Modern Approach-, PrenticeHall , 1995 .

16. Shepherdson , J.C. , Negation in logic programming , In Minker,J. (ed.), Foundations of Deductive Databases and Logic Programming , 19 - 88 , 1987 .

17. Winskel , G. , The Formal Semantics of Programming Languages , MIT Press, 1993 .

18. Yamasaki , S., A denotational semantics and dataflow construction for logic programs , Theoretical Computer Science , 124 , pp. 71 - 91 , 1994 .

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

20. Yamasaki , S. , Logic programming with default, weak and strict negations , Theory and Practice of Logic Programming , 6 , pp. 737 - 749 , 2006 .

21. Yamasaki , S. and Sasakura , M., A calculus effectively performing event formation with visualization , Lecture Notes in Computer Science , 4759 , pp. 287 - 294 , 2008 .