Blanqui, Frédéric Size-based termination of higher-order rewriting. (English) Zbl 1476.68048 J. Funct. Program. 28, Paper No. e11, 75 p. (2018). MSC: 68N18 68Q42 PDFBibTeX XMLCite \textit{F. Blanqui}, J. Funct. Program. 28, Paper No. e11, 75 p. (2018; Zbl 1476.68048) Full Text: DOI arXiv
Yamada, Akihisa; Winkler, Sarah; Hirokawa, Nao; Middeldorp, Aart AC-KBO revisited. (English) Zbl 1379.68277 Theory Pract. Log. Program. 16, No. 2, 163-188 (2016). MSC: 68T15 06A06 68Q42 PDFBibTeX XMLCite \textit{A. Yamada} et al., Theory Pract. Log. Program. 16, No. 2, 163--188 (2016; Zbl 1379.68277) Full Text: DOI
Bensaid, Hicham; Peltier, Nicolas A complete superposition calculus for primal grammars. (English) Zbl 1332.68201 J. Autom. Reasoning 53, No. 4, 317-350 (2014). MSC: 68T15 03B35 68Q42 PDFBibTeX XMLCite \textit{H. Bensaid} and \textit{N. Peltier}, J. Autom. Reasoning 53, No. 4, 317--350 (2014; Zbl 1332.68201) Full Text: DOI
Winkler, Sarah; Sato, Haruhiko; Middeldorp, Aart; Kurihara, Masahito Multi-completion with termination tools. (English) Zbl 1362.68253 J. Autom. Reasoning 50, No. 3, 317-354 (2013). MSC: 68T15 68Q42 PDFBibTeX XMLCite \textit{S. Winkler} et al., J. Autom. Reasoning 50, No. 3, 317--354 (2013; Zbl 1362.68253) Full Text: DOI
Codish, Michael; Giesl, Jürgen; Schneider-Kamp, Peter; Thiemann, René SAT solving for termination proofs with recursive path orders and dependency pairs. (English) Zbl 1276.68140 J. Autom. Reasoning 49, No. 1, 53-93 (2012). MSC: 68T20 68Q42 PDFBibTeX XMLCite \textit{M. Codish} et al., J. Autom. Reasoning 49, No. 1, 53--93 (2012; Zbl 1276.68140) Full Text: DOI
Fuhs, Carsten; Giesl, Jürgen; Parting, Michael; Schneider-Kamp, Peter; Swiderski, Stephan Proving termination by dependency pairs and inductive theorem proving. (English) Zbl 1243.68267 J. Autom. Reasoning 47, No. 2, 133-160 (2011). MSC: 68T15 68Q42 PDFBibTeX XMLCite \textit{C. Fuhs} et al., J. Autom. Reasoning 47, No. 2, 133--160 (2011; Zbl 1243.68267) Full Text: DOI
Winkler, Sarah; Middeldorp, Aart AC completion with termination tools. (English) Zbl 1341.68198 Bjørner, Nikolaj (ed.) et al., Automated deduction – CADE-23. 23rd international conference on automated deduction, Wrocław, Poland, July 31 – August 5, 2011. Proceedings. Berlin: Springer (ISBN 978-3-642-22437-9/pbk; 978-3-642-22438-6/ebook). Lecture Notes in Computer Science 6803. Lecture Notes in Artificial Intelligence, 492-498 (2011). MSC: 68T15 68Q42 PDFBibTeX XMLCite \textit{S. Winkler} and \textit{A. Middeldorp}, Lect. Notes Comput. Sci. 6803, 492--498 (2011; Zbl 1341.68198) Full Text: DOI
Lucas, Salvador Automatic proofs of termination with elementary interpretations. (English) Zbl 1294.68058 Lucio, Paqui (ed.) et al., Proceedings of the 9th Spanish conference on programming and computer languages (PROLE 2009), San Sebastián, Spain, September 9–11, 2009. Amsterdam: Elsevier. Electronic Notes in Theoretical Computer Science 258, No. 1, 41-61 (2009). MSC: 68N30 68Q42 68Q60 PDFBibTeX XMLCite \textit{S. Lucas}, Electron. Notes Theor. Comput. Sci. 258, No. 1, 41--61 (2009; Zbl 1294.68058) Full Text: DOI
Durán, Francisco; Lucas, Salvador; Meseguer, José Termination modulo combinations of equational theories. (English) Zbl 1193.68145 Ghilardi, Silvio (ed.) et al., Frontiers of combining systems. 7th international symposium, FroCoS 2009, Trento, Italy, September 16–18, 2009. Proceedings. Berlin: Springer (ISBN 978-3-642-04221-8/pbk). Lecture Notes in Computer Science 5749. Lecture Notes in Artificial Intelligence, 246-262 (2009). MSC: 68Q42 PDFBibTeX XMLCite \textit{F. Durán} et al., Lect. Notes Comput. Sci. 5749, 246--262 (2009; Zbl 1193.68145) Full Text: DOI Link
Waldmann, Johannes Automatic termination. (English) Zbl 1242.68143 Treinen, Ralf (ed.), Rewriting techniques and applications. 20th international conference, RTA 2009, Brasília, Brazil, June 29–July 1, 2009. Proceedings. Berlin: Springer (ISBN 978-3-642-02347-7/pbk). Lecture Notes in Computer Science 5595, 1-16 (2009). MSC: 68Q42 68Q45 68T15 PDFBibTeX XMLCite \textit{J. Waldmann}, Lect. Notes Comput. Sci. 5595, 1--16 (2009; Zbl 1242.68143) Full Text: DOI
Lucas, Salvador On the relative power of polynomials with real, rational, and integer coefficients in proofs of termination of rewriting. (English) Zbl 1103.68061 Appl. Algebra Eng. Commun. Comput. 17, No. 1, 49-73 (2006). MSC: 68Q42 03B70 PDFBibTeX XMLCite \textit{S. Lucas}, Appl. Algebra Eng. Commun. Comput. 17, No. 1, 49--73 (2006; Zbl 1103.68061) Full Text: DOI
Marché, Claude; Urbain, Xavier Modular and incremental proofs of AC-termination. (English) Zbl 1137.68419 J. Symb. Comput. 38, No. 1, 873-897 (2004). MSC: 68Q42 68W30 PDFBibTeX XMLCite \textit{C. Marché} and \textit{X. Urbain}, J. Symb. Comput. 38, No. 1, 873--897 (2005; Zbl 1137.68419) Full Text: DOI
Contejean, Evelyne; Marché, Claude; Tomás, Ana Paula; Urbain, Xavier Mechanically proving termination using polynomial interpretations. (English) Zbl 1108.03017 J. Autom. Reasoning 34, No. 4, 325-363 (2005). MSC: 03B35 68Q42 PDFBibTeX XMLCite \textit{E. Contejean} et al., J. Autom. Reasoning 34, No. 4, 325--363 (2005; Zbl 1108.03017) Full Text: DOI
Zantema, H. Termination of string rewriting proved automatically. (English) Zbl 1102.68649 J. Autom. Reasoning 34, No. 2, 105-139 (2005). MSC: 68T15 68Q42 PDFBibTeX XMLCite \textit{H. Zantema}, J. Autom. Reasoning 34, No. 2, 105--139 (2005; Zbl 1102.68649) Full Text: DOI
Lucas, Salvador Polynomials over the reals in proofs of termination: from theory to practice. (English) Zbl 1085.68076 Theor. Inform. Appl. 39, No. 3, 547-586 (2005). MSC: 68Q42 12Y05 68W30 PDFBibTeX XMLCite \textit{S. Lucas}, Theor. Inform. Appl. 39, No. 3, 547--586 (2005; Zbl 1085.68076) Full Text: DOI Numdam EuDML Link
Fissore, Olivier; Gnaedig, Isabelle; Kirchner, Hélène Outermost ground termination. (English) Zbl 1272.68181 Gadducci, Fabio (ed.) et al., WRLA 2002. Proceedings of the 4th international workshop on rewriting logic and its applications, Pisa, Italy, September 19–21, 2002. Amsterdam: Elsevier. Electronic Notes in Theoretical Computer Science 71, 188-207 (2004). MSC: 68Q42 PDFBibTeX XMLCite \textit{O. Fissore} et al., Electron. Notes Theor. Comput. Sci. 71, 188--207 (2004; Zbl 1272.68181) Full Text: Link
Rubio, Albert A fully syntactic AC-RPO. (English) Zbl 1049.68076 Inf. Comput. 178, No. 2, 515-533 (2002). MSC: 68Q42 PDFBibTeX XMLCite \textit{A. Rubio}, Inf. Comput. 178, No. 2, 515--533 (2002; Zbl 1049.68076) Full Text: DOI Link
Martin, Ursula; Shand, Duncan Invariants, patterns and weights for ordering terms. (English) Zbl 0963.68090 J. Symb. Comput. 29, No. 6, 921-957 (2000). MSC: 68Q42 PDFBibTeX XMLCite \textit{U. Martin} and \textit{D. Shand}, J. Symb. Comput. 29, No. 6, 921--957 (2000; Zbl 0963.68090) Full Text: DOI Link
Arts, T.; Giesl, J. Termination of term rewriting using dependency pairs. (English) Zbl 0938.68051 Theor. Comput. Sci. 236, No. 1-2, 133-178 (2000). MSC: 68Q42 PDFBibTeX XMLCite \textit{T. Arts} and \textit{J. Giesl}, Theor. Comput. Sci. 236, No. 1--2, 133--178 (2000; Zbl 0938.68051) Full Text: DOI
Bündgen, Reinhard Buchberger’s algorithm: The term rewriter’s point of view. (English) Zbl 0871.68088 Theor. Comput. Sci. 159, No. 2, 143-190 (1996). MSC: 68W10 68Q42 PDFBibTeX XMLCite \textit{R. Bündgen}, Theor. Comput. Sci. 159, No. 2, 143--190 (1996; Zbl 0871.68088) Full Text: DOI
Ferreira, M. C. F.; Zantema, H. Total termination of term rewriting. (English) Zbl 0847.68054 Appl. Algebra Eng. Commun. Comput. 7, No. 2, 133-162 (1996). MSC: 68Q42 PDFBibTeX XMLCite \textit{M. C. F. Ferreira} and \textit{H. Zantema}, Appl. Algebra Eng. Commun. Comput. 7, No. 2, 133--162 (1996; Zbl 0847.68054) Full Text: DOI
Rubio, Albert; Nieuwenhuis, Robert A total AC-compatible ordering based on RPO. (English) Zbl 0873.68102 Theor. Comput. Sci. 142, No. 2, 209-227 (1995). MSC: 68Q42 PDFBibTeX XMLCite \textit{A. Rubio} and \textit{R. Nieuwenhuis}, Theor. Comput. Sci. 142, No. 2, 209--227 (1995; Zbl 0873.68102) Full Text: DOI
Dershowitz, Nachum; Hoot, Charles Natural termination. (English) Zbl 0873.68103 Theor. Comput. Sci. 142, No. 2, 179-207 (1995). MSC: 68Q42 PDFBibTeX XMLCite \textit{N. Dershowitz} and \textit{C. Hoot}, Theor. Comput. Sci. 142, No. 2, 179--207 (1995; Zbl 0873.68103) Full Text: DOI
Kapur, Deepak; Sivakumar, G.; Zhang, Hantao A path ordering for proving termination of AC rewrite systems. (English) Zbl 0819.68115 J. Autom. Reasoning 14, No. 2, 293-316 (1995). MSC: 68T15 68Q42 PDFBibTeX XMLCite \textit{D. Kapur} et al., J. Autom. Reasoning 14, No. 2, 293--316 (1995; Zbl 0819.68115) Full Text: DOI
Lescanne, Pierre Termination of rewrite systems by elementary interpretations. (English) Zbl 0817.68095 Formal Asp. Comput. 7, No. 1, 77-90 (1995). MSC: 68Q42 PDFBibTeX XMLCite \textit{P. Lescanne}, Formal Asp. Comput. 7, No. 1, 77--90 (1995; Zbl 0817.68095) Full Text: DOI
Rusinowitch, Michaël; Vigneron, Laurent Automated deduction with associative-commutative operators. (English) Zbl 0823.68096 Appl. Algebra Eng. Commun. Comput. 6, No. 1, 23-56 (1995). MSC: 68T15 68Q42 PDFBibTeX XMLCite \textit{M. Rusinowitch} and \textit{L. Vigneron}, Appl. Algebra Eng. Commun. Comput. 6, No. 1, 23--56 (1995; Zbl 0823.68096) Full Text: DOI
Scott, E. A. Weights for total division orderings on strings. (English) Zbl 0829.68074 Theor. Comput. Sci. 135, No. 2, 345-359 (1994). MSC: 68Q42 PDFBibTeX XMLCite \textit{E. A. Scott}, Theor. Comput. Sci. 135, No. 2, 345--359 (1994; Zbl 0829.68074) Full Text: DOI
Steinbach, Joachim Generating polynomial orderings. (English) Zbl 0791.68092 Inf. Process. Lett. 49, No. 2, 85-93 (1994). Reviewer: Joachim Steinbach MSC: 68Q42 PDFBibTeX XMLCite \textit{J. Steinbach}, Inf. Process. Lett. 49, No. 2, 85--93 (1994; Zbl 0791.68092) Full Text: DOI
Bevers, Eddy; Lewi, Johan Proving termination of (conditional) rewrite systems. A semantic approach. (English) Zbl 0790.68054 Acta Inf. 30, No. 6, 537-568 (1993). Reviewer: E.Bevers (Leuven) MSC: 68Q42 68Q55 PDFBibTeX XMLCite \textit{E. Bevers} and \textit{J. Lewi}, Acta Inf. 30, No. 6, 537--568 (1993; Zbl 0790.68054) Full Text: DOI
Navarro, Marisa; Orejas, Fernando; Remy, Jean-Luc Contextual rewriting as a sound and complete proof method for conditional LOG-specifications. (English) Zbl 0790.68075 Acta Inf. 30, No. 2, 147-180 (1993). MSC: 68Q60 68Q42 68Q65 PDFBibTeX XMLCite \textit{M. Navarro} et al., Acta Inf. 30, No. 2, 147--180 (1993; Zbl 0790.68075) Full Text: DOI
Bockmayr, Alexander Conditional narrowing modulo a set of equations. (English) Zbl 0776.68068 Appl. Algebra Eng. Commun. Comput. 4, No. 3, 147-168 (1993). Reviewer: A.Bockmayr (Saarbrücken) MSC: 68Q42 PDFBibTeX XMLCite \textit{A. Bockmayr}, Appl. Algebra Eng. Commun. Comput. 4, No. 3, 147--168 (1993; Zbl 0776.68068) Full Text: DOI
Jouannaud, Jean-Pierre; Marché, Claude Termination and completion modulo associativity, commutativity and identity. (English) Zbl 0759.68047 Theor. Comput. Sci. 104, No. 1, 29-51 (1992). Reviewer: J.Avenhaus (Kaiserslautern) MSC: 68Q42 PDFBibTeX XMLCite \textit{J.-P. Jouannaud} and \textit{C. Marché}, Theor. Comput. Sci. 104, No. 1, 29--51 (1992; Zbl 0759.68047) Full Text: DOI
Lescanne, Pierre Well rewrite orderings and well quasi-orderings. (English) Zbl 0778.68048 J. Symb. Comput. 14, No. 5, 419-435 (1992). MSC: 68Q42 06A11 PDFBibTeX XMLCite \textit{P. Lescanne}, J. Symb. Comput. 14, No. 5, 419--435 (1992; Zbl 0778.68048) Full Text: DOI
Rouyer, Jocelyne Preuves de terminaison de systèmes de réécriture fondées sur les interprétations polynomiales. Une méthode basée sur le théorème de Sturm. (Termination proofs of rewriting systems by polynomial interpretations. A method founded on a theorem of Sturm.). (French) Zbl 0731.68061 RAIRO, Inform. Théor. Appl. 25, No. 2, 157-169 (1991). MSC: 68Q42 PDFBibTeX XMLCite \textit{J. Rouyer}, RAIRO, Inform. Théor. Appl. 25, No. 2, 157--169 (1991; Zbl 0731.68061) Full Text: DOI EuDML
Bellegarde, Françoise; Lescanne, Pierre Termination by completion. (English) Zbl 0723.68056 Appl. Algebra Eng. Commun. Comput. 1, No. 2, 79-96 (1990). MSC: 68Q42 PDFBibTeX XMLCite \textit{F. Bellegarde} and \textit{P. Lescanne}, Appl. Algebra Eng. Commun. Comput. 1, No. 2, 79--96 (1990; Zbl 0723.68056) Full Text: DOI
Dick, Jeremy; Kalmus, John; Martin, Ursula Automating the Knuth Bendix ordering. (English) Zbl 0715.68044 Acta Inf. 28, No. 2, 95-119 (1990). Reviewer: M.Jantzen MSC: 68Q42 03D03 PDFBibTeX XMLCite \textit{J. Dick} et al., Acta Inf. 28, No. 2, 95--119 (1990; Zbl 0715.68044) Full Text: DOI
Hermann, Miki Chain properties of rule closures. (English) Zbl 0703.68066 Formal Aspects Comput. 2, No. 3, 207-225 (1990). MSC: 68Q42 03D03 PDFBibTeX XMLCite \textit{M. Hermann}, Formal Asp. Comput. 2, No. 3, 207--225 (1990; Zbl 0703.68066) Full Text: DOI
Inverardi, Paola; Nesi, M. A rewriting strategy to verify observational congruence. (English) Zbl 0702.68074 Inf. Process. Lett. 35, No. 4, 191-199 (1990). MSC: 68Q42 68Q60 03D03 PDFBibTeX XMLCite \textit{P. Inverardi} and \textit{M. Nesi}, Inf. Process. Lett. 35, No. 4, 191--199 (1990; Zbl 0702.68074) Full Text: DOI
Lescanne, Pierre On the recursive decomposition ordering with lexicographical status and other related orderings. (English) Zbl 0698.68031 J. Autom. Reasoning 6, No. 1, 39-49 (1990). MSC: 68Q65 03D03 06A99 PDFBibTeX XMLCite \textit{P. Lescanne}, J. Autom. Reasoning 6, No. 1, 39--49 (1990; Zbl 0698.68031) Full Text: DOI
Gnaedig, Isabelle; Kirchner, Claude; Kirchner, Hélène Equational completion in order-sorted algebras. (English) Zbl 0698.68028 Theor. Comput. Sci. 72, No. 2-3, 169-202 (1990). MSC: 68Q65 03D03 08B05 68W30 PDFBibTeX XMLCite \textit{I. Gnaedig} et al., Theor. Comput. Sci. 72, No. 2--3, 169--202 (1990; Zbl 0698.68028) Full Text: DOI
Nipkow, Tobias Term rewriting and beyond – theorem proving in Isabelle. (English) Zbl 0694.68059 Formal Aspects Comput. 1, No. 4, 320-338 (1989). MSC: 68T15 68Q65 68P10 68W30 03D03 PDFBibTeX XMLCite \textit{T. Nipkow}, Formal Asp. Comput. 1, No. 4, 320--338 (1989; Zbl 0694.68059) Full Text: DOI
Kirchner, Hélène Schematization of infinite sets of rewrite rules generated by divergent completion processes. (English) Zbl 0686.68025 Theor. Comput. Sci. 67, No. 2-3, 303-332 (1989). MSC: 68W30 68Q65 03D03 PDFBibTeX XMLCite \textit{H. Kirchner}, Theor. Comput. Sci. 67, No. 2--3, 303--332 (1989; Zbl 0686.68025) Full Text: DOI
Bachmair, Leo; Dershowitz, Nachum Completion for rewriting modulo a congruence. (English) Zbl 0686.68021 Theor. Comput. Sci. 67, No. 2-3, 173-201 (1989). MSC: 68W30 68T15 08B05 68Q65 PDFBibTeX XMLCite \textit{L. Bachmair} and \textit{N. Dershowitz}, Theor. Comput. Sci. 67, No. 2--3, 173--201 (1989; Zbl 0686.68021) Full Text: DOI
Martin, Ursula; Nipkow, Tobias Boolean unification - the story so far. (English) Zbl 0682.68093 J. Symb. Comput. 7, No. 3-4, 275-293 (1989). MSC: 68T15 68Q65 68W30 PDFBibTeX XMLCite \textit{U. Martin} and \textit{T. Nipkow}, J. Symb. Comput. 7, No. 3--4, 275--293 (1989; Zbl 0682.68093) Full Text: DOI
Deleage, J. L.; Pallo, J. M. A decidable word problem without equivalent canonical term rewriting system. (English) Zbl 0665.03006 Int. J. Comput. Math. 28, No. 1-4, 67-74 (1989). MSC: 03B25 08A50 68Q65 03D40 PDFBibTeX XMLCite \textit{J. L. Deleage} and \textit{J. M. Pallo}, Int. J. Comput. Math. 28, No. 1--4, 67--74 (1989; Zbl 0665.03006) Full Text: DOI
Kapur, Deepak; Musser, David R.; Narendran, Paliath Only prime superpositions need be considered in the Knuth-Bendix completion procedure. (English) Zbl 0651.68029 J. Symb. Comput. 6, No. 1, 19-36 (1988). MSC: 68Q65 68W30 68T15 PDFBibTeX XMLCite \textit{D. Kapur} et al., J. Symb. Comput. 6, No. 1, 19--36 (1988; Zbl 0651.68029) Full Text: DOI
Kaplan, Stéphane Rewriting with a nondeterministic choice operator. (English) Zbl 0633.68013 Theor. Comput. Sci. 56, No. 1, 37-57 (1988). MSC: 68Q65 68T15 68N01 PDFBibTeX XMLCite \textit{S. Kaplan}, Theor. Comput. Sci. 56, No. 1, 37--57 (1988; Zbl 0633.68013) Full Text: DOI
Buchberger, Bruno History and basic features of the critical-pair/completion procedure. (English) Zbl 0645.68094 J. Symb. Comput. 3, 3-38 (1987). MSC: 68T15 68W30 68Q45 08A50 01-02 68-03 PDFBibTeX XMLCite \textit{B. Buchberger}, J. Symb. Comput. 3, 3--38 (1987; Zbl 0645.68094) Full Text: DOI
Kaplan, Stephane Simplifying conditional term rewriting systems: Unification, termination and confluence. (English) Zbl 0641.68046 J. Symb. Comput. 4, 295-334 (1987). MSC: 68Q65 68T15 PDFBibTeX XMLCite \textit{S. Kaplan}, J. Symb. Comput. 4, 295--334 (1987; Zbl 0641.68046) Full Text: DOI
Paige, Robert; Henglein, Fritz Mechanical translation of set theoretic problem specifications into efficient RAM code - a case study. (English) Zbl 0641.68025 J. Symb. Comput. 4, 207-232 (1987). MSC: 68Q60 68T20 68W30 PDFBibTeX XMLCite \textit{R. Paige} and \textit{F. Henglein}, J. Symb. Comput. 4, 207--232 (1987; Zbl 0641.68025) Full Text: DOI
Dershowitz, Nachum Termination of rewriting. (English) Zbl 0637.68035 J. Symb. Comput. 3, 69-115 (1987). MSC: 68Q65 68W30 PDFBibTeX XMLCite \textit{N. Dershowitz}, J. Symb. Comput. 3, 69--115 (1987; Zbl 0637.68035) Full Text: DOI
Ben Cherifa, Ahlem; Lescanne, Pierre Termination of rewriting systems by polynomial interpretations and its implementation. (English) Zbl 0625.68036 Sci. Comput. Program. 9, 137-159 (1987). MSC: 68Q99 68W30 68N99 PDFBibTeX XMLCite \textit{A. Ben Cherifa} and \textit{P. Lescanne}, Sci. Comput. Program. 9, 137--159 (1987; Zbl 0625.68036) Full Text: DOI
Ben Cherifa, Ahlem; Lescanne, Pierre An actual implementation of a procedure that mechanically proves termination of rewriting systems based on inequalities between polynomial interpretations. (English) Zbl 0642.68038 Automated deduction, Proc. 8th Int. Conf., Oxford/Engl. 1986, Lect. Notes Comput. Sci. 230, 42-51 (1986). MSC: 68Q65 68W30 68N99 PDFBibTeX XML
Hardin, Thérèse; Laville, Alain Proof of termination of the rewriting system SUBSET on CCL. (English) Zbl 0618.68031 Theor. Comput. Sci. 46, 305-312 (1986). MSC: 68Q65 03B40 68N01 PDFBibTeX XMLCite \textit{T. Hardin} and \textit{A. Laville}, Theor. Comput. Sci. 46, 305--312 (1986; Zbl 0618.68031) Full Text: DOI
Krishnamoorthy, M. S.; Narendran, P. On recursive path ordering. (English) Zbl 0602.68031 Theor. Comput. Sci. 40, 323-328 (1985). MSC: 68Q65 PDFBibTeX XMLCite \textit{M. S. Krishnamoorthy} and \textit{P. Narendran}, Theor. Comput. Sci. 40, 323--328 (1985; Zbl 0602.68031) Full Text: DOI
Aït-Kaci, Hassan An algorithm for finding a minimal recursive path ordering. (English) Zbl 0578.68029 RAIRO, Inf. Théor. 19, 359-382 (1985). MSC: 68Q65 PDFBibTeX XMLCite \textit{H. Aït-Kaci}, RAIRO, Inf. Théor. 19, 359--382 (1985; Zbl 0578.68029) Full Text: EuDML
Rety, Pierre; Kirchner, Claude; Kirchner, Hélène; Lescanne, Pierre NARROWER: a new algorithm for unification and its application to logic programming. (English) Zbl 0576.68002 Rewriting techniques and applications, 1st Int. Conf., Dijon/France 1985, Lect. Notes Comput. Sci. 202, 141-157 (1985). MSC: 68N01 68Q65 68T15 PDFBibTeX XML
Lescanne, Pierre Uniform termination of term rewriting systems. Recursive decomposition ordering with status. (English) Zbl 0546.68020 Trees in algebra and programming, 9th Colloq., Bordeaux/France 1984, 181-194 (1984). MSC: 68Q65 68N99 03D03 68-04 68T15 PDFBibTeX XML