On Local StratifiabUity of Logic Programs and Databases

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

On Local Stratifiability of Logic Prograns and Databases

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

Verifying local stratifiability of logic programs and databases II

We continue investigating ways of verifying local stratifiability of logic programs and databases. In a previous paper, we established a necessary and sufficient condition for local stratifiability of logic programs and databases and proposed an interactive procedure for performing the verification. In this paper, we extend our earlier work. We present a characterization of an infinite extending path and develop a non-interactive procedure for testing for local stratifiability of logic programs and databases. Although the unerlying problem is undecidable in general, our method proves to be powerful to treat a majority of logic programs and databases.     

Aggregation and negation-as-failure

Set-grouping and aggregation are powerful operations of practical interest in database query languages. An aggregate operation is a function that maps a set to some value, e.g., the maximum or minimum in the set, the cardinality of this set, the summation of all its members, etc. Since aggregate operations are typically non-monotonic in nature, recursive programs making use of aggregate operations must be suitably restricted in order that they have a well-defined meaning. In a recent paper we showed that partial-order clauses provide a well-structured means of formulating aggregate operations with recursion. In this paper, we consider the problem of expressing partial-order programs via negation-as-failure (NF), a well-known non-monotonic operation in logic programming. We show a natural translation of partial-order programs to normal logic programs: Anycost-monotonic partial-order programsP is translated to astratified normal program such that the declarative semantics ofP is defined as the stratified semantics of the translated program. The ability to effect such a translation is significant because the resulting normal programs do not make any explicit use of theaggregation capability, yet they are concise and intuitive. The success of this translation is due to the fact that the translated program is a stratified normal program. That would not be the case for other more general classes of programs thancost-monotonic partial-order programs. We therefore develop in stages a refined translation scheme that does not require the translated programs to be stratified, but requires the use of a suitable semantics. The class of normal programs originating from this refined translation scheme is itself interesting: Every program in this class has a clear intended total model, although these programs are in general neither stratified nor call-consistent, and do not have a stable model. The partial model given by the well-founded semantics is consistent with the intended total model and the extended well founded semantics,WFS ⁺, defines the intended model. Since there is a well-defined and efficient operational semantics for partial-order programs^{14, 15, 21)} we conclude that the gap between expression of a problem and computing its solution can be reduced with the right level of notation. Mauricio J. Osorio G., Ph.D.: He is an Associate Professor in the Department of Computer Systems Engineering, University of the Americas, Puebla, Mexico. He is the Head of the Laboratory of Theoretical Computer Science of the Center of Research (CENTIA), Puebla, Mexico. His research is currently funded by CENTIA and CONACYT (Ref. #C065-E9605). He is interested in Applications of Logic to Computer Science, with special emphasis on Logic Programming. He received his B.Sc. in Computer Science from the Universidad Autonoma de Puebla, his M.Sc. in Electrical Engineering from CINVESTAV in Mexico, and his Ph.D. from the State University of New York at Buffalo in 1995. Bharat Jayaraman, Ph.D.: He is an Associate Professor in the Department of Computer Science at the State University of New York at Buffalo. He obtained his bachelors degree in Electronics from the Indian Institute of Technology, Madras in 1975, and his Ph.D. from the University of Utah in 1981. His research interests are in Programming Languages and Declarative Modeling of Complex Systems. He has published over 50 research papers. He has served on the program committees of several conferences in the area of Programming Languages, and he is presently on the Editorial Board of the Journal of Functional and Logic Programming.     

Temporal disjunctive logic programming

In this paper we introduce the logic programming languageDisjunctive Chronolog which combines the programming paradigms of temporal and disjunctive logic programming. Disjunctive Chronolog is capable of expressing dynamic behaviour as well as uncertainty, two notions that are very common in a variety of real systems. We present the minimal temporal model semantics and the fixpoint semantics for the new programming language and demonstrate their equivalence. We also show how proof procedures developed for disjunctive logic programs can be easily extended to apply to Disjunctive Chronolog programs. Manolis Gergatsoulis, Ph.D.: He received his B.Sc. in Physics in 1983, the M.Sc. and the Ph.D. degrees in Computer Science in 1986 and 1995 respectively all from the University of Athens, Greece. Since 1996 he is a Research Associate in the Institute of Informatics and Telecommunications, NCSR ‘Demokritos’, Athens. His research interests include logic and temporal programming, program transformations and synthesis, as well as theory of programming languages. Panagiotis Rondogiannis, Ph.D.: He received his B.Sc. from the Department of Computer Engineering and Informatics, University of Patras, Greece, in 1989, and his M.Sc. and Ph.D. from the Department of Computer Science, University of Victoria, Canada, in 1991 and 1994 respectively. From 1995 to 1996 he served in the Greek army. From 1996 to 1997 he was a visiting professor in the Department of Computer Science, University of Ioannina, Greece, and since 1997 he is a Lecturer in the same Department. In January 2000 he was elected Assistant Professor in the Department of Informatics at the University of Athens. His research interests include functional, logic and temporal programming, as well as theory of programming languages. Themis Panayiotopoulos, Ph.D.: He received his Diploma on Electrical Engineering from the Department of Electrical Engineering, National Technical Univesity of Athens, in 1984, and his Ph.D. on Artificial Intelligence from the above mentioned department in 1989. From 1991 to 1994 he was a visiting professor at the Department of Mathematics, University of the Aegean, Samos, Greece and a Research Associate at the Institute of Informatics and Telecommunications of “Democritos” National Research Center. Since 1995 he is an Assistant Prof. at the Department of Computer Science, University of Piraeus. His research interests include temporal programming, logic programming, expert systems and intelligent agent architectures.     

FC-normal and extended stratified logic program

This paper investigates the consistency property of FC-normal logic program and presents an equivalent deciding condition whether a logic program P is an FC-normal program. The deciding condition describes the characterizations of FC-normal program. By the Petri-net presentation of a logic program, the characterizations of stratification of FC-normal program are investigated. The stratification of FC-normal program motivates us to introduce a new kind of stratification, extended stratification, over logic program. It is shown that an extended (locally) stratified logic program is an FC-normal program. Thus, an extended (locally) stratified logic program has at least one stable model. Finally, we have presented algorithms about computation of consistency property and a few equivalent deciding methods of the finite FC-normal program.     

Foundations of declarative testing in arbitrary logic programming

Declarative testing is very important in logic program developments, as without testing no one can guarantee that every program is definitely correct, no matter how elegant and high-level the programming languages used. Unfortunately, the activity of declarative testing for logic programs (or even the ordinary testing for conventional programs) has received little attention. There is little formal theory of testing, and attempts to develop a methodology of testing are rare. In this paper, we provide a theoretical foundation for declarative testing in arbitrary first order logic programming using recursion theories. In particular, we present a theoretical analysis of three kinds of declarative testing method: I/O testing, I/Y testing, and X/Y testing for logic programs.     

The expressiveness of locally stratified programs

This paper completes an investigation of the logical expressibility of finite, locally stratified, general logic programs. We show that every hyperarithmetic set can be defined by a suitably chosen locally stratified logic program (as a set of values of a predicate over its perfect model). This is an optimal result, since the perfect model of a locally stratified program is itself an implicitly definable hyperarithmetic set (under a recursive coding of the Herbrand base); hence, to obtain all hyperarithmetic sets requires something new, in this case selecting one predicate from the model. We find that the expressive power of programs does not increase when one considers the programs which have a unique stable model or a total well-founded model. This shows that all these classes of structures (perfect models of logically stratified logic programs, well-founded models which turn out to be total, and stable models of programs possessing a unique stable model) are all closely connected with Kleene's hyperarithmetical hierarchy. Thus, for general logic programming, negation with respect to two-valued logic is related to the hyperarithmetic hierarchy in the same way as Horn logic is to the class of recursively enumerable sets. In particular, a set is definable in the well-founded semantics by a programP whose well-founded partial model is total iff it is hyperarithmetic.Research partially supported by the U.S. Army Research Office through the Mathematical Sciences Institute of Cornell University.Research partially supported by NSF Grant IRI-9012902 and partially supported by the U.S. Army Research Office through the Mathematical Sciences Institute of Cornell University.Research partially supported by NSF Grant IRI-8905166 and partially supported by the U.S. Army Research Office through the Mathematical Sciences Institute of Cornell University.     

<Emphasis Type="Italic">FC</Emphasis>-normal and extended stratified logic program

This paper investigates the consistency property ofFC-normal logic program and presents an equivalent deciding condition whether a logic programP is anFC-normal program. The deciding condition describes the characterizations ofFC-normal program. By the Petri-net presentation of a logic program, the characterizations of stratification ofFC-normal program are investigated. The stratification ofFC-normal program motivates us to introduce a new kind of stratification, extended stratification, over logic program. It is shown that an extended (locally) stratified logic program is anFC-normal program. Thus, an extended (locally) stratified logic program has at least one stable model. Finally, we have presented algorithms about computation of consistency property and a few equivalent deciding methods of the finiteFC-normal program.     

Linear logic for deductive databases

This paper deals with deductive databases in linear logic. The semantics of queries, views, constraints, and (view) updates are defineddeclaratively in linear logic. In constrast to classical logic, we can formalise non-shared view, transition constraints, and (view) updates easily. Various proof search strategies are presented along with an algorithm for query evaluation from a bottom-up direction. An additional advantage is that the associated meaning of a given relation can be defined in terms of the validity of a legal update in a given relation. We also defined formally the update principles and showed the correctness of the update translation algorithms. In this approach, we provide virtual view updates along with real view updates, and view DELETIONs are special cases of view REPLACEMENTs. This permits three transactional view update operations (INSERTION, DELETION, REPLACEMENT) in comparison to only (INSERTION, DELETION) in most existing systems. Dong-Tsan Lee, Ph.D.: He is a computer scientist in the Department of Computer Science at University of Western Australia, Perth, Western Australia, Australia. He received the B.S. and M.S. degrees from the Department of Computer Science at National Chiao-Tung University, Taiwan, in 1983 and 1985, respectively, and earned the Ph.D. degree from the Department of Computer Science at University of Western Australia. His research interests include database and artificial intelligence, linear logic, and real-time software engineering. Chin-Ping Tsang, Ph.D.: He is currently an associate professor in the Department of Computer Science at University of Western Australia, Perth, Western Australia, Australia. He received the Ph.D. degree from the University of Western Australia. He was the head of the Department of Computer Science at the University of Western Australia from 1994 to 1997. His research interests include artificial intelligence, non-classicial logic and neural nets.     

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.     

A Prolog simulator for deterministic P systems with active membranes

In this paper we propose a new way to represent P systems with active membranes based on Logic Programming techniques. This representation allows us to express the set of rules and the configuration of the P system in each step of the evolution as literals of an appropriate language of first order logic. We provide a Prolog program to simulate, the evolution of these P systems and present some auxiliary tools to simulate the evolution of a P system with active membranes using 2-division which solves the SAT problem following the techniques presented in Reference.¹⁰ Andrés Cordón-Franco: He is a member of the Department of Computer Science and Artificial Intelligence at the University of Sevilla (Spain). He is also a member of the research group on Natural Computing of the University of Seville. His research interest includes Mathematical Logic, Logic in Computer Science, and Membrane Computing, both from a theoretical and from a practical (software implementation) point of view. Miguel A. Gutiérrez-Naranjo: He is an assistant professor in the Computer Science and Artificial Intelligence Department at University of Sevilla, Spain. He is also a member of the Research Group on Natural Computing of the University of Seville. His research interest includes Machine Learning, Logic Programming and Membrane Computing, both from a theoretical and a practical point of view. Mario J. Pérez-Jiménez, Ph.D.: He is professor of Department of Computer Science and Artificial Intelligence at University of Seville, where he is the head of the Group of Research on Natural Computing, He has published 8 books of Mathematics and Computation, and more than 90 scientific articles in prestigious scientific journals. He is member of European Molecular Computing Consortium. Fernando Sancho-Caparrini: He is a member of the Department of Computer Science and Artificial Intelligence at the University of Sevilla (Spain). He is also a member of the research group on Natural Computing of the University of Seville. His research interest includes Complex Systems, DNA Computing, Logic in Computer Science, and Membrane Computing, both from a theoretical and from a practical point of view.     

On the completeness of naive memoing in Prolog

Memoing is often used in logic programming to avoid redundant evaluation of similar goals, often on programs that are inherently recursive in nature. The interaction between memoing and recursion, however, is quite complex. There are several top-down evaluation strategies for logic programs that utilize memoing to achieve completeness in the presence of recursion. This paper’s focus, however, is on the use ofnaive memoing in Prolog. Using memoingnaively in conjunction with recursion in Prolog may not produce expected results. For example, adding naive memoing to Prolog’s evaluation of a right-recursive transitive closure may be incomplete, whereas adding naive memoing to Prolog’s evaluation of a left-recursive transitive closure may be terminating and complete. This paper examines the completeness of naive memoing in linear-recursive, function-free logic programs evaluated with Prolog’s top-down evaluation strategy. In addition, we assume that the program is definite and safe, having finite base relations and exactly one recursive predicate. The goal of the paper is a theoretical study of the completeness of naive memoing and recursion in Prolog, illustrating the limitations imposed even for this simplified class of programs. The naive memoing approach utilized for this study is based on extension tables, which provide a memo mechanism with immediate update view semantics for Prolog programs, through a source transformation known as ET. We introduce the concept ofET-complete, which refers to the completeness of the evaluation of a query over a Prolog program that memos selected predicates through the ET transformation. We show that left-linear recursions defined by a single recursive rule are ET-complete. We generalize the class of left-linear recursions that are ET-complete by introducing pseudo-left-linear recursions, which are also defined by a single linear recursive rule. To add left-linear recursions defined bymultiple linear recursive rules to the class of ET-complete recursions, we present a left-factoring algorithm that converts left-linear recursions defined by multiple recusive rules into pseudo-left-linear recursions defined by a single recursive rule. Based on these results, the paper concludes by identifying research directions for expanding the class of Prolog programs to be examined in future work. This work was partially supported by the National Science Foundation under Grant CCR-9008737. Suzanne Wagner Dietrich, Ph.D.: She is an Associate Professor in the Department of Computer Science and Engineering at Arizona State University. Her research emphasis is on the evaluation of declarative logic programs especially in the context of deductive databases, including materialized view maintenance and condition monitoring in active deductive databases. More recently, her research interests include the integration of active, object-oriented and deductive databases as well as the application of this emerging database technology to various disciplines such as software engineering. She received the B. S. degree in computer science in 1983 from the State University of New York at Stony Brook, and as the recipient of an Office of Naval Research Graduate Fellowship, earned her Ph.D. degree in computer science at Stony Brook in 1987. Changguan Fan, M.S.: He is a Ph.D. candidate in the Department of Computer Science and Engineering at Arizona State University and a software engineer at the Regenisys Corporation in Scottsdale, AZ. His research interests include the evaluation of logic programs, deductive database systems and database management systems. He received his B.S. in Computer Science from the Shanghai Institute of Railway Technology, Shanghai, China in 1982 and his M.S. in the Department of Computer Science and Engineering at Arizona State University in 1989.     

Complexity and undecidability results for logic programming

This paper surveys complexity, degree of uncomputability, and expressive power results for logic programming. Some major decision problem complexity results and other results for logic programming are also covered. It also proves several new results filling in previous gaps in the literature. The paper considers seven logic programming semantics: the van Emden-Kowalski semantics for definite (Horn) logic programs; the perfect model semantics for stratified and for locally stratified logic programs; and the two- and three-valued program completion semantics, the well-founded semantics, and the stable semantics, all for normal logic programs, under skeptical inference. The main results concern expressibility and query complexity/uncomputability in five contexts: for propositional logic programs, for first order logic programs with infinite Herbrand universes on their Herbrand universes (a closed domain assumption), for first order logic programs with infinite Herbrand universes on those universes extended with infinitely many new elements (an open domain assumption), and for logic programs without function or constant symbols evaluated over varying extensional databases (DATALOG-type results, data complexity results only) under both closed and open domain assumptions. Several of the open domain assumption results are new to this paper. Other results surveyed are (1) results about the family of all stable models of a program and (2) decision questions about when a logic program has nice properties with respect to a semantics (e.g., a unique stable model). One decision result, for well-founded semantics, is new to this paper.Work supported in part by NSF grant IRI-8905166.     

Stable semantics for disjunctive programs

We introduce the stable model semantics fordisjunctive logic programs and deductive databases, which generalizes the stable model semantics, defined earlier for normal (i.e., non-disjunctive) programs. Depending on whether only total (2-valued) or all partial (3-valued) models are used we obtain thedisjunctive stable semantics or thepartial disjunctive stable semantics, respectively. The proposed semantics are shown to have the following properties:

? For normal programs, the disjunctive (respectively, partial disjunctive) stable semantics coincides with thestable (respectively,partial stable) semantics.

? For normal programs, the partial disjunctive stable semantics also coincides with thewell-founded semantics.

? For locally stratified disjunctive programs both (total and partial) disjunctive stable semantics coincide with theperfect model semantics.

? The partial disjunctive stable semantics can be generalized to the class ofall disjunctive logic programs.

? Both (total and partial) disjunctive stable semantics can be naturally extended to a broader class of disjunctive programs that permit the use ofclassical negation.

? After translation of the programP into a suitable autoepistemic theory \( \hat P \) the disjunctive (respectively, partial disjunctive) stable semantics ofP coincides with the autoepistemic (respectively, 3-valued autoepistemic) semantics of \( \hat P \) .

     

A program specialiser for meta-level compositions of logic programs

Metal-level compositions of object logic programs are naturally implemented by means of meta-programming techniques. Metainterpreters defining program compositions however suffer from a computational overhead that is due partly to the interpretation layer present in all meta-programs, and partly to the specific interpretation layer needed to deal with program compositions. We show that meta-interpreters implementing compositions of object programs can be fruitfully specialised w.r.t. meta-level queries of the form Demo (E, G), where E denotes a program expression and G denotes a (partially instantiated) object level query. More precisely, we describe the design and implementation of declarative program specialiser that suitably transforms such meta-interpreters so as to sensibly reduce — if not to completely remove — the overhead due to the handling of program compositions. In many cases the specialiser succeeds in eliminating also the overhead due to meta-interpretation. Antonio Brogi, Ph.D.: He is currently assistant professor in the Department of Computer Science at the University of Pisa, Italy. He received his Laurea Degree in Computer Science (1987) and his Ph. D. in Computer Science (1993) from the University of Pisa. His research interests include programming language design and semantics, logic programming, deductive databases, and software coordination. Simone Contiero: He is currently a Ph. D. student at the Department of Computer Science, University of Pisa (Italy). He received his Laurea Degree in Computer Science from the University of Pisa in 1994. His research interests are in high-level programming languages, metaprogramming and logic-based coordination of software.     

Discovering rules to design newspapers: An inductive constraint logic programming approach

Inductive logic programming combines both machine learning and logic programming techniques. ILP uses first-order predicate logic restricted to Horn clauses as an underlying language. Thus, programs induced by an ILP system inherit the classical limitations of PROLOG programs. Constraint logic programming avoids some of the limitations of logic programming, and so ILP aims to induce programs that employ this paradigm. Current ILP systems that induce constrained logic programs extend systems based on the normal semantics ofILP. In this article we introduce IC-Log, a new system that induces constrained logic programs and relies on an extension ofa nonmonotonic semantics-based system. We then present an application of IC-Log in the field ofcomputer-aided publishing.     

Why untyped nonground metaprogramming is not (much of) a problem

We study a semantics for untyped, vanilla metaprograms, using the nonground representation for object level variables. We introduce the notion of language independence, which generalizes range restriction. We show that the vanilla metaprogram associated with a stratified normal object program is weakly stratified. For language independent, stratified normal object programs, we prove that there is a natural one-to-one correspondence between atoms p(t₁,…,t_r) in the perfect Herbrand model of the object program and solve(p(t₁,…,t_r)) atoms in the weakly perfect Herb and model of the associated vanilla metaprogram. Thus, for this class of programs, the weakly perfect Herbrand model provides a sensible semantics for the metaprogram. We show that this result generalizes to nonlanguage independent programs in the context of an extended Herbrand semantics, designed to closely mirror the operational behavior of logic programs. Moreover, we also consider a number of interesting extensions and/or variants of the basic vanilla metainterpreter. For instance, we demonstrate how our approach provides a sensible semantics for a limited form of amalgamation.