System Description
A system description of VMTL is available here (to appear in Proceedings of the 20th International Conference on Rewriting Techniques and Applications (RTA '09), Brasilia, Brazil, Lecture Notes in Computer Science, 2009. Springer Verlag.)References
VMTL is based on results from the following publications:- B. Alarcon, F. Emmes, C. Fuhs, J. Giesl, R. Gutierrez, S. Lucas, P. Schneider-Kamp, and R. Thiemann, Improving Context-Sensitive Dependency Pairs. In Proceedings of the 15th International Conference on Logic for Programming, Artificial Intelligence, and Reasoning (LPAR '08), Doha, Qatar, Lecture Notes in Artificial Intelligence, 2008. Springer-Verlag Extended version appeared as Technical Report AIB-2008-13, RWTH Aachen, Germany.
- B. Alarcon, R. Gutierrez, and S. Lucas Context-Sensitive Dependency Pairs. In Proceedings of the 26th Conference on Foundations of Software Technology and Theoretical Computer Science, FSTTCS'06, Kolkata, India, Lecture Notes in Computer Science 4337, pages 298-309, 2006. Springer-Verlag
- B. Alarcon, R. Gutierrez and S. Lucas, Improving the context-sensitive dependency graph. Electronic Notes in Theoretical Computer Science, 188:91-103, 2007, Elsevier.
- T. Arts and J. Giesl, Termination of Term Rewriting Using Dependency Pairs. Theoretical Computer Science 236:133-178, 2000.
- F. Duran, S. Lucas, C. Marche, J. Meseguer, and X. Urbain Proving Operational Termination of Membership Equational Programs. Higher-Order and Symbolic Computation, 21(1-2):59-88, June 2008. Springer-Verlag
- C. Fuhs, R. Navarro-Marset, C. Otto, J. Giesl, S. Lucas, P. Schneider-Kamp, Search Techniques for Rational Polynomial Orders. In Proceedings of the 9th International Conference on Artificial Intelligence and Symbolic Computation (AISC '08), Birmingham, UK, Lecture Notes in Computer Science 5144, pages 109-124, 2008. Springer-Verlag
- J. Giesl, R. Thiemann, P. Schneider-Kamp, and S. Falke, Mechanizing and Improving Dependency Pairs. Journal of Automated Reasoning, 37(3): 155-203, 2006. Springer-Verlag.
- F. Schernhammer and B. Gramlich Characterizing and Proving Operational Termination of Deterministic Conditional Term Rewriting Systems Technical Report E1852-2009-1, Vienna University of Technology. available here
- P. Schneider-Kamp, R. Thiemann, E. Annov, M. Codish, and J. Giesl, Proving Termination using Recursive Path Orders and SAT Solving. In Proceedings of the 6th International Symposium on Frontiers of Combining Systems (FroCoS '07), Liverpool, UK, Lecture Notes in Artificial Intelligence 4720, pages 267-282, 2007. ©Springer-Verlag
- R. Thiemann and J. Giesl, The Size-Change Principle and Dependency Pairs for Termination of Term Rewriting. Applicable Algebra in Engineering, Communication and Computing, 16(4):229-270, 2005. Springer-Verlag.