Partial deduction of updateable definite logic programs

In this paper, we study the partial deduction of updateable logic programs. Partial deduction is a transformation technique that, given a normal program P and a normal goal G, produces from P a residual program P′ wrt G. An updateable program is a normal program to which an update can be applied. An update is a sequence of additions of clauses to a program and deletions of clauses from a program. We present algorithms that, given a normal program P, a normal goal G, a residual program P′ wrt G, and an update t for P, compute the corresponding update t′ such that t′(P′) is a residual program of t(P) wrt G. Weprove the correctness of these algorithms. We also describe an application of one of the algorithms to updateable knowledge bases.     

Efficient reordering of Prolog programs

Prolog programs are often inefficient: execution corresponds to a depth-first traversal of an AND/OR graph; traversing subgraphs in another order can be less expensive. It is shown how the reordering of clauses within Prolog predicates, and especially of goals within clauses, can prevent unnecessary search. The characterization and detection of restrictions on reordering is discussed. A system of calling modes for Prolog, geared to reordering, is proposed, and ways to infer them automatically are discussed. The information needed for safe reordering is summarized, and which types can be inferred automatically and which must be provided by the user are considered. An improved method for determining a good order for the goals of Prolog clauses is presented and used as the basis for a reordering system     

Positive definite separable quadratic programs for non-convex problems

We propose to enforce positive definiteness of the Hessian matrix in a sequence of separable quadratic programs, without demanding that the individual contributions from the objective and the constraint functions are all positive definite. For problems characterized by non-convex objective or constraint functions, this may result in a notable computational advantage. Even though separable quadratic programs are of interest in their own right, they are of particular interest in structural optimization, due to the so-called ‘approximated-approximations’ approach. This approach allows for the construction of quadratic approximations to the reciprocal-like approximations used, for example, in CONLIN and MMA. To demonstrate some of the ideas proposed, the optimal topology design of a structure subject to local stress constraints is studied as one of the examples.     

Canonical logic programs

Consider the class of programs P where the greatest fixpoint of T_P is equal to the complement of the finite failure set of P. Programs in this calss possess some important properties which others do not. The main result in this paper proves that this class is representative of all programs. Specifically, we call the programs in this class canonical and we prove that for any program P₁, there exists a semantically equivalent program P₂ which is canonical.     

Propositional semantics for disjunctive logic programs

In this paper we study the properties of the class of head-cycle-free extended disjunctive logic programs (HEDLPs), which includes, as a special case, all nondisjunctive extended logic programs. We show that any propositional HEDLP can be mapped in polynomial time into a propositional theory such that each model of the latter corresponds to an answer set, as defined by stable model semantics, of the former. Using this mapping, we show that many queries over HEDLPs can be determined by solving propositional satisfiability problems. Our mapping has several important implications: It establishes the NP-completeness of this class of disjunctive logic programs; it allows existing algorithms and tractable subsets for the satisfiability problem to be used in logic programming; it facilitates evaluation of the expressive power of disjunctive logic programs; and it leads to the discovery of useful similarities between stable model semantics and Clark's predicate completion.     

Automatic mode inference for logic programs

In general, logic programs are undirected, i.e., there is no concept of “input” and “output” arguments to a procedure. An argument may be used either as an input or as an output argument, and programs may be executed either in a “forward” direction or in a “backward” direction. However, it is often the case that in a given program, a predicate is used with some of its arguments used consistently as input arguments and others as output arguments. Such mode information can be used by a compiler to effect various optimizations. This paper considers the problem of automatically inferring the models of the predicates in a program. The dataflow analysis we use is more powerful than approaches relying on syntactic characteristics of programs. Our work differs from that of Mellish in that (1) we give a sound and efficient treatment of variable aliasing in mode inference; (2) by propagating instantiation information using state transformations rather than through dependencies between variables, we achieve greater precision in the treatment of unification, e.g. through =/2; and (3) we describe an efficient implementation based on the dynamic generation of customized mode interpreters. Several optimizations to improve the performance of the mode inference algorithm are described, as are various program optimizations based on mode information.     

The strong semantics for logic programs

Recently, the well-founded semantics of a logic programP has been strengthened to the well-founded semantics-by-case (WF_C) and this in turn has been strengthened to the extended well-founded semantics (WF_E). Both WF_C(P) and WF_E(P) have thelogical consequence property, namely, if an atomAj is true in the theory Th(P), thenAj is true in the semantics as well. However, neither WF_C nor WF_E has the GCWA property, i.e., if an atomAj is false in all minimal models ofP,Aj may not be false in WF_C(P) (resp. WF_E(P)). We extend the ideas in WF_C and WF_E to define a strong well-founded semantics WF_S which has the GCWA property. The strong semantics WF_S(P) is defined by combining GCWA with the notion ofderived rules. Here we use a new Type-III derived rules in addition to those used in WF_C and WF_E. The relationship between WF_S and WF_C is also clarified.     

Three-valued completion for abductive logic programs

In this paper, we propose a three-valued completion semantics for abductive logic programs, which solves some problems associated with the Console et al. two-valued completion semantics. The semantics is a generalization of Kunen's completion semantics for general logic programs, which is known to correspond very well to a class of effective proof procedures for general logic programs. Secondly, we propose a proof procedure for abductive logic programs, which is a generalization of a proof procedure for general logic programs based on constructive negation. This proof procedure is sound and complete with respect to the proposed semantics. By generalizing a number of results on general logic programs to the class of abductive logic programs, we present further evidence for the idea that limited forms of abduction can be added quite naturally to general logic programs.     

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     

A type system for logic programs

A theory for a type system for logic programs is developed which addressesthe question of well-typing, type inference, and compile-time and run-time type checking. A type is a recursively enumerable set of ground atoms, which is tuple-distributive. The association of a type to a program is intended to mean that only ground atoms that are elements of the type may be derived from the program. A declarative definition of well-typed programs is formulated, based on an intuitive approach related to the fixpoint semantics of logic programs. Whether a program is well typed is undecidable in general. We define a restricted class of types, called regular types, for which type checking is decidable. Regular unary logic programs are proposed as a specification language for regular types. An algorithm for type-checking a logic program with respect to a regular type definition is described, and its complexity is analyzed. Finally, the practicality of the type system is discussed, and some examples are shown. The type system has been implemented in FCP for FCP and is incorporated in the Logix system.     

Transformations of logic programs

This paper introduces a new concept of computation trees of logic programs that will be used in reasoning about programs. Three types of transformations improving the structure of logic programs are described. There are two natural measures of complexity suggested by computation trees, namely, the number of nodes called by recursion and the maximal number of AND/OR alternations on a branch. Both measures are shown to collapse, or more precisely, it is shown how every logic program can be transformed to a program computing the same function of which the computation tree has at most one called node and at most two alternations on every branch. Some conclusions related to this Normal Form Theorem are discussed. Theoretical results with the attempts to develop a practical methodology for the construction of logic programs are compared.     

Equivalent logic programs and symmetric homogeneous forms of logic programs with equality

This article introduces the notion of CAS-equivalent logic programs: logic programs with identical correct answer substitutions. It is shown that the notions CAS-equivalence, refutational equivalence, and logical equivalence do not coincide in the case of definite clause logic programs. Least model criteria for refutational and CAS-equivalence are suggested and their correctness is proved. The least model approach is illustrated by two proofs of CAS-equivalence. It is shown that the symmetric extension of a logic program subsumes the symmetry axiom and the symmetric homogeneous form of a logic program with equality subsumes the symmetry, transitivity, and predicate substitutivity axioms of equality. These results contribute towards the goal of building equality into standard Prolog without introducing additional inference rules.     

Learning higher-order logic programs

Machine Learning - A key feature of inductive logic programming is its ability to learn first-order programs, which are intrinsically more expressive than propositional programs. In this paper, we...     

Parallelism in logic programs

There is a tension between the objectives of avoiding irrelevant computation and extracting parallelism, in that a computational step used to restrict another must precede the latter. Our thesis, following [3], is that evaluation methods can be viewed as implementing a choice ofsideways information propagation graphs, or sips, which determines the set of goals and facts that must be evaluated. Two evaluation methods that implement the same sips can then be compared to see which obtains a greater degree of parallelism, and we provide a formal measure of parallelism to make this comparison.Using this measure, we prove that transforming a program using the Magic Templates algorithm and then evaluating the fixpoint bottom-up provides a most parallel implementation for a given choice of sips, without taking resource constraints into account. This result, taken in conjunction with earlier results from [3,27], which show that bottom-up evaluation performs no irrelevant computation and is sound and complete, suggests that a bottom-up approach to parallel evaluation of logic programs is very promising. A more careful analysis of the relative overheads in the top-down and bottom-up evaluation paradigms is needed, however, and we discuss some of the issues.The abstract model allows us to establish several results comparing other proposed parallel evaluation methods in the logic programming and deductive database literature, thereby showing some natural, and sometimes surprising, connections. We consider the limitations of the abstract model and of the proposed bottom-up evaluation method, including the inability of sips to describe certain evaluation methods, and the effect of resource constraints. Our results shed light on the limits of the sip paradigm of computation, which we extend in the process.     

Most specific logic programs

More specific versions of definite logic programs are introduced. These are versions of a program in which each clause is further instantiated or removed and which have an equivalent set of successful derivations to those of the original program, but a possibly increased set of finitely failed goals. They are better than the original program because failure in a non-successful derivation may be detected more quickly. Furthermore, information about allowed variable bindings which is hidden in the original program may be made explicit in a more specific version of it. This allows better static analysis of the program's properties and may reveal errors in the original program. A program may have several more specific versions but there is always a most specific version which is unique up to variable renaming. Methods to calculate more specific versions are given and it is characterized when they give the most specific version.     

On computing logic programs

In this paper we present and compare some classical problem-solving methods for computing the stable models of logic programs with negation. Using a graph theoretic representation of logic programs and their stable models, we discuss and compare linear programming, propositional satisfiability, constraint satisfaction, and graph methods.     

Efficient access mechanisms for tabled logic programs

The use of tabling in logic programming allows bottom-up evaluation to be incorporated in a top-down framework, combining advantages of both. At the engine level, tabling also introduces issues not present in pure top-down evaluation, due to the need for subgoals and answers to access tables during resolution. This article describes the design, implementation, and experimental evaluation of data structures and algorithms for high-performance table access. Our approach uses tries as the basis for tables. Tries, a variant of discrimination nets, provide complete discrimination for terms, and permit a lookup and possible insertion to be performed in a single pass through a term. In addition, a novel technique of substitution factoring is proposed. When substitution factoring is used, the access cost for answers is proportional to the size of the answer substitution, rather than to the size of the answer itself. Answer tries can be implemented both as interpreted structures and as compiled WAM-like code. When they are compiled, the speed of computing substitutions through answer tries is competitive with the speed of unit facts compiled or asserted as WAM code. Because answer tries can also be created an order of magnitude more quickly than asserted code, they form a promising alternative for representing certain types of dynamic code, even in Prolog systems without tabling.