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.

Keywords for this software

Anything in here will be replaced on browsers that support the canvas element

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