Verifying local stratifiability of logic programs and databases

In this paper, we deal with the problem of verifying local stratifiability of logic programs and databases presented by Przymusinski. The notion of dependency graphs is generalized from representing the priority relation between predicate symbols to representing the priority between atoms. 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 easily be converted into a logic program P such that DB is locally stratified iff P is locally stratified. Yi-Dong Shen, Dr.: Department of Computer Science, Chongqing University, Chongqing, 630044, P.R. China (Present Address) c/o Ping Ran, Department of Heat Power Engineering, Chongqing UniversityResearch interests: Artificial Intelligence, Deductive Databases, Logic Programming, Non-Monotonic Reasoning, Parallel Processing     

Proving termination of context-sensitive rewriting by transformation

Context-sensitive rewriting (CSR) is a restriction of rewriting that forbids reductions on selected arguments of functions. With CSR, we can achieve a terminating behavior with non-terminating term rewriting systems, by pruning (all) infinite rewrite sequences. Proving termination of CSR has been recently recognized as an interesting problem with several applications in the fields of term rewriting and programming languages. Several methods have been developed for proving termination of CSR. Specifically, a number of transformations that permit treating this problem as a standard termination problem have been described. The main goal of this paper is to contribute to a better comprehension and practical use of transformations for proving termination of CSR. We provide new completeness results regarding the use of the transformations in two restricted (but relevant) settings: (a) proofs of termination of canonical CSR and (b) proofs of termination of CSR by using transformations together with simplification orderings. We have also made an experimental evaluation of the transformations, which complements the theoretical analysis from a practical point of view. This leads to new hierarchies of the transformations which are useful to guide their practical use when implementing tools for proving termination of CSR.     

Proving operational termination of membership equational programs

Reasoning about the termination of equational programs in sophisticated equational languages such as Elan, Maude, OBJ, CafeOBJ, Haskell, and so on, requires support for advanced features such as evaluation strategies, rewriting modulo, use of extra variables in conditions, partiality, and expressive type systems (possibly including polymorphism and higher-order). However, many of those features are, at best, only partially supported by current term rewriting termination tools (for instance mu-term, C i ME, AProVE, TTT, Termptation, etc.) while they may be essential to ensure termination. We present a sequence of theory transformations that can be used to bridge the gap between expressive membership equational programs and such termination tools, and prove the correctness of such transformations. We also discuss a prototype tool performing the transformations on Maude equational programs and sending the resulting transformed theories to some of the aforementioned standard termination tools.     

Operational termination of conditional term rewriting systems

We describe conditional rewriting by means of an inference system and capture termination as the absence of infinite inference: that is, all proof attempts must either successfully terminate, or they must fail in finite time. We call this notion operational termination. Our notion of operational termination is parametric on the inference system. We prove that operational termination of CTRSs is, in fact, equivalent to a very general notion proposed for 3-CTRSs, namely the notion of quasi-decreasingness, which is currently the most general one which is intended to be checked by comparing parts of the CTRS by means of term orderings. Therefore, existing methods for proving quasi-decreasingness of CTRSs immediately apply to prove operational termination of CTRSs.     

Performance of an OR-parallel logic programming system

The research focus in parallel logic programming is shifting rapidly from theoretical considerations and simulation on uniprocessors to implementation on true multiprocessors. This report presents performance figures from such a system,Boplog, for OR-parallel Horn clause logic programs on the BBN Butterfly Parallel Processor. Boplog is designed expressly for a large scale shared memory multiprocessor with an Omega interconnect. The target machine and underlying execution model are described briefly. The primary focus of the paper is on detailed statistics taken from the execution of benchmark programs to assess the performance of the model and clarify the impact of design and architecture decisions. They show that while speedup of this implementation on highly OR-parallel problems is very good, overall performance is poor. Despite its speed drawback, many aspcts of the implementation and its performance can prove useful in designing future systems for similar machines. A binding model that prohibits constant time access to bindings, and the inability of the machine to support an ambitious use of machine memory appear to be most damaging factors.This work was carried out at the University of Utah, Salt Lake City, Utah. It was supported by a University of Utah Graduate Research Fellowship, the National Science Foundation under Grant DCR-856000, and by an unrestricted gift from L. M. Ericsson Telefon AB, Stockholm, Sweden, Production of the document was supported by the Rockwell International Science Center.     

Proving pointer programs in higher-order logic

Building on the work of Burstall, this paper develops sound modelling and reasoning methods for imperative programs with pointers: heaps are modelled as mappings from addresses to values, and pointer structures are mapped to higher-level data types for verification. The programming language is embedded in higher-order logic. Its Hoare logic is derived. The whole development is purely definitional and thus sound. Apart from some smaller examples, the viability of this approach is demonstrated with a non-trivial case study. We show the correctness of the Schorr–Waite graph marking algorithm and present part of its readable proof in Isabelle/HOL.     

On the equivalence and range of applicability of graph-based representations of logic programs

Logic programs under Answer Sets semantics can be studied, and actual computation can be carried out, by means of representing them by directed graphs. Several reductions of logic programs to directed graphs are now available. We compare our proposed representation, called Extended Dependency Graph, to the Block Graph representation recently defined by Linke [Proc. IJCAI-2001, 2001, pp. 641-648]. On the relevant fragment of well-founded irreducible programs, extended dependency and block graph turns out to be isomorphic. So, we argue that graph representation of general logic programs should be abandoned in favor of graph representation of well-founded irreducible programs, which are more concise, more uniform in structure while being equally expressive.     

Compositional model-theoretic semantics for logic programs

We present a compositional model-theoretic semantics for logic programs, where the composition of programs is modelled by the composition of the admissible Herbrand models of the programs. An Herbrand model is admissible if it is supported by the assumption of a set of hypotheses. On one hand, the hypotheses supporting a model correspond to an open interpretation of the program intended to capture possible compositions with other programs. On the other hand, admissible models provide a natural model-theory for a form of hypothetical reasoning, called abduction. The application of admissibel models to programs with negation is discussed. Antonio Brogi: Dipartimento di Informatica, Università di Pisa, Corso Italia 40, 56125 Pisa, ItalyResearch interests: Programming Language Design and Semantics, Logic Programming and Artificial Intelligence     

命令式程序终止性验证方法综述

作为软件完全正确性的重要组成部分,程序终止性受到越来越多的关注。旨在跟踪国内外针对命令式程序的终止性验证方法,调研该领域的最新研究成果,同时提出解决该问题的建议性方法框架,对命令式程序终止性研究提供有意义的帮助。给出了程序终止性问题的定义,介绍了已有的数值程序、堆操作程序终止性验证方法,并分别进行了分析与对比。总结了当前研究中存在的难点与热点问题,给出了一种基于模型检验的C程序终止性验证框架,该框架可以作为研究命令式程序终止性的基本框架。     

Grammar-related transformations of logic programs

We investigate a simple transformation of logic programs capable of inverting the order of computation. Several examples are given which illustrate how this transformation may serve such purposes as left-recursion elimination, loop-elimination, simulation of forward reasoning, isotopic modification of programs and simulation of abductive reasoning.     

Towards the construction of distributed detection programs,with an application to distributed termination

Summary Methodological design of distributed programs is necessary if one is to master the complexity of parallelism. The class of control programs, whose purpose is to observe or detect properties of an underlying program, plays an important role in distributed computing. The detection of a property generally rests upon consistent evaluations of a predicate; such a predicate can be global, i.e. involve states of several processes and channels of the observed program. Unfortunately, in a distributed system, the consistency of an evaluation cannot be trivially obtained. This is a central problem in distributed evaluations. This paper addresses the problem of distributed evaluation, used as a basic tool for solution of general distributed detection problems. A new evaluation paradigm is put forward, and a general distributed detection program is designed, introducing the iterative scheme ofguarded waves sequence. The case of distributed termination detection is then taken to illustrate the proposed methodological design. Jean-Michel Hélary is currently professor of Computer Science at the University of Rennes, France. He received a first Ph.D. degree in Numerical Analysis in 1968, then another Ph.D. Degree in Computer Science in 1988. His research interests include distributed algorithms and protocols, specially the methodological aspects. He is a member of an INRIA research group working at IRISA (Rennes) on distributed algorithms and applications. Professor Jean-Michel Hélary has published several papers on these subjects, and is co-author of a book with Michel Raynal. He serves as a PC member in an international conference. Michel Raynal is currently professor of Computer Science at the University of Rennes, France. He received the Ph.D. degree in 1981. His research interests include distributed algorithms, operating systems, protocols and parallelism. He is the head of an INRIA research group working at IRISA (Rennes) on distributed algorithms and applications. Professor Michel Raynal has organized several international conferences and has served as a PC member in many international workshops, conferences and symposia. Over the past 9 years, he has written 7 books that constitute an introduction to distributed algorithms and distributed systems (among them: Algorithms for Mutual Exclusion, the MIT Press, 1986, and Synchronization and Control of Distributed Programs, Wiley, 1990, co-authored with J.M. Hélary). He is currently involved in two european Esprit projects devoted to large scale distributed systems.This work was supported by French Research Program C³ on Parallelism and Distributed ComputingAn extended abstract has been presented to ISTCS '92 [12]     

An extended variant of atoms loop check for positive logic programs

The Equality check and the Subsumption check are weakly sound, but are not complete even for function-free logic programs. Although the OverSize (OS) check is complete for positive logic programs, it is too general in the sense that it prunes SLD-derivations merely based on the depth-bound of repeated predicate symbols and the size of atoms, regardless of the inner structure of the atoms, so it may make wrong conclusions even for some simple programs. In this paper, we explore complete loop checking mechanisms for positive logic programs. We develop an extended Variant of Atoms (VA) check that has the following features: (1) it generalizes the concept of “variant” from “the same up to variable renaming” to “the same up to variable renaming except possibly with some arguments whose size recursively increases”, (2) it makes use of the depth-bound of repeated variants of atoms instead of depth-bound of repeated predicate symbols, (3) it combines the Equality/Subsumption check with the VA check, (4) it is complete w. r. t. the leftmost selection rule for positive logic programs, and (5) it is more sound than both the OS check and all the existing versions of the VA check. The research was completed when the author visited the University of Maryland Institute for Advanced Computer Studies. Yi-Dong Shen, Ph. D: He is a professor of Computer Science at Chongqing University, China. He received the Ph. D degree in computer Science from Chongqing University in 1991. He was a visiting researcher at the University of Valenciennes, France (1992–1993) and the University of Maryland Institute for Advanced Computer Studies (UMIACS), U. S. A. (1995–1996), respectively. His present interests include: Artificial Intelligence, Deductive and Object-Oriented Databases, Logic Programming and Parallel Processing.     

Well-founded semantics and stratification for ordered logic programs

This paper present an extension of traditional logic programming, called ordered logic (OL) programming, to support classical negation as well as constructs from the object-oriented paradigm. In particular, such an extension allows to cope with the notions of object, multiple inheritance and non-monotonic reasoning. The contribution of the work is mainly twofold. First, a rich wellfounded semantics for ordered logic programs is defined. Second, an efficient method for the well-founded model computation of a meaningful class of ordered logic programs, called stratified programs, is provided.     

Compile—time detection of aliasing in euclid programs

Aliasing of variables occurs when two or more identifiers accessible in the same scope refer to the same storage location. When aliasing is present, the meaning of assignments becomes obscure because assignment to one variable identifier may change the value of others. Some of the more obscure kinds of variable aliasing can be the cause of particularly insidious bugs in computer programs. Axiomatic proof systems, such as that used for the Euclid language, assume that no aliasing is present so that the meaning of assignment is clear. For this reason, Euclid requires that no aliasing be present in Euclid programs and requires the compiler to implement checks to ensure this. This paper discusses the features of Euclid that aid in the detection of aliasing. It enumerates the kinds of aliasing that can be present in Euclid programs and gives efficient one-pass algorithms for compile-time detection of potential aliases. Aliasing is related to interference between concurrent processes, and a similar algorithm for detection of inter-process interference in Concurrent Euclid programs is presented.     

Introduction of dosim predicate to Prolog

This paper proposes a predicate nameddosim which provides a new function for parallel execution of logic programs. The parallelism achieved by this predicate is a simultaneous mapping operation such as bagof and setof predicates. However, the degree of parallelism can be easily decided by arranging the arguments of the dosim goal. The parallel processing system with dosim was realized on a tight-coupled multiprocessor machine. To control the degree of parallelism and reduce the amount of memory required for execution, we introduce the grouping method for the goals executed in parallel and some variations of the dosim predicate. The effectiveness of the proposed method is demonstrated by the results of the execution of several applications.     

Abstraction-Carrying Code: a Model for Mobile Code Safety

Proof-Carrying Code (PCC) is a general approach to mobile code safety in which programs are augmented with a certificate (or proof). The intended benefit is that the program consumer can locally validate the certificate w.r.t. the “untrusted” program by means of a certificate checker—a process which should be much simpler, efficient, and automatic than generating the original proof. The practical uptake of PCC greatly depends on the existence of a variety of enabling technologies which allow both proving programs correct and replacing a costly verification process by an efficient checking procedure on the consumer side. In this work we propose Abstraction-Carrying Code (ACC), a novel approach which uses abstract interpretation as enabling technology. We argue that the large body of applications of abstract interpretation to program verification is amenable to the overall PCC scheme. In particular, we rely on an expressive class of safety policies which can be defined over different abstract domains. We use an abstraction (or abstract model) of the program computed by standard static analyzers as a certificate. The validity of the abstraction on the consumer side is checked in a single pass by a very efficient and specialized abstract-interpreter. We believe that ACC brings the expressiveness, flexibility and automation which is inherent in abstract interpretation techniques to the area of mobile code safety.

---

     

Matrix Interpretations for Proving Termination of Term Rewriting

We present a new method for automatically proving termination of term rewriting. It is based on the well-known idea of interpretation of terms where every rewrite step causes a decrease, but instead of the usual natural numbers we use vectors of natural numbers, ordered by a particular nontotal well-founded ordering. Function symbols are interpreted by linear mappings represented by matrices. This method allows us to prove termination and relative termination. A modification of the latter, in which strict steps are only allowed at the top, turns out to be helpful in combination with the dependency pair transformation. By bounding the dimension and the matrix coefficients, the search problem becomes finite. Our implementation transforms it to a Boolean satisfiability problem (SAT), to be solved by a state-of-the-art SAT solver.     

Proving termination of nonlinear command sequences

We describe a simple and efficient algorithm for proving the termination of a class of loops with nonlinear assignments to variables. The method is based on divergence testing for each variable in the cone-of-influence of the loop’s condition. The analysis allows us to automatically prove the termination of loops that cannot be handled using previous techniques. We also describe a method for integrating our nonlinear termination proving technique into a larger termination proving framework that depends on linear reasoning.     

约束归纳逻辑程序设计方法的研究

提出了一种新的约束归纳逻辑程序设计方法。该方法能够与自顶向下的归纳逻辑程序设计系统结合,通过在自顶向下归纳方法的一步特殊化操作中引入Fisher判别分析等方法,使得系统能够导出不受变量个数限制的多种形式的线性约束,在不需要用户诱导,不依赖约束求解器的情况下,学习出覆盖正例而排斥负例的含约束的Horn子句程序。