All Publications
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.
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.
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.
Pólya’s Proof of the Weighted Arithmetic-Geometric Mean Inequality
Manuel Eberl
Archive of Formal Proofs 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.
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.
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.
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.
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.
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 TRUONG HOANG, CEZARY KALISZYK, VICTOR MAGRON, SEAN MCLAUGHLIN, TAT THANG NGUYEN, QUANG TRUONG NGUYEN, TOBIAS NIPKOW, STEVEN OBUA, JOSEPH PLESO, JASON RUTE, ALEXEY SOLOVYEV, THI HOAI AN TA, NAM TRUNG TRAN, THI DIEP TRIEU, JOSEF URBAN, KY VU, ROLAND ZUMKELLER
Forum of Mathematics, Pi,
5,
pp. 1-29,
2017.
Parsing and Printing of and with Triples
Sebastiaan J. C. Joosten
Relational and Algebraic Methods in Computer Science. RAMICS 2017,
Lecture Notes in Computer Science 10226,
pp. 159 – 176,
2017.
Certifying Confluence Proofs via Relative Termination and Rule Labeling
Julian Nagele, Bertram Felgenhauer, and Harald Zankl
Logical Methods in Computer Science,
13(2:4),
pp. 1 – 27,
2017.
Deep Network Guided Proof Search
Sarah Loos, Geoffrey Irving, Christian Szegedy, Cezary Kaliszyk.
21st International Conference on Logic for Programming, Artificial Intelligence and Reasoning,
EPiC 46,
pp. 85-105,
2017.
TacticToe: Learning to Reason with HOL4 Tactics
Thibault Gauthier, Cezary Kaliszyk, Josef Urban
21st International Conference on Logic for Programming, Artificial Intelligence and Reasoning,
EPIC 46,
pp. 125-143,
2017.
Wikis and Collaborative Systems for Large Formal Mathematics
Cezary Kaliszy, Josef Urban
Post proceedings of Semantic Web Collaborative Spaces,
LNCS
pp. 35-52,
2016.
A Formalization of the Berlekamp-Zassenhaus Factorization Algorithm
Jose Divason, Sebastiaan J. C. Joosten, Rene Thiemann and Akihisa Yamada
Proceedings of the 6th ACM SIGPLAN Conference on Certified Programs and Proofs (CPP 2017),
pp. 17 – 29,
2017.
Subresultants
Sebastiaan Joosten and René Thiemann and Akihisa Yamada
Archive of Formal Proofs 2017.
Reachability, Confluence, and Termination Analysis with State-Compatible Automata
Bertram Felgenhauer and René Thiemann
Information and Computation 253(3),
pp. 467 – 483,
2017.
Towards Formal Proof Metrics
David Aspinall, Cezary Kaliszyk
19th International Conference on Fundamental Approaches to Software Engineering,
LNCS 9633,
pp. 325-341,
2016.
Relative Termination via Dependency Pairs
José Iborra, Naoki Nishida, Germán Vidal, Akihisa Yamada
Journal of Automated Reasoning 58(3),
pp. 391 – 411,
2017.
Complexity of Conditional Term Rewriting
Cynthia Kop, Aart Middeldorp, Thomas Sternagel
Logical Methods in Computer Science 13(1:6),
pp. 1 – 56,
2017.
Analyzing Program Termination and Complexity Automatically with AProVE
Jürgen Giesl, Cornelius Aschermann, Marc Brockschmidt, Fabian Emmes, Florian Frohn, Carsten Fuhs, Jera Hensel, Carsten Otto, Martin Plücker, Peter Schneider-Kamp, Thomas Ströder, Stephanie Swiderski, René Thiemann
Journal of Automated Reasoning,
58(1),
pp. 3 – 31,
2017.
Bar Recursion over Finite Partial Functions
Paulo Oliva and Thomas Powell
Annals of Pure and Applied Logic 2016.
Distance-Integrated Combinatorial Testing
Eun-Hye Choi, Cyrille Artho, Takashi Kitamura, Osamu Mizuno, and Akihisa Yamada
Proceedings of the 27th International Symposium on Software Reliability Engineering (ISSRE 2016),
pp. 93 – 104,
2016.
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.
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.