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 ﬂavors: 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 7 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 conﬂuence 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 ﬁnite presentations of the monoids, allowing their manipulation by a computer. Even b...

RTA

2010

Springer

13 years 8 months ago
2010

Springer

Inﬁnitary Term Rewriting allows to express inﬁnitary terms and inﬁnitary reductions that converge to them. As their notion of transﬁnite 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 conﬂuent term rewrite systems (TRSs for short), innermost polynomial runtime complexity induces polytime computability of the functions de...