RTA
2010
Springer
13 years 2 months ago
2010
Springer
We consider here a number of variations on the System F, that are predicative second-order systems whose terms are intermediate between the Curry style and Church style. The terms ...
RTA
2010
Springer
13 years 2 months ago
2010
Springer
Polynomial interpretations are a useful technique for proving termination of term rewrite systems. They come in various flavors: polynomial interpretations with real, rational and...
RTA
2010
Springer
13 years 6 months ago
2010
Springer
We consider the problem of computing, out of a set C of trees and a rewrite system R, those trees in C that cannot be rewritten into a tree in C. We solve this problem for sets of ...
RTA
2010
Springer
13 years 8 months ago
2010
Springer
We present an automated approach to prove termination of Java Bytecode (JBC) programs by automatically transforming them to term rewrite systems (TRSs). In this way, the numerous t...
RTA
2010
Springer
13 years 8 months ago
2010
Springer
Decreasing diagrams technique (van Oostrom, 1994) is a technique that can be widely applied to prove confluence of rewrite systems. To directly apply the decreasing diagrams techn...
RTA
2010
Springer
13 years 8 months ago
2010
Springer
Rewriting systems on words are very useful in the study of monoids. In good cases, they give finite presentations of the monoids, allowing their manipulation by a computer. Even b...
RTA
2010
Springer
13 years 8 months ago
2010
Springer
Infinitary Term Rewriting allows to express infinitary terms and infinitary reductions that converge to them. As their notion of transfinite reduction in general, and as binary...
RTA
2010
Springer
13 years 8 months ago
2010
Springer
Matrix interpretations can be used to bound the derivational complexity of rewrite systems. We present a criterion that completely characterizes matrix interpretations that are pol...
RTA
2010
Springer
13 years 8 months ago
2010
Springer
In usual proof systems, like the sequent calculus, only a very limited way of combining proofs is available through the tree structure. We present in this paper a logicindependent ...
RTA
2010
Springer
13 years 8 months ago
2010
Springer
In earlier work, we have shown that for confluent term rewrite systems (TRSs for short), innermost polynomial runtime complexity induces polytime computability of the functions de...