cl-banner

All Publications


2021 | 2020 | 2019 | 2018 | 2017 | 2016 | 2015 | 2014 | 2013 | 2012 | 2011 | 2010 | 2009 | 2008 | 2007 | 2006 | 2005 | 2004

Publications 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.
Publications 2020

Publications 2019

  • Declarative Proof Translation
    Cezary Kaliszyk, Karol Pąk
    10th International Conference on Interactive Theorem Proving, LIPIcs 141, pp. 35:1 – 35:7, 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.
  • Abstract Completion, Formalized
    Nao Hirokawa, Aart Middeldorp, Christian Sternagel, Sarah Winkler
    Logical Methods in Computer Science,  15(3), pp. 19:1 – 19:42, 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.
  • Linear Inequalities
    Ralph Bottesch, Alban Reynaud, René Thiemann
    Archive of Formal Proofs 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.
  • Publications 2021A Hierarchy of Polynomial Kernels
    Jouke Witteveen, Ralph Bottesch, Leen Torenvliet
    45th International Conference on Current Trends in Theory and Practice of Computer Science (SOFSEM 2019), Lecture Notes in Computer Science 11376, pp. 504 – 518, 2019.
  • Certified ACKBO
    Alexander Lochmann, Christian Sternagel
    8th ACM SIGPLAN International Conference on Certified Programs and Proofs,   pp. 144 – 151, 2019.
Publications 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.
  • 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.
  • 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.
  • 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.
  • CoCo 2018 Participant: CeTA 2.33
    Bertram Felgenhauer, Franziska Rapp, Christian Sternagel and Sarah Winkler
    Proceedings of the 7th International Workshop on Confluence (IWC 2018), pp. 63, 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.
Publications 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.
  • 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.
  • 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.
  • 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.
  • 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.
  • Subresultants
    Sebastiaan Joosten and René Thiemann and Akihisa Yamada
    Archive of Formal Proofs 2017.
  • Towards Formal Proof Metrics
    David Aspinall, Cezary Kaliszyk
    19th International Conference on Fundamental Approaches to Software Engineering, LNCS 9633, pp. 325-341, 2016.
Publications 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.
  • 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.
  • 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.
  • 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.
  • 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.
  • 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.
  • Hammering towards QED
    Jasmin C. Blanchette, Cezary Kaliszyk, Lawrence C. Paulson, and Josef Urban
    Journal of Formalized Reasoning 9(1), pp. 101 – 148, 2016.
  • The Complexity of Interaction
    Stéphane Gimenez and Georg Moser
    Proceedings of the 43rd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL 2016),  243 – 255, 2016.
Publications 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.
  • MizAR 40 for Mizar 40
    Cezary Kaliszyk and Josef Urban
    Journal of Automated Reasoning 55(3), pp. 245 – 256, 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.
  • 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.
  • 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.
  • 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.
  • 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.
  • 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.
  • 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.
  • A Framework for Developing Stand-Alone Certifiers
    Christian Sternagel and René Thiemann
    Proceedings of the 9th Workshop on Logical and Semantic Frameworks, with Applications (LSFA 2014), Electronic Notes in Theoretical Computer Science 312, pp. 51 – 67, 2015.
  • Layer Systems for Proving Confluence
    Bertram Felgenhauer, Aart Middeldorp, Harald Zankl, and Vincent van Oostrom
    ACM Transactions on Computational Logic 16(2:14), pp. 1 – 32, 2015.
Publications 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.
  • 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.
  • 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.
  • 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.
  • 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.
  • 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.
Publications 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.
  • 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.
  • 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.
  • 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.
  • 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.
  • 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.
Publications 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.
  • 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.
Publications 2011

  • 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.
  • 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.
  • 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.
Publications 2010

  • 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.
  • 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.
  • 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.
  • 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.
  • 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.
  • 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.
  • 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.
Publications 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.
  • 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.
  • 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.
  • 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.
  • 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.
Publications 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.
  • 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.
    Publications 2004
  • 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.
  • 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.
Publications 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.
  • 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.
  • 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.
  • 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.
Publications 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.
Publications 2005

  • 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.
  • 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.
Publications 2004

  • Polynomial Interpretations with Negative Coefficients
    Nao Hirokawa and Aart Middeldorp
    Proceedings of the 7th International Conference on Artificial Intelligence and Symbolic Mathematical Computation (AISC 2004), Lecture Notes in Artificial Intelligence 3249, pp. 185 – 198, 2004.
  • Dependency Pairs Revisited
    Nao Hirokawa and Aart Middeldorp
    Proceedings of the 15th International Conference on Rewriting Techniques and Applications (RTA 2004), Lecture Notes in Computer Science 3091, pp. 249 – 268, 2004.
Nach oben scrollen