Welcome to ReSMT’s documentation!¶
This Python 3 library comprises a collection of algorithms realizing an implementation of compositional rewriting theories (in the sense of 1) based upon a “translation-based” approach (in the sense of 2), and is part of an ongoing work in progress with M. Ghaffari Saadat and R. Heckel (U Leicester). The main motivation for this work consisted in the desire to experiment with the Microsoft Z3 Theorem Prover as a computational core for rewriting-theoretic algorithms, with the “translation-based” approach consisting in translating both categorical data structures as well as the rewriting-theoretic concepts into a format accessible to Z3. For further conceptual and technical details on this work, please refer to our recent preprint “Efficient Computation of Graph Overlaps for Rule Composition: Theory and Z3 Prototyping” 3.
- 1
N. Behr, “Tracelets and Tracelet Analysis Of Compositional Rewriting Systems” (accepted for ACT 2019 in Oxford), 2019, arXiv: 1904.12829 [cs.LO].
- 2
R. Heckel, L. Lambers and M.G. Saadat, “Analysis of Graph Transformation Systems: Native Vs Translation-Based Techniques.”, Electronic Proceedings in Theoretical Computer Science 309 (2019) , pp. 1–22.
- 3
N. Behr, M. Ghaffari Saadat and R. Heckel, “Efficient Computation of Graph Overlaps for Rule Composition: Theory and Z3 Prototyping” (contained in the pre-proceedings of the GCM 2020: Eleventh International Workshop on Graph Computation Models)