Papers for Term Papers

  1. Thomas Arts, Jurgen Giesl. Termination of term rewriting using dependency pairs, Journal of Theoretical Computer Science 236, 133-178, 2000.
  2. Leo Bachmair, Ashish Tiwari, and Laurent Vigneron, Abstract Congruence Closure, To appear in J. of Automated Reasoning.
  3. J. Beauquier, B. Berard, L. Fribourg, and F. Magniette. Proving convergence of self-stabilizing systems using first-order rewriting and regular languages. Distributed Computing, 14(2):83-95, 2001.
  4. I. Bethke, J.W. Klop and R. de Vrijer. Descendents and origins in term rewriting. Technical Report, Vrije Universiteit, Faculteit der Exacte Wetenschappen, IR-458, 1998. To appear in Information and Computation.
  5. Miquel Bofill, Guillem Godoy, Robert Nieuwenhuis and Albert Rubio. Paramodulation and Knuth-Bendix Completion with Nontotal and Nonmonotonic Orderings. Journal of Automated Reasoning. To appear.
  6. Guillaume Bonfante, Adam Cichon, Jean-Yves Marion and Hélène Touzet . Complexity Classes and Rewrite Systems with Polynomial Interpretation  CSL'98 - LNCS 1584
  7. H. Comon, G. Godoy, and R. Nieuwenhuis. The confluence of ground term rewrite systems is decidable in polynomial time. In Proc. 42nd Symp. Foundations of Computer Science (FOCS'2001), Las Vegas, NV, USA, Oct. 2001. IEEE Comp. Soc. Press, 2001.
  8. Hubert Comon, Paliath Narendran, Robert Nieuwenhuis and Michael Rusinowitch. Deciding the Confluence of Ordered Rewriting. ACM Transactions on Computational Logic (TOCL). To appear.
  9. Nachum Dershowitz, June 1997, Innocuous Constructor-Sharing Combinations, Proceedings of the Eighth International Conference on Rewriting Techniques and Applications (Sitges, Spain), H. Comon, ed., Lecture Notes in Computer Science, vol. 1232, Springer-Verlag, Berlin, pp. 202-216.
  10. Bernhard Gramlich. On Interreduction of Semi-Complete Term Rewriting Systems, Theoretical Computer Science 258(1-2), pp. 435-451, April 2001.
  11. Jean-Pierre Jouannaud and Albert Rubio. Higher-Order Recursive Path Orderings "a la carte".
  12. Deepak Kapur and G. Sivakumar. Proving Associative-Commutative Termination Using RPO-compatible Orderings. Proc. Automated Deduction in Classical and Non-Classical Logics. Springer LNAI 1761, Jan 2000.
  13. Deepak Kapur. Shostak's Congruence Closure as Completion. International Conference on Rewriting Techniques and Applications, RTA `97. Springer LNCS 1232, June 1997, Barcelona, Spain, 23-37.
  14. J.W. Klop, V. van Oostrom and R. de Vrijer. A geometric proof of confluence by decreasing diagrams. Technical Report, Vrije Universiteit, Faculteit der Exacte Wetenschappen, IR-456, 1998 (revision December 1999).
  15. Konstantin Korovin and Andrei Voronkov. Orienting Rewrite Rules with the Knuth-Bendix Order. Information and Computation, submitted.
  16. Christopher Lynch. Goal Directed Completion using SOUR Graphs, Proceedings of Eighth International Conference on Rewriting Techniques and Applications (RTA), Lecture Notes in Computer Science, volume 1232, pp. 8-22, 1997, Springer Verlag.
  17. Christopher Lynch and Barbara Morawska. Automatic Decidability. Proceedings of IEEE Symposium on Logic in Computer Science (LICS), 2002.
  18. Massimo Marchiori. Modularity of Completeness Revisited. Proceedings of the Sixth International Conference on Rewriting Techniques and Applications (RTA'95) , Kaiserslautern, Germany, LNCS 914, pages 2-10, Springer-Verlag, 1995.
  19. Y. Matiyasevich and Géraud Sénizergues.  Decision problems for semi-Thue systems with a few rules.(Short version in proceedings LICS'96, IEEE computer press, p.523-531).
  20. Richard Mayr, Tobias Nipkow. Higher-Order Rewrite Systems and their Confluence. Theoretical Computer Science, 192:3-29, 1998. 
  21. Sergei Vorobyov. The Undecidability of the First-Order Theories of One Step Rewriting in Linear Canonical Systems. Information and Computation, to appear.
  22. Toshiyuki Yamada, Jürgen Avenhaus, Carlos Loría-Sáenz, and Aart Middeldorp.  Logicality of Conditional Rewrite Systems , Theoretical Computer Science 236(1,2), pp. 209-232, 2000.