% Chew's theorem.
@INPROCEEDINGS{Chew:81,
    AUTHOR = "P. Chew",
    TITLE = "Unique normal forms in term rewriting systems with repeated 
		variables",
    BOOKTITLE = "Proc. the 13th ACM STOC",
    YEAR = 1981,
    PAGES = "7--18",
    }

% UN of CL + PC
@TECHREPORT{deVrijer:90,
    AUTHOR = "R. C. de Vrijer",
    TITLE = "Unique normal forms for combinatory logic with parallel 
		conditional, a case study in conditional rewriting",
    INSTITUTION = "Institute for Language, Logic and Information,
		  University of Amsterdam",
    NUMBER = "CT-90-09",
    YEAR = 1990
    }

% Incomplete proof
@INPROCEEDINGS{Ogawa:92,
    AUTHOR = "M. Ogawa",
    TITLE = "Chew's theorem revisited - uniquely normalizing property of 
             non-linear term rewriting systems",
    BOOKTITLE = "Proc. the International symposium on algorithms and 
	computation",
    PAGES = "309--318",
    YEAR = 1992,
    NOTE = "LNCS 650"
    }


@MISC{OpenProblems, 
    Title = "Open Problems in Rewriting", 
    HOWPUBLISHED = "http://www.lri.fr/~rtaloop/index.html"
    }

% Problem 79 was posed. 
@TECHREPORT{Mizuhito:89,
    AUTHOR = "M. Ogawa and S. Ono",
    TITLE = "On the Uniquely Converging Property of Nonlinear Term 
             Rewriting Systems",
    INSTITUTION = "IEICE COMP89-7",
    YEAR = 1989
    }

% Unification with infinite terms
@INPROCEEDINGS{Martelli:84,
    AUTHOR = "A. Martelli and G. Rossi",
    TITLE = "Efficient unification with infinite terms in logic programming",
    BOOKTITLE = "the International conference on fifth generation computer 
                 systems",
    YEAR = 1984,
    PAGES = "202--209",
    }


% A non-$E$-overlapping and non-duplicating TRS is UN. Furthermore,
% A non-$E$-overlapping and right-ground TRS is CR. 
% The statement, a non-$E$-overlapping and right-linear TRS is CR, has a gap.
% (Corollary 3)
@INPROCEEDINGS{ToyamaOyamaguchi:94,
    AUTHOR = "Y. Toyama and M. Oyamaguchi",
    TITLE = "Church-{R}osser property and unique normal form property of 
             non-duplicating term rewriting systems",
    BOOKTITLE = "Proc. the 4th CTRS",
    YEAR = 1994,
    PAGES = "316--331", 
    NOTE = "LNCS 968"
    }


% A non-$E$-overlapping and right-ground TRS is CR. 
@ARTICLE{OyamaguchiOhta:93,
    AUTHOR = "M. Oyamaguchi and Y. Ohta",
    TITLE = "On the confluent property of right-ground term rewriting 
             systems",
    JOURNAL = "Trans. IEICE",
    VOLUME = "76-D-I",
    NUMBER = 2,
    PAGES = "39--45",
    YEAR = 1993, 
    Note = "({\it in Japanese})"
    }

% A non-$E$-overlapping and simple-right-linear TRS is CR. See Problem 58. 
@ARTICLE{OyamaguchiOhtaToyama:95,
    AUTHOR = "M. Oyamaguchi and Y. Ohta and Y. Toyama",
    TITLE = "On the confluent property of simple-right-linear term rewriting
        systems",
    JOURNAL = "Trans. IEICE",
    VOLUME = "78-D-I",
    NUMBER = 3,
    PAGES = "263--268",
    YEAR = 1995,
    NOTE = "({\it in Japanese})"
    }


% A non-$E$-overlapping and strongly depth-preserving TRS is CR. 
@ARTICLE{GomiOyamaguchiOhta:96a,
    AUTHOR = "H. Gomi and M. Oyamaguchi and Y. Ohta",
    TITLE = "On  the  Church-Rosser property of non-E-overlapping and strongly
	depth-preserving term rewriting systems", 
    JOURNAL = "Trans. IPSJ",
    VOLUME = 37, 
    NUMBER = 12, 
    PAGES = "2147--2160",
    YEAR = 1996
    }

% A non-$E$-overlapping and strongly depth-preserving TRS is CR. 
@TECHREPORT{GomiOyamaguchiOhta:96b,
    AUTHOR = "H. Gomi and M. Oyamaguchi and Y. Ohta",
    TITLE = "On  the  Church-Rosser property of non-E-overlapping and 
	weight-preserving TRS's", 
    INSTITUTION = "RIMS Research Report", 
    NUMBER = 950, 
    PAGES = "167--173", 
    YEAR = 1996
    }

% Include GomiOyamaguchiOhta:96b. 
@ARTICLE{GomiOyamaguchiOhta:98,
    AUTHOR = "H. Gomi and M. Oyamaguchi and Y. Ohta",
    TITLE = "On  the  Church-Rosser property of root-E-overlapping and strongly
	depth-preserving term rewriting systems", 
    JOURNAL = "Trans. IPSJ",
    VOLUME = 39, 
    NUMBER = 4, 
    PAGES = "992--1005",
    YEAR = 1998
    }


% A non-$\omega$-overlapping and depth-preserving TRS is non-$E$-overlapping.
@ARTICLE{MatsuuraOyamaguchiOhtaOgawa:98,
    AUTHOR = "K. Matsuura and M. Oyamaguchi and Y. Ohta and M. Ogawa",
    TITLE = "On the E-overlapping property of nonlinear term rewriting 
	systems", 
    JOURNAL = "Trans. IEICE",
    VOLUME = "80 D-I", 
    NUMBER = 11,  
    PAGES = "847--855",
    YEAR = 1997, 
    NOTE = "({\it in Japanese})"
    }



% Persistence (wrt reduction), weaker than non-$E$-overlapping (wrt conversion)
% Key Claim 8 (pp.365) is suspicious.
@INPROCEEDINGS{Verma:95, 
    AUTHOR = "R.M. Verma", 
    TITLE = "Unique Normal Forms and Confluence of Rewrite Systems: 
	Persistence", 
    BOOKTITLE = "Proc. IJCAI-95", 
    YEAR = 1995,
    PAGES = "362--368", 
    VOLUME = 1
    }

% Gap in Key lemma 6. A non-$\omega$-overlapping and non-duplicating TRS is UN.
@INPROCEEDINGS{Verma:97, 
    AUTHOR = "R.M. Verma", 
    TITLE = "Unique Normal Forms for Nonlinear Term Rewriting Systems:
	Root Overlaps", 
    BOOKTITLE = "Proc. Fundamentals of Computation Theory, FCT'97", 
    YEAR = 1997,
    PAGES = "452--462", 
    NOTE = "LNCS 1279"
    }


% Higher-order rewrite systems, Lambda calculus with nonlinear rules
% Counter example to CR, UN of Lambda with D.
@MISC{KlopThesis:80,
    TITLE = "Combinatory reduction systems",
    AUTHOR = "J. W. Klop",
    NOTE = "Mathematical Centre Tracts Nr.127, Centre for Mathematics
	    and Computer Science, Amsterdam, 1980.",
    }

% UN of Lambda with surjective pairing.
@ARTICLE{KlopVrijer:89,
    AUTHOR = "J. W. Klop and R. C. de Vrijer",
    TITLE = "Unique normal forms for lambda calculus with surjective pairing",
    JOURNAL = "Information and Computation",
    VOLUME = 80,
    PAGES = "97--113",
    YEAR = 1989
    }

% Conservative extension of Lambda with surjective pairing.
@INPROCEEDINGS{deVrijer:89,
    AUTHOR = "R. C. de Vrijer",
    TITLE = "Extending the Lambda calculus with Surjective Pairing 
                is Conservative", 
    BOOKTITLE = "Proc. the 4th IEEE LICS", 
    YEAR = 1989,
    PAGES = "204--215"
    }

% Extension of Klop's non-CR examples of lambda calculus + Dxx -> M rules.
@ARTICLE{Bunder:85, 
    AUTHOR = "Bunder, M.W.", 
    TITLE = "An extension of {K}lop's counterexample to the {C}hurch-{R}osser
	property to $lambda$-calculus with other ordered pair combinators", 
    JOURNAL = "Theoretical Computer Science",
    VOLUME = 39,
    NUMBER = 2,
    PAGES = "337--342",
    YEAR = 1985
    }

% Yet another counter exmaple of CR. 
@ARTICLE{CurienHardin:94,
    AUTHOR = "P.-L. Curien and T. Hardin",
    TITLE = "Theoretical Pearl: {Y}et yet a counterexample for $\lambda + SP$",
    JOURNAL = "Journal of Functional Programming",
    VOLUME = 4,
    NUMBER = 1,
    PAGES = "113--115",
    YEAR = 1994
    }