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; Jambox; MU-TERM; CeTA; Isabelle/HOL; TPA; TPDB; Maude; OBJ3; CoLoR; MiniSat; Chaff; Tsukuba; term-rewriting; GitHub; SeaHorn Cited in: 23 Publications all top 5 Cited by 24 Authors 7 Waldmann, Johannes 5 Hofbauer, Dieter 5 Middeldorp, Aart 5 Zantema, Hans 4 Geser, Alfons 4 Sternagel, Christian 3 Lucas, Salvador 3 Thiemann, René 2 Giesl, Jürgen 2 Korp, Martin 2 Zankl, Harald 1 Aschermann, Cornelius 1 Endrullis, Jörg 1 Frohn, Florian 1 Gutiérrez, Raúl 1 Hensel, Jera 1 Hirokawa, Nao 1 Hogg, Jonathan D. 1 Meseguer Guaita, José 1 Payet, Étienne 1 Schneider-Kamp, Peter 1 Scott, Jennifer A. 1 Sternagel, Thomas 1 Ströder, Thomas all top 5 Cited in 6 Serials 5 Information and Computation 4 Journal of Automated Reasoning 1 Theoretical Computer Science 1 Numerical Linear Algebra with Applications 1 Annals of Mathematics and Artificial Intelligence 1 Journal of Automata, Languages and Combinatorics Cited in 4 Fields 22 Computer science (68-XX) 1 Mathematical logic and foundations (03-XX) 1 Combinatorics (05-XX) 1 Numerical analysis (65-XX) Citations by Year