Fundamenta Informaticae - Volume 24, issue 1-2

Authors: Plaisted, David A.

Article Type: Other

DOI: 10.3233/FI-1995-24129

Citation: Fundamenta Informaticae, vol. 24, no. 1-2, pp. 1-2, 1995

Authors: Gramlich, Bernhard

Article Type: Research Article

Abstract: We investigate restricted termination and confluence properties of term rewriting systems, in particular weak termination, weak innermost termination, (strong) innermost termination, (strong) termination, and their interrelations. New criteria are provided which are sufficient for the equivalence of these properties. These criteria provide interesting possibilities to infer completeness, i.e. termination plus confluence, from restricted termination and confluence properties. Our main result states that any (strongly) innermost terminating, locally confluent overlay system is terminating, and hence confluent and complete. Using these basic results we are also able to prove some new results about modular termination of rewriting. In particular, we show that …termination is modular for some classes of innermost terminating and locally confluent term rewriting systems, namely for non-overlapping and even for overlay systems. As an easy consequence this latter result also entails a simplified proof of the fact that completeness is a decomposable property of constructor systems. Similarly, a combined overlay system with shared constructors is complete if and only if its component sytems are complete overlay systems. Interestingly, these modularity results are obtained by means of a proof technique which itself constitutes a modular approach. Show more

Keywords: Term rewriting systems, confluence, termination, weak termination, innermost termination, modularity, disjoint union, constructor systems, combination of constructor systems, combined systems with shared constructors

DOI: 10.3233/FI-1995-24121

Citation: Fundamenta Informaticae, vol. 24, no. 1-2, pp. 3-23, 1995

Authors: Martin, Ursula

Article Type: Research Article

Abstract: We describe two new families of orderings on words, and show that each has continuum many distinct members.

DOI: 10.3233/FI-1995-24122

Citation: Fundamenta Informaticae, vol. 24, no. 1-2, pp. 25-46, 1995

Authors: Steinbach, Joachim

Article Type: Research Article

Abstract: We focus on termination proof techniques for unconditional term rewriting systems using simplification orderings. Throughout the last few years numerous (simplification) orderings have been defined by various authors. This paper provides an overview on different aspects of these techniques. Additionally, we introduce a formalism that allows clear representations of orderings.

DOI: 10.3233/FI-1995-24123

Citation: Fundamenta Informaticae, vol. 24, no. 1-2, pp. 47-87, 1995

Authors: Zantema, H.

Article Type: Research Article

Abstract: A new kind of transformation of term rewriting systems (TRS) is proposed, depending on a choice for a model for the TRS. The labelled TRS is obtained from the original one by labelling operation symbols, possibly creating extra copies of some rules. This construction has the remarkable property that the labelled TRS is terminating if and only if the original TRS is terminating. Although the labelled version has more operation symbols and may have more rules (sometimes infinitely many), termination is often easier to prove for the labelled TRS than for the original one. This provides a new technique for …proving termination, making classical techniques like path orders and polynomial interpretations applicable even for non-simplifying TRS’s. The requirement of having a model can slightly be weakened, yielding a remarkably simple termination proof of the system SUBST of [11] describing explicit substitution in λ-calculus. Show more

DOI: 10.3233/FI-1995-24124

Citation: Fundamenta Informaticae, vol. 24, no. 1-2, pp. 89-105, 1995

Authors: Zhang, Hantao

Article Type: Research Article

Abstract: Contextual rewriting as a generalization of conditional rewriting has been found in different forms in the papers whose major subject is not contextual rewriting. Here, we put the scattered information together and give it a systematic study. Among various properties of contextual rewriting, we show that contextual rewriting is a powerful simplification rule for the first-order theorem proving with equality and preserves the refutational completeness of many reasoning systems. We compare definitions of contextual rewriting by Boyer-Moore, Rémy, Zhang-Rémy, Ganzinger, Zhang-Kapur, and Bouhoula-Rusinowitch in regard to its efficiency and power. We provide a detailed procedure for simplifying clauses using contextual …rewriting and a solution on how to handle variables which appear only in the condition of a conditional rewrite rule. Show more

DOI: 10.3233/FI-1995-24125

Citation: Fundamenta Informaticae, vol. 24, no. 1-2, pp. 107-123, 1995

Authors: Bockmayr, Alexander | Krischer, Stefan | Werner, Andreas

Article Type: Research Article

Abstract: Narrowing is a universal unification procedure for equational theories defined by a,canonical term rewriting system. In its original form it is extremely inefficient. Therefore, many optimizations have been proposed during the last years. In this paper, we present the narrowing strategies for arbitrary canonical systems in a uniform framework and introduce the new narrowing strategy LSE narrowing. LSE narrowing is complete and improves all other strategies which are complete for arbitrary-canonical systems. It is optimal in the sense that two different LSE narrowing derivations cannot generate the same narrowing substitution. Moreover, LSE narrowing computes only normalized narrowing substitutions.

DOI: 10.3233/FI-1995-24126

Citation: Fundamenta Informaticae, vol. 24, no. 1-2, pp. 125-155, 1995

Authors: Gilleron, Rémy | Tison, Sophie

Article Type: Research Article

Abstract: We present a collection of results on regular tree languages and rewrite systems. Moreover we prove the undecidability of the preservation of regularity by rewrite systems. More precisely we prove that it is undecidable whether or not for a set E of equations the set E(R) congruence closure of set R is a regular tree language whenever R is a regular tree language. It is equally undecidable whether or not for a confluent and terminating rewrite system S the set S(R) of ground S-normal forms of set R is a regular tree language whenever R is a regular tree language. …Finally we study fragments of the theory of ground term algebras modulo congruence generated by a set of equations which can be compiled in a terminating, confluent rewrite system which preserves regularity. Show more

DOI: 10.3233/FI-1995-24127

Citation: Fundamenta Informaticae, vol. 24, no. 1-2, pp. 157-175, 1995

Authors: Bonacina, Maria Paola | Hsiang, Jieh

Article Type: Research Article

Abstract: This paper describes a methodology for parallel theorem proving in a distributed environment, called deduction by Clause-Diffusion. This methodology utilizes parallelism at the search level, by having concurrent, asynchronous deductive processes searching in parallel the search space of the problem. The search space is partitioned among the processes by distributing the clauses and by subdividing certain classes of inferences. The processes communicate by exchanging data. Policies for distributing the clauses and for scheduling inference and communication steps complete the picture. A distributed derivation is made of the collection of the derivations computed by the concurrent deductive processes and it halts …successfully as soon as one of them does. While the Clause-Diffusion methodology applies to theorem proving in general, it has been designed to provide solutions to the problems in the parallelization of contraction-based strategies, such as rewriting-based methods. We identify backward contraction, i.e. the task of maintaining clauses reduced in a dynamically changing data base, as the main obstacle in parallel theorem proving with contraction. In parallel implementations of contraction-based strategies in shared memory, this difficulty appears as a write-bottleneck, which we have termed the backward contraction bottleneck. The Clause-Diffusion approach avoids this problem by adopting a mostly distributed memory and distributed global contraction schemes. We conclude by reporting some of our results with an implementation of Clause-Diffusion. Show more

DOI: 10.3233/FI-1995-24128

Citation: Fundamenta Informaticae, vol. 24, no. 1-2, pp. 177-207, 1995