The Community for Technology Leaders
2013 IEEE 54th Annual Symposium on Foundations of Computer Science (1991)
San Juan, Puerto Rico
Oct. 1, 1991 to Oct. 4, 1991
ISBN: 0-8186-2445-0
pp: 348-357
R.M. Verma , Dept. of Comput. Sci., Houston Univ., TX, USA
ABSTRACT
A general theory of using a congruence closure based simplifier (CCNS) proposed by P. Chew (1980) for computing normal forms is developed, and several applications are presented. An independent set of postulates is given, and it is proved that CCNS can be used for any system that satisfies them. It is then shown that CCNS can be used for consistent convergent systems and for various kinds of priority rewrite systems. A simple translation scheme for converting priority systems into effectively nonoverlapping convergent systems is presented.
INDEX TERMS
translation scheme, equational systems, congruence closure based simplifier, normal forms, consistent convergent systems, priority rewrite systems
CITATION
R.M. Verma, "A theory of using history for equational systems with applications", 2013 IEEE 54th Annual Symposium on Foundations of Computer Science, vol. 00, no. , pp. 348-357, 1991, doi:10.1109/SFCS.1991.185390
98 ms
(Ver 3.3 (11022016))