Abstract
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.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
Similar content being viewed by others
References
Dershowitz, N.: Termination of linear rewriting systems. In: Even, S., Kariv, O. (eds.) ICALP 1981. LNCS, vol. 115, pp. 448–458. Springer, Heidelberg (1981)
Dershowitz, N.: Termination of rewriting. J. Symbolic Comput. 3(1–2), 69–115 (1987)
Geser, A.: Decidability of Termination of Grid String Rewriting Rules. SIAM J. Comput. 31(4), 1156–1168 (2002)
Geser, A., Hofbauer, D., Waldmann, J.: Match-bounded string rewriting systems. In: Rovan, B., Vojtáš, P. (eds.) MFCS 2003. LNCS, vol. 2747, pp. 449–459. Springer, Heidelberg (2003)
Geser, A., Hofbauer, D., Waldmann, J.: Match-bounded string rewriting systems and automated termination proofs. In: Rubio, A. (ed.) Proc. 6th Int. Workshop on Termination WST-03, Technical Report DSIC-II/15/03, Universidad Politécnica de Valencia, Spain, pp. 19–22 (2003)
Geser, A., Hofbauer, D., Waldmann, J.: Match-bounded string rewriting systems. NIA Report 2003-09, National Institute of Aerospace, Hampton, VA, USA., Available at http://research.nianet.org/~geser/papers/nia-matchbounded.html
Geser, A., Hofbauer, D., Waldmann, J.: Termination proofs for string rewriting systems via inverse match-bounds. NIA Report 2003-XX, National Institute of Aerospace, Hampton, VA, USA., Available at http://research.nianet.org/~geser/papers/nia-inverse.html
Geser, A., Hofbauer, D., Waldmann, J.: Deciding Termination for Ancestor Match-Bounded String Rewriting Systems. submitted to RTA-04
Hibbard, T.N.: Context-limited grammars. J. ACM 21(3), 446–453 (1974)
Hofbauer, D., Waldmann, J.: Deleting string rewriting systems preserve regularity. In: Ésik, Z., Fülöp, Z. (eds.) DLT 2003. LNCS, vol. 2710, pp. 337–348. Springer, Heidelberg (2003)
Lankford, D.S., Musser, D.R.: A finite termination criterion. Technical Report, Information Sciences Institute, Univ. of Southern California, Marina-del-Rey, CA (1978)
Rahn, M., Waldmann, J.: The Leipzig autotool System for Grading Student Homework. In: Hanus, M., Krishnamurthi, S., Thompson, S. (eds.) Proc. Functional and Declarative Programming in Education FDPE-02. Technical Report No. 0210, Universitt Kiel (2002)
Ravikumar, B.: Peg-solitaire, string rewriting systems and finite automata. In: Leong, H.-V., Jain, S., Imai, H. (eds.) ISAAC 1997. LNCS, vol. 1350, pp. 233–242. Springer, Heidelberg (1997)
Zantema, H.: TORPA: Termination Of Rewriting Proved Automatically, version 1.2 (2004), Available at http://www.win.tue.nl/~hzantema/torpa.html
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2004 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Waldmann, J. (2004). Matchbox: A Tool for Match-Bounded String Rewriting. In: van Oostrom, V. (eds) Rewriting Techniques and Applications. RTA 2004. Lecture Notes in Computer Science, vol 3091. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-25979-4_6
Download citation
DOI: https://doi.org/10.1007/978-3-540-25979-4_6
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-22153-1
Online ISBN: 978-3-540-25979-4
eBook Packages: Springer Book Archive