|
 REFERENCES
Note: OCR errors may be found in this Reference List extracted from the full text article. ACM has opted to expose the complete List rather than only correct and linked references.
| |
1
|
AHO, A., SETHI, R, ULLIman J. Code optimtzaUon and fmite Church-Rosser systems In Proceedmgs of Courant Computer Science Symposmm 5, R Rustm, Ed., Prenuce Hall, Englewood Cliffs, N.J, 1972, pp 89-105
|
| |
2
|
BROWN, T Structured design method for specialized proof p~ocedures Ph D Thesis, Cahforma lnsutute of TechnolOgy, Pasadena, Calif., 1975
|
| |
3
|
BURSTALL, R Provmg properties of programs by structural induction Comput J. 12 (1969), 41-48
|
| |
4
|
CHURCH, A., AND ROSSER, J.B. Some properues of conversion. Trans. AMS 39 (1936), 472-482.
|
| |
5
|
COHIN, P M Universal algebra. Harper and Row, New York, 1965.
|
| |
6
|
CURRY, H B., AND FEYS, R Combmatory Logic, Vol 1 North Holland, Amsterdam, 1958
|
 |
7
|
|
| |
8
|
|
| |
9
|
HINDLEY,R An abstract Church-Rosser theorem Pt 1, J Symbohc Logic 34 (1969), 545-560, Pt 2, J Symbohc Logic 39 (1974), 1-21.
|
| |
10
|
HINDLEY, R, LERCHER, B., AND SELDIN, J.P.Introduction to combmatory logxc In London Mathemaucal Society Lecture Notes 7, Cambridge Umversity Press, Cambridge, England, 1972
|
| |
11
|
HUET, G. Experiments w,th an mteracttve prover for log,c with equahty Rep. i106, Jennmgs Computmg Center, Case Western Reserve Umv, Cleveland, Ohio, 1970.
|
| |
12
|
Hue~r, G REsolut,on d'6quauons dans des langages d'ordre 1, 2 ....These d'Etat, Umv Pans VII, Parts, Sept 1976.
|
| |
13
|
HUET, G, AND LANKFORD, D.S On the uniform haltmg problem for term rewrmng systems Lab Rep No 283, INRIA, Le Chesnay, France, March 1978
|
| |
14
|
HUET, G., AND LI~vY, J J. Call by need computat,ons m non-amb,guous hnear term rewritmg systems. Lab. Rep. No. 359, INRIA, Le Chesnay, France, Aug. 1979
|
| |
15
|
KLOP, J W A counter example to the Church-Rosser property for lambda calculus with subjecuve pamng Preprint No 102, Dep of Mathematics, Umv. of Utrecht, Utrecht, The Netherlands, 1978.
|
| |
16
|
KNUTH, D., AND BENDIX, P. Simple word problems m umversal algiebras In Computatwnal Problems in Abstract Algebra, J Leech, Ed., Pergamon Press, Elmsford, N.Y, 1970, pp. 263-297
|
| |
17
|
LANKFORD, DS. Canonical mference Rep ATP-25, Dep. Mathemat,cs and Computer Sc,ences, Un,v. of Texas, Austin, Texas, Dec 1975
|
| |
18
|
LANKFORD, D S., AND BALLANTYNE, A.M Dec,slon procedures for s,mple equauonal theories w,th cornmutatlve axioms" Complete sets of commutative reductions. Rep. ATP-35, Dep. Mathemaucs and Computer Sciences, Umv of Texas, Ausun, Texas, March 1977
|
| |
19
|
LANKFORD, D.S, AND BALLANTYNE, A M. Decision procedures for simple equauonal theories w,th permutattve ax,oms' Complete sets of permutat,ve reduct,ons Rep. ATP-37, Dep. of Mathemat,cs and Computer Sc,ences, Umv of Texas, Austm, Texas, Apnl 1977
|
| |
20
|
LANKFORD, D.S, AND BALLANTYNE, A.M Dec,s,on procedures for s,mple equational theories w,th cornmutative-assoctat,ve axioms: Complete sets of commutattve-assooattve reductions Rep ATP-39, Dep Mathemaucs and Computer Sciences, Untv. of Texas, Austin, Texas, Aug. 1977.
|
| |
21
|
LIPTON, R.J, AND SNYDER, L On the hal,mR of tree replacement systems Proc of Waterloo Conf. on Theoret,cal Computer Sc,ence, Univ of Waterloo, Waterloo, Ontario, Aug 1977, pp 43--46
|
| |
22
|
MANNA, Z., AND NESS, S. On the term,nat,on of Markov algorithms. Proc 3rd Hawau Int. Conf. on System Sc,ences, Jan. 1970, pp. 789-792.
|
| |
23
|
NEWMAN, M.H A On theories wtth a comb,atonal definmon of "eqmvalence" Ann Math, 43 (1942), 223-243
|
| |
24
|
|
| |
25
|
|
| |
26
|
PETERSON, G E, AND STICKEL, M E Complete sets of reduct,ons for equational theories w,th complete unification algonthms Tech. Rep., Dep. of Computer Sc,ence, Umv. of Arizona, Tucson, Ariz., Sept 1977.
|
| |
27
|
PLAISTED, D. Well-founded ordermgs for provmg termmatton of systems of rewnte rules Tech Rep. 78- 932, Dep. of Computer Science, Umv. of Ill,no,s, Urbana-Champalgn, 111, July 1978.
|
| |
28
|
PLAISTED, D.A recurs~vely defined ordermg for proving term,at,on of term rewriting systems Tech. Rep 78-943, Dep of Computer Science, Umv of Ill,no,s, Urbana-Champa,gn, 111, Sept 1978
|
| |
29
|
PLOTKIN, G Lattice-theoretic properties ofsubsumption Memo MIP-R77, Univ. of Edinburgh, Edinburgh, Scotland, 1970
|
| |
30
|
PLOTKIN G. Buddmg-m equational theories In Machine intelhgence 7, B. Meltzer and D. Michie, Eds., American Elscwer, New York, 1972, pp 73-90
|
| |
31
|
REYNOLDS, J Transformational systems and the algebraic structure of atomzc formulas. In Machine Intelhgence 5, B Meltzer and D Michie, Eds, American Elsevier, New York, 1970, pp. 135-152.
|
| |
32
|
|
| |
33
|
|
| |
34
|
|
| |
35
|
|
| |
36
|
STAPLES, J Church-Rosser theorems for replacement systems In Algebra and Logic, J. Crossley, Ed., Lecture Notes m Mathematics No 450, Sprmger-Verlag, 1975
|
CITED BY 92
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
Alexander Aiken , Jennifer Widom , Joseph M. Hellerstein, Behavior of database production rules: termination, confluence, and observable determinism, ACM SIGMOD Record, v.21 n.2, p.59-68, June 1, 1992
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
Nachum Dershowitz , S. Kaplan, Rewrite, rewrite, rewrite, rewrite, rewrite..., Proceedings of the 16th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.250-259, January 11-13, 1989, Austin, Texas, United States
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
K. Blasius , N. Fisinger , J. Siekmann , G. Smolka , A. Herold , C. Walther, The Markgraf Karl refutation procedure, Proceedings of the 7th international joint conference on Artificial intelligence, p.511-518, August 24-28, 1981, Vancouver, BC, Canada
|
|
|
C. Kirchner , H. Kirchner , J. P. Jouannaud, Algebraic manipulations as a unification and matching strategy for linear equations in signed binary trees: application to LISP program synthesis and derecursivation, Proceedings of the 7th international joint conference on Artificial intelligence, p.1016-1023, August 24-28, 1981, Vancouver, BC, Canada
|
|
|
|
|
|
|
|
|
|
|
Adobe Acrobat
QuickTime
Windows Media Player
Real Player
Pdf
F.4