Publications in 2012

New Order-theoretic Characterisation of the Polytime Computable Functions
Martin Avanzini, Naohi Eguchi, and Georg Moser
Proceedings of the 10th Asian Symposium on Programming Languages and Systems (APLAS 2012), Lecture Notes in Computer Science 7705, pp. 280 – 295, 2012.

Termination Analysis of Term Rewriting by Polynomial Interpretations and Matrix Interpretations
Friedrich Neurauter
PhD thesis, University of Innsbruck, 2012.

Certification of Nontermination Proofs
Christian Sternagel and René Thiemann
Proceedings of the 3rd International Conference on Interactive Theorem Proving (ITP 2012), Lecture Notes in Computer Science 7406, pp. 266 – 282, 2012.

KBCV – Knuth-Bendix Completion Visualizer
Thomas Sternagel and Harald Zankl
Proceedings of the 6th International Joint Conference on Automated Reasoning (IJCAR 2012), Lecture Notes in Artificial Intelligence 7364, pp. 530 – 536, 2012.

General Bindings and Alpha-Equivalence in Nominal Isabelle
Christian Urban and Cezary Kaliszyk
Logical Methods in Computer Science 8(2), pp. 1 – 35, 2012.

SAT Solving for Termination Proofs with Recursive Path Orders and Dependency Pairs
Michael Codish, Jürgen Giesl, Peter Schneider-Kamp, and René Thiemann
Journal of Automated Reasoning 49(1), pp. 53 – 93, 2012.

On the Formalization of Termination Techniques based on Multiset Orderings
René Thiemann, Guillaume Allais, and Julian Nagele
Proceedings of the 23rd International Conference on Rewriting Techniques and Applications (RTA 2012), Leibniz International Proceedings in Informatics 15, pp. 339 – 354, 2012.

Deciding Confluence of Ground Term Rewrite Systems in Cubic Time
Bertram Felgenhauer
Proceedings of the 23rd International Conference on Rewriting Techniques and Applications (RTA 2012), Leibniz International Proceedings in Informatics 15, pp. 165 – 175, 2012.

Derivational Complexity Analysis Revisited
Andreas Schnabl
PhD thesis, University of Innsbruck, 2012.

Ordinals and Knuth-Bendix Orders
Sarah Winkler, Harald Zankl, and Aart Middeldorp
Proceedings of the 18th International Conference on Logic for Programming, Artificial Intelligence, and Reasoning (LPAR-18), Lecture Notes in Artificial Intelligence (Advanced Research in Computing and Software Science) 7180, pp. 420 – 434, 2012.

On the Domain and Dimension Hierarchy of Matrix Interpretations
Friedrich Neurauter and Aart Middeldorp
Proceedings of the 18th International Conference on Logic for Programming, Artificial Intelligence, and Reasoning (LPAR-18), Lecture Notes in Artificial Intelligence (Advanced Research in Computing and Software Science) 7180, pp. 320 – 334, 2012.