Matchbox

Matchbox: A tool for match-bounded string rewriting. The program Matchbox implements the exact computation of the set of descendants of a regular language, and of the set of non-terminating strings, with respect to an (inverse) match-bounded string rewriting system. Matchbox can search for proof or disproof of a Boolean combination of match-height properties of a given rewrite system, and some of its transformed variants. This is applied in various ways to search for proofs of termination and non-termination. Matchbox is the first program that delivers automated proofs of termination for some difficult string rewriting systems.


References in zbMATH (referenced in 22 articles )

Showing results 1 to 20 of 22.
Sorted by year (citations)

1 2 next

  1. Frohn, Florian; Giesl, Jürgen; Hensel, Jera; Aschermann, Cornelius; Ströder, Thomas: Lower bounds for runtime complexity of term rewriting (2017)
  2. Sternagel, Christian; Sternagel, Thomas: Certifying confluence of quasi-decreasing strongly deterministic conditional term rewrite systems (2017)
  3. Hogg, Jonathan; Scott, Jennifer: On the use of suboptimal matchings for scaling and ordering sparse symmetric matrices. (2015)
  4. Korp, Martin; Middeldorp, Aart: Match-bounds revisited (2009)
  5. Thiemann, René; Sternagel, Christian: Certification of termination proofs using CeTA (2009)
  6. Thiemann, René; Sternagel, Christian: Loops under strategies (2009)
  7. Zankl, Harald; Middeldorp, Aart: Increasing interpretations (2009)
  8. Korp, Martin; Middeldorp, Aart: Match-bounds with dependency pairs for proving termination of rewrite systems (2008)
  9. Lucas, Salvador; Meseguer, José: Termination of just/fair computations in term rewriting (2008)
  10. Payet, Étienne: Loop detection in term rewriting using the eliminating unfoldings (2008)
  11. Geser, Alfons; Hofbauer, Dieter; Waldmann, Johannes; Zantema, Hans: On tree automata that certify termination of left-linear term rewriting systems (2007)
  12. Hirokawa, Nao; Middeldorp, Aart: Tyrolean termination tool: techniques and features (2007)
  13. Waldmann, Johannes: Weighted automata for proving termination of string rewriting (2007)
  14. Endrullis, Jörg; Waldmann, Johannes; Zantema, Hans: Matrix interpretations for proving termination of term rewriting (2006)
  15. Hofbauer, Dieter; Waldmann, Johannes: Termination of string rewriting with matrix interpretations (2006)
  16. Lucas, Salvador: Proving termination of context-sensitive rewriting by transformation (2006)
  17. Geser, Alfons; Hofbauer, Dieter; Waldmann, Johannes: Termination proofs for string rewriting systems via inverse match-bounds (2005)
  18. Geser, Alfons; Hofbauer, Dieter; Waldmann, Johannes; Zantema, Hans: Finding finite automata that certify termination of string rewriting (2005)
  19. Geser, Alfons; Hofbauer, Dieter; Waldmann, Johannes; Zantema, Hans: On tree automata that certify termination of left-linear term rewriting systems (2005)
  20. Giesl, Jürgen; Thiemann, René; Schneider-Kamp, Peter: Proving and disproving termination of higher-order functions (2005)

1 2 next