Hirokawa, Nao; Nagele, Julian; van Oostrom, Vincent; Oyamaguchi, Michio Confluence by critical pair analysis revisited. (English) Zbl 07178984 Fontaine, Pascal (ed.), Automated deduction – CADE 27. 27th international conference on automated deduction, Natal, Brazil, August 27–30, 2019. Proceedings. Cham: Springer (ISBN 978-3-030-29435-9/pbk; 978-3-030-29436-6/ebook). Lecture Notes in Computer Science 11716. Lecture Notes in Artificial Intelligence, 319-336 (2019). MSC: 03B35 68V15 PDF BibTeX XML Cite \textit{N. Hirokawa} et al., Lect. Notes Comput. Sci. 11716, 319--336 (2019; Zbl 07178984) Full Text: DOI
Aoto, Takahito; Toyama, Yoshihito; Kimura, Yuta Improving rewriting induction approach for proving ground confluence. (English) Zbl 1434.68215 Miller, Dale (ed.), 2nd international conference on formal structures for computation and deduction. FSCD 2017, Oxford, UK, September 3–9, 2017. Proceedings. Wadern: Schloss Dagstuhl – Leibniz Zentrum für Informatik. LIPIcs – Leibniz Int. Proc. Inform. 84, Article 7, 18 p. (2017). MSC: 68Q42 68V15 PDF BibTeX XML Cite \textit{T. Aoto} et al., LIPIcs -- Leibniz Int. Proc. Inform. 84, Article 7, 18 p. (2017; Zbl 1434.68215) Full Text: DOI
Rocha-Oliveira, Ana Cristina; Galdino, André Luiz; Ayala-Rincón, Mauricio Confluence of orthogonal term rewriting systems in the prototype verification system. (English) Zbl 1407.68441 J. Autom. Reasoning 58, No. 2, 231-251 (2017). MSC: 68T15 68N30 68Q42 PDF BibTeX XML Cite \textit{A. C. Rocha-Oliveira} et al., J. Autom. Reasoning 58, No. 2, 231--251 (2017; Zbl 1407.68441) Full Text: DOI
Nagele, Julian; Felgenhauer, Bertram; Zankl, Harald Certifying confluence proofs via relative termination and rule labeling. (English) Zbl 1398.68485 Log. Methods Comput. Sci. 13, No. 2, Paper No. 4, 27 p. (2017). MSC: 68T15 68Q42 PDF BibTeX XML Cite \textit{J. Nagele} et al., Log. Methods Comput. Sci. 13, No. 2, Paper No. 4, 27 p. (2017; Zbl 1398.68485) Full Text: DOI
Aoto, Takahito; Toyama, Yoshihito Ground confluence prover based on rewriting induction. (English) Zbl 1387.68205 Kesner, Delia (ed.) et al., 1st international conference on formal structures for computation and deduction, FSCD 2016, Porto, Portugal, June 22–26, 2016. Proceedings. Wadern: Schloss Dagstuhl – Leibniz Zentrum für Informatik (ISBN 978-3-95977-010-1). LIPIcs – Leibniz International Proceedings in Informatics 52, Article 33, 12 p. (2016). MSC: 68T15 68Q42 PDF BibTeX XML Cite \textit{T. Aoto} and \textit{Y. Toyama}, LIPIcs -- Leibniz Int. Proc. Inform. 52, Article 33, 12 p. (2016; Zbl 1387.68205) Full Text: DOI
Sternagel, Christian; Sternagel, Thomas Certifying confluence of almost orthogonal CTRSs via exact tree automata completion. (English) Zbl 1388.68155 Kesner, Delia (ed.) et al., 1st international conference on formal structures for computation and deduction, FSCD 2016, Porto, Portugal, June 22–26, 2016. Proceedings. Wadern: Schloss Dagstuhl – Leibniz Zentrum für Informatik (ISBN 978-3-95977-010-1). LIPIcs – Leibniz International Proceedings in Informatics 52, Article 29, 16 p. (2016). MSC: 68Q42 68Q45 68T15 PDF BibTeX XML Cite \textit{C. Sternagel} and \textit{T. Sternagel}, LIPIcs -- Leibniz Int. Proc. Inform. 52, Article 29, 16 p. (2016; Zbl 1388.68155) Full Text: DOI
Aoto, Takahito; Kikuchi, Kentaro Nominal confluence tool. (English) Zbl 06623260 Olivetti, Nicola (ed.) et al., Automated reasoning. 8th international joint conference, IJCAR 2016, Coimbra, Portugal, June 27 – July 2, 2016. Proceedings. Cham: Springer (ISBN 978-3-319-40228-4/pbk; 978-3-319-40229-1/ebook). Lecture Notes in Computer Science 9706. Lecture Notes in Artificial Intelligence, 173-182 (2016). MSC: 68T15 PDF BibTeX XML Cite \textit{T. Aoto} and \textit{K. Kikuchi}, Lect. Notes Comput. Sci. 9706, 173--182 (2016; Zbl 06623260) Full Text: DOI
Nagele, Julian; Zankl, Harald Certified rule labeling. (English) Zbl 1366.68126 Fernández, Maribel (ed.), 26th international conference on rewriting techniques and applications, RTA’13, Warsaw, Poland, June 29 – July 1, 2015. Proceedings. Wadern: Schloss Dagstuhl – Leibniz Zentrum für Informatik (ISBN 978-3-939897-85-9). LIPIcs – Leibniz International Proceedings in Informatics 36, 269-284 (2015). MSC: 68Q42 68T15 PDF BibTeX XML Cite \textit{J. Nagele} and \textit{H. Zankl}, LIPIcs -- Leibniz Int. Proc. Inform. 36, 269--284 (2015; Zbl 1366.68126) Full Text: DOI
Nagele, Julian; Felgenhauer, Bertram; Middeldorp, Aart Improving automatic confluence analysis of rewrite systems by redundant rules. (English) Zbl 1366.68125 Fernández, Maribel (ed.), 26th international conference on rewriting techniques and applications, RTA’13, Warsaw, Poland, June 29 – July 1, 2015. Proceedings. Wadern: Schloss Dagstuhl – Leibniz Zentrum für Informatik (ISBN 978-3-939897-85-9). LIPIcs – Leibniz International Proceedings in Informatics 36, 257-268 (2015). MSC: 68Q42 68T15 PDF BibTeX XML Cite \textit{J. Nagele} et al., LIPIcs -- Leibniz Int. Proc. Inform. 36, 257--268 (2015; Zbl 1366.68125) Full Text: DOI
Lemaire, Vincent; Pagès, Gilles; Panloup, Fabien Invariant measure of duplicated diffusions and application to Richardson-Romberg extrapolation. (English. French summary) Zbl 1329.60281 Ann. Inst. Henri Poincaré, Probab. Stat. 51, No. 4, 1562-1596 (2015). MSC: 60J60 60J65 60F05 60H10 60H35 60G10 65C30 65C05 49Q20 PDF BibTeX XML Cite \textit{V. Lemaire} et al., Ann. Inst. Henri Poincaré, Probab. Stat. 51, No. 4, 1562--1596 (2015; Zbl 1329.60281) Full Text: DOI Euclid
Zankl, Harald; Felgenhauer, Bertram; Middeldorp, Aart Labelings for decreasing diagrams. (English) Zbl 1315.68226 J. Autom. Reasoning 54, No. 2, 101-133 (2015). MSC: 68T15 68Q42 PDF BibTeX XML Cite \textit{H. Zankl} et al., J. Autom. Reasoning 54, No. 2, 101--133 (2015; Zbl 1315.68226) Full Text: DOI
Sternagel, Thomas; Middeldorp, Aart Conditional confluence (system description). (English) Zbl 1416.68181 Dowek, Gilles (ed.), Rewriting and typed lambda calculi. Joint international conference, RTA-TLCA 2014, held as part of the Vienna summer of logic, VSL 2014, Vienna, Austria, July 14–17, 2014. Proceedings. Berlin: Springer. Lect. Notes Comput. Sci. 8560, 456-465 (2014). MSC: 68T15 68Q42 PDF BibTeX XML Cite \textit{T. Sternagel} and \textit{A. Middeldorp}, Lect. Notes Comput. Sci. 8560, 456--465 (2014; Zbl 1416.68181) Full Text: DOI
Komori, Yuichi; Matsuda, Naosuke; Yamakawa, Fumika A simplified proof of the Church-Rosser theorem. (English) Zbl 1338.03017 Stud. Log. 102, No. 1, 175-183 (2014). MSC: 03B40 PDF BibTeX XML Cite \textit{Y. Komori} et al., Stud. Log. 102, No. 1, 175--183 (2014; Zbl 1338.03017) Full Text: DOI
Endrullis, Jörg; Klop, Jan Willem De Bruijn’s weak diamond property revisited. (English) Zbl 1360.68533 Indag. Math., New Ser. 24, No. 4, 1050-1072 (2013). MSC: 68Q42 03B40 68T15 PDF BibTeX XML Cite \textit{J. Endrullis} and \textit{J. W. Klop}, Indag. Math., New Ser. 24, No. 4, 1050--1072 (2013; Zbl 1360.68533) Full Text: DOI
Aoto, Takahito Disproving confluence of term rewriting systems by interpretation and ordering. (English) Zbl 1398.68268 Fontaine, Pascal (ed.) et al., Frontiers of combining systems. 9th international symposium, FroCoS 2013, Nancy, France, September 18–20, 2013. Proceedings. Berlin: Springer (ISBN 978-3-642-40884-7/pbk). Lecture Notes in Computer Science 8152. Lecture Notes in Artificial Intelligence, 311-326 (2013). MSC: 68Q42 68T15 PDF BibTeX XML Cite \textit{T. Aoto}, Lect. Notes Comput. Sci. 8152, 311--326 (2013; Zbl 1398.68268) Full Text: DOI
Stump, Aaron; Kimmell, Garrin; Zantema, Hans; El Haj Omar, Ruba A rewriting view of simple typing. (English) Zbl 1272.03142 Log. Methods Comput. Sci. 9, No. 1, Paper No. 4, 29 p. (2013). MSC: 03B70 68Q42 03B40 68T15 PDF BibTeX XML Cite \textit{A. Stump} et al., Log. Methods Comput. Sci. 9, No. 1, Paper No. 4, 29 p. (2013; Zbl 1272.03142) Full Text: DOI
Busaniche, Manuela; Cabrer, Leonardo; Mundici, Daniele Confluence and combinatorics in finitely generated unital lattice-ordered abelian groups. (English) Zbl 1277.06007 Forum Math. 24, No. 2, 253-271 (2012). Reviewer: Belmesnaoui Aqzzouz (Salajadida) MSC: 06F20 52B11 52B20 57Q15 46L05 PDF BibTeX XML Cite \textit{M. Busaniche} et al., Forum Math. 24, No. 2, 253--271 (2012; Zbl 1277.06007) Full Text: DOI arXiv
Zankl, Harald Confluence by decreasing diagrams – formalized. (English) Zbl 1356.68207 van Raamsdonk, Femke (ed.), 24th international conference on rewriting techniques and applications (RTA 2013), Eindhoven, The Netherlands, June 24–26, 2013. Wadern: Schloss Dagstuhl – Leibniz Zentrum für Informatik (ISBN 978-3-939897-53-8). LIPIcs – Leibniz International Proceedings in Informatics 21, 352-367 (2013). MSC: 68T15 68Q42 PDF BibTeX XML Cite \textit{H. Zankl}, LIPIcs -- Leibniz Int. Proc. Inform. 21, 352--367 (2011; Zbl 1356.68207) Full Text: DOI
Sternagel, Christian; Thiemann, René Formalizing Knuth-Bendix orders and Knuth-Bendix completion. (English) Zbl 1356.68201 van Raamsdonk, Femke (ed.), 24th international conference on rewriting techniques and applications (RTA 2013), Eindhoven, The Netherlands, June 24–26, 2013. Wadern: Schloss Dagstuhl – Leibniz Zentrum für Informatik (ISBN 978-3-939897-53-8). LIPIcs – Leibniz International Proceedings in Informatics 21, 287-302 (2013). MSC: 68T15 03B35 68Q42 PDF BibTeX XML Cite \textit{C. Sternagel} and \textit{R. Thiemann}, LIPIcs -- Leibniz Int. Proc. Inform. 21, 287--302 (2011; Zbl 1356.68201) Full Text: DOI
Felgenhauer, Bertram; Van Oostrom, Vincent Proof orders for decreasing diagrams. (English) Zbl 1356.03054 van Raamsdonk, Femke (ed.), 24th international conference on rewriting techniques and applications (RTA 2013), Eindhoven, The Netherlands, June 24–26, 2013. Wadern: Schloss Dagstuhl – Leibniz Zentrum für Informatik (ISBN 978-3-939897-53-8). LIPIcs – Leibniz International Proceedings in Informatics 21, 174-189 (2013). MSC: 03B35 68Q42 68T15 PDF BibTeX XML Cite \textit{B. Felgenhauer} and \textit{V. Van Oostrom}, LIPIcs -- Leibniz Int. Proc. Inform. 21, 174--189 (2011; Zbl 1356.03054) Full Text: DOI
Hirokawa, Nao; Middeldorp, Aart Decreasing diagrams and relative termination. (English) Zbl 1243.68199 J. Autom. Reasoning 47, No. 4, 481-501 (2011). MSC: 68Q42 68T15 PDF BibTeX XML Cite \textit{N. Hirokawa} and \textit{A. Middeldorp}, J. Autom. Reasoning 47, No. 4, 481--501 (2011; Zbl 1243.68199) Full Text: DOI
Zankl, Harald; Felgenhauer, Bertram; Middeldorp, Aart CSI – a confluence tool. (English) Zbl 1341.68199 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, 499-505 (2011). MSC: 68T15 68Q42 PDF BibTeX XML Cite \textit{H. Zankl} et al., Lect. Notes Comput. Sci. 6803, 499--505 (2011; Zbl 1341.68199) Full Text: DOI
Saurin, Alexis Typing streams in the \({\Lambda}{\mu}\)-calculus. (English) Zbl 1351.68065 ACM Trans. Comput. Log. 11, No. 4, Article No. 28, 34 p. (2010). MSC: 68N18 PDF BibTeX XML Cite \textit{A. Saurin}, ACM Trans. Comput. Log. 11, No. 4, Article No. 28, 34 p. (2010; Zbl 1351.68065) Full Text: DOI
Kozen, Dexter Church-Rosser made easy. (English) Zbl 1231.03012 Fundam. Inform. 103, No. 1-4, 129-136 (2010). MSC: 03B40 PDF BibTeX XML Cite \textit{D. Kozen}, Fundam. Inform. 103, No. 1--4, 129--136 (2010; Zbl 1231.03012) Full Text: DOI
Bouhoula, Adel Simultaneous checking of completeness and ground confluence for algebraic specifications. (English) Zbl 1351.68171 ACM Trans. Comput. Log. 10, No. 3, Article No. 20, 33 p. (2009). MSC: 68Q65 68Q42 68T15 PDF BibTeX XML Cite \textit{A. Bouhoula}, ACM Trans. Comput. Log. 10, No. 3, Article No. 20, 33 p. (2009; Zbl 1351.68171) Full Text: DOI
Krstić, Sava; Jones, Robert B.; O’Leary, John Mothers of pipelines. (English) Zbl 1277.68137 Cook, B. (ed.) et al., Combined proceedings of the fourth workshop on pragmatics of decision procedures in automated reasoning (PDPAR 2006) and the first international workshop on probabilistic automata and logics (PaUL 2006), Seattle, WA, USA, August 2006. Amsterdam: Elsevier. Electronic Notes in Theoretical Computer Science 174, No. 8, 7-22 (2007). MSC: 68Q60 68T15 PDF BibTeX XML Cite \textit{S. Krstić} et al., Electron. Notes Theor. Comput. Sci. 174, No. 8, 7--22 (2007; Zbl 1277.68137) Full Text: DOI
Kanovich, Max A note on rewriting proofs and Fibonacci numbers. (English) Zbl 1133.05006 Artemov, Sergei N. (ed.) et al., Logical foundations of computer science. International symposium, LFCS 2007, New York, NY, USA, June 4–7, 2007. Proceedings. Berlin: Springer (ISBN 978-3-540-72732-3/pbk). Lecture Notes in Computer Science 4514, 284-292 (2007). MSC: 05A17 05A20 68Q42 68T15 PDF BibTeX XML Cite \textit{M. Kanovich}, Lect. Notes Comput. Sci. 4514, 284--292 (2007; Zbl 1133.05006) Full Text: DOI
Mitsuhashi, Ichiro; Oyamaguch, Michio; Jacquemard, Florent The confluence problem for flat TRSs. (English) Zbl 1156.68433 Calmet, Jacques (ed.) et al., Artificial intelligence and symbolic computation. 8th international conference, AISC 2006, Beijing, China, September 20–22, 2006. Proceedings. Berlin: Springer (ISBN 978-3-540-39728-1/pbk). Lecture Notes in Computer Science 4120. Lecture Notes in Artificial Intelligence, 68-81 (2006). MSC: 68Q42 68T15 PDF BibTeX XML Cite \textit{I. Mitsuhashi} et al., Lect. Notes Comput. Sci. 4120, 68--81 (2006; Zbl 1156.68433) Full Text: DOI
Vestergaard, René; Brotherston, James A formalised first-order confluence proof for the \(\lambda\)-calculus using one-sorted variable names. (English) Zbl 1054.68028 Inf. Comput. 183, No. 2, 212-244 (2003). MSC: 68N18 03B40 68T15 PDF BibTeX XML Cite \textit{R. Vestergaard} and \textit{J. Brotherston}, Inf. Comput. 183, No. 2, 212--244 (2003; Zbl 1054.68028) Full Text: DOI
Oyamaguchi, Michio; Ohta, Yoshikatsu The unification problem for confluent right-ground term rewriting systems. (English) Zbl 1054.68081 Inf. Comput. 183, No. 2, 187-211 (2003). MSC: 68Q42 68T15 PDF BibTeX XML Cite \textit{M. Oyamaguchi} and \textit{Y. Ohta}, Inf. Comput. 183, No. 2, 187--211 (2003; Zbl 1054.68081) Full Text: DOI
Blom, Stefan; van de Pol, Jaco State space reduction by proving confluence. (English) Zbl 1010.68527 Brinksma, Ed (ed.) et al., Computer aided verification. 14th international conference, CAV 2002, Copenhagen, Denmark, July 27-31, 2002. Proceedings. Berlin: Springer. Lect. Notes Comput. Sci. 2404, 596-609 (2002). MSC: 68Q85 68Q60 68T15 PDF BibTeX XML Cite \textit{S. Blom} and \textit{J. van de Pol}, Lect. Notes Comput. Sci. 2404, 596--609 (2002; Zbl 1010.68527)
Siekmann, Jörg; Wrightson, Graham An open research problem: Strong completeness of R. Kowalski’s connection graph proof procedure. (English) Zbl 0997.03013 Log. J. IGPL 10, No. 1, 85-103 (2002). MSC: 03B35 68T15 PDF BibTeX XML Cite \textit{J. Siekmann} and \textit{G. Wrightson}, Log. J. IGPL 10, No. 1, 85--103 (2002; Zbl 0997.03013) Full Text: DOI
Baumgartner, P.; Eisinger, N.; Furbach, U. A confluent connection calculus. (English) Zbl 0997.03007 Hölldobler, Steffen (ed.), Intellectics and computational logic. Papers in honor of Wolfgang Bibel. Dordrecht: Kluwer Academic Publishers. Appl. Log. Ser. 19, 3-26 (2000). MSC: 03B35 68T15 PDF BibTeX XML Cite \textit{P. Baumgartner} et al., Appl. Log. Ser. 19, 3--26 (2000; Zbl 0997.03007)
Massacci, Fabio Single step tableaux for modal logics. Computational properties, complexity and methodology. (English) Zbl 0951.03008 J. Autom. Reasoning 24, No. 3, 319-364 (2000). MSC: 03B35 03B45 03D15 03B25 68T15 PDF BibTeX XML Cite \textit{F. Massacci}, J. Autom. Reasoning 24, No. 3, 319--364 (2000; Zbl 0951.03008) Full Text: DOI
Baumgartner, Peter; Eisinger, Norbert; Furbach, Ulrich A confluent connection calculus. (English) Zbl 0937.03016 Ganzinger, Harald (ed.), Automated deduction - CADE-16. 16th international conference, Trento, Italy, July 7-10, 1999. Proceedings. Berlin: Springer. Lect. Notes Comput. Sci. 1632, 329-343 (1999). MSC: 03B35 68T15 PDF BibTeX XML Cite \textit{P. Baumgartner} et al., Lect. Notes Comput. Sci. 1632, 329--343 (1999; Zbl 0937.03016)
Lafaye de Micheaux, N.; Rambaud, C. Confluence for graph transformations. (English) Zbl 0872.68079 Theor. Comput. Sci. 154, No. 2, 329-348 (1996). MSC: 68Q42 68R10 PDF BibTeX XML Cite \textit{N. Lafaye de Micheaux} and \textit{C. Rambaud}, Theor. Comput. Sci. 154, No. 2, 329--348 (1996; Zbl 0872.68079) Full Text: DOI
Seeger, A.; Lay, W.; Slavyanov, S. Yu. Confluence of Fuchsian second-order differential equations. (English. Russian original) Zbl 0857.34017 Theor. Math. Phys. 104, No. 2, 950-960 (1995); translation from Teor. Mat. Fiz. 104, No. 2, 233-247 (1995). MSC: 34M99 PDF BibTeX XML Cite \textit{A. Seeger} et al., Theor. Math. Phys. 104, No. 2, 950--960 (1995; Zbl 0857.34017); translation from Teor. Mat. Fiz. 104, No. 2, 233--247 (1995) Full Text: DOI
Huet, Gérard Residual theory in \(\lambda\)-calculus: A formal development. (English) Zbl 0826.03008 J. Funct. Program. 4, No. 3, 371-394 (1994). Reviewer: R.David (Chambéry) MSC: 03B35 03B40 PDF BibTeX XML Cite \textit{G. Huet}, J. Funct. Program. 4, No. 3, 371--394 (1994; Zbl 0826.03008) Full Text: DOI
Klop, Jan Willem; van Oostrom, Vincent; van Raamsdonk, Femke Combinatory reduction systems: Introduction and survey. (English) Zbl 0796.03024 Theor. Comput. Sci. 121, No. 1-2, 279-308 (1993). Reviewer: R.David (Chambéry) MSC: 03B40 68Q42 PDF BibTeX XML Cite \textit{J. W. Klop} et al., Theor. Comput. Sci. 121, No. 1--2, 279--308 (1993; Zbl 0796.03024) Full Text: DOI
Padawitz, Peter Inductive expansion: A calculus for verifying and synthesizing functional and logic programs. (English) Zbl 0723.68074 J. Autom. Reasoning 7, No. 1, 27-103 (1991). MSC: 68Q60 68T15 68N17 PDF BibTeX XML Cite \textit{P. Padawitz}, J. Autom. Reasoning 7, No. 1, 27--103 (1991; Zbl 0723.68074) Full Text: DOI
Fülöp, Zoltán; Vágvölgyi, Sándor Ground term rewriting rules for the word problem of ground term equations. (English) Zbl 0757.68069 Bull. EATCS 45, 186-201 (1991). MSC: 68Q42 68Q05 68T15 PDF BibTeX XML Cite \textit{Z. Fülöp} and \textit{S. Vágvölgyi}, Bull. EATCS 45, 186--201 (1991; Zbl 0757.68069)
Dershowitz, Nachum; Okada, Mitsuhiro A rationale for conditional equational programming. (English) Zbl 0702.68034 Theor. Comput. Sci. 75, No. 1-2, 111-138 (1990). MSC: 68N01 68N17 68Q42 68T15 PDF BibTeX XML Cite \textit{N. Dershowitz} and \textit{M. Okada}, Theor. Comput. Sci. 75, No. 1--2, 111--138 (1990; Zbl 0702.68034) Full Text: DOI
Hofbauer, D.; Kutsche, R.-D. Proving inductive theorems based on term rewriting systems. (English) Zbl 0708.68028 Algebraic and logic programming, Proc. Int. Workshop, Gaussig/GDR 1988, Lect. Notes Comput. Sci. 343, 180-190 (1989). Reviewer: M.Steinby MSC: 68Q42 03D03 68T15 PDF BibTeX XML
Fribourg, Laurent A strong restriction of the inductive completion procedure. (English) Zbl 0682.68029 J. Symb. Comput. 8, No. 3, 253-276 (1989). MSC: 68W30 68T15 PDF BibTeX XML Cite \textit{L. Fribourg}, J. Symb. Comput. 8, No. 3, 253--276 (1989; Zbl 0682.68029) Full Text: DOI
Yokouchi, Hirofumi Church-Rosser theorem for a rewriting system on categorical combinators. (English) Zbl 0672.03006 Theor. Comput. Sci. 65, No. 3, 271-290 (1989). Reviewer: A.Pettorossi MSC: 03B40 68N01 PDF BibTeX XML Cite \textit{H. Yokouchi}, Theor. Comput. Sci. 65, No. 3, 271--290 (1989; Zbl 0672.03006) Full Text: DOI
Jorrand, Philippe Fundamental mechanisms for artificial intelligence programming languages - an introduction. (English) Zbl 0698.68007 Advanced topics in artificial intelligence, Proc. 2nd Adv. Course, Oslo/Norway 1987, Lect. Notes Comput. Sci. 345, 1-40 (1988). MSC: 68N01 68T15 68T99 68W30 03D03 68Q65 PDF BibTeX XML
Dershowitz, Nachum; Okada, Mitsuhiro; Sivakumar, G. Canonical conditional rewrite systems. (English) Zbl 0667.68043 Automated deduction, Proc. 9th Int. Conf., Argonne/Ill. 1988, Lect. Notes Comput. Sci. 310, 538-549 (1988). Reviewer: G.Mints MSC: 68Q65 68T15 PDF BibTeX XML
Dershowitz, Nachum; Okada, Mitsuhiro; Sivakumar, G. Confluence of conditional rewrite systems. (English) Zbl 0666.68094 Conditional term rewriting systems, 1st Int. Workshop, Orsay/France 1987, Lect. Notes Comput. Sci. 308, 31-44 (1988). Reviewer: T.Tammet MSC: 68T15 03B35 PDF BibTeX XML
van den Broek, P. M. Confluence of indirection reductions in graph rewrite systems. (English) Zbl 0661.68094 Inf. Process. Lett. 29, No. 3, 143-148 (1988). Reviewer: F.-L.Tiplea MSC: 68T15 68Q45 PDF BibTeX XML Cite \textit{P. M. van den Broek}, Inf. Process. Lett. 29, No. 3, 143--148 (1988; Zbl 0661.68094) 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 PDF BibTeX XML Cite \textit{S. Kaplan}, Theor. Comput. Sci. 56, No. 1, 37--57 (1988; Zbl 0633.68013) 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 PDF BibTeX XML Cite \textit{S. Kaplan}, J. Symb. Comput. 4, 295--334 (1987; Zbl 0641.68046) Full Text: DOI
Göbel, Richard Ground confluence. (English) Zbl 0639.68029 Rewriting techniques and applications, Proc. 2nd Int. Conf., Bordeaux/France 1987, Lect. Notes Comput. Sci. 256, 156-167 (1987). Reviewer: J.Hromkovič MSC: 68Q65 68N01 68Q45 68T15 PDF BibTeX XML
Hsiang, Jieh; Rusinowitch, Michael On word problems in equational theories. (English) Zbl 0625.68068 Automata, languages and programming, Proc. 14th Int. Colloq., Karlsruhe/FRG 1987, Lect. Notes Comput. Sci. 267, 54-71 (1987). MSC: 68T15 03C05 08A50 PDF BibTeX XML
Eisinger, Norbert What you always wanted to know about clause graph resolution. (English) Zbl 0642.68155 Automated deduction, Proc. 8th Int. Conf., Oxford/Engl. 1986, Lect. Notes Comput. Sci. 230, 316-336 (1986). MSC: 68T15 68W99 05C10 PDF BibTeX XML
Göbel, Richard Completion of globally finite term rewriting systems for inductive proofs. (English) Zbl 0624.68078 Artificial intelligence, 9th Ger. Workshop, Dassel/FRG 1985, Inf.- Fachber. 118, 101-110 (1986). MSC: 68T15 PDF BibTeX XML
Küchlin, Wolfgang Equational completion by proof transformation. (English) Zbl 0678.68095 Zürich: Swiss Federal Institute of Technology, Thesis, III, 40 p. (1986). MSC: 68T15 68T99 68Q65 03D03 PDF BibTeX XML Cite \textit{W. Küchlin}, Equational completion by proof transformation. Zurich: ETH, Swiss Federal Institute of Technology (1986; Zbl 0678.68095)
Paul, Etienne Equational methods in first order predicate calculus. (English) Zbl 0577.03003 J. Symb. Comput. 1, 7-29 (1985). Reviewer: H.P.Schmitt MSC: 03B35 03C05 68T15 03B20 PDF BibTeX XML Cite \textit{E. Paul}, J. Symb. Comput. 1, 7--29 (1985; Zbl 0577.03003) Full Text: DOI
Dietrich, Roland Eine Programmierumgebung für Termersetzungssysteme. (German) Zbl 0565.68033 Arbeitspapiere der GMD 130. St. Augustin: GMD. 185 p. (1985). MSC: 68Q65 68T15 68N01 PDF BibTeX XML Cite \textit{R. Dietrich}, Eine Programmierumgebung für Termersetzungssysteme. St. Augustin: GMD (1985; Zbl 0565.68033)
Perdrix, H. Propriétés Church-Rosser de systèmes de réecriture equationnels ayant la propriété de termination faible. (French) Zbl 0583.68005 Theoretical aspects of computer science, Symp., Paris 1984, Lect. Notes Comput. Sci. 166, 97-108 (1984). Reviewer: A.Pettorossi MSC: 68Q65 68T15 68Q55 PDF BibTeX XML
Guttag, J. V.; Kapur, D.; Musser, D. R. On proving uniform termination and restricted termination of rewriting systems. (English) Zbl 0526.68036 SIAM J. Comput. 12, 189-214 (1983). MSC: 68Q65 68T15 PDF BibTeX XML Cite \textit{J. V. Guttag} et al., SIAM J. Comput. 12, 189--214 (1983; Zbl 0526.68036) Full Text: DOI
Jouannaud, Jean-Pierre Confluent and coherent equational term rewriting systems application to proofs in abstract data types. (English) Zbl 0522.68013 Trees in algebra and programming, CAAP ’83, Proc. 8th Colloq., L’Aquila/Italy 1983, Lect. Notes Comput. Sci. 159, 269-283 (1983). MSC: 68Q60 68W30 68P05 68T15 08A50 03F05 PDF BibTeX XML
Huet, Gerard Confluent reductions: Abstract properties and applications to term rewriting systems. (English) Zbl 0458.68007 J. Assoc. Comput. Mach. 27, 797-821 (1980). MSC: 68Q65 68Q60 PDF BibTeX XML Cite \textit{G. Huet}, J. Assoc. Comput. Mach. 27, 797--821 (1980; Zbl 0458.68007) Full Text: DOI