Matchbox
swMATH ID: | 10115 |
Software Authors: | Waldmann, J. |
Description: | 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. |
Homepage: | http://link.springer.com/chapter/10.1007/978-3-540-25979-4_6 |
Source Code: | https://github.com/jwaldmann/matchbox/ |
Related Software: | AProVE; Tyrolean; Haskell; TORPA; CiME; TPDB; Jambox; MiniSat; Chaff; Isabelle/HOL; MU-TERM; CeTA; TPA; Nagoya Termination Tool; GitHub; Maude; OBJ3; CoLoR; Tsukuba; Sugar |
Cited in: | 25 Documents |
all
top 5
Cited by 27 Authors
all
top 5
Cited in 6 Serials
Cited in 4 Fields
24 | Computer science (68-XX) |
1 | Mathematical logic and foundations (03-XX) |
1 | Combinatorics (05-XX) |
1 | Numerical analysis (65-XX) |