Publications in 2015

Sharing HOL4 and HOL Light Proof Knowledge
Thibault Gauthier and Cezary Kaliszyk
Proceedings of the 20th International Conference on Logic for Programming, Artificial Intelligence, and Reasoning (LPAR-20), Lecture Notes in Computer Science (Advanced Research in Computing and Software Science) 9450, pp. 372 – 386, 2015.

FEMaLeCoP: Fairly Efficient Machine Learning Connection Prover
Cezary Kaliszyk and Josef Urban
Proceedings of the 20th International Conference on Logic for Programming, Artificial Intelligence, and Reasoning (LPAR-20), Lecture Notes in Computer Science (Advanced Research in Computing and Software Science) 9450, pp. 88 – 96, 2015.

Constrained Term Rewriting tooL
Cynthia Kop and Naoki Nishida
Proceedings of the 20th International Conference on Logic for Programming, Artificial Intelligence, and Reasoning (LPAR-20), Lecture Notes in Computer Science (Advanced Research in Computing and Software Science) 9450, pp. 549 – 557, 2015.

Metis-based Paramodulation Tactic for HOL Light
Michael Färber, Cezary Kaliszyk
Proceedings of the 1st Global Conference on Artificial Intelligence (GCAI 2015), EPiC Series in Computing 36, pp. 127-136, 2015.

MizAR 40 for Mizar 40
Cezary Kaliszyk and Josef Urban
Journal of Automated Reasoning 55(3), pp. 245 – 256, 2015.

Formalizing Soundness and Completeness of Unravelings
Sarah Winkler and René Thiemann
Proceedings of the 10th International Symposium on Frontiers of Combining Systems (FroCoS 2015), Lecture Notes in Artificial Intelligence 9322, pp. 239 – 255, 2015.

Lemmatization for Stronger Reasoning in Large Theories
Cezary Kaliszyk, Josef Urban, and Jiří Vyskočil
Proceedings of the 10th International Symposium on Frontiers of Combining Systems (FroCoS 2015), Lecture Notes in Artificial Intelligence 9322, pp. 341 – 356, 2015.

Random Forests for Premise Selection
Michael Färber and Cezary Kaliszyk
Proceedings of the 10th International Symposium on Frontiers of Combining Systems (FroCoS 2015), Lecture Notes in Artificial Intelligence 9322, pp. 325 – 340, 2015.

Efficient Low-Level Connection Tableaux
Cezary Kaliszyk
Proceedings of the 24th International Conference on Automated Reasoning with Analytic Tableaux and Related Methods (TABLEAUX 2015), Lecture Notes in Artificial Intelligence 9323, pp. 102 – 111, 2015.

Analysing the Complexity of Functional Programs: Higher-Order Meets First-Order
Martin Avanzini, Ugo Dal Lago, and Georg Moser
Proceedings of the 20th ACM SIGPLAN International Conference on Functional Programming (ICFP 2015),   pp. 152 – 164, 2015.

Deriving Comparators and Show Functions in Isabelle/HOL
Christian Sternagel and René Thiemann
Proceedings of the 6th International Conference on Interactive Theorem Proving (ITP 2015), Lecture Notes in Computer Science 9236, pp. 421 – 437, 2015.

Learning to Parse on Aligned Corpora (Rough Diamond)
Cezary Kaliszyk, Josef Urban, and Jiří Vyskočil
Proceedings of the 6th International Conference on Interactive Theorem Proving (ITP 2015), Lecture Notes in Computer Science 9236, pp. 227 – 233, 2015.

Combinatorial Testing for Tree-Structured Test Models with Constraints
Takashi Kitamura, Akihisa Yamada, Goro Hatayama, Cyrille Artho, Eun-Hye Choi, Ngoc Thi Bich Do, Yutaka Oiwa, and Shinya Sakuragi
Proceedings of the 2015 IEEE International Conference on Software Quality, Reliability & Security (QRS 2015),   pp. 141 – 150, 2015.

Termination Competition (termCOMP 2015)
Jürgen Giesl, Frédéric Mesnard, Albert Rubio, René Thiemann, and Johannes Waldmann
Proceedings of the 25th International Conference on Automated Deduction (CADE-25), Lecture Notes in Computer Science 9195, pp. 105 – 108, 2015.

Encoding Dependency Pair Techniques and Control Strategies for Maximal Completion
Haruhiko Sato and Sarah Winkler
Proceedings of the 25th International Conference on Automated Deduction (CADE-25), Lecture Notes in Artificial Intelligence 9195, pp. 152 – 162, 2015.

Reducing Relative Termination to Dependency Pair Problems
José Iborra, Naoki Nishida, Germán Vidal, and Akihisa Yamada
Proceedings of the 25th International Conference on Automated Deduction (CADE-25), Lecture Notes in Artificial Intelligence 9195, pp. 163 – 178, 2015.

Confluence Competition 2015
Takahito Aoto, Nao Hirokawa, Julian Nagele, Naoki Nishida, and Harald Zankl
Proceedings of the 25th International Conference on Automated Deduction (CADE-25), Lecture Notes in Artificial Intelligence 9195, pp. 101 – 104, 2015.

Automated Deduction (CADE-25)
Amy Felty and Aart Middeldorp (eds.)
Proceedings of the 25th International Conference, Berlin, Lecture Notes in Artificial Intelligence 9195, 2015.

Proof eXchange for Theorem Proving (PxTP 2015)
Cezary Kaliszyk and Andrei Paskevich (eds.)
Proceedings of the 4th Workshop, Electronic Proceedings in Theoretical Computer Science 186, 2015.

Efficient Semantic Features for Automated Reasoning over Large Theories
Cezary Kaliszyk, Josef Urban, and Jiří Vyskočil
Proceedings of the 24th International Joint Conference on Artificial Intelligence (IJCAI 2015),   pp. 3084 – 3090, 2015.

System Description: E.T. 0.1
Cezary Kaliszyk, Stephan Schulz, Josef Urban, and Jiří Vyskočil
Proceedings of the 25th International Conference on Automated Deduction (CADE-25), Lecture Notes in Artificial Intelligence 9195, pp. 389 – 398, 2015.

Machine Learner for Automated Reasoning 0.4 and 0.5
Cezary Kaliszyk, Josef Urban, and Jiří Vyskočil
Proceedings of the 4th Workshop on Practical Aspects of Automated Reasoning (PAAR 2014), EasyChair Proceedings in Computer Science 31, pp. 60 – 66, 2015.

Beagle as a HOL4 External ATP Method
Thibault Gauthier, Cezary Kaliszyk, Chantal Keller, and Michael Norrish
Proceedings of the 4th Workshop on Practical Aspects of Automated Reasoning (PAAR 2014), EasyChair Proceedings in Computer Science 31, pp. 50 – 59, 2015.

Multivariate Amortised Resource Analysis for Term Rewrite System
Martin Hofmann and Georg Moser
Proceedings of the 13th International Conference on Typed Lambda Calculi and Applications (TLCA 2015), Leibniz International Proceedings in Informatics 38, pp. 241 – 256, 2015.

Priority Integration for Weighted Combinatorial Testing
Eun-Hye Choi, Takashi Kitamura, Cyrille Artho, Akihisa Yamada, and Yutaka Oiwa
Proceedings of the 39th IEEE Annual Computer Software and Applications Conference (COMPSAC 2015),  2, pp. 242 – 247, 2015.

Intelligent Computer Mathematics (CICM 2015)
Manfred Kerber, Jacques Carette, Cezary Kaliszyk, Florian Rabe, and Volker Sorge (eds.)
Proceedings of the International Conference, Washington DC, Lecture Notes in Artificial Intelligence 9150, 2015.

Formalizing Physics: Automation, Presentation and Foundation Issues
Cezary Kaliszyk, Josef Urban, Umair Siddique, Sanaz Khan Afshar, Cvetan Dunchev, and Sofiène Tahar
Proceedings of the 8th Conference on Intelligent Computer Mathematics (CICM 2015), Lecture Notes in Computer Science 9150, pp. 288 – 295, 2015.

A New Order-Theoretic Characterisation of the Polytime Computable Functions
Martin Avanzini, Naohi Eguchi, and Georg Moser
Theoretical Computer Science 585, pp. 3 – 24, 2015.

On the Computational Content of Termination Proofs
Georg Moser and Thomas Powell
Proceedings of the 11th Conference on Computability in Europe (CiE 2015), Lecture Notes in Computer Science 9136, pp. 276 – 285, 2015.

Certified Rule Labeling
Julian Nagele and Harald Zankl
Proceedings of the 26th International Conference on Rewriting Techniques and Applications (RTA 2015), Leibniz International Proceedings in Informatics 36, pp. 269 – 284, 2015.

Improving Automatic Confluence Analysis of Rewrite Systems by Redundant Rules
Julian Nagele, Bertram Felgenhauer, and Aart Middeldorp
Proceedings of the 26th International Conference on Rewriting Techniques and Applications (RTA 2015), Leibniz International Proceedings in Informatics 36, pp. 257 – 268, 2015.

Conditional Complexity
Cynthia Kop, Aart Middeldorp, and Thomas Sternagel
Proceedings of the 26th International Conference on Rewriting Techniques and Applications (RTA 2015), Leibniz International Proceedings in Informatics 36, pp. 223 – 240, 2015.

Leftmost Outermost Revisited
Nao Hirokawa, Aart Middeldorp, and Georg Moser
Proceedings of the 26th International Conference on Rewriting Techniques and Applications (RTA 2015), Leibniz International Proceedings in Informatics 36, pp. 209 – 222, 2015.

Certification of Complexity Proofs using CeTA
Martin Avanzini, Christian Sternagel, and René Thiemann
Proceedings of the 26th International Conference on Rewriting Techniques and Applications (RTA 2015), Leibniz International Proceedings in Informatics 36, pp. 23 – 39, 2015.

Confluence for Term Rewriting: Theory and Automation
Bertram Felgenhauer
PhD thesis, University of Innsbruck, 2015.

A Framework for Developing Stand-Alone Certifiers
Christian Sternagel and René Thiemann
Proceedings of the 9th Workshop on Logical and Semantic Frameworks, with Applications (LSFA 2014), Electronic Notes in Theoretical Computer Science 312, pp. 51 – 67, 2015.

Layer Systems for Proving Confluence
Bertram Felgenhauer, Aart Middeldorp, Harald Zankl, and Vincent van Oostrom
ACM Transactions on Computational Logic 16(2:14), pp. 1 – 32, 2015.

HOL(y)Hammer: Online ATP Service for HOL Light
Cezary Kaliszyk and Josef Urban
Mathematics in Computer Science 9(1), pp. 5 – 22, 2015.

Recording Completion for Certificates in Equational Reasoning
Thomas Sternagel, Sarah Winkler, and Harald Zankl
Proceedings of the 4th ACM-SIGPLAN Conference on Certified Programs and Proofs (CPP 2015),   pp. 41 – 47, 2015.

Premise Selection and External Provers for HOL4
Thibault Gauthier and Cezary Kaliszyk
Proceedings of the 4th ACM-SIGPLAN Conference on Certified Programs and Proofs (CPP 2015),   pp. 49 – 57, 2015.

Certified Connection Tableaux Proofs for HOL Light and TPTP
Cezary Kaliszyk, Josef Urban, and Jiří Vyskočil
Proceedings of the 4th ACM-SIGPLAN Conference on Certified Programs and Proofs (CPP 2015),   pp. 59 – 66, 2015.

Beyond Polynomials and Peano Arithmetic – Automation of Elementary and Ordinal Interpretations
Harald Zankl, Sarah Winkler, and Aart Middeldorp
Journal of Symbolic Computation 69, pp. 129 – 158, 2015.

Learning-assisted Theorem Proving with Millions of Lemmas
Cezary Kaliszyk and Josef Urban
Journal of Symbolic Computation 69, pp. 109 – 128, 2015.

Labelings for Decreasing Diagrams
Harald Zankl, Bertram Felgenhauer, and Aart Middeldorp
Journal of Automated Reasoning 54(2), pp. 101 – 133, 2015.