REVE
Computer experiments with the REVE term rewriting system generator. A term rewriting system generator called REVE is described. REVE builds confluent and uniformly terminating term rewriting systems from sets of equations. Particular emphasis is placed on mechanization of termination proof. Indeed, REVE is one of the few such systems which can actually be called automatic because termination is fully integrated into the algorithms. REVE uses an incremental termination method based on recursive decomposition ordering which constructs the termination proof step by step from the presentation of the set of equations and which requires little knowledge of termination methods from the user. All examples from this paper are taken from abstract data type specifications.
Keywords for this software
References in zbMATH (referenced in 67 articles , 1 standard article )
Showing results 1 to 20 of 67.
Sorted by year (- Blanqui, Frédéric: Size-based termination of higher-order rewriting (2018)
- Stratulat, Sorin: Mechanically certifying formula-based Noetherian induction reasoning (2017)
- Yamada, Akihisa; Winkler, Sarah; Hirokawa, Nao; Middeldorp, Aart: AC-KBO revisited (2016)
- Bensaid, Hicham; Peltier, Nicolas: A complete superposition calculus for primal grammars (2014)
- Winkler, Sarah; Sato, Haruhiko; Middeldorp, Aart; Kurihara, Masahito: Multi-completion with termination tools (2013)
- Codish, Michael; Giesl, Jürgen; Schneider-Kamp, Peter; Thiemann, René: SAT solving for termination proofs with recursive path orders and dependency pairs (2012)
- Fuhs, Carsten; Giesl, Jürgen; Parting, Michael; Schneider-Kamp, Peter; Swiderski, Stephan: Proving termination by dependency pairs and inductive theorem proving (2011)
- Winkler, Sarah; Middeldorp, Aart: AC completion with termination tools (2011)
- Durán, Francisco; Lucas, Salvador; Meseguer, José: Termination modulo combinations of equational theories (2009)
- Lucas, Salvador: Automatic proofs of termination with elementary interpretations (2009)
- Waldmann, Johannes: Automatic termination (2009)
- Lucas, Salvador: On the relative power of polynomials with real, rational, and integer coefficients in proofs of termination of rewriting (2006)
- Contejean, Evelyne; Marché, Claude; Tomás, Ana Paula; Urbain, Xavier: Mechanically proving termination using polynomial interpretations (2005)
- Lucas, Salvador: Polynomials over the reals in proofs of termination: from theory to practice (2005)
- Marché, Claude; Urbain, Xavier: Modular and incremental proofs of AC-termination (2005)
- Zantema, H.: Termination of string rewriting proved automatically (2005)
- Fissore, Olivier; Gnaedig, Isabelle; Kirchner, Hélène: Outermost ground termination (2004)
- Rubio, Albert: A fully syntactic AC-RPO. (2002)
- Waldmann, Uwe: Cancellative Abelian monoids and related structures in refutational theorem proving. I (2002)
- Arts, T.; Giesl, J.: Termination of term rewriting using dependency pairs (2000)