Sciweavers

RTA
2004
Springer
13 years 9 months ago
TORPA: Termination of Rewriting Proved Automatically
Abstract. In this paper it is described how a combination of polynomial interpretations, recursive path order, RFC match-bounds, the dependency pair method and semantic labelling c...
Hans Zantema
RTA
2004
Springer
13 years 9 months ago
The Joinability and Unification Problems for Confluent Semi-constructor TRSs
Ichiro Mitsuhashi, Michio Oyamaguchi, Yoshikatsu O...
RTA
2004
Springer
13 years 9 months ago
A Visual Environment for Developing Context-Sensitive Term Rewriting Systems
Over the past decade, researchers have found context-sensitive term-rewriting semantics to be powerful and expressive tools for modeling programming languages, particularly in esta...
Jacob Matthews, Robert Bruce Findler, Matthew Flat...
RTA
2004
Springer
13 years 9 months ago
mu-term: A Tool for Proving Termination of Context-Sensitive Rewriting
Restrictions of rewriting can eventually achieve termination by pruning all infinite rewrite sequences issued from every term. Contextsensitive rewriting (CSR) is an example of su...
Salvador Lucas
RTA
2004
Springer
13 years 9 months ago
Rewriting for Fitch Style Natural Deductions
Logical systems in natural deduction style are usually presented in the Gentzen style. A different definition of natural deduction, that corresponds more closely to proofs in ord...
Herman Geuvers, Rob Nederpelt
RTA
2004
Springer
13 years 9 months ago
Dependency Pairs Revisited
Abstract. In this paper we present some new refinements of the dependency pair method for automatically proving the termination of term rewrite systems. These refinements are ver...
Nao Hirokawa, Aart Middeldorp
RTA
2004
Springer
13 years 9 months ago
Automated Termination Proofs with AProVE
We describe the system AProVE, an automated prover to verify (innermost) termination of term rewrite systems (TRSs). For this system, we have developed and implemented efficient al...
Jürgen Giesl, René Thiemann, Peter Sch...
RTA
2004
Springer
13 years 9 months ago
Querying Unranked Trees with Stepwise Tree Automata
The problem of selecting nodes in unranked trees is the most basic querying problem for XML. We propose stepwise tree automata for querying unranked trees. Stepwise tree automata c...
Julien Carme, Joachim Niehren, Marc Tommasi
RTA
2004
Springer
13 years 9 months ago
A Type-Based Termination Criterion for Dependently-Typed Higher-Order Rewrite Systems
Several authors devised type-based termination criteria for ML-like languages allowing non-structural recursive calls. We extend these works to general rewriting and dependent type...
Frédéric Blanqui