A new completion theory for logic programming called strong completion, is introduced. Similar to the Clark's completion, the strong completion can be interpreted either in two-valued or three-valued logic. We show that Since the strong completion of a logic program P is also a circumscription of P, the open problem as whether or not there exists a circumscriptive specification of a logic program P which specifies the stable semantics as well as the well-founded semantics of P, is solved. We show that the call-consistency condition is sufficient for a logic program to have a stable model. Further we prove that the stable semantics is equivalent to the well-founded semantics if the program is strict and call-consistent.
We discuss various semantics of many-sorted logic programs with equality both from the viewpoint of algebraic specifications as well as from the viewpoint of logic programming. We define model-theoretic semantics based on initial models, least generalized Herbrand models and a least fixpoint construction, and we investigate proof-theoretic semantics based on resolution and unification modulo a set of conditional equations. Generalizing ordinary SLD derivations, we introduce so-called SLDE derivations and SLDE trees and study their correctness and completeness properties. We define a translation of logic programs LPE with equality into equivalent logic programs LPø with empty equational part such that LPE satisfies a goal G if and only if LPø satisfies G.
The paper presents a new schematization of infinite families of terms called the primal grammars, based on the notion of primitive recursive rewrite systems. This schematization is presented by a generating term and a canonical rewrite system. It is proved that the class of primal grammars, covers completely the class of crossed rewrite systems. This proof contains a construction of a primal grammar from a crossed rewrite system.
In this paper, a paramodulation calculus for equational reasoning is presented that combines the advantages of both Knuth-Bendix completion and goal directed strategies like the set of support strategy. Its soundness and completeness is proved, and finally the practical aspects of this method are discussed.
Modular properties of term rewriting systems, i.e. properties which are preserved under disjoint unions, have attracted an increasing attention within the last few years. Whereas confluence is modular this does not hold true in general for termination. By means of a careful analysis of potential counterexamples we prove the following abstract result. Whenever the disjoint union ℛ_1 ⊕ℛ_2 of two (finite) terminating term rewriting systems ℛ_1 ,ℛ_2 is non-terminating, then one of the systems, say ℛ_1 , enjoys an interesting (undecidable) property, namely it is not termination preserving under non-deterministic collapses, i.e. ℛ_1 ⊕G(x,y) → x,G(x, y) → y is non-terminating, and the other system ℛ_2 is collapsing, i.e. contains a rule with a variable right hand side. This result generalizes known sufficient syntactical criteria for modular termination of rewriting and provides the basis for a couple of derived modularity results. Furthermore, we prove that the minimal rank of potential counterexamples in disjoint unions may be arbitrarily high which shows that interaction of systems in such disjoint unions may be very subtle. Finally, extensions and generalizations of our main results in various directions are discussed and sketched.
The set of irreducible ground terms w. r. t. a term rewriting system R can often be characterized by a finite test set. We describe a fast algorithm to compute such a test set for all left-linear and well-behaved non-left-linear term rewriting systems. Our algorithm uses a new data structure called top set tree which is expanded in a dynamic programming like manner. The tree expansion technique we use to generate the test sets elucidate the connection between the test set approaches and grammatical appraoches to ground reducibility. Our method can also be extended to term rewriting systems modulo AC.
In this paper we study a declarative (fixpoint) semantics for logic programs which correctly models several kinds of partial answers and call patterns. We first show how the Ω-semantics [5,4] can model these observables when the selection rule is not taken into account. We then define a suitable immediate consequence operator, and hence a fixpoint semantics, for partial answers and call patterns which considers also the selection rule. Each observable induces an observational equivalence on programs. The semantics are then related to the observational equivalences by investigating correctness and full abstraction properties.
Abstract programming includes two important approaches which are called functional and relational. We choose algebraic specification and the programming language Prolog as representatives of the two approaches to study the relation between them.
This paper presents some ways to prove theorems in first and second order logic, such that rewriting does the routine work automatically, and partially successful proofs often return information that suggests what to try next. The theoretical framework makes extensive use of general algebra, and main results include an extension of many-sorted equational logic to universal quantification over functions, some techniques for handling first order logic, and some structural induction principles. The OBJ language is used for illustration, and initiality is a recurrent theme.
In this paper we study final algebra semantics for constructive equational systems, A class of models of a constructive system is described, and proven to have a final algebra. Then we develop a method for proof by consistency with respect to the final model. Finally we show that the method contains the proof methods of Musser [11], Goguen [2], and Huet and Hullot
This paper describes how to model and solve boolean satisfiability problems with the constraint logic programming language CHIP. Although CHIP has not been developed as a specialised propositional calculus prover, it can solve these problems quite efficiently. Several different methods of describing satisfiability problems in CHIP are presented and compared. This flexibility of modelling is a major advantage of CHIP over closed problem solvers. We have evaluated various sets of benchmarks taken from [31] [16] [21]. With one exception, CHIP performs as well or better as specialised programs on these examples. We also shortly discuss an alternative modeling technique using finite domain variables not restricted to 0/1 values.
In the last years there have been several proposals to extend logic programming with the constructs for concurrency, aiming at the development of a concurrent language which would maintain the typical advantages of logic programming: declarative reading, computations as proofs, amenability to metaprogramming etc. Examples of concurrent logic languages include PARLOG [6], Concurrent Prolog [12], Guarded Horn Clauses [15] and their so-called flat versions.
A group can be specified as a set of equations. It is shown that there exist canonical term rewriting systems for finite groups which are generated from a finite set of relators such that in this term rewriting system the inversion operator is a defined function. Then it is possible to compute all ground normal forms of these term rewriting systems. Since this set of ground normal forms is generally not generated by a set of free constructors it can be computed using methods developped for ground reducibility tests. We also show that some of the rules defining a group are inductive consequences of other rules in the canonical term rewriting system. This can be proven by inductive completion.
Equational algebraic specifications and the corresponding specification morphisms have been defined in the literature in several ways. Although apparently equivalent, they are significantly different with respect to standard categorical constructions, leading to categories of algebraic spacifications which are not equivalent. The nonequivalence of these categories of algebraic specifications is also significant in the context of high-level-replacement (HLR) systems, a generalization at the categorical level of the well known algebraic approach to graph grammars based on double pushout. Unexpectedely, only for some of the categories the properties needed to prove the Church-Rosser, Parallelism and Concurrency Theorems for High-Level-Replacement systems are valid.
We focus on termination proofs of rewrite systems, especially of rewrite systems containing associative and commutative operators. We prove their termination by elementary interpretations, more specifically, by functions defined by addition, multiplication and exponentiation. We discuss a method based on polynomial interpretations and propose an implementation of a mechanization of the comparison of expressions built with polynomials and exponentials.
In this document, we present Dislog, an extension to Prolog designed to deal with long-distance relations and constraints in a transparent and declarative way. We then give a meta-interpreter for Dislog and present two interpretations for Dislog: a well-formedness constraint on proof trees interpretation and a constraint logic programming interpretation.
Sufficient criteria for an equation to be in the inductive theory of a term rewriting system are given. Inspecting only special critical pairs, we need not require the underlying system to be confluent, not even on ground terms. We are able to deal with equations which — if viewed as rules — are possibly not terminating if added to the given rewrite system; we have to restrict, however, their use in the induction process. Modular use of lemmata, already known inductive theorems, is incorporated into the results. As examples we treat natural number arithmetic, sorting lists of natural numbers, and sorting lists over arbitrary data structures.
In this paper we present the semantics of a functional logic language with parametric and order-sorted polymorphism. Typed programs consist of a polymorphic signature and a set of constructor-based conditional rewriting rules for which we define a semantic calculus. The denotational semantics of the language is based on Scott domains interpreting constructors and functions by monotonic and continuous mappings, respectively, in every instance of the declared type. We prove initiality results for the free ground term algebra. We also prove that the free term algebra with variables is freely generated in the category of models. The semantic calculus is proved to be sound and complete w.r.t. the denotational semantics. As in logic programming, we define the immediate consequence operator, proving that the Hebrand model is the least model of a program.
Given a logic program P and a goal G, we introduce a notion which states when an SLD-tree for P∪{G} instantiates a, set of variables V with respect to another one, W. We call this notion weak instantiation, as it is a generalization of the instantiation property introduced in [3]. A negation rule based on instantiation, the so-called Negation As Instantiation rule (NAI), allows for inferring existentially closed negative queries, that is formulas of the form ∃¬Q, from logic programs. We show that, by using the new notion, we can infer a larger class of negative queries, namely the class of the queries of the form ∨W∃V¬Q and of the form ∨W∃V∨Z¬Q, where Z is the set of the remaining variables of Q.
