×

zbMATH — the first resource for mathematics

Orderings for term-rewriting systems. (English) Zbl 0525.68054

MSC:
68T15 Theorem proving (deduction, resolution, etc.) (MSC2010)
68W30 Symbolic computation and algebraic computation
68N01 General topics in the theory of software
Software:
NQTHM; REDUCE
PDF BibTeX XML Cite
Full Text: DOI
References:
[1] Ballantyne, A.M.; Bledsoe, W.W., Automatic proofs of theorems in analysis using nonstandard techniques, J. ACM, 24, 3, 353-374, (1977) · Zbl 0359.68109
[2] Boyer, R.S.; Moore, J.S., A lemma driven automatic theorem prover for recursive function theory, (), 511-519
[3] Carter, W.C.; Ellozy, H.A.; Joyner, W.H.; Leeman, G.B., Techniques for microprogram validation, ()
[4] Cohen, P.J., Decision procedures for real and p-adic fields, Comm. pure appl. math., 22, 2, 131-151, (1969) · Zbl 0167.01502
[5] Dershowitz, N., A note on simplification orderings, Information processing lett., 9, 5, 212-215, (1979) · Zbl 0433.68044
[6] Dershowitz, N.; Manna, Z., Proving termination with multiset orderings, Comm. ACM, 22, 8, 465-476, (1979) · Zbl 0431.68016
[7] Griesmer, J.H.; Jenks, R.D., SCRATCHPAD/1—an interactive facility for symbolic mathematics, (), 42-48
[8] Hearn, A.C., REDUCE 2—A system and language for algebraic manipulation, (), 128-133
[9] Huet, G., Confluent reductions: abstract properties and applications to term rewriting systems, J. ACM, 27, 4, 797-821, (1980) · Zbl 0458.68007
[10] Huet, G.; Lankford, D.S., On the uniform halting problem for term rewriting systems, ()
[11] Iturriaga, R., Contributions to mechanical mathematics, ()
[12] Kamin, S.; Levy, J.-J., Two generalizations of the recursive path orderings, (1980), Department of Computer Science, University of Illinois Urbana, IL, Unpublished note
[13] Knuth, D.E.; Bendix, P.B., Simple word problems in universal algebras, (), 263-297 · Zbl 0188.04902
[14] Kruskal, J.B., Well-quasi-ordering, the tree theorem, and Vazsonyi’s conjecture, Trans. amer. math. soc., 95, 210-225, (1960) · Zbl 0158.27002
[15] Lankford, D.S., Canonical algebraic simplification in computational logic, ()
[16] Lankford, D.S., On proving term rewriting systems are Noetherian, ()
[17] Lankford, D.S.; Ballantyne, A.M., Decision procedures for simple equational theories with permutative axioms: complete sets of permutative reductions, () · Zbl 0449.20059
[18] Lipton, R.J.; Snyder, L., On the halting of tree replacement systems, (), 43-46 · Zbl 0408.68046
[19] Manna, Z.; Ness, S., Proc. 3rd Hawaii International Conference on System Sciences, Honolulu, HI, On the termination of Markov algorithms, 789-792, (1970)
[20] Moses, J., Algebraic simplification, a guide for the perplexed, Comm. ACM, 14, 8, 527-537, (1971) · Zbl 0222.68017
[21] Musser, D.R., A data type verification system based on rewrite rules, (1978), Information Sciences Institute, University of Southern California Marina del Ray, CA, Memo
[22] Nash-Williams, C.St.J.A., On well-quasi-ordering finite trees, Proc. Cambridge philos. soc., 59, 833-835, (1963) · Zbl 0122.25001
[23] Plaisted, D., Well-founded orderings for proving termination of systems of rewrite rules, ()
[24] Plaisted, D., A recursively defined ordering for proving termination of term rewriting systems, ()
[25] Slagle, J.R., Automated theorem-proving for theories with simplifiers, commutativity and associativity, J. ACM, 21, 4, 622-642, (1974) · Zbl 0296.68092
[26] Stickel, M.E.; Peterson, G.E., Complete sets of reductions for some equational theories, J. ACM, 28, 2, 233-264, (1981) · Zbl 0479.68092
[27] Tarski, A., A decision method for elementary algebra and geometry, (1951), University of California Press Berkeley, CA · Zbl 0044.25102
[28] Weyhrauch, R.W., A users manual for FOL, ()
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. It attempts to reflect the references listed in the original paper as accurately as possible without claiming the completeness or perfect precision of the matching.