The Logic Programming Paradigm

The paper presents an ongoing research project that uses Logic Programming, Linear Logic Programming, and their related techniques for executable specifications and rapid prototyping of Multi-Agent Systems. The MAS paradigm is an extremely rich one and we believe that Logic Programming will play a very effective role in this area, both as a tool for developing real applications and as a semantically well founded language for basing program analysis and proof of properties on.

We introduce Jinni (Java INference engine and Networked Interactor), a lightweight, multi-threaded, logic programming language, intended to be used as a flexible scripting tool for gluing together knowledge processing components and Java objects in networked client/server applications, as well as through applets over the Web.

Mobile threads, implemented by capturing first order continuations in a compact data structure sent over the network, allow Jinni to interoperate with remote high performance BinProlog servers for CPU-intensive knowledge processing and with other Jinni components over the Internet.

These features make Jinni a perfect development platform for intelligent mobile agent systems.

Jinni is fully implemented and is being used in a growing number of industrial and academic projects. The latest version is available from http://www.binnetcorp.com/Jinni

We provide here a computational interpretation of first-order logic based on a constructive interpretation of satisfiability w.r.t. a fixed but arbitrary interpretation. In this approach the formulas themselves axe programs. This contrasts with the so-called formulas as types approach in which the proofs of the formulas are typed terms that can be taken as programs. This view of computing is inspired by logic programming and constraint logic programming but differs from them in a number of crucial aspects.

Formulas as programs is argued to yield a realistic approach to programming that has been realized in the implemented programming language Alma-0 [ABPS98] that combines the advantages of imperative and logic programming. The work here reported can also be used to reason about the correctness of non-recursive Alma-0 programs that do not include destructive assignment.

Different programming languages have different strengths and weaknesses, and typically are suited for different application domains. Because of this, for many applications, using a single programming language to implement all aspects of the program may not be the best or most effective way to build the application. However, current language implementation technology does not make it easy to construct good multi-language programs: in particular, there is usually a nontrivial performance overhead associated with the use of multiple languages. This article discusses the use of link-time optimizations on machine-executable files to reduce such overheads.

In spite of decades of work, the practical impact of programming language semantics (denotational semantics) has been limited. Our thesis is that a major contributing factor to this lack of practical impact is the declarative notation used for expressing the semantics, namely, the λ-calculus. We propose to use Horn Logic (and eventually Constraint Logic) instead of the λ-calculus to express denotational semantics. This simple change leads to many practical applications, most notably to automatic program verification and automatic generation of compilers from semantics specifications. These Horn Logic denotations and their applications axe discussed at length in this paper.

We present a framework for the application of abstract interpretation as an aid during program development, rather than in the more traditional application of program optimization. Program validation and detection of errors is first performed statically by comparing (partial) specifications written in terms of assertions against information obtained from static analysis of the program. The results of this process are expressed in the user assertion language. Assertions (or parts of assertions) which cannot be verified statically are translated into run-time tests. The framework allows the use of assertions to be optional. It also allows using very general properties in assertions, beyond the predefined set understandable by the static analyzer and including properties defined by means of user programs. We also report briefly on an implementation of the framework. The resulting tool generates and checks assertions for Prolog, CLP(R), and CHIP/CLP(fd) programs, and integrates compile-time and run-time checking in a uniform way. The tool allows using properties such as types, modes, non-failure, determinacy, and computational cost, and can treat modules separately, performing incremental analysis. In practice, this modularity allows detecting statically bugs in user programs even if they do not contain any assertions.

We make an assessment of the area of theory and program development in Computational Logic. We point out what we believe to be main causes for success or failure in this area. We revisit the “Algorithm = Logic + Control” equation of Kowalski and show how we believe it could be better understood and used. We indicate some promising directions for further work.

Logic programming and functional programming row in the same boat. Methods used to achieve success with one often transpose to the other, and both face similar obstacles. Here I offer a compendium of success stories for functional programs, followed by a list of obstacles to more widespread use of functional programming, in the belief that much of this experience is relevant to logic programmers. This material first appeared as columns in ACM SIGPLAN Notices [29,30]. The final section contains a few remarks specific to the relations between functional and logic programming.

Although CLP(R) is a promising application of the logic programming paradigm to numerical computation, it has not addressed what has long been known as “the pitfalls of [numerical] computation” [12]. These show that rounding errors induce a severe correctness problem wherever floating-point computation is used. Independently of logic programming, constraint processing has been applied to problems in terms of real-valued variables. By using the techniques of interval arithmetic, constraint processing can be regarded as a computer-generated proof that a certain real-valued solution lies in a narrow interval. In this paper we propose a method for interfacing this technique with CLP(R). This is done via a real-valued analogy of Apt’s proof-theoretic framework for constraint processing.

The paper presents an introduction to some of the problems in computational molecular biology (CMB) viewed from a logic programming (LP) perspective. Non-deterministic formal grammars are presented to define biologically interesting subsequences of DNA. Also presented are compact representations of ambiguities by directed acyclic graphs. Various problems in CMB are discussed; their solutions using dynamic programming, hidden Markov models, and inductive logic programming are briefly described. It is believed that a study of these and related problems can contribute to provide a new impetus to LP research and its extensions.

Constraints are predefined relations with a special implementation mechanism. Logic formalisms provide specific reasoning facilities. We look at the effect of adding constraints to existing logic-based executable formalisms, focusing on the semantics of the combined formalisms. We find that in cases where this has been successful the operations of the formalism can be formulated logically and then extended easily to constraints. In many cases a disjunctive property of the constraints is reflected in the combined formalism, to the detriment of efficiency.

The state-of-the-art in inductive logic programming is surveyed by analyzing the approach taken by this field over the past 8 years. The analysis investigates the roles of 1) logic programming and machine learning, 2) theory, techniques and applications, and 3) various technical problems addressed within inductive logic programming.

This paper describes how Inductive Logic Programming is related to Logic Programming. It first introduces Model Inference System developed by Ehud Shapiro and then new Inductive Logic Programming technologies. It shows the technical progress from “subsumption” to “logical entailment” and insists the importance of utilizing “background knowledge.” A new computational model for computing induction is presented. It is defined by an iteration consisting of the computation of the Most Specific Hypothesis (MSH) and search in a reduced concept lattice brought by the MSH. This computation model provides an efficient algorithm for computing induction in terms of deduction followed by an efficient search algorithm. This implies that the inversion of deduction can be solved rather efficiently when the problem is restricted to Horn clauses.

This is a discussion of some of the achievements and challenges related to representing actions and the design of planners from the perspective of logic programming. We talk about recent work on action languages and translating them into logic programming, on representing possible histories of an action domain by answer sets, on efficient implementations of the answer set semantics and their use for generating plans, and on causal logic and its relation to planning algorithms. Recent progress in these areas may lead to the creation of planners which are based on the ideas of logic programming and combine the use of expressive action description languages with efficient computational procedures.

In this paper we reexamine the place and role of stable model semantics in logic programming and contrast it with a least Herbrand model approach to Horn programs. We demonstrate that inherent features of stable model semantics naturally lead to a logic programming system that offers an interesting alternative to more traditional logic programming styles of Horn logic programming, stratified logic programming and logic programming with well-founded semantics. The proposed approach is based on the interpretation of program clauses as constraints. In this setting, a program does not describe a single intended model, but a family of its stable models. These stable models encode solutions to the constraint satisfaction problem described by the program. Our approach imposes restrictions on the syntax of logic programs. In particular, function symbols are eliminated from the language. We argue that the resulting logic programming system is well-attuned to problems in the class NP, has a well-defined domain of applications, and an emerging methodology of programming. We point out that what makes the whole approach viable is recent progress in implementations of algorithms to compute stable models of propositional logic programs.

In this paper, we provide logic-based foundations for the extended aggregate constructs required by advanced database applications. In particular, we focus on data mining applications and show that they require user-defined aggregates extended with early returns. Thus, we propose a simple formalization of extended user-defined aggregates using the nondeterministic construct of choice. We obtain programs that have a formal semantics based on the concept of total stable models, but are also amenable to efficient implementation. Our formalization leads to a simple syntactic characterization of user-defined aggregates that are monotone with respect to set containment. Therefore, these aggregates can be freely used in recursive programs, and the fixpoints for such programs can be computed efficiently using the standard techniques of deductive databases. We describe the many new applications of user-defined aggregates, and their implementation for the logical data language LDL++. Finally, we discuss the transfer of this technology to SQL databases.

We argue that logic is an inseparable part of language and that it can play an important role in natural language processing. We first examine families of formalisms from linguistics and computational linguistics, drawing their connections to logic. Next we examine the pros and cons of logic programming as a general paradigm for language processing, and we consider which kinds of logic and logic programming features it would be desirable to include as standard in order to make natural language applications of logic programming more natural and easier to use. We then introduce Assumptive Logic Programming- that is, logic programming augmented with linear, intuitionistic and timeless assumptions. We briefly discuss a few of its recent applications, such as controlling virtual worlds and robots through natural language, extracting concepts from web documents, and generating VRML animations through English commands; and we develop in some more detail the design of a novel application: creating databases through natural language discourse.