1. Arvind & X. Shen (1999): Using Term Rewriting Systems to Design and Verify Processors. IEEE Micro 19(3), pp. 36–46, doi:10.1109/40.768501.
  2. M. Ayala-Rincón, C. Llanos, R. P. Jacobi & R. W. Hartenstein (2006): Prototyping Time and Space Efficient Computations of Algebraic Operations over Dynamically Reconfigurable Systems Modeled by Rewriting-Logic. ACM Trans. Design Autom. Electr. Syst. 11(2), pp. 251–281, doi:10.1145/1142155.1142156.
  3. F. Baader & T. Nipkow (1998): Term Rewriting and All That. Cambridge University Press.
  4. M. Bezem, J.W. Klop & R. de Vrijer (2003): Term Rewriting Systems by TeReSe. Cambridge Tracts in Theoretical Computer Science 55. Cambridge University Press.
  5. A. L. Galdino & M. Ayala-Rincón (2008): A Formalization of Newman's and Yokouchi Lemmas in a Higher-Order Language. Journal of Formalized Reasoning 1(1), pp. 39–50.
  6. A. L. Galdino & M. Ayala-Rincón (2009): A PVS Theory for Term Rewriting Systems. In: Proceedings of the Third Workshop on Logical and Semantic Frameworks, with Applications - LSFA 2008, Electronic Notes in Theoretical Computer Science 247, pp. 67–83, doi:10.1016/j.entcs.2009.07.049.
  7. A. L. Galdino & M. Ayala-Rincón (2010): A Formalization of the Knuth-Bendix(-Huet) Critical Pair Theorem. J. of Automated Reasoning 45(3), pp. 301–325, doi:10.1007/s10817-010-9165-2.
  8. G. Huet (1980): Confluent Reductions: Abstract Properties and Applications to Term Rewriting Systems. Journal of the Association for Computing Machinery 27(4), pp. 797–821, doi:10.1145/322217.322230.
  9. D. E. Knuth & P. B. Bendix (1970): Computational Problems in Abstract Algebra, chapter Simple Words Problems in Universal Algebras, pp. 263–297. J. Leech, ed. Pergamon Press, Oxford, U. K..
  10. C. Morra, J. Becker, M. Ayala-Rincón & R. W. Hartenstein (2005): FELIX: Using Rewriting-Logic for Generating Functionally Equivalent Implementations. In: 15th Int. Conference on Field Programmable Logic and Applications - FPL 2005. IEEE CS, pp. 25–30, doi:10.1109/FPL.2005.1515694.
  11. C. Morra, J. Bispo, J.M.P. Cardoso & J. Becker (2008): Combining Rewriting-Logic, Architecture Generation, and Simulation to Exploit Coarse-Grained Reconfigurable Architectures. In: Kenneth L. Pocek & Duncan A. Buell: FCCM. IEEE Computer Society, pp. 320–321, doi:10.1109/FCCM.2008.37.
  12. B. K. Rosen (1973): Tree-Manipulating Systems and Church-Rosser Theorems. J. of the ACM 20(1), pp. 160–187, doi:10.1145/321738.321750.
  13. R. Thiemann (2012): Certification of Confluence Proofs using CeTA. In: First International Workshop on Confluence (IWC 2012), pp. 45.
  14. Theory trs (consulted January 2013): Available in the NASA LaRC PVS library, 9118\p@ plus2\p@ minus4\p@ \z@ plus\p@ 4\p@ plus2\p@ minus2\p@ \defłeftmarginłeftmargini 2.5\p@ plus1.5\p@ minus\p@ 5\p@ plus2\p@ minus5\p@ıtemsep 2.5\p@ plus1.5\p@ minus\p@łeftmarginłeftmargini 4\p@ plus2\p@ minus2\p@ 2\p@ plus\p@ minus\p@ıtemsep PVS-library/pvslib.html.

Comments and questions to:
For website issues: