Gérard Huet
- 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-105Google Scholar
- 2 BROWN, T Structured design method for specialized proof p~ocedures Ph D Thesis, Cahforma lnsutute of TechnolOgy, Pasadena, Calif., 1975Google Scholar
- 3 BURSTALL, R Provmg properties of programs by structural induction Comput J. 12 (1969), 41-48Google Scholar
- 4 CHURCH, A., AND ROSSER, J.B. Some properues of conversion. Trans. AMS 39 (1936), 472-482.Google Scholar
- 5 COHIN, P M Universal algebra. Harper and Row, New York, 1965.Google Scholar
- 6 CURRY, H B., AND FEYS, R Combmatory Logic, Vol 1 North Holland, Amsterdam, 1958Google Scholar
- 7 DERSHOWITZ, N, AND MANNA, Z Provmg termination with multiset ordermgs Commun A CM 22, 8 (Aug. 1979), 465-476 Google Scholar
- 8 GUARD, J R, OGLi~SBY, F.C, BE~qNETT, J.H., AND SETTLE, L.G. Sem,-automated mathemattcs J. ACM 16 (1969), 49-62. Google Scholar
- 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.Google Scholar
- 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, 1972Google Scholar
- 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.Google Scholar
- 12 Hue~r, G REsolut,on d'6quauons dans des langages d'ordre 1, 2 ..These d'Etat, Umv Pans VII, Parts, Sept 1976.Google Scholar
- 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 1978Google Scholar
- 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. 1979Google Scholar
- 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.Google Scholar
- 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-297Google Scholar
- 17 LANKFORD, DS. Canonical mference Rep ATP-25, Dep. Mathemat,cs and Computer Sc,ences, Un,v. of Texas, Austin, Texas, Dec 1975Google Scholar
- 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 1977Google Scholar
- 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 1977Google Scholar
- 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.Google Scholar
- 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--46Google Scholar
- 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.Google Scholar
- 23 NEWMAN, M.H A On theories wtth a comb,atonal definmon of "eqmvalence" Ann Math, 43 (1942), 223-243Google Scholar
- 24 NIVAT, M. Congruences parfa,tes et quas,-parfa,tes Sdmmmre Dubreud 7, 1971-72, see also prehmmary version- On some famthes of languages related to the Dyck language. Proc 2nd Ann, ACM Syrup on Theory of Computmg, Northampton, Mass., Ma3~ 1970, pp. 221-225 Google Scholar
- 25 PATERSON, M.S., AND WEGMAN, M N Lmear umficauon Proc 8th Ann ACM Symp. on Theory of Computmg, Hershey, Pa, May 1976, pp. 181-186. Google Scholar
- 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.Google Scholar
- 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.Google Scholar
- 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 1978Google Scholar
- 29 PLOTKIN, G Lattice-theoretic properties ofsubsumption Memo MIP-R77, Univ. of Edinburgh, Edinburgh, Scotland, 1970Google Scholar
- 30 PLOTKIN G. Buddmg-m equational theories In Machine intelhgence 7, B. Meltzer and D. Michie, Eds., American Elscwer, New York, 1972, pp 73-90Google Scholar
- 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.Google Scholar
- 32 ROBINSON, J. A. A machine-oriented 16gic based on the resoluuon principle J. ACM 12, 1 (Jan. 1965), 23- 41 Google Scholar
- 33 ROSEN, B K. Tree-mampulatmg systems and Church-Rosser theorems J. ACM 20, I (Jan. 1973), 160--187 Google Scholar
- 34 SETHI, R Testing for the Church-Rosscr property J ACM 21, 4 (Oct 1974), 671-679, Errata, J. ACM 22, 3 (July 1975), 424 Google Scholar
- 35 SLAGLE, J R Automated theorem-proving for theories with simphfiers, commutattvity, and associativity. J ACM 21, 4 (Oct 1974), 622-642 Google Scholar
- 36 STAPLES, J Church-Rosser theorems for replacement systems In Algebra and Logic, J. Crossley, Ed., Lecture Notes m Mathematics No 450, Sprmger-Verlag, 1975Google Scholar
Index Terms
- Confluent Reductions: Abstract Properties and Applications to Term Rewriting Systems: Abstract Properties and Applications to Term Rewriting Systems
Recommendations
Confluent term rewriting systems
RTA'05: Proceedings of the 16th international conference on Term Rewriting and ApplicationsThe confluence property is one of the most important properties of term rewriting systems, and various sufficient criteria for proving this property have been widely investigated. A necessary and sufficient criterion for confluence of terminating term ...
The unification problem for confluent right-ground term rewriting systems
RTA 2001The unification problem for term rewriting systems (TRSs) is the problem of deciding, for a given TRS R and two terms M and N, whether there exists a substitution θ such that Mθ and Nθ are congruent modulo R (i.e., Mθ ↔R* Nθ). In this paper, the ...
The Unification Problem for Confluent Right-Ground Term Rewriting Systems
RTA '01: Proceedings of the 12th International Conference on Rewriting Techniques and ApplicationsThe unification problem for term rewriting systems(TRSs) is the problem of deciding, for a given TRS R and two terms M and N, whether there exists a substitution θ such that Mθ and Nθ are congruent modulo R (i.e., Mθ ↔R* Nθ). In this paper, the ...
Comments