Sciweavers

IEICET
2007
110views more  IEICET 2007»
13 years 3 months ago
A Higher-Order Knuth-Bendix Procedure and Its Applications
The completeness (i.e. confluent and terminating) property is an important concept when using a term rewriting system (TRS) as a computational model of functional programming lang...
Keiichirou Kusakari, Yuki Chiba
ENTCS
2008
85views more  ENTCS 2008»
13 years 3 months ago
Comparing CSP and SAT Solvers for Polynomial Constraints in Termination Provers
Proofs of termination in term rewriting involve solving constraints between terms coming from (parts of) the rules of the term rewriting system. A common way to deal with such con...
Salvador Lucas, Rafael Navarro-Marset
AAECC
2007
Springer
148views Algorithms» more  AAECC 2007»
13 years 3 months ago
Enhancing dependency pair method using strong computability in simply-typed term rewriting
We enhance the dependency pair method in order to prove termination using recursive structure analysis in simply-typed term rewriting systems, which is one of the computational mod...
Keiichirou Kusakari, Masahiko Sakai
AISC
2006
Springer
13 years 7 months ago
The Confluence Problem for Flat TRSs
We prove that the properties of reachability, joinability and confluence are undecidable for flat TRSs. Here, a TRS is flat if the heights of the left and right-hand sides of each ...
Ichiro Mitsuhashi, Michio Oyamaguchi, Florent Jacq...
LOPSTR
2004
Springer
13 years 9 months ago
Natural Rewriting for General Term Rewriting Systems
We address the problem of an efficient rewriting strategy for general term rewriting systems. Several strategies have been proposed over the last two decades for rewriting, the mos...
Santiago Escobar, José Meseguer, Prasanna T...
RTA
2005
Springer
13 years 9 months ago
Partial Inversion of Constructor Term Rewriting Systems
Abstract. Partial-inversion compilers generate programs which compute some unknown inputs of given programs from a given output and the rest of inputs whose values are already give...
Naoki Nishida, Masahiko Sakai, Toshiki Sakabe
RTA
2005
Springer
13 years 9 months ago
On Tree Automata that Certify Termination of Left-Linear Term Rewriting Systems
We present a new method for proving termination of term rewriting systems automatically. It is a generalization of the match bound method for string rewriting. To prove that a term...
Alfons Geser, Dieter Hofbauer, Johannes Waldmann, ...