Software Science and Engineering

The following sections are included:

• Editorial Board

• PREFACE

• Table of Contents

The TRS (term rewriting system) Working Group of ICOT has been studying applications of TRSs to the intelligent programming system. As a result, we have implemented a TRS generator called Metis, an experimental tool with the many functions required for such a system. This paper describes the features of Metis and several experiments with it.

The following sections are included:

• Introduction

• An example

• Formal definition of a regulated accumulating array grammar

• Computer simulations

• Restricted version: Accumalting array grammar

• Acknowledgments

• References

In this paper, a method is presented for verifying the progress property of a communication protocol whose specification is described algebraically in a style of an "abstract sequential machine", and Stenning's data transfer protocol is used as a running example. At first, the set of sequences of states is introduced, and several theorems (invariants) on the specification are verified by algebraic methods, and then, they are transformed into the theorems for the sequences of states. Next, such a hypothesis as "if the packets with the same contents have been retransmitted repeatedly, at least one of them will be eventually received by the receiver" is also formulated as theorems for the sequences of states. Finally, by using those theorems and several axioms which denote inference rules of Temporal logic, the formula (term) which expresses the progress property is proved to be true by using our interactive verification support system for algebraic specifications.

An algebraic specification (or text) specifies a congruence relation on a set of expressions. In algebraic language ASL/*, a pair (G, AX) is called a text, where G is a context-free grammar and AX is a set of axioms. A text t=(G, AX) specifies the set E_G of expressions generated by G and the least congruence relation on E_G satisfying all the axioms in AX, where 'congruency' is defined based on the syntax (phrase structure) of the expressions. In general, for a text t in ASL/*, the condition, (A) e is congruent with e' in t, is not logically equivalent to the condition, (B) e' is obtained from e by rewriting e when the axioms in t are regarded as 'bidirectional' rewrite rules. We present a sufficient condition for a text t under which (A) and (B) are equivalent for any pair of expressions e and e', which means that the congruence relation specified by t is simply defined operationally.

This paper shows a method of constructing a dataflow for a logic program to extract a functional from it, by means of a dataflow dealing with sequences from the set of idempotent substitutions. The dataflow is expressed as a functional involving fair merge functions in order to represent the atom set union over a sequence domain, as well as manipulations of unifiers for the unit resolution deductions of clauses. The functional completely and soundly denotes the atom generation in terms of idempotent substitutions without using atom forms. An equivalence relation on the idempotent substitution set is exploited. Its least fixpoint is interpreted as denoting the whole atom generation in terms of manipulations on idempotent substitutions.

This paper presents a new diagnosis algorithm for Prolog programs. Bugs are located by examining the record of execution trace in some systematic manner, which corresponds to tracing either proof trees or search trees in a top-down manner. Human programmers just need to answer "Yes" or "No" for queries issued during the top-down tracing. Moreover, queries about atoms with the same predicates are issued continually so that not only are segments containing bugs identified more quickly but also queries are easier for human programmers to answer. The outline of an implementation of the diagnosis algorithm is shown as well.

In this paper, We explain a discourse understanding model, ADAM (Actual Discourse Assistant Model) [7] and show the example of its practical use. In the computer system which has an knowledge base, it is a very important issue how a user communicates with the system. Natural language is one of the way to communicate with it, and the discourse understanding is necessary to comprehend natural language deeply.

ADAM gives a more intuitive expression of the real world by introducing the object-oriented concept into situation semantics. In this model, an object has about the same meaning as the one which is called a parameter in situation semantics. An object is a unit of information to be operated by a knowledge system. All the information, such as the character of individual or a causal relation among objects, are extracted from the objects in a knowledge base. Thus, in ADAM, a knowledge system which has a natural language user interface system can cope with lots of user's requests by utilizing these information.

The following sections are included:

• Introduction

• An example of negation technique

• Term logic

• General context-free grammars

• Negation technique

• Discussions

• References

Much work has been devoted to special-purpose reasoning assistant systems whose underlying logics are fixed. In contrast with such a trend, this paper is devoted to a new dimension of computer-assisted reasoning research, that is, a general-purpose reasoning assistant system that allows a user to define his or her own logical system relevant for the intended problem domain and to reason about it.

In the first half of the paper, the need, significance and design principle of EUODHILOS : a general-purpose system for computer-assisted reasoning, are discussed. Then the system overview is described, with emphasis on the following three points : (1) a formal system description language based on definite clause grammar, (2) a methodology for proving based on several sheets for logical thought, (3) visual human-computer interface for reasoning. In the latter half of the paper, the potential and usefulness of EUODHILOS are demonstrated through experiments and experiences of its use by a number of logics and proof examples therein. These have been used or devised in a circle of computer science, artificial intelligence and so on.

Knowledge engineering should have a fundamental logic as its theoretical basis. As a conceptual tool underlying various activities in knowledge engineering, the logic should be as natural as possible for human logical thinking. Many current theoretical research on knowledge engineering is directly or indirectly based on classical mathematical logic or its various extensions. However, the mathematical logic is not a natural model of human logical thinking in the sense that it has no natural representation for conditionals and its logical theorems include a lot of implicational paradoxes. Relevance logic and entailment logic are two kinds of logic systems which are independently established for the purpose of constructing a "more natural" logic for human logical thinking than the classical mathematical logic. A major feature of the logics is that they have a primitive intensional connective as a natural representation for conditionals and their logical theorems include no implicational paradoxes. This paper presents a comparative study for the two kinds of logics. We compare differences between the relevance logic and the entailment logic in some aspects including claim, syntax, semantics, admissibility of Disjunctive Syllogism, decidability, and modality. A conclusion of the comparison is that the entailment logic is more natural for human logical thinking than the relevance logic. This is mainly because the entailment logic allow us to have a natural interpretation for human logical reasoning to get new and valid knowledge from known or assumed premises. Therefore, the entailment logic is a hopeful candidate for the logic to be used as the fundamental theory of knowledge engineering.

Reference counting schemes are suitable for garbage collection on distributed systems because they do not require global information to find garbage. However, reference counting schemes have a serious drawback: they cannot reclaim garbage which form cyclic structures. In this paper, we propose an extension of the traditional reference counting scheme, group reference counting, which alleviates the drawback. This scheme is able to reclaim circularly referenced objects which are contained in object groups. We describe how this scheme can be implemented on distributed object-oriented concurrent systems. The overhead of this scheme does not depend on the number of nodes. Thus this scheme works efficiently on distributed systems containing large number of nodes.

In this paper we present the class of general logic programs which has a special kind of stratifications, called the locally finite stratification. For the class, good properties of propositional logic programs, such as termination and safeness, are preserved. Using these properties, we show the completeness of a kind of SLDNF-resolution that use a depth bound, called depth bounded resolution, with respect to the perfect model semantics. Finally we syntactically characterize a subclass of the class, called weakly reducing programs and show that the depth bounded resolution is complete and effective for weakly reducing programs.