No CrossRef data available.
Article contents
Finding small counterexamples for abstract rewriting properties
Published online by Cambridge University Press: 25 July 2018
Abstract
Core share and HTML view are not available for this content. However, as you have access to this content, a full PDF is available via the 'Save PDF' action button.
Rewriting notions like termination, normal forms and confluence can be described in an abstract way referring to rewriting only as a binary relation. Several theorems on rewriting, like Newman's lemma, can be proved in this abstract setting. For investigating possible generalizations of such theorems, it is fruitful to have counterexamples showing that particular generalizations do not hold. In this paper, we develop a technique to find such counterexamples fully automatically, and we describe our tool Carpa that follows this technique. The basic idea is to fix the number of objects of the abstract rewrite system, and to express the conditions and the negation of the conclusion in a satisfiability (SAT) formula, and then call a current SAT solver. In case the formula turns out to be satisfiable, the resulting satisfying assignment yields a counterexample to the encoded property. We give several examples of finite abstract rewrite systems having remarkable properties that are found in this way fully automatically.
Information
- Type
- Paper
- Information
- Mathematical Structures in Computer Science , Volume 28 , Special Issue 8: Term and Graph Rewriting , September 2018 , pp. 1485 - 1505
- Copyright
- Copyright © Cambridge University Press 2018
References
Baader, F. and Nipkow, T. (1998). Term Rewriting and All That, Cambridge University Press.Google Scholar
Bachmair, L. and Dershowitz, N. (1986). Commutation, transformation and termination. In: Siekmann, J. (eds.) Proceedings of the 8th International Conference on Automated Deduction (CADE-8), Lecture Notes in Computer Science, vol. 230, Springer, 5–20.Google Scholar
Bellegarde, F. and Lescanne, P. (1990). Termination by completion. Applicable Algebra in Engineering, Communication and Computing 1 (2) 79–96.Google Scholar
Doornbos, H. and von Karger, B. (1998). On the union of well-founded relations. Logic Journal of the IGPL 6 (2) 195–201.Google Scholar
Dutertre, B. and de Moura, L. Yices: An SMT solver. Available at http://yices.csl.sri.com/.Google Scholar
Stump, A., Kimmell, G. and El Haj Omar, R. (2011). Type preservation as a confluence problem. In: Schmidt-Schauß, M. (ed.) Proceedings of the 22nd International Conference on Rewriting Techniques and Applications, LIPIcs, vol. 10, 345–360.Google Scholar
Stump, A., Kimmell, G., Zantema, H. and El Haj Omar, R. (2013). A rewriting view of simple typing. Logical Methods in Computer Science 9 (1).Google Scholar
Terese. (2003). Term Rewriting Systems, Cambridge Tracts in Theoretical Computer Science, vol. 55, Cambridge University Press.Google Scholar
van Oostrom, V. (1994). Confluence by decreasing diagrams, Theoretical Computer Science 126 (2) 259–280.Google Scholar
van Oostrom, V. (2008). Confluence by decreasing diagrams, converted. In: Voronkov, A. (ed.) Proceedings of the 19th Conference on Rewriting Techniques and Applications, Lecture Notes in Computer Science, vol. 5117, Springer, 306–320.Google Scholar
van Oostrom, V. and Zantema, H. (2012). Triangulation in rewriting. In: Tiwari, A. (eds.) Proceedings of the 23rd International Conference on Rewriting Techniques and Applications, volume 15 of Leibniz International Proceedings in Informatics (LIPIcs), Leibniz International Proceedings in Informatics (LIPIcs), vol. 15, Dagstuhl, Germany, Schloss Dagstuhl–Leibniz-Zentrum für Informatik, 240–255.Google Scholar
Zantema, H. (2013). Automatically finding particular term rewriting systems. Available via http://www.win.tue.nl/~hzantema/carpa.html.Google Scholar
You have
Access
- 1
- Cited by