Sciweavers

CADE
2012
Springer
11 years 9 months ago
Rewriting Induction + Linear Arithmetic = Decision Procedure
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...
Stephan Falke, Deepak Kapur
CAV
2012
Springer
270views Hardware» more  CAV 2012»
11 years 9 months ago
Automated Termination Proofs for Java Programs with Cyclic Data
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...
Marc Brockschmidt, Richard Musiol, Carsten Otto, J...
FROCOS
2011
Springer
12 years 7 months ago
Harnessing First Order Termination Provers Using Higher Order Dependency Pairs
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...
Carsten Fuhs, Cynthia Kop
RTA
2011
Springer
12 years 10 months ago
Modular Termination Proofs of Recursive Java Bytecode Programs by Term Rewriting
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...
Marc Brockschmidt, Carsten Otto, Jürgen Giesl
FSTTCS
2010
Springer
13 years 5 months ago
Uniqueness of Normal Forms is Decidable for Shallow Term Rewrite Systems
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 ...
Nicholas Radcliffe, Rakesh M. Verma
JFLP
2002
101views more  JFLP 2002»
13 years 7 months ago
Complete Selection Functions for a Lazy Conditional Narrowing Calculus
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...
Aart Middeldorp, Taro Suzuki, Mohamed Hamada
CORR
2006
Springer
100views Education» more  CORR 2006»
13 years 7 months ago
Using groups for investigating rewrite systems
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...
Patrick Dehornoy
RTA
1995
Springer
13 years 11 months ago
(Head-) Normalization of Typeable Rewrite Systems
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...
Steffen van Bakel, Maribel Fernández
AISC
2004
Springer
13 years 11 months ago
Polynomial Interpretations with Negative Coefficients
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...
Nao Hirokawa, Aart Middeldorp
RTA
2010
Springer
13 years 11 months ago
Closing the Gap Between Runtime Complexity and Polytime Computability
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...
Martin Avanzini, Georg Moser