The maintenance sequences of a knowledge base and their limits are intro-duced. Some concepts used in knowledge base maintenance, such as new laws,user's rejections, and reconstructions of a knowledge base are defined; the re-lated theorems are proved. A procedure is defined using transition systems; itgenerates maintenance sequences for a given user's model and a knowledge base.It is proved that all sequences produced by the procedure are convergent, andtheir limit is the set of true sentences of the model…

This paper deals with model genemtion for equational theories, i.e, auto-matically generating (finite) models of a given set of (logical) equations. Ourmethod of finite model generation and a tool for automatic construction of finitealgebras is described. Some examples are given to show the applications of ourprogram. We argue that, the combination of model generators and theoremprovers enables us to get a better understanding of logical theories. A briefcomparison between our tool and other similar tools i…

A simple abstract model of Eiffel is introduced, and its denotational seman-tics is defined using VDM style. A static analysis approach is presented to treatmultiple inheritance and renaming mechanism. Within the framework of deno-tational semantics iatroduced in this paper, the key features of Eiffel, such asidentification, classification, multiple inheritance, polymorphism and dynamicbinding, can be adequately characterized.

Traditional AI systems are brittle in the sense that they fail miserably whenpresented with problems even slightly outside of their limited range of expertise.A powerful, extensible strategy of Distributed Artificial Intelligence (DAI) forovercoming such bounds is to put the system in a society of systems. So theability to coordinate group activities of individuals and to communicate betweeneach other is necessary for a language describing DAI systems. Agent-orientedlanguage NUML is such a language. It is a…

Cyber nets are also known as self modifying nets. Though proposed anddefined some 20 years ago, they have never been under thorough study eversince. The reason for this is simple: the nonlinear nature of such nets keeps themaway from applications of well developed methods known to the whole Petri NetSociety in the world. This paper attempts to make a start of studying cybernets in depth by proposing a way to define and to verify S-invariants and T-invariants in such nets. These invariants reflect important …

The concepts of the nonuniform and strong nonuniform lownesss are in-troduced. Those notions provide a uniform framework to study connectionsbetween the polynomiaLtime hierarchy and sparse sets.

The problem of putting consistent theories together in institutions is dis-cussed. A general necessary condition for consistency of the resulting theory iscarried out, and some sufficient conditions are given for diagrams of theories inwhich shapes are tree bundles or directed graphs. Moreover, some transforma-tions from complicated cases to simple ones are established.

The concept of institution of variable truth values is introduced and somemain results about institutions are generalized. In particular, some propertiesof institutions of variable truth vaues preserved by change of truth values areestablished.

This paper presents and analyzes three fundamental problems in knowledgeacquisition, and proposes a general method for tackling them. The methoddivides the whole process of knowledge acquisition into a set of almost indepen-dent pieces, each of which can be finished by knowledge engineers, experts andassistants, respectively.

Further research about nonterminating rewritings is introduced. First, the previousdefinition of head boundedness is modified to exclude nonfair reduction sequences.A sufficient condition is then given to determine head boundedness of term rewritingsystems. The condition is then developed to a method to determine head boundednessof constructor systems.

Kapur and Musser studied the theoretical basis for proof by consistency and ob-tained an inductive completeness result: p q if and only if p = q is true in everyinductive model. However, there is a loophole in their proof for the soundness part:p = q implies p = q is true in every inductive model. The aim of this paper is to give acorrect characterization of inductive soundness from an algebraic view by introducingstrong inductive models.