In this paper,we deal with the problem of verifying local stratifiability of logic programs and databases presented by Przymusinski.Necessary and sufficient conditions for the local stratifiability of logic programs are presented and algorithms for performing the verification are developed.Finally,we prove that a database DB containing clauses with disjunctive consequents can be easily converted into a logic program P such that DB is locally stratified iff P is locally stratified.

Przymusinski extended the notion of stratified logic programs,developed by Apt,Blair and Walker,and by van Gelder,to stratified databases that allow both negative premises and disjunctive consequents.However,he did not provide a fixpoint theory for such class of databases.On the other hand,although a fixpoint semantics has been developed by Minker and Rajasekar for non-Horn logic programs,it is tantamount to traditional minimal model semantics which is not sufficient to capture the intended meaning of negat…

Machine learning(ML)is a major subfield of artificial intelligence(AI).It has been seen as a feasi- ble way of avoiding the knowledge bottleneck problem in knowledge-based systems development.Re- search on ML has concentrated in the main on inductive learning,a paradigm for inducing rules from unordered sets of exmaples.AQ11 and ID3,the two most widespread algorithms in ML,are both induc- tive.This paper first summarizes AQ11,ID3 and the newly-developed extension matrix approach based HCV algorithm;and then…

Some criteria based on mode inference for validating inductive hypotheses are presented in this pa- per.Mode inference is carried out mechanically,thus such kind of validation can result in low overhead in consistency check and high efficiency in performance.

FGSPEC is a wide spectrum specification language intended to facilitate the software specification and the expression of transformation process from the functional specification which describes“what to do”to the corresponding design(operational)specification which describes“how to do”.The design emphasizes the coherence of multi-level specification mechanisms and a tree structure model is provided which unifies the wide spectrum specification styles from“what”to“how”.

The loop invariants take a very important role in the design,proof and derivation of the algorithmic program.We point out the limitations of the traditional standard strategy for developing loop invariants, and propose two new strategies for proving the existing algorithmic program and developing new ones. The strategies use recurrence as vehicle and integrate some effective methods of designing algorithms, e.g.Dynamic Programming,Greedy and Divide Conquer,into the recurrence relation of problem solving seq…

In this paper we try to introduce a new approach to operational semantics of recursive programs by using ideas in the“priority method”which is a fundamental tool in Recursion Theory.In lieu of modelling partial functions by introducing undefined values in a traditional approach,we shall define a priority derivation tree for every term,and by respecting the rule“attacking the subterm of the highest priority first”we define transition relations,computation sequences etc.directly based on a standard interpreta…

We define here the concept of head boundedness,head normal form and head confluence of term rewriting systems that allow infinite derivations.Head confluence is weaker than confluence,but suffi- cient to guarantee the correctness of lazy implementations of equational logic programming languages. Then we prove several results.First,if a left-linear system is locally confluent and head-bounded,then it is head-confluent.Second,head-confluent and head-bounded systems have the head Church-Rosser proper- ty.Last,…

This paper describes the design rationale of OOMMS,a module management system based on an object-oriented model.The concepts of object and module are defined.Modules refer to the software products in general which have interface parts and body parts.Related concepts of a cluster of modules,versions of a module,and revisions of a version are also defined.The tools for checking in C program modules into OOMMS are discussed.

The true value simulation is necessary in the critical path tracing fault simulation algorithm.The critical and non-critical inputs can be known after the number of controlling and non-controlling inputs and the criticality of output of every gate are determined.Single output region(SOR)is defined for non-critical lines,so many other non-critical lines can be obtained before fault simulation.Then deductive fault simulation algorithm is used to compute the fault list for every possible critical line from bot…

This paper proposes a knowledge-based specification technique(KST)for protocol development. This technique semi-automatically translates a protocol described in an informal description(natural languages or graphs)into one described in formal specifications(Estelle and SDL).The translation processes are supported by knowledge stored in the knowledge base.This paper discusses the concept, the specification control mechanism of KST and the rules and algorithms for production of FSM's which is the basis of Este…