Page
%P
14 Result(s)
within
Enno Ohlebusch
Computer System Implementation
Mathematical Logic and Formal Languages
-
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
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
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...
