Page
%P
20 Result(s)
within
Enno Ohlebusch
Mathematical Logic and Formal Languages
-
Chapter and Conference Paper
A Space Efficient Solution to the Frequent String Mining Problem for Many Databases
In the frequent string mining problem, one is given m databases \({\cal D}_1,...,{\cal D}_m\) of strings and searches f...
-
Book
-
Chapter
Confluence
In this chapter, we will recall several well-known results concerning confluence. First, it will be shown that confluence is in general an undecidable property of TRSs. Then we shall see that confluence is dec...
-
Chapter
Motivation
Equations were among the first mathematical achievements of mankind. For example, they appear in old Babylonian texts written in cuneiform characters that date back to the third millennium B.C. This is not surpri...
-
Chapter
Term Rewriting Systems
In this chapter we will present the basic concepts of term rewriting that are needed in this book. More details on term rewriting, its applications, and related subjects can be found in the textbook of Baader ...
-
Chapter
Abstract Reduction Systems
We will introduce term rewriting by first abstracting from the term structure. In other words, to start, we will concentrate on the so-called abstract reduction systems (ARSs).
-
Chapter
Relative Undecidability
In order to motivate relative undecidability, let us consider the following scenario. All methods for proving termination of a TRS ℛ fail but an implementation of the dependency pair method is able to prove in...
-
Chapter
Modularity
Modularity is a well-known programming paradigm in computer science. Programmers should design their programs in a modular way, that is, as a combination of small programs. These so-called modules are implemen...
-
Chapter
Proving Termination of Logic Programs
Proving correctness of a program consists in showing partial correctness (that is, the program meets its specification) and termination (that is, the program cannot run forever). Methods for deciding terminati...
-
Chapter
Termination
In this chapter we will first sketch a proof of the well-known fact that termination is undecidable. In Chapter 6 this result will be strengthened in several respects. In Section 5.2 standard methods for provi...
-
Chapter
Conditional Rewrite Systems
Conditional term rewriting systems naturally come into play in the algebraic specification of abstract data types. The specification by positive conditional equations is not only more natural but also more exp...
-
Chapter
Graph Rewriting
For reasons of efficiency, term rewriting is usually implemented by graph rewriting. In term rewriting, expressions are represented as terms, whereas in graph rewriting1 these are represented as directed graphs. ...
-
Chapter and Conference Paper
TALP: A Tool for the Termination Analysis of Logic Programs
In the last decade, the automatic termination analysis of logic programs has been receiving increasing attention. Among other methods, techniques have been proposed that transform a well-moded logic program in...
-
Chapter and Conference Paper
Transforming Conditional Rewrite Systems with Extra Variables into Unconditional Systems
Deterministic conditional rewrite systems are interesting because they permit extra variables on the right-hand sides of the rules. If such a system is quasi-reductive, then it is terminating and has a computa...
-
Chapter and Conference Paper
Church-Rosser theorems for abstract reduction modulo an equivalence relation
A very powerful method for proving the Church-Rosser property for abstract rewriting systems has been developed by van Oostrom. In this paper, his technique is extended in two ways to abstract rewriting modulo...
-
Chapter and Conference Paper
Conditional term graph rewriting
For efficiency reasons, term rewriting is usually implemented by graph rewriting. It is known that graph rewriting is a sound and complete implementation of (almost) orthogonal term rewriting systems; see [BEG+87...
-
Chapter and Conference Paper
Relative undecidability in term rewriting
For two hierarchies of properties of term rewriting systems related to confluence and termination, respectively, we prove relative undecidability: for implications X⇒Y in the hierarchies the property X is undecid...
-
Chapter and Conference Paper
Modular properties of constructor-sharing conditional term rewriting systems
First, using a recent modularity result [Ohl94b] for unconditional term rewriting systems (TRSs), it is shown that semi-completeness is a modular property of constructor-sharing join conditional term rewriting...
-
Chapter and Conference Paper
A new calculus for semantic matching
In this paper, we present Reverse Restructuring, a new calculus for solving the semantic matching problem. For narrowing, advanced selection rules are commonly seen as an appropriate method to reduce the searc...
-
Chapter and Conference Paper
Combinations of simplifying conditional term rewriting systems
A conditional term rewriting system (CTRS) is called simplifying if there exists a simplification ordering > on terms such that the left-hand side of any rewrite rule is greater than the right-hand side and th...
