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 25 articles )

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

1 2 next

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

1 2 next