Publications in 2013

Logic for Programming, Artificial Intelligence, and Reasoning
Ken McMillan, Aart Middeldorp, and Andrei Voronkov (eds.)
Proceedings of the 19th International Conference, Stellenbosch, South Africa, Lecture Notes in Computer Science (Advanced Research in Computing and Software Science) 8312, 2013.

Lemma Mining over HOL Light
Cezary Kaliszyk and Josef Urban
Proceedings of the 19th International Conference on Logic for Programming, Artificial Intelligence, and Reasoning (LPAR-19), Lecture Notes in Computer Science (Advanced Research in Computing and Software Science) 8312, pp. 503 – 517, 2013.

Verifying Polytime Computability Automatically
Martin Avanzini
PhD thesis, University of Innsbruck, 2013.

Decreasing Diagrams
Harald Zankl
Archive of Formal Proofs, 2013.

Polynomial Path Orders
Martin Avanzini and Georg Moser
Logical Methods in Computer Science 9(4), pp. 1 – 42, 2013.

Term Rewriting with Logical Constraints
Cynthia Kop and Naoki Nishida
Proceedings of the 9th International Symposium on Frontiers of Combining Systems (FroCoS 2013), Lecture Notes in Artificial Intelligence 8152, pp. 343 – 358, 2013.

Algebraic Analysis of Huzita’s Origami Operations and Their Extensions
Fadoua Ghourabi, Asem Kasem, and Cezary Kaliszyk
Proceedings of the 9th International Workshop on 9th International Workshop on Automated Deduction in Geometry, Lecture Notes in Computer Science 7993, pp. 143 – 160, 2013.

The Structure of Interaction
Stéphane Gimenez and Georg Moser
Proceedings of the 27th International Workshop on Computer Science Logic / 22nd Annual Conference of the EACSL (CSL 2013), Leibniz International Proceedings in Informatics 23, pp. 316 – 331, 2013.

Initial Experiments with External Provers and Premise Selection on HOL Light Corpora
Cezary Kaliszyk and Josef Urban
Proceedings of the 3rd Workshop on Practical Aspects of Automated Reasoning (PAAR 2012), EasyChair Proceedings in Computing 21, pp. 72 – 81, 2013.

Communicating Formal Proofs: The Case of Flyspeck
Carst Tankink, Cezary Kaliszyk, Josef Urban, and Herman Geuvers
Proceedings of the 4th International Conference on Interactive Theorem Proving (ITP 2013), Lecture Notes in Computer Science 7998, pp. 451 – 456, 2013.

Formalizing Bounded Increase
René Thiemann
Proceedings of the 4th International Conference on Interactive Theorem Proving (ITP 2013), Lecture Notes in Computer Science 7998, pp. 245 – 260, 2013.

MaSh: Machine Learning for Sledgehammer
Daniel Kühlwein, Jasmin Christian Blanchette, Cezary Kaliszyk, and Josef Urban
Proceedings of the 4th International Conference on Interactive Theorem Proving (ITP 2013), Lecture Notes in Computer Science 7998, pp. 35 – 50, 2013.

Scalable LCF-style Proof Translation
Cezary Kaliszyk and Alexander Krauss
Proceedings of the 4th International Conference on Interactive Theorem Proving (ITP 2013), Lecture Notes in Computer Science 7998, pp. 51 – 66, 2013.

Formal Mathematics on Display: A Wiki for Flyspeck
Carst Tankink, Cezary Kaliszyk, Josef Urban, and Herman Geuvers
Proceedings of the 6th Conference on Intelligent Computer Mathematics (CICM 2013), Lecture Notes in Computer Science 7961, pp. 152 – 167, 2013.

Automated Reasoning Service for HOL Light
Cezary Kaliszyk and Josef Urban
Proceedings of the 6th Conference on Intelligent Computer Mathematics (CICM 2013), Lecture Notes in Computer Science 7961, pp. 120 – 135, 2013.

Tyrolean Complexity Tool: Features and Usage
Martin Avanzini and Georg Moser
Proceedings of the 24th International Conference on Rewriting Techniques and Applications (RTA 2013), Leibniz International Proceedings in Informatics 21, pp. 71 – 80, 2013.

A Combination Framework for Complexity
Martin Avanzini and Georg Moser
Proceedings of the 24th International Conference on Rewriting Techniques and Applications (RTA 2013), Leibniz International Proceedings in Informatics 21, pp. 55 – 70, 2013.

Formalizing Knuth-Bendix Orders and Knuth-Bendix Completion
Christian Sternagel and René Thiemann
Proceedings of the 24th International Conference on Rewriting Techniques and Applications (RTA 2013), Leibniz International Proceedings in Informatics 21, pp. 287 – 302, 2013.

Proof Orders for Decreasing Diagrams
Bertram Felgenhauer and Vincent van Oostrom
Proceedings of the 24th International Conference on Rewriting Techniques and Applications (RTA 2013), Leibniz International Proceedings in Informatics 21, pp. 174 – 189, 2013.

Normalized Completion Revisited
Sarah Winkler and Aart Middeldorp
Proceedings of the 24th International Conference on Rewriting Techniques and Applications (RTA 2013), Leibniz International Proceedings in Informatics 21, pp. 319 – 334, 2013.

Beyond Peano Arithmetic – Automatically Proving Termination of the Goodstein Sequence
Sarah Winkler, Harald Zankl, and Aart Middeldorp
Proceedings of the 24th International Conference on Rewriting Techniques and Applications (RTA 2013), Leibniz International Proceedings in Informatics 21, pp. 335 – 351, 2013.

Confluence by Decreasing Diagrams – Formalized
Harald Zankl
Proceedings of the 24th International Conference on Rewriting Techniques and Applications (RTA 2013), Leibniz International Proceedings in Informatics 21, pp. 352 – 367, 2013.

PRocH: Proof Reconstruction for HOL Light
Cezary Kaliszyk and Josef Urban
Proceedings of the 24th International Joint Conference on Automated Deduction (CADE 2013), Lecture Notes in Artificial Intelligence 7898, pp. 267 – 274, 2013.

Stronger Automation for Flyspeck by Feature Weighting and Strategy Evolution
Cezary Kaliszyk and Josef Urban
Proceedings of the 3rd International Workshop on Proof Exchange for Theorem Proving (PxTP 2013), EasyChair Proceedings in Computing 14, pp. 87 – 95, 2013.

Initial Experiments on Deriving a Complete HOL Simplification Set
Cezary Kaliszyk and Thomas Sternagel
Proceedings of the 3rd International Workshop on Proof Exchange for Theorem Proving (PxTP 2013), EasyChair Proceedings in Computing 14, pp. 77 – 86, 2013.

Termination Tools in Automated Reasoning
Sarah Winkler
PhD thesis, University of Innsbruck, 2013.

Uncurrying for Termination and Complexity
Nao Hirokawa, Aart Middeldorp, and Harald Zankl
Journal of Automated Reasoning 50(3), pp. 279 – 315, 2013.

Multi-Completion with Termination Tools
Sarah Winkler, Haruhiko Sato, Aart Middeldorp, and Masahito Kurihara
Journal of Automated Reasoning 50(3), pp. 317 – 354, 2013.

A Formalization of Termination Techniques in Isabelle/HOL
René Thiemann
Habilitation thesis, University of Innsbruck, 2013.

Computing N-th Roots using the Babylonian Method
René Thiemann
Archive of Formal Proofs 2013.