Logic Programming

Type-safe, high-level languages such as Java ensure that a wide class of failures, including buffer overruns and format string attacks, simply cannot happen. Unfortunately, our computing infrastructure is built with type-unsafe low-level languages such as C, and it is economically impossible to throw away our existing operating systems, databases, routers, etc. and re-code them all in Java.Fortunately, a number of recent advances in static analysis, language design, compilation, and run-time systems have given us a set of tools for achieving type safety for legacy C code. In this talk, I will survey some of the progress that has been made in the last few years, and focus on the issues that remain if we are to achieve type safety, and more generally, security for our computing infrastructure.

Logic Information Systems (lis) use logic in a uniform way to describe their contents, to query it, to navigate through it, to analyze it, and to update it. They can be given an abstract specification that does not depend on the choice of a particular logic, and concrete instances can be obtained by instantiating this specification with a particular logic. In fact, a logic plays in a lis the role of a schema in data-bases. We present the principles of lis, and a system-level implementation. We compare with the use of logic in Logic Programming, in particular through the notions of intention and extension.

An approach to authorization that is based on attributes of the resource requester provides flexibility and scalability that is essential in the context of large distributed systems. Logic programming provides an elegant, expressive, and well-understood framework in which to work with attribute-based authorization policy. We summarize one specific attribute-based authorization framework built on logic programming: RT, a family of Role-based Trust-management languages. RT’s logic programming foundation has facilitated the conception and specification of several extensions that greatly enhance its expressivity with respect to important security concepts such as parameterized roles, thresholds, and separation of duties. After examining language design issues, we consider the problem of assessing authorization policies with respect to vulnerability of resource owners to a variety of security risks due to delegations to other principals, risks such as undesired authorizations and unavailability of critical resources. We summarize analysis techniques for assessing such vulnerabilities.

The verification of infinite state systems is one of the most challenging areas in the field of computer aided verification. In fact these systems arise naturally in many application fields, ranging from communication protocols to multi-threaded programs and time-dependent systems, and are quite difficult to analyze and to reason about.The main approaches developed so far consist in the extension to the infinite case of techniques already developed for finite state systems, notably model checking suitably integrated with abstractions which allow to finitely represent infinite sets of states. Constraints have also been quite useful in representing and manipulating infinite sets of states, both directly and indirectly.Particularly relevant in this context is the issue of compositionality: In fact, a compositional methodology could allow to reduce the complexity of the verification procedure by splitting a big system into smaller pieces. Moreover, when considering systems such as those arising in distributed and mobile computing, compositional verification is imperative in some cases, as the environment in which software agents operate cannot be fixed in advance.In this talk we will first illustrate some techniques based on constraints and multi set rewriting (MSR) for the automatic verification of systems and protocols parametric in several directions. Then we will discuss some ongoing research aiming at developing a compositional model for reasoning on MSR specifications.

Lattice Protein Models are used for hierarchical approaches to protein structure prediction, as well as for investigating general principles of protein folding. So far, one has the problem that either the lattice does not model real protein conformations with good quality, or there is no efficient method known for finding native conformations.We present a constraint-based method that largely improves this situation. It outperforms all existing approaches in lattice protein folding on the type of model we have chosen (namely the HP-Model by Lau and Dill [34], which models the important aspect of hydrophobicity). It is the only exact method that has been applied to two different lattices. Furthermore, It is the only exact method for the face-centered cubic lattice. This lattice is important since it has been shown [38] that the FCC lattice can model real protein conformations with coordinate root mean square deviation below 2 Å.Our method uses a constraint-based approach. It works by first calculating maximally compact sets of points (hydrophobic cores), and then threading the given HP-sequence to the hydrophobic cores such that the core is occupied by H-monomers.

Concurrent constraint programming (ccp) is a model of concurrency for systems in which agents (also called processes) interact with one another by telling and asking information in a shared medium. Timed (or temporal) ccp extends ccp by allowing agents to be constrained by time requirements. The novelty of timed ccp is that it combines in one framework an operational and algebraic view based upon process calculi with a declarative view based upon temporal logic. This allows the model to benefit from two well-established theories used in the study of concurrency.This essay offers an overview of timed ccp covering its basic background and central developments. The essay also includes an introduction to a temporal ccp formalism called the ntcc calculus.

In recent years, molecular biology has engaged in a large-scale effort to elucidate high-level cellular processes in terms of their biochemical basis at the molecular level. The mass production of post genomic data, such as ARN expression, protein production and protein-protein interaction, raises the need of a strong parallel effort on the formal representation of biological processes.

Component-based Software Development (CBD) represents a paradigm shift in software development. In the tutorial I will explain what CBD is about, briefly survey current component technology, and posit that Logic Programming can play a role in next-generation CBD. In this abstract, I give an overview of the material that I plan to cover in the tutorial.

Abstract logic programming is about designing logic programming languages via the proof theoretic notion of uniform provability. It allows the design of purely logical, very expressive logic programming languages, endowed with a rich meta theory. This tutorial intends to expose the main ideas of this discipline in the most direct and simple way.

The current proposals for the inclusion of modules in the ISO Prolog standard are not very consensual. Since a program-structuring feature is required for a production programming language, several alternatives have been explored over the years.In this article we recall and expand on the concepts of Contextual Logic Programming, a powerful and simple mechanism which addresses the general issue of modularity in Logic Programs. We claim that unit arguments are an essential addition to this programming model, illustrate the claim with examples and draw parallels with Object-Oriented programming. We argue that Contextual Logic Programming is an interesting and effective tool for the development of large-scale programs built upon the Contextual Logic Programming paradigm and argue that contexts with arguments actually provide a powerful, expressive and very convenient means of structuring large applications upon a Prolog basis. We substantiate our claims with examples taken mostly from a “real world” application, Universidade de Évora’s Academic Information System, which is currently being developed using the prototype implementation described in this article.We sketch the most relevant aspects of a new implementation of Contextual Logic Programming, GNU Prolog/CX, focusing on the impact on performance of the features which were added to a regular Prolog system, highlighting the low overhead which is incurred in case these extensions are not used.Categories:. D.2.2–Modules and interfaces, D.1.6–Logic Programming, D.1.5–Object-oriented Programming.General Terms:. Contextual Logic Programming.

We present a method that deals effectively with existential derived predicates during view updating. Existing methods either consider all instantiations of a given existential variable or request the instantiation directly to the user. Clearly, these approaches are not appropriate since either they are not practical or rely on the user’s best guess to assign the most appropriate values. On the contrary, our proposal considers only patterns of the variable instantiations that are relevant to the view update request, rather than taking into account all possible instantiations.

Many data integration systems provide transparent access to heterogeneous data sources through a unified view of all data in terms of a global schema, which may be equipped with integrity constraints on the data. Since these constraints might be violated by the data retrieved from the sources, methods for handling such a situation are needed. To this end, recent approaches model query answering in data integration systems in terms of nonmonotonic logic programs. However, while the theoretical aspects have been deeply analyzed, there are no real implementations of this approach yet. A problem is that the reasoning tasks modeling query answering are computationally expensive in general, and that a direct evaluation on deductive database systems is infeasible for large data sets. In this paper, we investigate techniques which make user query answering by logic programs effective. We develop pruning and localization methods for the data which need to be processed in a deductive system, and a technique for the recombination of the results on a relational database engine. Experiments indicate the viability of our methods and encourage further research of this approach.

We introduce a proposal to give argumentation capacity to databases. A database is said to have argumentation capacity if it can extract from the information available to it a set of interacting arguments for and against claims and to determine the overall status of some information given all the interactions among all the arguments. We represent conflicts among arguments using a construct called a contestation, which permits us to represent various degrees of conflicts among statements. Argumentation databases as proposed here give exactly the same answers to queries as a database without argumentation capacity, but which are annotated with confidence values reflecting the degree of confidence one should have in the answer, where the degree of confidence is determined by the overall effect of all the interactions among the arguments.

We equip ordered logic programs with negation as failure, using a simple generalization of the preferred answer set semantics for ordered programs. This extension supports a convenient formulation of certain problems, which is illustrated by means of an intuitive simulation of logic programming with ordered disjunction. The simulation also supports a broader application of “ordered disjunction”, handling problems that would be cumbersome to express using ordered disjunction logic programs.Interestingly, allowing negation as failure in ordered logic programs does not yield any extra computational power: the combination of negation as failure and order can be simulated using order (and true negation) alone.

We propose and study algorithms for computing minimal models, stable models and answer sets of 2- and 3-CNF theories, and normal and disjunctive 2- and 3-programs. We are especially interested in algorithms with non-trivial worst-case performance bounds. We show that one can find all minimal models of 2-CNF theories and all answer sets of disjunctive 2-programs in time O(m 1.4422..n) (n is the number of atoms in an input theory or program and m is its size). Our main results concern computing stable models of normal 3-programs, minimal models of 3-CNF theories and answer sets of disjunctive 3-programs. We design algorithms that run in time O(m1.6701..n), in the case of the first problem, and in time O(mn22.2720..n), in the case of the latter two. All these bounds improve by exponential factors the best algorithms known previously. We also obtain closely related upper bounds on the number of minimal models, stable models and answer sets a 2- or 3-theory or program may have.

In recent research on nonmonotonic logic programming, repeatedly strong equivalence of logic programs P and Q has been considered, which holds if the programs P ∪ R and Q∪ R have the same stable models for any other program R. This property strengthens equivalence of P and Q with respect to stable models (which is the particular case for R= ∅), and has an application in program optimization. In this paper, we consider the more liberal notion of uniform equivalence, in which R ranges only over the sets of facts rather than all sets of rules. This notion, which is well-known, is particularly useful for assessing whether programs P and Q are equivalent as components in a logic program which is modularly structured. We provide semantical characterizations of uniform equivalence for disjunctive logic programs and some restricted classes, and analyze the computational cost of uniform equivalence in the propositional (ground) case. Our results, which naturally extend to answer set semantics, complement the results on strong equivalence of logic programs and pave the way for optimizations in answer set solvers as a tool for input-based problem solving.

We study the following problems on some classes of randomly generated logic programs under the answer set semantics: the existence of an answer set and the hardness of finding one answer set, if any.Firstly in logic programs with 3 or more literals in the rules, for the first problem, despite the non-monotonicity of the answer set semantics, we observe a phase transition occurring on some particular critical values of L/N, where L and N are the number of rules and atoms in a program, respectively. More specifically, the probability of having an answer set drops from near 1 to near 0 abruptly and monotonically when the ratio increases from 0 to ∞. For the second problem, we find that for all three of the systems that we have tested: Smodels, DLV, and ASSAT, the problem of finding one answer set becomes much harder when the ratio falls into a certain region. Our experiments also show that a logic program without answer sets is much harder to compute than those with. This suggests that the most effective strategies for improving the performance of ASP systems should be those that can detect the non-existence of answer sets early on. In a class of logic program with 2 or 3 literals in the rules, we observe an interesting non-monotonicity on the probability of existing answer sets, which coincides with the non-monotonicity of the answer set semantics.

In this paper we show how we can use size and groundness analyses lifted to regular and (polymorphic) Hindley/Milner typed programs to determine more accurate termination of (type correct) programs. Type information for programs may be either inferred automatically or declared by the programmer. The analysis of the typed logic programs is able to completely reuse a framework for termination analysis of untyped logic programs by using abstract compilation of the type abstraction. We show that our typed termination analysis is uniformly more accurate than untyped termination analysis for regularly typed programs, and demonstrate how it is able to prove termination of programs which the untyped analysis can not.

Tracers give some insight of program executions: with an execution trace a programmer can debug and tune programs. Traces can also be used by analysis tools, for example to produce statistics or build graphical views of program behaviors. Constraint propagation tracers are especially needed because constraint propagation problems are particularly hard to debug. Yet, there is no satisfactory tracer for CLP(FD) systems. Some do not provide enough information, others are very inefficient. The tracer formally described in this article provides more complete information than existing propagation tracers. Benchmarks show that its implementation is efficient. Its formal specification is useful both to implement the tracer and to understand the produced trace. It is designed to cover many debugging needs.

We propose a parametric introduction of intensionally defined sets into any $CLP(\mathcal \{D\})$ language. The result is a language $CLP({\mathcal \{D\}})$, where constraints over sets of elements of $\mathcal D$ and over sets of sets of elements, and so on, can be expressed. The semantics of $CLP({\mathcal \{D\}})$ is based on the semantics of logic programs with aggregates and the semantics of CLP over sets. We investigate the problem of constraint resolution in $CLP({\mathcal \{D\}})$ and propose algorithms for constraints simplification.

Constraint propagation is a general algorithmic approach for pruning the search space of a constraint satisfaction problem. In a uniform way, K. R. Apt [1] has defined computation as an iteration of reduction functions over a domain. In [2], he has also demonstrated the need for integrating static properties of reduction functions (commutativity and semi-commutativity) to design specialized algorithms such as AC3 and DAC. We introduce here a set of operators for modeling compositions of reduction functions in an iteration framework. Two of the major goals are to tackle parallel computations, and to manage dynamic behaviors such as slow convergences in numerical computations. An object-oriented software architecture is described using the Unified Modeling Language.

One recent development in logic programming has been the application of abstract interpretation to verify the partial correctness of a logic program with respect to a given set of assertions. One approach to verification is to apply forward analysis that starts with an initial goal and traces the execution in the direction of the control-flow to approximate the program state at each program point. This is often enough to verify that the assertions hold. The dual approach is to apply backward analysis to propagate properties of the allowable states against the control-flow to infer queries for which the program will not violate any assertion. This paper is a systematic comparison of these two approaches to verification. The paper reports some equivalence results that relate the relative power of various forward and backward analysis frameworks.

Concurrency is an attractive property of a language to exploit multi-CPU hardware or perform multiple tasks concurrently. In recent years we see Prolog systems experimenting with multiple threads only sharing the database. Such systems are relatively easy to build and remain very close to standard Prolog while providing valuable extra functionality. This article describes the introduction of multiple threads in SWI-Prolog exploiting OS-native threading. We discuss the extra primitives available to the Prolog programmer as well as implementation issues. We explored speedup on multi-processor hardware and speed degradation when executing a single task.

Logic variables pioneered by (concurrent) logic and concurrent constraint programming are powerful mechanisms for automatically synchronizing concurrent computations. They support a declarative model of concurrency that avoids explicitly suspending and resuming computations. This paper presents Flow Java which conservatively extends Java with single assignment variables and futures as variants of logic variables. The extension is conservative with respect to object-orientation, types, parameter passing, and concurrency in Java. Futures support secure concurrent abstractions and are essential for seamless integration of single assignment variables into Java. We show how Flow Java supports the construction of simple and concise concurrent programming abstractions. We present how to moderately extend compilation and the runtime architecture of an existing Java implementation for Flow Java. Evaluation using standard Java benchmarks shows that in most cases the overhead is between 10% and 40%. For some pathological cases the runtime increases by up to 75%.

We present results concerning the computational complexity of the key execution mechanisms required to handle Dependent And-Parallel executions in logic programming. We develop formal abstractions of the problems in terms of dynamic trees, design efficient data structures, and present some lower bound results. This work is part of a larger effort to understand, formalize, and study the complexity-theoretic and algorithmic issues in parallel implementations of logic programming.

We present a higher-order term indexing strategy based on substitution trees. The strategy is based in linear higher-order patterns where computationally expensive parts are delayed. Insertion of terms into the index is based on computing the most specific linear generalization of two linear higher-order patterns. Retrieving terms is based on matching two linear higher-order patterns. This indexing structure is implemented as part of the Twelf system to speed-up the execution of the tabled higher-logic programming interpreter. Experimental results show substantial performance improvements, between 100% and over 800%.

Tabling has emerged as an important evaluation technique in logic programming. Currently, changes to a program (due to addition/deletion of rules/facts) after query evaluation compromise the completeness and soundness of the answers in the tables. This paper presents incremental algorithms for maintaining the freshness of tables upon addition or deletion of facts. Our algorithms improve on existing materialized view maintenance algorithms and can be easily extended to handle changes to rules as well. We describe an implementation of our algorithms in the XSB tabled logic programming system. Preliminary experimental results indicate that our incremental algorithms are efficient. Our implementation represents a first step towards building a practical system for incremental evaluation of tabled logic programs.

Logic programming is based on the idea that computation is controlled inference. The Extended Andorra Model provides a very powerful framework that supports both co-routining and parallelism. In this work we show that David H. D. Warren’s design for the EAM with Implicit Control does not perform well for deterministic computations and we present several optimisations that allow the BEAM to achieve performance matching or even exceeding related systems. Our optimisations refine the original EAM control rule demonstrate that overheads can be reduced through combined execution rules, and show that a good design and emulator implementation is relevant, even for a complex system such as the BEAM.

The ntcc process calculus is a timed concurrent constraint programming (ccp) model equipped with a first-order linear-temporal logic (LTL) for expressing process specifications. A typical behavioral observation in ccp is the strongest postcondition (sp). The ntcc sp denotes the set of all infinite output sequences that a given process can exhibit. The verification problem is then whether the sequences in the sp of a given process satisfy a given ntcc LTL formula.This paper presents new positive decidability results for timed ccp as well as for LTL. In particular, we shall prove that the following problems are decidable: (1) The sp equivalence for the so-called locally-independentntcc fragment; unlike other fragments for which similar results have been published, this fragment can specify infinite-state systems. (2) Verification for locally-independent processes and negation-free first-order formulae of the ntcc LTL. (3) Implication for such formulae. (4) Satisfiability for a first-order fragment of Manna and Pnueli’s LTL. The purpose of the last result is to illustrate the applicability of ccp to well-established formalisms for concurrency.

Apt [1] has proposed a denotational semantics for first-order logic with equality, which is an instance of the computation as deduction paradigm: given a language $\mathcal L$ together with an interpretation $\mathcal I$ and a formula φ in $\mathcal L$, the semantics consists of a (possibly empty) set of substitutions θ such that φθ is true in $\mathcal I$, or it may contain error to indicate that there might be further such substitutions, but that they could not be computed. The definition of the semantics is generic in that it assumes no knowledge about $\mathcal I$ except that a ground term can effectively be evaluated. We propose here an improvement of this semantics, using an algorithm based on syntactic unification. Although one can argue for the optimality of this semantics informally, it is not optimal in any formal sense, since there seems to be no satisfactory formalisation of what it means to have “no knowledge about $\mathcal I$ except that a ground term can effectively be evaluated”. It is always possible to “improve” a semantics in a formal sense, but such semantics become more and more contrived.

We extend Clark’s definition of a completed program and the definition of a loop formula due to Lin and Zhao to disjunctive logic programs. Our main result, generalizing the Lin/Zhao theorem, shows that answer sets for a disjunctive program can be characterized as the models of its completion that satisfy the loop formulas. The concept of a tight program and Fages’ theorem are extended to disjunctive programs as well.

Many frameworks have been proposed to manage uncertain information in logic programming. Essentially, they differ in the underlying notion of uncertainty and how these uncertainty values, associated to rules and facts, are managed. The goal of this paper is to allow the reasoning with non-uniform default assumptions, i.e. with any arbitrary assignment of default values to the atoms. Informally, rather than to rely on the same default certainty value for all atoms, we allow arbitrary assignments to complete information. To this end, we define both epistemologically and computationally the semantics according to any given assumption. For reasons of generality, we present our work in the framework presented in [17] as a unifying umbrella for many of the proposed approaches to the management of uncertainty in logic programming. Our extension is conservative in the following sense: (i) if we restrict our attention to the usual uniform Open World Assumption, then the semantics reduces to the Kripke-Kleene semantics, and (ii) if we restrict our attention to the uniform Closed World Assumption, then our semantics reduces to the well-founded semantics.

Mutable state is traditionally implemented in Prolog and other (C)LP systems by performing dynamic modifications to predicate definitions at runtime, i.e. to dynamic predicates of the internal database. Dynamic facts are often used to store information accessible per module or globally and which can be preserved through backtracking. These database updates, despite the obvious drawback of their non-declarative nature, have practical applications and they are given a practical semantics by the so-called logical view of (internal) database updates.

The work described here is motivated by our interest in the methodology of answer set programming (ASP). The idea of ASP is to solve a problem by writing a logic program the answer sets of which correspond to solutions.

A tabled logic programming (TLP) system can be thought of as an engine for efficiently computing fixed points. In a TLP system, a global data structure table is introduced to memorize the answers of any subgoals to tabled predicates, whose purpose is to never do the same computation twice. Consider the tabled predicate reach/2 defined as follows for the reachability relation. Given a query reach(a,X), a TLP system returns answers X=b, X=c and X=a, albeit the predicate is defined left-recursively.

In studying the semantic web, the main area is to build web ontologies and create the relationships between concepts. Until now, the capabilities of markup languages for expressing the relationships have improved a great deal but it is insufficient for representing the temporal relationships. In this paper, we define the new axioms for representing the temporal relationships.

The framework of learning from entailment introduced by Angluin (1988) and Frazier and Pitt (1993) allows the following types of queries. Through an entailment equivalence queryEQUIV(H), the learner asks the teacher whether his theory (a set of first-order formulas) H is logically equivalent to the target theory H* or not. The teacher answers ‘yes’ to this query if H and H* are equivalent, i.e., H⊧H* and H*⊧H. Otherwise, the teacher produces a formula C such that H*⊧C but $H \nvDash C$ or $H^* \nvDash C$ but H⊧C. The request-for-hint query REQ(C) returns (1) an answer ‘not-entailed’ if $H^* \nvDash C$, or (2) an answer ‘subsumed’ if C is subsumed by a formula in H*, or (3) a formula (hint) B in the proof of H*⊧C if C is not subsumed by any formula in H* but H*⊧C.

This paper presents an intelligent method for corpus-based word sense disambiguation (WSD), which utilizes the integrated noun and verb semantic networks through the selectional restriction relations in sentences. Experiments show that the presented intelligent method performs the verb translation better than the concept-based method and the statistics-based method. Integration of noun semantic networks into verb semantic networks will play an important role in both computational linguistic applications and psycholinguistic models of language processing.

One of the most interesting and promising approaches to programming Internet agents is logic programming of agents. This approach has good prospects, because the ideology and principles of logic programming are very convenient for searching, recognition, and analysis of unstructured, poorly structured, and hypertext information. Many ideas and methods of logic programming of Internet agents based on various modifications of Prolog and non-classical logic (linear, modal, etc.) were developed during the recent decade. Nevertheless, there has been no mathematical apparatus providing sound and complete operation of logic programs in the dynamic Internet environment (i.e., under conditions of permanent update and revision of information). To solve this problem, we have created a mathematical apparatus based on the principle of repeated proving of sub-goals (so-called logical actors).

Logic Programming has been advocated as a language for system specification, especially for logical behaviours, rules and knowledge. However, modeling problems involving negation, which is quite natural in many cases, is somewhat restricted if Prolog is used as the specification/implementation language. These constraints are not related to theory viewpoint, where users can find many different models with their respective semantics; they concern practical implementation issues. The negation capabilities supported by current Prolog systems are rather limited, and a correct and complete implementation there is not available. Of all the proposals, constructive negation [1,2] is probably the most promising because it has been proven to be sound and complete [4], and its semantics is fully compatible with Prolog’s.

We describe a model for managing time-oriented security system and methods to perform simulation on this systems like forward and backward-chaining. Ad hoc solutions may be obtained but often fail to address various issues. Or method in pratice, provides a new trend for design and verify a security system, to ensure themselves of maintain integrite walls of compartments and to ensure of the correct operation of those, while verifiant that the good configuration of the syteme allows resiter well to predefined temperatures.

Justification is the process of computing an evidence for the truth or falsity of an answer to a query in a logic program. There are two well known approaches for computing the evidence: Post-processing based techniques that use tabling engine [3,1] and trace-based techniques such as 4-port debuggers.

Previous research in learning sets of rules in a musical context has included a broad spectrum of music domains. Widmer [8] has focused on the task of discovering general rules of expressive classical piano performance from real performance data via inductive machine learning. The performance data used for the study are MIDI recordings of 13 piano sonatas by W.A. Mozart performed by a skilled pianist. In addition to these data, the music score was also coded. When trained on the data the inductive rule learning algorithm discovered a small set of 17 quite simple classification rules [8] that predict a large number of the note-level choices of the pianist.

Tamaki and Sato were perhaps among the first to study folding in logic programs. These authors considered the folding of a single clause (E) using a single-clause definition (D) to give a folded clause (F):$\frac{B \leftarrow Q (D) A \leftarrow Q\Theta, R (E)}{A \leftarrow B\Theta, R(F)}$foldplus some syntactic conditions, later refined by Gardner and Shepherdson. Here and throughout, A and B denote atoms, and Q and R denote tuples of literals.

Termination is well-known to be one of the most intriguing aspects of program verification. Since logic programs are Turing-complete, it follows by the undecidability of the halting problem that there exists no algorithm which, given an arbitrary logic program, decides whether the program terminates. However, one can propose both conditions that are equivalent to termination and their approximations that imply termination and can be verified automatically. This paper briefly discusses these kinds of conditions that were studied in [2].

Program changes take up a substantial part of the entire programming effort. Often a preliminary step of improving the design without altering the external behaviour can be recommended. This is the idea behind refactoring, a source-to-source program transformation that recently came to prominence in the OO-community [1]. Unlike the existing results on automated program transformation, refactoring does not aim at transforming the program entirely automatically. The decision on whether the transformation should be applied and how it should be done is left to the program developer. However, providing automated support for refactoring is useful and an important challenge.

The standard selection rule in logic programming always selects the leftmost atom in each query. But for some applications this rule is not adequate, and dynamic scheduling, i.e. a mechanism to determine the selected atom at runtime, is needed. The complex (non-)termination behaviour related to dynamic scheduling has first been observed by Naish [3].

Planning—in its classical sense—is the problem of finding a sequence of actions that achieves a predefined goal. As such, much of the research in AI planning has been focused on methodologies and issues related to the development of efficient planners. To date, several efficient planning systems have been developed (e.g., see [3] for a summary of planners that competed in the International Conference on Artificial Intelligent Planning and Scheduling). These developments can be attributed to the discovery of good domain-independent heuristics, the use of domain-specific knowledge, and the development of efficient data structures used in the implementation of the planning algorithms. Logic programming has played a significant role in this line of research, providing a declarative framework for the encoding of different forms of knowledge and its effective use during the planning process [5].

The programming of agents that are capable of reasoning about their actions is a major application of logic programming in Artificial Intelligence. FLUX is a recent, constraint logic programming-based method for designing reasoning agents that can sense, act, and plan under incomplete information [3]. An agent program in this language consists of a background theory, which endows the agent with the necessary knowledge of its actions, along with a high-level acting and planning strategy. The reasoning facilities are provided by a constraint solver, which is formally based on the action theory of the fluent calculus and its solution to the frame problem under incomplete states.

LMNtal is a simple language model based on the rewriting of hierarchical graphs that use logical variables to represent links. The two major goals of the model are (i) to unify various computational models featuring multisets and (ii) to serve as the basis of a truly general-purpose language covering various platforms ranging from wide-area to embedded computation. Another contribution of the model is it greatly facilitates programming with dynamic data structures. The “four elements” of LMNtal are $\underline{l}ogical~\underline{l}inks,~\underline{m}ultisets,~\underline{n}ested~\underline{n}odes$, and $\underline{t}ransform\underline{a}tion$.