CADE
2012
Springer
12 years 1 months ago
2012
Springer
Abstract. This paper presents new results on the decidability of inductive validity of conjectures. For these results, a class of term rewrite systems (TRSs) with built-in linear i...
CAV
2012
Springer
12 years 1 months ago
2012
Springer
Abstract. In earlier work, we developed a technique to prove termination of Java programs automatically: first, Java programs are automatically transformed to term rewrite systems...
FROCOS
2011
Springer
12 years 11 months ago
2011
Springer
Many functional programs and higher order term rewrite systems contain, besides higher order rules, also a significant first order part. We discuss how an automatic termination p...
RTA
2011
Springer
13 years 2 months ago
2011
Springer
In [5, 15] we presented an approach to prove termination of non-recursive Java Bytecode (JBC) programs automatically. Here, JBC programs are first transformed to finite terminat...
FSTTCS
2010
Springer
13 years 9 months ago
2010
Springer
Uniqueness of normal forms (UN= ) is an important property of term rewrite systems. UN= is decidable for ground (i.e., variable-free) systems and undecidable in general. Recently ...
JFLP
2002
13 years 11 months ago
2002
In this paper we extend the lazy narrowing calculus lnc of Middeldorp, Okui, and Ida [26] to conditional rewrite systems. The resulting lazy conditional narrowing calculus lcnc is...
CORR
2006
Springer
13 years 11 months ago
2006
Springer
We describe several technical tools that prove to be efficient for investigating the rewrite systems associated with an equational specification. These tools consist in introducing...
RTA
1995
Springer
14 years 3 months ago
1995
Springer
In this paper we study normalization properties of rewrite systems that are typeable using intersection types with and with sorts. We prove two normalization properties of typeable...
AISC
2004
Springer
14 years 3 months ago
2004
Springer
Polynomial interpretations are a useful technique for proving termination of term rewrite systems. We show how polynomial interpretations with negative coefficients, like x - 1 for...
RTA
2010
Springer
14 years 3 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...