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.
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.
F. Baader & T. Nipkow (1998):
Term Rewriting and All That.
Cambridge University Press.
M. Bezem, J.W. Klop & R. de Vrijer (2003):
Term Rewriting Systems by TeReSe.
Cambridge Tracts in Theoretical Computer Science 55.
Cambridge University Press.
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.
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.
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.
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.
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..
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.
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.
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.
R. Thiemann (2012):
Certification of Confluence Proofs using CeTA.
In: First International Workshop on Confluence (IWC 2012),
pp. 45.
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 http://shemesh.larc.nasa.gov/fm/ftp/larc/ PVS-library/pvslib.html.
eptcs@eptcs.org