All Publications

Infinite Runs in Abstract Completion
Nao Hirokawa, Aart Middeldorp, Sarah Winkler, Christian Sternagel
2nd International Conference on Formal Structures for Computation and Deduction, Leibniz International Proceedings in Informatics 84, pp. 19:1-19:16, 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.

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, Aart Middeldorp
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.

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, 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, 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.

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.

Layer Systems for Proving Confluence
Bertram Felgenhauer, Harald Zankl, and Aart Middeldorp
Proceedings of the 30th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2011), Leibniz International Proceedings in Informatics 13, pp. 288 – 299, 2011.

Generalized and Formalized Uncurrying
Christian Sternagel and René Thiemann
Proceedings of the 8th International Symposium on Frontiers of Combining Systems (FroCoS 2011), Lecture Notes in Artificial Intelligence 6989, pp. 243 – 258, 2011.

The Exact Hardness of Deciding Derivational and Runtime Complexity
Andreas Schnabl and Jakob Grue Simonsen
Proceedings of the 25th International Workshop on Computer Science Logic / 20th Annual Conference of the EACSL (CSL 2011), Leibniz International Proceedings in Informatics 12, pp. 481 – 495, 2011.

Decreasing Diagrams and Relative Termination
Nao Hirokawa and Aart Middeldorp
Journal of Automated Reasoning 47(4), pp. 481 – 501, 2011.

Termination of Isabelle Functions via Termination of Rewriting
Alexander Krauss, Christian Sternagel, René Thiemann, Carsten Fuhs, and Jürgen Giesl
Proceedings of the 2nd International Conference on Interactive Theorem Proving (ITP 2011), Lecture Notes in Computer Science 6898, pp. 152 – 167, 2011.

CSI – A Confluence Tool
Harald Zankl, Bertram Felgenhauer, and Aart Middeldorp
Proceedings of the 23rd International Conference on Automated Deduction (CADE 2011), Lecture Notes in Artificial Intelligence 6803, pp. 499 – 505, 2011.

AC Completion with Termination Tools
Sarah Winkler and Aart Middeldorp
Proceedings of the 23rd International Conference on Automated Deduction (CADE 2011), Lecture Notes in Artificial Intelligence 6803, pp. 492 – 498, 2011.

On Transfinite Knuth-Bendix Orders
Laura Kovács, Georg Moser, and Andrei Voronkov
Proceedings of the 23rd International Conference on Automated Deduction (CADE 2011), Lecture Notes in Artificial Intelligence 6803, pp. 384 – 399, 2011.

The Derivational Complexity Induced by the Dependency Pair Method
Georg Moser and Andreas Schnabl
Logical Methods in Computer Science 7(3:1), pp. 1 – 38, 2011.

Joint Spectral Radius Theory for Automated Complexity Analysis of Rewrite Systems
Aart Middeldorp, Georg Moser, Friedrich Neurauter, Johannes Waldmann, and Harald Zankl
Proceedings of the 4th International Conference on Algebraic Informatics (CAI 2011), Lecture Notes in Computer Science 6742, pp. 1 – 20, 2011.

Labelings for Decreasing Diagrams
Harald Zankl, Bertram Felgenhauer, and Aart Middeldorp
Proceedings of the 22nd International Conference on Rewriting Techniques and Applications (RTA 2011), Leibniz International Proceedings in Informatics 10, pp. 377 – 392, 2011.

Modular and Certified Semantic Labeling and Unlabeling
Christian Sternagel and René Thiemann
Proceedings of the 22nd International Conference on Rewriting Techniques and Applications (RTA 2011), Leibniz International Proceedings in Informatics 10, pp. 329 – 344, 2011.

Revisiting Matrix Interpretations for Proving Termination of Term Rewriting
Friedrich Neurauter and Aart Middeldorp
Proceedings of the 22nd International Conference on Rewriting Techniques and Applications (RTA 2011), Leibniz International Proceedings in Informatics 10, pp. 251 – 266, 2011.

Termination Proofs in the Dependency Pair Framework May Induce Multiple Recursive Derivational Complexity
Georg Moser and Andreas Schnabl
Proceedings of the 22nd International Conference on Rewriting Techniques and Applications (RTA 2011), Leibniz International Proceedings in Informatics 10, pp. 235 – 250, 2011.

A Path Order for Rewrite Systems that Compute Exponential Time Functions
Martin Avanzini, Naohi Eguchi, and Georg Moser
Proceedings of the 22nd International Conference on Rewriting Techniques and Applications (RTA 2011), Leibniz International Proceedings in Informatics 10, pp. 123 – 138, 2011.

Executable Transitive Closures of Finite Relations
Christian Sternagel and René Thiemann
The Archive of Formal Proofs, 2011.

Uncurrying for Innermost Termination and Derivational Complexity
Harald Zankl, Nao Hirokawa, and Aart Middeldorp
Proceedings of the 5th International Workshop on Higher-Order Rewriting (HOR 2010), Electronic Proceedings in Theoretical Computer Science 49, pp. 46 – 57, 2011.

Automated Termination Proofs for Haskell by Term Rewriting
Jürgen Giesl, Matthias Raffelsieper, Peter Schneider-Kamp, Stephan Swiderski, and René Thiemann
ACM Transactions on Programming Languages and Systems 33(2), 2011.

Loops under Strategies … Continued
René Thiemann, Christian Sternagel, Jürgen Giesl, and Peter Schneider-Kamp
Proceedings of the 1st International Workshop on Strategies in Rewriting, Proving, and Programming (IWS 2010), Electronic Proceedings in Theoretical Computer Science 44, pp. 51 – 65, 2010.

Automatic Certification of Termination Proofs
Christian Sternagel
PhD thesis, University of Innsbruck, 2010.

Termination Analysis by Tree Automata Completion
Martin Korp
PhD thesis, University of Innsbruck, 2010.

Revisiting Matrix Interpretations for Polynomial Derivational Complexity of Term Rewriting
Friedrich Neurauter, Harald Zankl, and Aart Middeldorp
Proceedings of the 17th International Conference on Logic for Programming, Artificial Intelligence, and Reasoning (LPAR-17), Lecture Notes in Computer Science (Advanced Research in Computing and Software Science) 6397, pp. 550 – 564, 2010.

Characterising Space Complexity Classes via Knuth-Bendix Orders
Guillaume Bonfante and Georg Moser
Proceedings of the 17th International Conference on Logic for Programming, Artificial Intelligence, and Reasoning (LPAR-17), Lecture Notes in Computer Science (Advanced Research in Computing and Software Science) 6397, pp. 142 – 156, 2010.

Signature Extensions Preserve Termination – An Alternative Proof via Dependency Pairs
Christian Sternagel and René Thiemann
Proceedings of the 19th Annual Conference of the European Association for Computer Science Logic (CSL 2010), Lecture Notes in Computer Science 6247, pp. 514 – 528, 2010.

Executable Multivariate Polynomials
Christian Sternagel and René Thiemann
The Archive of Formal Proofs, 2010.

POP* and Semantic Labeling using SAT
Martin Avanzini
Interfaces: Explorations in Logic, Language and Computation, Lecture Notes in Artificial Intelligence 6211, pp. 155 – 166, 2010.

Cdiprover3: A Tool for Proving Derivational Complexities of Term Rewriting Systems
Andreas Schnabl
Interfaces: Explorations in Logic, Language and Computation, Lecture Notes in Artificial Intelligence 6211, pp. 142 – 154, 2010.

Termination Tools in Ordered Completion
Sarah Winkler and Aart Middeldorp
Proceedings of the 5th International Joint Conference on Automated Reasoning (IJCAR 2010), Lecture Notes in Artificial Intelligence 6173, pp. 518 – 532, 2010.

Monotonicity Criteria for Polynomial Interpretations over the Naturals
Friedrich Neurauter, Harald Zankl, and Aart Middeldorp
Proceedings of the 5th International Joint Conference on Automated Reasoning (IJCAR 2010), Lecture Notes in Artificial Intelligence 6173, pp. 502 – 517, 2010.

Decreasing Diagrams and Relative Termination
Nao Hirokawa and Aart Middeldorp
Proceedings of the 5th International Joint Conference on Automated Reasoning (IJCAR 2010), Lecture Notes in Artificial Intelligence 6173, pp. 487 – 501, 2010.

Executable Matrix Operations on Matrices of Arbitrary Dimensions
Christian Sternagel and René Thiemann
The Archive of Formal Proofs, 2010.

Abstract Rewriting
Christian Sternagel and René Thiemann
The Archive of Formal Proofs, 2010.

Optimizing mkbTT (System Description)
Sarah Winkler, Haruhiko Sato, Aart Middeldorp, and Masahito Kurihara
Proceedings of the 21st International Conference on Rewriting Techniques and Applications (RTA 2010), Leibniz International Proceedings in Informatics 6, pp. 373 – 384, 2010.

Modular Complexity Analysis via Relative Complexity
Harald Zankl and Martin Korp
Proceedings of the 21st International Conference on Rewriting Techniques and Applications (RTA 2010), Leibniz International Proceedings in Informatics 6, pp. 385 – 400, 2010.

Certified Subterm Criterion and Certified Usable Rules
Christian Sternagel and René Thiemann
Proceedings of the 21st International Conference on Rewriting Techniques and Applications (RTA 2010), Leibniz International Proceedings in Informatics 6, pp. 325 – 340, 2010.

Polynomial Interpretations over the Reals do not Subsume Polynomial Interpretations over the Integers
Friedrich Neurauter and Aart Middeldorp
Proceedings of the 21st International Conference on Rewriting Techniques and Applications (RTA 2010), Leibniz International Proceedings in Informatics 6, pp. 243 – 258, 2010.

Closing the Gap Between Runtime Complexity and Polytime Complexity
Martin Avanzini and Georg Moser
Proceedings of the 21st International Conference on Rewriting Techniques and Applications (RTA 2010), Leibniz International Proceedings in Informatics 6, pp. 33 – 48, 2010.

Satisfiability of Non-Linear (Ir)rational Arithmetic
Harald Zankl and Aart Middeldorp
Proceedings of the 16th International Conference on Logic for Programming and Automated Reasoning (LPAR-16), Lecture Notes in Artificial Intelligence 6355, pp. 481 – 500, 2010.

Complexity Analysis by Graph Rewriting
Martin Avanzini and Georg Moser
Proceedings of the 10th International Symposium on Functional and Logic Programming (FLOPS 2010), Lecture Notes in Computer Science 6009, pp. 257 – 271, 2010.

Finding and Certifying Loops
Harald Zankl, Christian Sternagel, Dieter Hofbauer, and Aart Middeldorp
Proceedings of the 36th International Conference on Current Trends in Theory and Practice of Computer Science (SOFSEM 2010), Lecture Notes in Computer Science 5901, pp. 755 – 766, 2010.

Lazy Termination Analysis
Harald Zankl
PhD thesis, University of Innsbruck, 2009.

Increasing interpretations
Harald Zankl and Aart Middeldorp
Annals of Mathematics and Artificial Intelligence 56(1), pp. 87 – 108, 2009.

Match-Bounds Revisited
Martin Korp and Aart Middeldorp
Information and Computation 207(11), pp. 1259 – 1283, 2009.

Automated Termination Proofs for Logic Programs by Term Rewriting
Peter Schneider-Kamp, Jürgen Giesl, Alexander Serebrenik, and René Thiemann
ACM Transactions on Computational Logic 11(1), pp. 1 – 52, 2009.

Proof Theory at Work: Complexity Analysis of Term Rewrite Systems
Georg Moser
Habilitation thesis, University of Innsbruck,  2009.

Certification of Termination Proofs using CeTA
René Thiemann and Christian Sternagel
Proceedings of the 22nd International Conference on Theorem Proving in Higher-Order Logics (TPHOLs 2009), Lecture Notes in Computer Science 5674, pp. 452 – 468, 2009.

Transforming SAT into Termination of Rewriting
Harald Zankl, Christian Sternagel, and Aart Middeldorp
Proceedings of the 17th International Workshop on Functional and (Constraint) Logic Programming (WFLP 2008), Electronic Notes in Theoretical Computer Science 246, pp. 199 – 214, 2009.

Beyond Dependency Graphs
Martin Korp and Aart Middeldorp
Proceedings of the 22nd International Conference on Automated Deduction (CADE 2009), Lecture Notes in Artificial Intelligence 5663, pp. 339 – 354, 2009.

KBO Orientability
Harald Zankl, Nao Hirokawa, and Aart Middeldorp
Journal of Automated Reasoning 43(2), pp. 173 – 201, 2009.

The Hydra Battle and Cichon’s Principle
Georg Moser
Applicable Algebra in Engineering, Communication and Computing 20(2), pp. 133 – 158, 2009.