Linear Termination is Undecidable

Fabian Mitterwallner, Aart Middeldorp, René Thiemann
Proceedings of the 39th Annual ACM/IEEE Symposium on Logic in Computer Science (LICS 2024), ACM  pp. 57:1-57:12, 2024.

Equational Theories and Validity for Logically Constrained Term Rewriting

Takahito Aoto, Naoki Nishida, Jonas Schöpf
Proceedings of the 9th International Conference on Formal Structures for Computation and Deduction (FSCD 2024), Leibniz International Proceedings in Informatics (LIPIcs) 299, pp. 31:1-31:21, 2024.

Confluence of Logically Constrained Rewrite Systems Revisited

Jonas Schöpf, Fabian Mitterwallner, Aart Middeldorp
Proceedings of the 12th International Joint Conference on Automated Reasoning (IJCAR 2024), Lecture Notes in Artificial Intelligence 14740, pp. 298-316, 2024.

Guiding Enumerative Program Synthesis with Large Language Models

Yixuan Li, Julian Parsert, Elizabeth Polgreen
Computer Aided Verification – 36th International Conference (CAV), Lecture Notes in Computer Science 14682, pp. 280-301, 2024.

Details

Category: Publications

Published: 25 April 2025

Lambert Series

Manuel Eberl
Archive of Formal Proofs 2023.

The Polylogarithm Function

Manuel Eberl
Archive of Formal Proofs 2023.

The Cardinality of the Continuum

Manuel Eberl
Archive of Formal Proofs 2023.

Two theorems about the geometry of the critical points of a complex polynomial

Manuel Eberl
Archive of Formal Proofs 2023.

Elimination of Repeated Factors Algorithm

Katharina Kreuzer, Manuel Eberl
Archive of Formal Proofs 2023.

Perfect Fields

Manuel Eberl, Katharina Kreuzer
Archive of Formal Proofs 2023.

Chebyshev Polynomials

Manuel Eberl
Archive of Formal Proofs 2023.

Learning Proof Transformations and Its Applications in Interactive Theorem Proving

Liao Zhang, Lasse Blaauwbroek, Cezary Kaliszyk, Josef Urban
Frontiers of Combining Systems – 14th International Symposium, FroCoS 2023, pp. 236-254, 2023.

Confluence Criteria for Logically Constrained Rewrite Systems

Jonas Schöpf, Aart Middeldorp
Proceedings of the 29th International Conference on Automata Deduction (CADE-29), Lecture Notes in Artificial Intelligence 14132, pp. 474-490, 2023.

Left-Linear Completion with AC Axioms

Johannes Niederhauser, Nao Hirokawa, Aart Middeldorp
Proceedings of the 29th International Conference on Automata Deduction (CADE-29), Lecture Notes in Artificial Intelligence 14132, pp. 401-418, 2023.

VizAR: Visualization of Automated Reasoning Proofs (System Description)

Jan Jakubův and Cezary Kaliszyk
Intelligent Computer Mathematics – 16th International Conference, CICM 2023, pp. 303-308, 2023.

Formalizing Almost Development Closed Critical Pairs

Christina Kohl, Aart Middeldorp
Proceedings of the 14th International Conference on Interactive Theorem Proving, Leibniz International Proceedings in Informatics 268, pp. 38:1-38:8, 2023.

MizAR 60 for Mizar 50

Jan Jakubův, Karel Chvalovský, Zarathustra Amadeus Goertzel, Cezary Kaliszyk, Mirek Olšák, Bartosz Piotrowski, Stephan Schulz, Martin Suda, Josef Urban
14th International Conference on Interactive Theorem Proving, pp. 19:1-19:22, 2023.

Hydra Battles and AC Termination

Nao Hirokawa, Aart Middeldorp
Proceedings of the 8th International Conference on Formal Structures for Computation and Deduction, Leibniz International Proceedings in Informatics 260, pp. 22:1-12:16, 2023.

Executable Randomized Algorithms

Emin Karayel, Manuel Eberl
Archive of Formal Proofs 2023.

Experiments on Infinite Model Finding in SMT Solving

Julian Parsert, Chad E. Brown, Mikolas Janota, Cezary Kaliszyk
24th International Conference on Logic for Programming, Artificial Intelligence and Reasoning, pp. 317-328, 2023.

A Verified Efficient Implementation of the Weighted Path Order

René Thiemann, Elias Wenninger
Archive of Formal Proofs 2023.

Combining Higher-Order Logic with Set Theory Formalizations

Cezary Kaliszyk and Karol Pąk
Journal of Automated Reasoning 2023.

First-Order Theory of Rewriting for Linear Variable-Separated Rewrite Systems: Automation, Formalization, Certification

Aart Middeldorp, Alexander Lochmann, Fabian Mitterwallner
Journal of Automated Reasoning 67, 2023.

A Formalization of the Development Closedness Criterion for Left-Linear Term Rewrite Systems

Christina Kohl, Aart Middeldorp
Proceedings of the 12th ACM SIGPLAN International Conference on Certified Programs and Proofs (CPP 2023), pp. 197-210, 2023.

Details

Category: Publications

Published: 25 April 2025

The Incompatibility of Strategy-Proofness and Representation in Party-Approval Multi-Winner Elections

Théo Delemazure, Tom Demeulemeester, Manuel Eberl, Jonas Israel, Patrick Lederer
Archive of Formal Proofs 2022.

Proofgold: Blockchain for Formal Methods

Chad E. Brown, Cezary Kaliszyk, Thibault Gauthier, Josef Urban
4th International Workshop on Formal Methods for Blockchains, FMBC 2022, pp. 4:1-4:15, 2022.

The Hales-Jewett Theorem

Ujkan Sulejmani, Manuel Eberl, Katharina Kreuzer
Archive of Formal Proofs 2022.

Lazy Paramodulation in Practice

Grzegorz Prusak, Cezary Kaliszyk
Proceedings of the Workshop on Practical Aspects of Automated Reasoning, PAAR 2022, 2022.

The Isabelle Enigma

Zar Goerzel, Jan Jakubův, Cezary Kaliszyk, Mirek Olšák, Jelle Piepenbroek, Josef Urban
13th International Conference on Interactive Theorem Proving, ITP 2022, pp. 16:1—16:21, 2022.

Formalizing a diophantine description of the set of primes (short paper)

Karol Pąk, Cezary Kaliszyk
13th International Conference on Interactive Theorem Proving, ITP 2022, pp. 26:1—26:8, 2022.

Learning Higher-Order Programs without Meta-Interpretive Learning

Stanisław Purgał, David Cerna, Cezary Kaliszyk
31st International Joint Conference on Artificial Intelligence, IJCAI 2022, pp. 2726-2733, 2022.

Lash 1.0 (System Description)

Chad E. Brown, Cezary Kaliszyk
Automated Reasoning – 11th International Joint Conference, IJCAR 2022, pp. 250-358, 2022.

Development Closed Critical Pairs: Towards a Formalized Proof

Christina Kohl, Aart Middeldorp
Proceedings of the 11th International Workshop on Confluence (IWC 2022), pp. 2-6, 2022.

Pólya’s Proof of the Weighted Arithmetic-Geometric Mean Inequality

Manuel Eberl
Archive of Formal Proofs 2022.

Formalized Signature Extension Results for Equivalence

Alexander Lochmann, Fabian Mitterwallner, Aart Middeldorp
Proceedings of the 11th International Workshop on Confluence (IWC 2022), pp. 42-47, 2022.

Polynomial Termination over N is Undecidable

Fabian Mitterwallner, Aart Middeldorp
Proceedings of the 7th International Conference on Formal Structures for Computation and Deduction, Leibniz International Proceedings in Informatics 228, pp. 27:1-27:17, 2022.

A Formalization of the Smith Normal Form in Higher-Order Logic

Jose Divasón, René Thiemann
Journal of Automated Reasoning online first, 2022.

Clique is not solvable by monotone circuits of polynomial size

René Thiemann
Archive of Formal Proofs 2022.

The Generalized Multiset Ordering is NP-Complete

René Thiemann, Lukas Schmidinger
Archive of Formal Proofs 2022.

The Sophomore’s Dream

Manuel Eberl
Archive of Formal Proofs 2022.

Adversarial Learning to Reason in an Arbitrary Logic

Stanisław Purgał and Cezary Kaliszyk
Proceedings of the Thirty-Fifth International Florida Artificial Intelligence Research Society Conference, 2022.

A Proof from THE BOOK: The Partial Fraction Expansion of the Cotangen

Manuel Eberl
2022.

First-Order Theory of Rewriting

Alexander Lochmann, Bertram Felgenhauer
Archive of Formal Proofs 2022 2022.

Duality of Linear Programming

René Thiemann
Archive of Formal Proofs 2022.

Details

Category: Publications

Published: 25 April 2025

Regular Tree Relations

Alexander Lochmann, Bertram Felgenhauer, Christian Sternagel, René Thiemann, Thomas Sternagel
Archive of Formal Proofs 2021.

Factorization of Polynomials with Algebraic Coefficients

Manuel Eberl, René Thiemann
Archive of Formal Proofs 2021.

A Formalization of Weighted Path Orders and Recursive Path Orders

Christian Sternagel, René Thiemann, Akihisa Yamada
Archive of Formal Proofs 2021.

Fast and Slow Enigmas and Parental Guidance

Zarathustra Amadeus Goertzel, Karel Chvalovský, Jan Jakubův, Miroslav Olšák, Josef Urban
Frontiers of Combining Systems (FroCoS), Lecture Notes in Computer Science 12941, pp. 173 - 191, 2021.

Learning Theorem Proving Components

Karel Chvalovský, Jan Jakubův, Miroslav Olšák, Josef Urban
Automated Reasoning with Analytic Tableaux and Related Methods (TABLEAUX), Lecture Notes in Computer Science 12842, pp. 266 - 278, 2021.

Solving Cubic and Quartic Equations

René Thiemann
Archive of Formal Proofs 2021.

JEFL: Joint Embedding of Formal Proof Libraries

Qingxiang Wang, Cezary Kaliszyk
Frontiers of Combining Systems – 13th International Symposium, FroCoS 2021, pp. 154-170, 2021.

Towards Finding Longer Proofs

Zsolt Zombori, Adrián Csiszárik, Henryk Michalewski, Cezary Kaliszyk, Josef Urban
Automated Reasoning with Analytic Tableaux and Related Methods (TABLEAUX 2021), pp. 167-186, 2021.

Machine Learning Guidance for Connection Tableaux

Michael Färber, Cezary Kaliszyk, Josef Urban
Journal of Automated Reasoning 65, pp. 287 - 320, 2021.

TacticToe: Learning to Prove with Tactics

Thibault Gauthier,Cezary Kaliszyk,Josef Urban,Ramana Kumar,Michael Norrish
Journal of Automated Reasoning 65, pp. 257 - 286, 2021.

Multi-redexes and multi-treks induce residual systems; least upper bounds and left-cancellation up to homotopy

Vincent van Oostrom
10th International Workshop on Confluence (IWC 2021), pp. 7, 2021.

Formalized Signature Extension Results for Confluence, Commutation and Unique Normal Forms

Alexander Lochmann, Fabian Mitterwallner, Aart Middeldorp
Proceedings of the 10th International Workshop on Confluence (IWC 2021), pp. 25 - 30, 2021.

Online Machine Learning Techniques for Coq: A Comparison

Liao Zhang, Lasse Blaauwbroek, Bartosz Piotrowski, Prokop Cerný, Cezary Kaliszyk, Josef Urban
Intelligent Computer Mathematics – 14th International Conference, CICM 2021, pp. 67-83, 2021.

Characteristic Subsets of SMT-LIB Benchmarks

Jan Jakubův, Mikoláš Janota, Andrew Reynolds
International Workshop on Satisfiability Modulo Theories (SMT), CEUR Workshop Proceedings 2908, 2021.

Polynomial Termination over N is Undecidable

Fabian Mitterwallner, Aart Middeldorp
Proceedings of the 17th International Workshop on Termination (WST 2021), pp. 21 - 26, 2021.

GeoLogic - Graphical Interactive Theorem Prover for Euclidean Geometry

Miroslav Olšák
International Congress on Mathematical Software (ICMS 2020), pp. 263 - 271, 2020.

Z; Syntax-Free Developments

Vincent van Oostrom
6th International Conference on Formal Structures for Computation and Deduction (FSCD 2021), Leibniz International Proceedings in Informatics (LIPIcs) 195, pp. 24:1 - 24:22, 2021.

ENIGMA Anonymous: Symbol-Independent Inference Guiding Machine (System Description)

Jan Jakubův, Karel Chvalovský, Miroslav Olšák, Bartosz Piotrowski, Martin Suda, Josef Urban
International Joint Conference on Automated Reasoning (IJCAR), pp. 448 - 463, 2020.

A Perron–Frobenius theorem for deciding matrix growth

René Thiemann
Journal of Logical and Algebraic Methods in Programming 123, 2021.

Artificial Intelligence and Domain-Specific Languages for Interactive Theorem Proving

Yutaka Nagashima
PhD thesis, University of Innsbruck 2021.

CoCo 2019: Report on the Eighth Confluence Competition

Aart Middeldorp, Julian Nagele, Kiraku Shintani
International Journal on Software Tools for Technology Transfer 23, pp. 905 - 916, 2021.

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.

Two algorithms based on modular arithmetic: lattice basis reduction and Hermite normal form computation

Ralph Bottesch, Jose Divasón, René Thiemann
Archive of Formal Proofs 2021.

The Sunflower Lemma of Erdős and Rado

René Thiemann
Archive of Formal Proofs 2021.

A study of continuous vector representations for theorem proving

Stanisław Purgał, Julian Parsert, Cezary Kaliszyk
Journal of Logic and Computation pp. 27, 2021.

Maltsev conditions for general congruence meet-semidistributive algebras

Miroslav Olšák
The Journal of Symbolic Logic pp. 20, 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.

Disambiguating Symbolic Expressions in Informal Documents

Dennis Müller and Cezary Kaliszyk
International Conference on Learning Representations (ICLR), pp. 16, 2021.

Details

Category: Publications

Published: 25 April 2025

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.

Maximal Non-compactness of Sobolev Embeddings

Jan Lang, Vít Musil, Miroslav Olšák, Luboš Pick
The Journal of Geometric Analysis 31, pp. 9406 - 9431, 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.

Some symmetries of commutation diamonds

Vincent van Oostrom
9th International Workshop on Confluence (IWC 2020), pp. 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.

A Formalization of Knuth-Bendix Orders

Christian Sternagel, René Thiemann
Archive of Formal Proofs 2020.

Verifying a Solver for Linear Mixed Integer Arithmetic in Isabelle/HOL

Ralph Bottesch, Max W. Haslbeck, Alban Reynaud, René Thiemann
12th International NASA Formal Methods Symposium (NFM 2020), LNCS 12229, pp. 233 – 250, 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.

The local loop lemma

Miroslav Olšák
Algebra universalis 81, pp. 23, 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.

Details

Category: Publications

Published: 25 April 2025

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.

Farkas’ Lemma and Motzkin’s Transposition Theorem

Ralph Bottesch, Max W. Haslbeck, René Thiemann
Archive of Formal Proofs 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.

Details

Category: Publications

Published: 25 April 2025

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.

An Incremental Simplex Algorithm with Unsatisfiable Core Generation

Filip Marić, Mirko Spasić, René Thiemann
Archive of Formal Proofs 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 Jakubův, 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.

A verified factorization algorithm for integer polynomials with polynomial complexity

Jose Divasón, Sebastiaan Joosten, René Thiemann, Akihisa Yamada
Archive of Formal Proofs 2018.

A verified LLL algorithm

Ralph Bottesch, Jose Divasón, Max Haslbeck, Sebastiaan Joosten, René Thiemann, Akihisa Yamada
Archive of Formal Proofs 2018.

First-Order Terms

Christian Sternagel, René Thiemann
Archive of Formal Proofs, 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.

Details

Category: Publications

Published: 25 April 2025

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.

Stochastic Matrices and the Perron-Frobenius Theorem

René Thiemann
Archive of Formal Proofs 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 Truomg 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.

Details

Category: Publications

Published: 25 April 2025

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.

The Factorization Algorithm of Berlekamp and Zassenhaus

Jose Divasón and Sebastiaan Joosten and René Thiemann and Akihisa Yamada
Archive of Formal Proofs 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.

Polynomial Factorization

René Thiemann and Akihisa Yamada
Archive of Formal Proofs 2016.

Polynomial Interpolation

René Thiemann and Akihisa Yamada
Archive of Formal Proofs 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.

Details

Category: Publications

Published: 25 April 2025

Algebraic Numbers in Isabelle/HOL

René Thiemann and Akihisa Yamada
Archive of Formal Proofs 2015.

Sharing HOL4 and HOL Light Proof Knowledge

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

FEMaLeCoP: Fairly Efficient Machine Learning Connection Prover

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

Constrained Term Rewriting tooL

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

Metis-based Paramodulation Tactic for HOL Light

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

MizAR 40 for Mizar 40

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

Formalizing Soundness and Completeness of Unravelings

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

Lemmatization for Stronger Reasoning in Large Theories

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

Random Forests for Premise Selection

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

Efficient Low-Level Connection Tableaux

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

Analysing the Complexity of Functional Programs: Higher-Order Meets First-Order

Martin Avanzini, Ugo Dal Lago, and Georg Moser
Proceedings of the 20th ACM SIGPLAN International Conference on Functional Programming (ICFP 2015), pp. 152 – 164, 2015.

Deriving Comparators and Show Functions in Isabelle/HOL

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

Matrices, Jordan Normal Forms, and Spectral Radius Theory

René Thiemann and Akihisa Yamada
Archive of Formal Proofs 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.

Deriving class instances for datatypes

Christian Sternagel and René Thiemann
Archive of Formal Proofs 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.

Details

Category: Publications

Published: 25 April 2025

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.

Lifting Definition Option

René Thiemann
Archive of Formal Proofs 2014.

XML

Christian Sternagel and René Thiemann
Archive of Formal Proofs 2014.

Certification Monads

Christian Sternagel and René Thiemann
Archive of Formal Proofs 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.

Haskell’s Show-Class in Isabelle/HOL

Christian Sternagel and René Thiemann
Archive of Formal Proofs 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.

Implementing field extensions of the form Q[sqrt(b)]

René Thiemann
Archive of Formal Proofs 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.

Mutually Recursive Partial Functions

René Thiemann
Archive of Formal Proofs 2014.

Details

Category: Publications

Published: 25 April 2025

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.

Computing N-th Roots using the Babylonian Method

René Thiemann
Archive of Formal Proofs 2013.

Details

Category: Publications

Published: 25 April 2025

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.

Details

Category: Publications

Published: 25 April 2025

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.

Details

Category: Publications

Published: 25 April 2025

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.

Details

Category: Publications

Published: 25 April 2025

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.

Loops under Strategies

René Thiemann and Christian Sternagel
Proceedings of the 20th International Conference on Rewriting Techniques and Applications (RTA 2009), Lecture Notes in Computer Science 5595, pp. 17 – 31, 2009.

Dependency Pairs and Polynomial Path Orders

Martin Avanzini and Georg Moser
Proceedings of the 20th International Conference on Rewriting Techniques and Applications (RTA 2009), Lecture Notes in Computer Science 5595, pp. 48 – 62, 2009.

The Derivational Complexity Induced by the Dependency Pair Method

Georg Moser and Andreas Schnabl
Proceedings of the 20th International Conference on Rewriting Techniques and Applications (RTA 2009), Lecture Notes in Computer Science 5595, pp. 255 – 269, 2009.

Tyrolean Termination Tool 2

Martin Korp, Christian Sternagel, Harald Zankl, and Aart Middeldorp
Proceedings of the 20th International Conference on Rewriting Techniques and Applications (RTA 2009), Lecture Notes in Computer Science 5595, pp. 295 – 304, 2009.

8th International Workshop on Reduction Strategies in Rewriting and Programming (WRS 2008)

Aart Middeldorp (ed.)
special issue, Electronic Notes in Theoretical Computer Science 237, pp. 1 – 126, 2009.

Constraint-Based Multi-Completion Procedures for Term Rewriting Systems

Haruhiko Sato, Masahito Kurihara, Sarah Winkler, and Aart Middeldorp
IEICI Transactions on Information and Systems E92-D(2), pp. 220 – 234, 2009.

From Outermost Termination to Innermost Termination

René Thiemann
Proceedings of the 35th International Conference on Current Trends in Theory and Practice of Computer Science (SOFSEM 2009), Lecture Notes in Computer Science 5404, pp. 533 – 545, 2009.

Details

Category: Publications

Published: 25 April 2025

Complexity Analysis of Term Rewriting Based on Matrix and Context Dependent Interpretations

Georg Moser, Andreas Schnabl, and Johannes Waldmann
Proceedings of the 28th International Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2008), pp. 304 – 315, 2008.

Uncurrying for Termination

Nao Hirokawa, Aart Middeldorp, and Harald Zankl
Proceedings of the 15th International Conference on Logic for Programming, Artificial Intelligence, and Reasoning (LPAR 2008), Lecture Notes in Artificial Intelligence 5330, pp. 667 – 681, 2008.

Complexity, Graphs, and the Dependency Pair Method

Nao Hirokawa and Georg Moser
Proceedings of the 15th International Conference on Logic for Programming, Artificial Intelligence, and Reasoning (LPAR 2008), Lecture Notes in Artificial Intelligence 5330, pp. 652 – 666, 2008.

Improving Context-Sensitive Dependency Pairs

Beatriz Alarcón, Fabian Emmes, Carsten Fuhs, Jürgen Giesl, Raúl Gutiérrez, Salvador Lucas, Peter Schneider-Kamp, and René Thiemann
Proceedings of the 15th International Conference on Logic for Programming, Artificial Intelligence, and Reasoning (LPAR 2008), Lecture Notes in Artificial Intelligence 5330, pp. 636 – 651, 2008.

Match-Bounds with Dependency Pairs for Proving Termination of Rewrite Systems

Martin Korp and Aart Middeldorp
Proceedings of the 2nd International Conference on Language and Automata Theory and Application (LATA 2008), Lecture Notes in Computer Science 5196, pp. 321 – 332, 2008.

Multi-Completion with Termination Tools (System Description)

Haruhiko Sato, Sarah Winkler, Masahito Kurihara, and Aart Middeldorp
Proceedings of the 4th International Joint Conference on Automated Reasoning (IJCAR 2008), Lecture Notes in Artificial Intelligence 5195, pp. 306 – 312, 2008.

Automated Implicit Computational Complexity Analysis (System Description)

Martin Avanzini, Georg Moser, and Andreas Schnabl
Proceedings of the 4th International Joint Conference on Automated Reasoning (IJCAR 2008), Lecture Notes in Artificial Intelligence 5195, pp. 132 – 139, 2008.

Automated Complexity Analysis Based on the Dependency Pair Method

Nao Hirokawa and Georg Moser
Proceedings of the 4th International Joint Conference on Automated Reasoning (IJCAR 2008), Lecture Notes in Artificial Intelligence 5195, pp. 364 – 380, 2008.

Increasing Interpretations

Harald Zankl and Aart Middeldorp
Proceedings of the 9th International Conference on Artificial Intelligence and Symbolic Computation (AISC 2008), Lecture Notes in Artificial Intelligence 5144, pp. 191 – 205, 2008.

Proving Quadratic Derivational Complexities using Context Dependent Interpretations

Georg Moser and Andreas Schnabl
Proceedings of the 19th International Conference on Rewriting Techniques and Applications (RTA 2008), Lecture Notes in Computer Science 5117, pp. 276 – 290, 2008.

Deciding Innermost Loops

René Thiemann, Jürgen Giesl, and Peter Schneider-Kamp
Proceedings of the 19th International Conference on Rewriting Techniques and Applications (RTA 2008), Lecture Notes in Computer Science 5117, pp. 366 – 380, 2008.

Root-Labeling

Christian Sternagel and Aart Middeldorp
Proceedings of the 19th International Conference on Rewriting Techniques and Applications (RTA 2008), Lecture Notes in Computer Science 5117, pp. 336 – 350, 2008.

Maximal Termination

Carsten Fuhs, Jürgen Giesl, Aart Middeldorp, Peter Schneider-Kamp, René Thiemann, and Harald Zankl
Proceedings of the 19th International Conference on Rewriting Techniques and Applications (RTA 2008), Lecture Notes in Computer Science 5117, pp. 110 – 125, 2008.

Complexity Analysis by Rewriting

Martin Avanzini and Georg Moser
Proceedings of the 9th International Symposium on Functional and Logic Programming (FLOPS 2008), Lecture Notes in Computer Science 4989, pp. 130 – 146, 2008.

Innermost Termination of Rewrite Systems by Labeling

René Thiemann and Aart Middeldorp
Proceedings of the 7th International Workshop on Reduction Strategies in Rewriting and Programming (WRS 2007), Electronic Notes in Theoretical Computer Science 204, pp. 3 – 19, 2008.

A Database Approach to Distributed State Space Generation

Stefan Blom, Bert Lisser, Jaco van de Pol, and Michael Weber
Proceedings of the 6th International Workshop on Parallel and Distributed Methods in Verification (PDMC 2007), Electronic Notes in Theoretical Computer Science 198(1), pp. 17 – 32, 2008.

Adding Constants to String Rewriting

René Thiemann, Hans Zantema, Jürgen Giesl, and Peter Schneider-Kamp
Applicable Algebra in Engineering, Communication and Computing 19(1), pp. 27 – 38, 2008.

A Mechanized Proof of the Basic Perturbation Lemma

Jesús Aransay, Clemens Ballarin, and Julio Rubio
Journal of Automated Reasoning 40(4), pp. 271 – 292, 2008.

Details

Category: Publications

Published: 25 April 2025

Simulated Time for Host-Based Testing with TTCN-3

Stefan Blom, Thomas Deiß, Natalia Ioustinova, Ari Kontio, Jaco van de Pol, Axel Rennoch, and Natalia Sidorova
Software Testing, Verification and Reliability 18(1), pp. 29 – 49, 2007.

TTCN-3 for Distributed Testing Embedded Software

Stefan Blom, Thomas Deiß, Natalia Ioustinova, Ari Kontio, Jaco van de Pol, Axel Rennoch, and Natalia Sidorova
Proceedings of the 6th International Andrei Ershov Memorial Conference: Perspectives of System Informatics (PSI 2006), Lecture Notes in Computer Science 4378, pp. 98 – 111, 2007.

Predictive Labeling with Dependency Pairs using SAT

Adam Koprowski and Aart Middeldorp
Proceedings of the 21st International Conference on Automated Deduction (CADE 2007), Lecture Notes in Artificial Intelligence 4603, pp. 410 – 425, 2007.

Satisfying KBO Constraints

Harald Zankl and Aart Middeldorp
Proceedings of the 18th International Conference on Rewriting Techniques and Applications (RTA 2007), Lecture Notes in Computer Science 4533, pp. 389 – 403, 2007.

Proving Termination of Rewrite Systems using Bounds

Martin Korp and Aart Middeldorp
Proceedings of the 18th International Conference on Rewriting Techniques and Applications (RTA 2007), Lecture Notes in Computer Science 4533, pp. 273 – 287, 2007.

The Hydra Battle Revisited

Nachum Dershowitz and Georg Moser
Rewriting, Computation and Proof; Essays Dedicated to Jean-Pierre Jouannaud on the Occasion of his 60th Birthday, Lecture Notes in Computer Science 4600, pp. 1 – 27, 2007.

SAT Solving for Termination Analysis with Polynomial Interpretations

Carsten Fuhs, Jürgen Giesl, Aart Middeldorp, Peter Schneider-Kamp, René Thiemann, and Harald Zankl
Proceedings of the 10th International Conference on Theory and Applications of Satisfiability Testing (SAT 2007), Lecture Notes in Computer Science 4501, pp. 340 – 254, 2007.

Tyrolean Termination Tool: Techniques and Features

Nao Hirokawa and Aart Middeldorp
Information and Computation 205(4), pp. 474 – 511, 2007.

Distributed Analysis with µCRL: A Compendium of Case Studies

Stefan Blom, Jens R. Calamé, Bert Lisser, Simona Orzan, Jun Pang, Jaco van de Pol, Mohammad Torabi Dashti, and Anton J. Wijs
Proceedings of the 13th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS 2007), Lecture Notes in Computer Science 4424, pp. 683 – 689, 2007.

Constraints for Argument Filterings

Harald Zankl, Nao Hirokawa, and Aart Middeldorp
Proceedings of the 33rd International Conference on Current Trends in Theory and Practice of Computer Science (SOFSEM 2007), Lecture Notes in Computer Science 4362, pp. 579 – 590, 2007.

Details

Category: Publications

Published: 25 April 2025

Derivational Complexity of Knuth-Bendix Orders Revisited

Georg Moser
Proceedings of the 13th International Conference on Logic for Programming, Artificial Intelligence, and Reasoning (LPAR 2006), Lecture Notes in Computer Science 4246, pp. 75 – 89, 2006.

Ackermann’s Substitution Method (remixed)

Georg Moser
Annals of Pure and Applied Logic 142(1-3), pp. 1 – 18, 2006.

Uncurrying for Termination

Nao Hirokawa and Aart Middeldorp
Proceedings of the 3rd International Workshop on Higher-Order Rewriting (HOR 2006), pp. 19 – 24, 2006.

Predictive Labeling

Nao Hirokawa and Aart Middeldorp
Proceedings of the 17th International Conference on Rewriting Techniques and Applications (RTA 2006), Lecture Notes in Computer Science 4098, pp. 313 – 327, 2006.

Simulated Time for Testing Railway Interlockings with TTCN-3

Stefan Blom, Natalia Ioustinova, Jaco van de Pol, Axel Rennoch, and Natalia Sidorova
Proceedings of the 5th International Workshop on Formal Approaches to Software Testing (FATES 2005), Lecture Notes in Computer Science 3997, pp. 1 – 15, 2006.

Automated Termination Analysis for Term Rewriting

Nao Hirokawa
PhD thesis, University of Innsbruck, 2006.

Herbrand’s Theorem and Term Induction

Matthias Baaz and Georg Moser
Archive for Mathematical Logic 45(4), pp. 447 – 503, 2006.

The Epsilon Calculus and Herbrand Complexity

Georg Moser and Richard Zach
Studia Logica 82(1), pp. 133 – 155, 2006.

Details

Category: Publications

Published: 25 April 2025

Skew and ω-Skew Confluence and Abstract Böhm Semantics

Zena M. Ariola and Stefan Blom
Processes, Terms and Cycles: Steps on the Road to Infinity; Essays Dedicated to Jan Willem Klop on the Occasion of his 60th Birthday, Lecture Notes in Computer Science 3838, pp. 368 – 403, 2005.

Processes, Terms and Cycles: Steps on the Road to Infinity

Aart Middeldorp, Vincent van Oostrom, Femke van Raamsdonk, and Roel de Vrijer (eds.)
Essays Dedicated to Jan Willem Klop on the Occasion of his 60th Birthday, Lecture Notes in Computer Science 3838, 2005.

Proofs of Termination of Rewrite Systems for Polytime Functions

Toshiyasu Arai and Georg Moser
Proceedings of the 25th International Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2005), Lecture Notes in Computer Science 3821, pp. 529 – 540, 2005.

Automating the Dependency Pair Method

Nao Hirokawa and Aart Middeldorp
Information and Computation 199(1,2), pp. 172 – 199, 2005.

Tyrolean Termination Tool

Nao Hirokawa and Aart Middeldorp
Proceedings of the 16th International Conference on Rewriting Techniques and Applications (RTA 2005), Lecture Notes in Computer Science 3467, pp. 175 – 184, 2005.

Decidable Call-by-Need Computations in Term Rewriting

Irène Durand and Aart Middeldorp
Information and Computation 196(2), pp. 95 – 126, 2005.

Details

Category: Publications

Published: 25 April 2025