All Publications

Certifying Proofs in the First-Order Theory of Rewriting
Fabian Mitterwallner, Alexander Lochmann, Aart Middeldorp, Bertram Felgenhauer
27th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS 2021), LNCS 12652, pp. 127 – 144, 2021.

An Isabelle/HOL formalization of AProVE’s termination method for LLVM IR
Max Haslbeck, Rene Thiemann
10th ACM SIGPLAN International Conference on Certified Programs and Proofs (CPP 2021),   pp. 238 – 249, 2021.

A Verified Decision Procedure for the First-Order Theory of Rewriting for Linear Variable-Separated Rewrite Systems
Alexander Lochmann, Aart Middeldorp, Fabian Mitterwallner, Bertram Felgenhauer
10th ACM SIGPLAN International Conference on Certified Programs and Proofs (CPP 2021),   pp. 250 – 263, 2021.

Property Invariant Embedding for Automated Reasoning
Miroslav Olšák, Cezary Kaliszyk, Josef Urban
24th European Conference on Artificial Intelligence (ECAI 2020), Frontiers in Artificial Intelligence and Applications 325, pp. 1395 – 1402, 2020.

Improving Expressivity of Graph Neural Networks
Stanisław Purgał
International Joint Conference on Neural Networks (IJCNN),   pp. 1 – 7, 2020.

A Survey of Languages for Formalizing Mathematics
Cezary Kaliszyk, Florian Rabe
Intelligent Computer Mathematics (CICM 2020), LNCS 12236, pp. 138 – 156, 2020.

Some symmetries of commutation diamonds
Vincent van Oostrom
9th International Workshop on Confluence,   pp. 1 – 5, 2020.

Certifying the Weighted Path Order
Rene Thiemann, Jonas Schöpf, Christian Sternagel, Akihisa Yamada
5th International Conference on Formal Structures for Computation and Deduction (FSCD 2020), Leibniz International Proceedings in Informatics (LIPIcs) 167, pp. 4:1 – 4:20, 2020.

Formalizing the LLL Basis Reduction Algorithm and the LLL Factorization Algorithm in Isabelle/HOL
René Thiemann, Ralph Bottesch, Jose Divasón, Max W. Haslbeck, Sebastiaan J.C. Joosten, Akihisa Yamada
Journal of Automated Reasoning 64, pp. 827 – 856, 2020.

Property Preserving Embedding of First-order Logic
Julian Parsert, Stephanie Autherith, Cezary Kaliszyk
6th Global Conference on Artificial Intelligence (GCAI 2020), EPiC Series in Computing 72, pp. 70 – 82, 2020.

Formalized Proofs of the Infinity and Normal Form Predicates in the First-Order Theory of Rewriting
Alexander Lochmann, Aart Middeldorp
26th International Conference on Tools and Algorithms for the Construction and Analysis of Systems, LCNS 12079, pp. 25 – 40, 2020.

Relaxed Weighted Path Order in Theorem Proving
Jan Jakubův, Cezary Kaliszyk
Mathematics in Computer Science,  14, pp. 657 – 670, 2020.

Tools in Term Rewriting for Education
Sarah Winker, Aart Middeldorp
8th International Workshop on Theorem Proving Components for Educational Software, EPTCS 313, pp. 54 – 72, 2020.

Verified Analysis of Random Binary Tree Structures
Manuel Eberl, Max W. Haslbeck, Tobias Nipkow
Journal of Automated Reasoning 64, pp. 879 – 910, 2020.

Mac Lane’s Comparison Theorem for the Kleisli Construction Formalized in Coq
Burak Ekici, Cezary Kaliszyk
Mathematics in Computer Science,  14, pp. 533 – 549, 2020.

Exploration of neural machine translation in autoformalization of mathematics in Mizar
Qingxiang Wang, Chad Brown, Cezary Kaliszyk, Josef Urban
International Conference on Certified Programs and Proofs (CPP 2020), ACM  pp. 85 – 98, 2020.

Loop conditions for strongly connected digraphs
Miroslav Olšák
International Journal of Algebra and Computation  pp. 1 – 33, 2019.

Higher-order Tarski Grothendieck as a Foundation for Formal Proof
Chad Brown, Cezary Kaliszyk, Karol Pąk
10th International Conference on Interactive Theorem Proving, LIPIcs 141, pp. 9:1 – 9:16, 2019.

Declarative Proof Translation
Cezary Kaliszyk, Karol Pąk
10th International Conference on Interactive Theorem Proving, LIPIcs 141, pp. 35:1 – 35:7, 2019.

Certification of Nonclausal Connection Tableaux Proofs
Michael Färber, Cezary Kaliszyk
28th International Conference on Automated Reasoning with Analytic Tableaux and Related Methods, LNCS 11714, pp. 21 – 38, 2019.

Confluence by Critical Pair Analysis Revisited
Nao Hirokawa, Julian Nagele, Vincent van Oostrom, Michio Oyamaguchi
27th International Conference on Automated Deduction, Lecture Notes in Computer Science 11716, pp. 319 – 336, 2019.

Verifying Bit-vector Invertibility Conditions in Coq (Extended Abstract)
Burak Ekici, Arjun Viswanathan, Yoni Zohar, Clark W. Barrett, Cesare Tinelli
6th Workshop on Proof eXchange for Theorem Proving, EPTCS 301, pp. 18 – 26, 2019.

Abstract Completion, Formalized
Nao Hirokawa, Aart Middeldorp, Christian Sternagel, Sarah Winkler
Logical Methods in Computer Science,  15(3), pp. 19:1 – 19:42, 2019.

Certified Equational Reasoning via Ordered Completion
Christian Sternagel and Sarah Winkler
27th International Conference on Automated Deduction, Lecture Notes in Computer Science 11716, pp. 508 – 525, 2019.

GRUNGE: A Grand Unified ATP Challenge
Chad Brown, Thibault Gauthier, Cezary Kaliszyk, Geoff Sutcliffe, Josef Urban
27th International Conference on Automated Deduction, LNCS 11716, pp. 123 – 141, 2019.

Composing Proof Terms
Christina Kohl and Aart Middeldorp
27th International Conference on Automated Deduction, Lecture Notes in Artificial Intelligence 11716, pp. 337 – 353, 2019.

Verifying an Incremental Theory Solver for Linear Arithmetic in Isabelle/HOL
Ralph Bottesch, Max W. Haslbeck, and René Thiemann
International Symposium on Frontiers of Combining Systems, Lecture Notes in Computer Science 11715, pp. 223 – 239, 2019.

Linear Inequalities
Ralph Bottesch, Alban Reynaud, René Thiemann
Archive of Formal Proofs 2019.

A Verified Implementation of the Berlekamp—Zassenhaus Factorization Algorithm
Jose Divasón, Sebastiaan Joosten, René Thiemann, and Akihisa Yamada
Journal of Automated Reasoning 64(4), pp. 699 – 735, 2020.

Can Neural Networks Learn Symbolic Rewriting?
Bartosz Piotrowski, Josef Urban, Chad Brown, Cezary Kaliszyk
Learning and Reasoning with Graph-Structured Representations, ICML 2019 Workshop,  2019.

Reachability Analysis for Termination and Confluence of Rewriting
Christian Sternagel, Akihisa Yamada
25th International Conference on Tools and Algorithms for the Construction and Analysis of Systems, Lecture Notes in Computer Science 11427, pp. 262 – 278, 2019.

The Termination and Complexity Competition
Jürgen Giesl, Albert Rubio, Christian Sternagel, Johannes Waldmann, Akihisa Yamada
25th International Conference on Tools and Algorithms for the Construction and Analysis of Systems, Lecture Notes in Computer Science 11429, pp. 155 – 166, 2019.

nonreach – A Tool for Nonreachability Analysis
Florian Meßner, Christian Sternagel
25th International Conference on Tools and Algorithms for the Construction and Analysis of Systems, Lecture Notes in Computer Science 11427, pp. 337 – 343, 2019.

Confluence Competition 2019
Aart Middeldorp, Julian Nagele, and Kiraku Shintani
Proceedings of the 25th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS 2019, part III), Lecture Notes in Computer Science 11429, pp. 25 – 40, 2019.

A Hierarchy of Polynomial Kernels
Jouke Witteveen, Ralph Bottesch, Leen Torenvliet
45th International Conference on Current Trends in Theory and Practice of Computer Science (SOFSEM 2019), Lecture Notes in Computer Science 11376, pp. 504 – 518, 2019.

Certified ACKBO
Alexander Lochmann, Christian Sternagel
8th ACM SIGPLAN International Conference on Certified Programs and Proofs,   pp. 144 – 151, 2019.

A Verified Ground Confluence Tool for Linear Variable-Separated Rewrite Systems in Isabelle/HOL
Bertram Felgenhauer, Aart Middeldorp, T. V. H. Prathamesh, and Franziska Rapp
8th ACM SIGPLAN International Conference on Certified Programs and Proofs,   pp. 132 – 143, 2019.

A Verified Implementation of Algebraic Numbers in Isabelle/HOL
Sebastiaan Joosten, René Thiemann, Akihisa Yamada
Journal of Automated Reasoning 64, pp. 363 – 389, 2020.

Reinforcement Learning of Theorem Proving
Cezary Kaliszyk, Josef Urban, Henryk Michalewski, Mirek Olsák
Advances in Neural Information Processing Systems,  31, pp. 8836 – 8847, 2018.

Learning Proof Search in Proof Assistants
Michael Färber
PhD thesis, University of Innsbruck, 2018.

A Verified Efficient Implementation of the LLL Basis Reduction Algorithm
Ralph Bottesch, Max W. Haslbeck, René Thiemann
22nd International Conference on Logic for Programming Artificial Intelligence and Reasoning, EPiC Series in Computing 57, pp. 164 – 180, 2018.

Deciding Confluence and Normal Form Properties of Ground Term Rewrite Systems Efficiently
Bertram Felgenhauer
Logical Methods in Computer Science 14(4:7), pp. 1 – 35, 2018.

IMP with Exceptions over Decorated Logic
Burak Ekici
Discrete Mathematics and Theoretical Computer Science 20(2), pp. 1 – 43, 2018.

Layer Systems for Confluence — Formalized
Bertram Felgenhauer and Franziska Rapp
Proceedings of the 15th International Colloquium on Theoretical Aspects of Computing (ICTAC 2018), Lecture Notes in Computer Science 11187, pp. 173 – 190, 2018.

Semantics of Mizar as an Isabelle Object Logic
Cezary Kaliszyk, Karol Pąk
Journal of Automated Reasoning  pp. 1 – 39, 2018.

On W[1]-Hardness as Evidence for Intractability
Ralph C. Bottesch
43rd International Symposium on Mathematical Foundations of Computer Science, Leibniz International Proceedings in Informatics 117, pp. 73:1 – 73:15, 2018.

Towards Mac Lane’s Comparison Theorem for the (co)Kleisli Construction in Coq
Burak Ekici
4th Workshop on Formal Mathematics for Mathematicians, CEUR Workshop Proceedings,  pp. 1 – 5, 2018.

First Experiments with Neural Translation of Informal to Formal Mathematics
Qingxiang Wang, Cezary Kaliszyk, Josef Urban
11th International Conference on Intelligent Computer Mathematics, LNCS 11006, pp. 255 – 270, 2018.

Isabelle Import Infrastructure for the Mizar Mathematical Library
Cezary Kaliszyk and Karol Pąk
11th International Conference on Intelligent Computer Mathematics, LNCS 11006, pp. 131 – 146, 2018.

MaedMax: A Maximal Ordered Completion Tool
Sarah Winkler, Georg Moser
Proceedings of the 9th International Joint Conference on Automated Reasoning, Lecture Notes in Artificial Intelligence 10900, pp. 472 – 480, 2018.

Towards a Unified Ordering for Superposition-Based Automated Reasoning
Jan Jakubuv, Cezary Kaliszyk
6th International Conference on Mathematical Software, Lecture Notes in Computer Science 10931, pp. 245 – 254, 2018.

Confluence Competition 2018
Takahito Aoto, Makoto Hamana, Nao Hirokawa, Aart Middeldorp, Julian Nagele, Naoki Nishida, Kiraku Shintani, and Harald Zankl
Proceedings of the 3rd International Conference on Formal Structures for Computation and Deduction (FSCD 2018), Leibniz International Proceedings in Informatics 108, pp. 32:1 – 32:5, 2018.

ProTeM: A Proof Term Manipulator (System Description)
Christina Kohl and Aart Middeldorp
Proceedings of the 3rd International Conference on Formal Structures for Computation and Deduction (FSCD 2018), Leibniz International Proceedings in Informatics 108, pp. 31:1 – 31:8, 2018.

Completion for Logically Constrained Rewriting
Sarah Winkler and Aart Middeldorp
Proceedings of the 3rd International Conference on Formal Structures for Computation and Deduction, Leibniz International Proceedings in Informatics 108, pp. 30:1 – 30:18, 2018.

Towards Formal Foundations for Game Theory
Julian Parsert, Cezary Kaliszyk
Interactive Theorem Proving, Lecture Notes in Computer Science 10895, pp. 495 – 503, 2018.

A Formalization of the LLL Basis Reduction Algorithm
Jose Divasón, Sebastiaan Joosten, René Thiemann, Akihisa Yamada
Proceedings of the 9th International Conference on Interactive Theorem Proving, Lecture Notes in Computer Science 10895, pp. 160 – 177, 2018.

CoCo 2018 Participant: CSI 1.2.1
Bertram Felgenhauer, Aart Middeldorp, Fabian Mitterwallner, and Julian Nagele
Proceedings of the 7th International Workshop on Confluence (IWC 2018),   pp. 76, 2018.

A Formally Verified Solver for Homogeneous Linear Diophantine Equations
Florian Meßner, Julian Parsert, Jonas Schöpf, Christian Sternagel
9th International Conference on Interactive Theorem Proving, Lecture Notes in Computer Science 10895, pp. 441 – 458, 2018.

Cops and CoCoWeb: Infrastructure for Confluence Tools
Nao Hirokawa, Julian Nagele, and Aart Middeldorp
Proceedings of the 9th International Joint Conference on Automated Reasoning (IJCAR 2018), Lecture Notes in Artificial Intelligence 10900, pp. 346 – 353, 2018.

FORT 2.0
Franziska Rapp, Aart Middeldorp
Proceedings of the 9th International Joint Conference on Automated Reasoning, Lecture Notes in Artificial Intelligence 10900, pp. 81 – 88, 2018.

Aligning Concepts across Proof Assistant Libraries
Thibault Gauthier, Cezary Kaliszyk
J. Symbolic Computation 90, pp. 89 – 123, 2018.

Learning-Assisted Reasoning within Proof Assistants
Thibault Gauthier
PhD thesis, University of Innsbruck,  2018.

Mechanizing Confluence: Automated and Certified Analysis of First- and Higher-Order Rewrite Systems
Julian Nagele
PhD thesis, University of Innsbruck, 2017.

Elementary equivalence in Artin groups of finite type
Arpan Kabira, T. V. H. Prathamesh, Rishi Vyas
International Journal of Algebra and Computation 28, pp. 331-344, 2018.

Hammer for Coq: Automation for Dependent Type Theory
Łukasz Czajka, Cezary Kaliszyk
J. Autom. Reasoning 61, pp. 423 – 453, 2018.

Efficient Certification of Complexity Proofs – Formalizing the Perron-Frobenius Theorem
Jose Divasón, Sebastiaan Joosten, Ondřej Kunčar, René Thiemann, Akihisa Yamada
7th ACM SIGPLAN International Conference on Certified Programs and Proofs (CPP 2018),   pp. 2-13, 2018.

Formal Microeconomic Foundations and the First Welfare Theorem
Julian Parsert, Cezary Kaliszyk
7th ACM SIGPLAN International Conference on Certified Programs and Proofs (CPP 2018),   pp. 91-101, 2018.

Isabelle Formalization of Set Theoretic Structures and Set Comprehensions
Cezary Kaliszyk, Karol Pąk
International Conference on Mathematical Aspects of Computer and Information Sciences (MACIS 2017), Lecture Notes in Computer Science 10693, pp. 163 – 178, 2017.

Reliable Confluence Analysis of Conditional Term Rewrite Systems
Thomas Sternagel
PhD thesis, University of Innsbruck, 2017.

System Description: Statistical Parsing of Informalized Mizar Formulas
Cezary Kaliszyk, Josef Urban, Jirí Vyskocil
19th International Symposium on Symbolic and Numeric Algorithms for Scientific Computing, IEEE Computer Society  pp. 169 – 172, 2017.

Constructing Cycles in the Simplex Method for DPLL(T)
Bertram Felgenhauer and Aart Middeldorp
Proceedings of the 14th International Colloquium on Theoretical Aspects of Computing (ICTAC 2017), Lecture Notes in Computer Science 10580, pp. 213 – 228, 2017.

CoCo 2017 Participant: FORT 1.0
Franziska Rapp and Aart Middeldorp
Proceedings of the 6th International Workshop on Confluence (IWC 2017),   pp. 78, 2017.

CoCo 2017 Participant: CSI 1.1
Bertram Felgenhauer, Aart Middeldorp, and Julian Nagele
Proceedings of the 6th International Workshop on Confluence (IWC 2017),   pp. 76, 2017.

Infinite Runs in Abstract Completion
Nao Hirokawa, Aart Middeldorp, Sarah Winkler, and Christian Sternagel
Proceedings of the 2nd International Conference on Formal Structures for Computation and Deduction (FSCD 2017), Leibniz International Proceedings in Informatics 84, pp. 19:1 – 19:16, 2017.

Progress in the Independent Certification of Mizar Mathematical Library in Isabelle
Cezary Kaliszyk and Karol Pąk
Federated Conference on Computer Science and Information Systems (2017), Annals of Computer Science and Information Systems 11, pp. 227 – 236, 2017.

Foundational (Co)datatypes and (Co)recursion for Higher-Order Logic
Julian Biendarra, Jasmin Blanchette, Aymeric Bouzy, Martin Desharnais, Mathias Fleury, Johannes Hölzl, Ondřej Kunčar, Andreas Lochbihler, Fabian Meier, Lorenz Panny, Andrei Popescu, Christian Sternagel, René Thiemann, Dmitriy Traytel
Proceedings of the 14th International Symposium on Frontiers of Combining Systems, LNCS 10483, pp. 3-21, 2017.

Automating Formalization by Statistical and Semantic Parsing of Mathematics
Cezary Kaliszyk, Josef Urban, Jiřı́ Vyskočil
8th International Conference on Interactive Theorem Proving, Lecture Notes in Computer Science 10499, pp. 12 – 27, 2017.

Certifying Safety and Termination Proofs for Integer Transition Systems
Marc Brockschmidt, Sebastiaan J. C. Joosten, René Thiemann, Akihisa Yamada
Proceedings of the 26th International Confluence on Automated Deduction, Lecture Notes in Computer Science 10395, pp. 454-471, 2017.

Certifying Confluence of Quasi-Decreasing Strongly Deterministic Conditional Term Rewrite Systems
Christian Sternagel, Thomas Sternagel
Proceedings of the 26th International Confluence on Automated Deduction, LNCS 10395, pp. 413-431, 2017.

CSI: New Evidence – A Progress Report
Julian Nagele, Bertram Felgenhauer, and Aart Middeldorp
Proceedings of the 26th International Conference on Automated Deduction (CADE-26), Lecture Notes in Artificial Intelligence 10395, pp. 385 – 397, 2017.

Monte Carlo Tableau Proof Search
Michael Färber, Cezary Kaliszyk, Josef Urban
26th International Conference on Automated Deduction, LNCS 10395, pp. 563-579, 2017.

Classification of Alignments Between Concepts of Formal Mathematical Systems
Dennis Müller, Thibault Gauthier, Cezary Kaliszyk, Michael Kohlhase, Florian Rabe
10th International Conference on Intelligent Computer Mathematics, LNCS 10383, pp. 83-98, 2017.

Presentation and Manipulation of Mizar Properties in an Isabelle Object Logic
Cezary Kaliszyk and Karol Pąk
10th International Conference on Intelligent Computer Mathematics, LNCS 10383, pp. 193-207, 2017.

Verifying Procedural Programs via Constrained Rewriting Induction
Carsten Fuhs, Cynthia Kop, Naoki Nishida
ACM Transactions on Computational Logic 18(2), pp. 14:1 – 14:50, 2017.

A formal proof of the Kepler conjecture
THOMAS HALES, MARK ADAMS, GERTRUD BAUER, TAT DAT DANG, JOHN HARRISON, LE TRUONG HOANG, CEZARY KALISZYK, VICTOR MAGRON, SEAN MCLAUGHLIN, TAT THANG NGUYEN, QUANG TRUONG NGUYEN, TOBIAS NIPKOW, STEVEN OBUA, JOSEPH PLESO, JASON RUTE, ALEXEY SOLOVYEV, THI HOAI AN TA, NAM TRUNG TRAN, THI DIEP TRIEU, JOSEF URBAN, KY VU, ROLAND ZUMKELLER
Forum of Mathematics, Pi,  5, pp. 1-29, 2017.

Parsing and Printing of and with Triples
Sebastiaan J. C. Joosten
Relational and Algebraic Methods in Computer Science. RAMICS 2017, Lecture Notes in Computer Science 10226, pp. 159 – 176, 2017.

Certifying Confluence Proofs via Relative Termination and Rule Labeling
Julian Nagele, Bertram Felgenhauer, and Harald Zankl
Logical Methods in Computer Science,  13(2:4), pp. 1 – 27, 2017.

Deep Network Guided Proof Search
Sarah Loos, Geoffrey Irving, Christian Szegedy, Cezary Kaliszyk.
21st International Conference on Logic for Programming, Artificial Intelligence and Reasoning, EPiC 46, pp. 85-105, 2017.

TacticToe: Learning to Reason with HOL4 Tactics
Thibault Gauthier, Cezary Kaliszyk, Josef Urban
21st International Conference on Logic for Programming, Artificial Intelligence and Reasoning, EPIC 46, pp. 125-143, 2017.

Wikis and Collaborative Systems for Large Formal Mathematics
Cezary Kaliszy, Josef Urban
Post proceedings of Semantic Web Collaborative Spaces, LNCS  pp. 35-52, 2016.

A Formalization of the Berlekamp-Zassenhaus Factorization Algorithm
Jose Divason, Sebastiaan J. C. Joosten, Rene Thiemann and Akihisa Yamada
Proceedings of the 6th ACM SIGPLAN Conference on Certified Programs and Proofs (CPP 2017),   pp. 17 – 29, 2017.

Subresultants
Sebastiaan Joosten and René Thiemann and Akihisa Yamada
Archive of Formal Proofs 2017.

Reachability, Confluence, and Termination Analysis with State-Compatible Automata
Bertram Felgenhauer and René Thiemann
Information and Computation 253(3), pp. 467 – 483, 2017.

Towards Formal Proof Metrics
David Aspinall, Cezary Kaliszyk
19th International Conference on Fundamental Approaches to Software Engineering, LNCS 9633, pp. 325-341, 2016.

Relative Termination via Dependency Pairs
José Iborra, Naoki Nishida, Germán Vidal, Akihisa Yamada
Journal of Automated Reasoning 58(3), pp. 391 – 411, 2017.

Complexity of Conditional Term Rewriting
Cynthia Kop, Aart Middeldorp, Thomas Sternagel
Logical Methods in Computer Science 13(1:6), pp. 1 – 56, 2017.

Analyzing Program Termination and Complexity Automatically with AProVE
Jürgen Giesl, Cornelius Aschermann, Marc Brockschmidt, Fabian Emmes, Florian Frohn, Carsten Fuhs, Jera Hensel, Carsten Otto, Martin Plücker, Peter Schneider-Kamp, Thomas Ströder, Stephanie Swiderski, René Thiemann
Journal of Automated Reasoning,  58(1), pp. 3 – 31, 2017.

Bar Recursion over Finite Partial Functions
Paulo Oliva and Thomas Powell
Annals of Pure and Applied Logic 2016.

Distance-Integrated Combinatorial Testing
Eun-Hye Choi, Cyrille Artho, Takashi Kitamura, Osamu Mizuno, and Akihisa Yamada
Proceedings of the 27th International Symposium on Software Reliability Engineering (ISSRE 2016),   pp. 93 – 104, 2016.

Improving Statistical Linguistic Algorithms for Parsing Mathematics
Cezary Kaliszyk, Josef Urban, Jiri Vyskočil
11th International Workshop on the Implementation of Logics, EPiC 40, pp. 27-36, 2016.

Greedy Combinatorial Test Case Generation using Unsatisfiable Cores
Akihisa Yamada, Armin Biere, Cyrille Artho, Takashi Kitamura, and Eun-Hye Choi
Proceedings of the 31st IEEE/ACM International Conference on Automated Software Engineering (ASE 2016),   pp. 614 – 624, 2016.

AC Dependency Pairs Revisited
Akihisa Yamada, Christian Sternagel, René Thiemann, and Keiichirou Kusakari
Proceedings of the 25th EACSL Annual Conference on Computer Science Logic (CSL 2016), Leibniz International Proceedings in Informatics 62, pp. 8:1 – 8:16, 2016.

Algebraic Numbers in Isabelle/HOL
René Thiemann and Akihisa Yamada
Proceedings of the 7th International Conference on Interactive Theorem Proving (ITP 2016), Lecture Notes in Computer Science 9807, pp. 391 – 408, 2016.

Certification of Classical Confluence Results for Left-Linear Term Rewrite Systems
Julian Nagele and Aart Middeldorp
Proceedings of the 7th International Conference on Interactive Theorem Proving (ITP 2016), Lecture Notes in Computer Science 9807, pp. 290 – 306, 2016.

What’s in a Theorem Name?
David Aspinall and Cezary Kaliszyk
Proceedings of the 7th Interactive Theorem Proving (ITP 2016), Lecture Notes in Computer Science 9807, pp. 459 – 465, 2016.

No Choice: Reconstruction of First-order ATP Proofs without Skolem Function
Michael Färber, Cezary Kaliszyk
5th Workshop on Practical Aspects of Automated Reasoning, CEUR-WS 1635, pp. 24-31, 2016.

TH1: The TPTP Typed Higher-Order Form with Rank-1 Polymorphism
Cezary Kaliszyk, Geoff Sutcliffe, Florian Rabe
5th Workshop on Practical Aspects of Automated Reasoning, CEUR-WS 1635, pp. 41-55, 2016.

Gödel’s Functional Interpretation and the Concept of Learning
Thomas Powell
Proceedings of the 31st Annual ACM/IEEE Symposium on Logic in Computer Science (LICS 2016),   pp. 136 – 145, 2016.

Normalisation by Random Descent
Vincent van Oostrom and Yoshihito Toyama
Proceedings of the 1st International Conference on Formal Structures for Computation and Deduction (FSCD 2016), Leibniz International Proceedings in Informatics 52, pp. 32:1 – 32:18, 2016.

Interaction Automata and the ia2d Interpreter
Stéphane Gimenez and David Obwaller
Proceedings of the 1st International Conference on Formal Structures for Computation and Deduction (FSCD 2016), Leibniz International Proceedings in Informatics 52, pp. 35:1 – 35:11, 2016.

Certifying Confluence of Almost Orthogonal CTRSs via Exact Tree Automata Completion
Christian Sternagel and Thomas Sternagel
Proceedings of the 1st International Conference on Formal Structures for Computation and Deduction (FSCD 2016), Leibniz International Proceedings in Informatics 52, pp. 29:1-29:16, 2016.

Goal Translation for a Hammer for Coq
Łukasz Czajka and Cezary Kaliszyk
1st International Workshop on Hammers for Type Theories, EPTCS 210, pp. 13-20, 2016.

Complexity of Acyclic Term Graph Rewriting
Martin Avanzini and Georg Moser
Proceedings of the 1st International Conference on Formal Structures for Computation and Deduction (FSCD 2016), Leibniz International Proceedings in Informatics 52, pp. 10:1 – 10:18, 2016.

Automating the First-Order Theory of Left-Linear Right-Ground Term Rewrite Systems
Franziska Rapp and Aart Middeldorp
Proceedings of the 1st International Conference on Formal Structures for Computation and Deduction (FSCD 2016), Leibniz International Proceedings in Informatics 52, pp. 36:1 – 36:12, 2016.

A combination framework for complexity
Martin Avanzini and Georg Moser
Information and Computation 248, pp. 22 – 55, 2016.

Perron-Frobenius Theorem for Spectral Radius Analysis
Jose Divasón and Ondřej Kunčar and René Thiemann and Akihisa Yamada
Archive of Formal Proofs 2016.

TcT: Tyrolean Complexity Tool
Martin Avanzini, Georg Moser and Michael Schaper
Proceedings of the 22nd International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS 2016), Lecture Notes in Computer Science 9636, pp. 407 – 423, 2016.

AC-KBO Revisited
Akihisa Yamada, Sarah Winkler, Nao Hirokawa, and Aart Middeldorp
Theory and Practice of Logic Programming 16(2), pp. 163 – 188, 2016.

A Learning-Based Fact Selector for Isabelle/HOL
Jasmin Christian Blanchette, David Greenaway, Cezary Kaliszyk, Daniel Kühlwein, and Josef Urban
Journal of Automated Reasoning Volume 53, Number 3, pp. 219 – 244, 2016.

Hammering towards QED
Jasmin C. Blanchette, Cezary Kaliszyk, Lawrence C. Paulson, and Josef Urban
Journal of Formalized Reasoning 9(1), pp. 101 – 148, 2016.

The Complexity of Interaction
Stéphane Gimenez and Georg Moser
Proceedings of the 43rd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL 2016),  243 – 255, 2016.

Towards a Mizar Environment for Isabelle: Foundations and Language
Cezary Kaliszyk, Karol Pąk, and Josef Urban
Proceedings of the 5th ACM SIGPLAN Conference on Certified Programs and Proofs (CPP 2016),   pp. 58 – 65, 2016.

Formalizing Jordan Normal Forms in Isabelle/HOL
René Thiemann and Akihisa Yamada
Proceedings of the 5th ACM SIGPLAN Conference on Certified Programs and Proofs (CPP 2016),   pp. 88 – 99, 2016.

Improving Automation in Interactive Theorem Provers by Efficient Encoding of Lambda-Abstractions
Łukasz Czajka
Proceedings of the 5th ACM SIGPLAN Conference on Certified Programs and Proofs (CPP 2016),   pp. 49 – 57, 2016.

Workshop on Hammers for Type Theory 2016
Jasmin Blanchette, Cezary Kaliszyk (eds)
Proceedings First Workshop on Hammers for Type Theory, HaTT 2016,  210, 2016.

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.

Machine Learning of Coq Proof Guidance: First Experiments
Cezary Kaliszyk, Lionel Mamane, and Josef Urban
Proceedings of the 6th International Symposium on Symbolic Computation in Software Science (SCSS 2014), EasyChair Proceedings in Computer Science 30, pp. 27 – 34, 2014.

The Certification Problem Format
Christian Sternagel and René Thiemann
Proceedings of the 11th International Workshop on User Interfaces for Theorem Provers (UITP 2014), Electronic Proceedings in Theoretical Computer Science 167, pp. 61 – 72, 2014.

Automatic Constrained Rewriting Induction towards Verifying Procedural Programs
Cynthia Kop and Naoki Nishida
Proceedings of the 12th Asian Symposium on Programming Languages and Systems (APLAS 2014), Lecture Notes in Computer Science 8858, pp. 334 – 353, 2014.

Certification of Nontermination Proofs using Strategies and Nonlooping Derivations
Julian Nagele, René Thiemann, and Sarah Winkler
Proceedings of the 6th International Conference on Verified Software: Theories, Tools, and Experiments (VSTTE 2014), Lecture Notes in Computer Science 8471, pp. 216 – 232, 2014.

Challenges in Automation of Rewriting
Harald Zankl
Habilitation thesis, University of Innsbruck, 2014.

Polynomial Interpretations over the Natural, Rational and Real Numbers Revisited
Friedrich Neurauter and Aart Middeldorp
Logical Methods in Computer Science 10(3:22), pp. 1 – 28, 2014.

Proving Termination of Programs Automatically with AProVE
Jürgen Giesl, Marc Brockschmidt, Fabian Emmes, Florian Frohn, Carsten Fuhs, Carsten Otto, Martin Plücker, Peter Schneider-Kamp, Thomas Ströder, Stephanie Swiderski, and René Thiemann
Proceedings of the 7th International Joint Conference on Automated Reasoning (IJCAR 2014), Lecture Notes in Computer Science 8562, pp. 184 – 191, 2014.

Automating Elementary Interpretations
Harald Zankl, Sarah Winkler, and Aart Middeldorp
Proceedings of the 14th International Workshop on Termination (WST 2014),   pp. 75 – 79, 2014.

A New and Formalized Proof of Abstract Completion
Nao Hirokawa, Aart Middeldorp, and Christian Sternagel
Proceedings of the 5th International Conference on Interactive Theorem Proving (ITP 2014), Lecture Notes in Computer Science 8558, pp. 292 – 307, 2014.

Conditional Confluence (System Description)
Thomas Sternagel and Aart Middeldorp
Proceedings of the Joint 25th International Conference on Rewriting Techniques and Applications and 12th International Conference on Typed Lambda Calculi and Applications (RTA-TLCA 2014), Lecture Notes in Computer Science 8560, pp. 456 – 465, 2014.

Automated Complexity Analysis Based on Context-Sensitive Rewriting
Nao Hirokawa and Georg Moser
Proceedings of the Joint 25th International Conference on Rewriting Techniques and Applications and 12th International Conference on Typed Lambda Calculi and Applications (RTA-TLCA 2014), Lecture Notes in Computer Science 8560, pp. 257 – 271, 2014.

Amortised Resource Analysis and Typed Polynomial Interpretations
Martin Hofmann and Georg Moser
Proceedings of the Joint 25th International Conference on Rewriting Techniques and Applications and 12th International Conference on Typed Lambda Calculi and Applications (RTA-TLCA 2014), Lecture Notes in Computer Science 8560, pp. 272 – 286, 2014.

First-Order Formative Rules
Carsten Fuhs and Cynthia Kop
Proceedings of the Joint 25th International Conference on Rewriting Techniques and Applications and 12th International Conference on Typed Lambda Calculi and Applications (RTA-TLCA 2014), Lecture Notes in Computer Science 8560, pp. 240 – 256, 2014.

Formalizing Monotone Algebras for Certification of Termination and Complexity Proofs
Christian Sternagel and René Thiemann
Proceedings of the Joint 25th International Conference on Rewriting Techniques and Applications and 12th International Conference on Typed Lambda Calculi and Applications (RTA-TLCA 2014), Lecture Notes in Computer Science 8560, pp. 441 – 455, 2014.

Initial Experiments with TPTP-style Automated Theorem Provers on ACL2 Problems
Sebastiaan Joosten, Cezary Kaliszyk, and Josef Urban
Proceedings of the 12th International Workshop on the ACL2 Theorem Prover and its Applications (ACL2 2014), Electronic Proceedings in Theoretical Computer Science 152, pp. 77 – 85, 2014.

Developing Corpus-based Translation Methods between Informal and Formal Mathematics
Cezary Kaliszyk, Josef Urban, Jiří Vyskočil, and Herman Geuvers
Proceedings of the 7th Conference on Intelligent Computer Mathematics (CICM 2014), Logical Methods in Computer Science 8543, pp. 435 – 439, 2014.

Towards Knowledge Management for HOL Light
Cezary Kaliszyk and Florian Rabe
Proceedings of the 7th Conference on Intelligent Computer Mathematics (CICM 2014), Lecture Notes in Computer Science 8543, pp. 357 – 372, 2014.

Matching Concepts across HOL Libraries
Thibault Gauthier and Cezary Kaliszyk
Proceedings of the 7th Conference on Intelligent Computer Mathematics (CICM 2014), Lecture Notes in Computer Science 8543, pp. 267 – 281, 2014.

Learning-Assisted Automated Reasoning with Flyspeck
Cezary Kaliszyk and Josef Urban
Journal of Automated Reasoning 53(2), pp. 173 – 213, 2014.

Certified Kruskal’s Tree Theorem
Christian Sternagel
Journal of Formalized Reasoning 7(1), pp. 45 – 62, 2014.

AC-KBO Revisited
Akihisa Yamada, Sarah Winkler, Nao Hirokawa, and Aart Middeldorp
Proceedings of the 12th International Symposium on Functional and Logic Programming (FLOPS 2014), Lecture Notes in Computer Science 8475, pp. 319 – 335, 2014.

Modular Complexity Analysis for Term Rewriting
Harald Zankl and Martin Korp
Logical Methods in Computer Science 10(1:19), pp. 1 – 33, 2014.

Reachability Analysis with State-Compatible Automata
Bertram Felgenhauer and René Thiemann
Proceedings of the 8th International Conference on Language and Automata Theory and Applications (LATA 2014), Lecture Notes in Computer Science 8370, pp. 347 – 359, 2014.

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.

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.

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.

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.

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.