Priv.-Doz. Dr. Harald Zankl
Home Projects Publications Software Talks Teaching Walking
publications
theses journal articles papers in proceedings others

Theses

Journal Articles

  1. J. Nagele, B. Felgenhauer, and H. Zankl
    Certifying Confluence Proofs via Relative Termination and Rule Labeling open access
    Logical Methods in Computer Science, 13(2), 1-27, 2017. © Creative-Commons
  2. B. Felgenhauer, A. Middeldorp, H. Zankl, and V. van Oostrom
    Layer Systems for Proving Confluence open access
    ACM Transactions on Computational Logic, 16(2:14), 1-32, 2015. © Creative-Commons
  3. H. Zankl, B. Felgenhauer, and A. Middeldorp
    Labelings for Decreasing Diagrams open access
    Journal of Automated Resoning 54(2), 101-133, 2015. © Creative-Commons
  4. H. Zankl, S. Winkler, and A. Middeldorp
    Beyond Polynomials and Peano Arithmetic – Automation of Elementary and Ordinal Interpretations (preprint)
    Journal of Symbolic Computation 69, 129-158, 2015. © Elsevier
  5. H. Zankl and M. Korp
    Modular Complexity Analysis for Term Rewriting open access
    Logical Methods in Computer Science 10(1:19), 1-33, 2014. © Creative-Commons
    Invited to special issue of RTA 2010.
  6. N. Hirokawa, A. Middeldorp, and H. Zankl
    Uncurrying for Termination and Complexity open access
    Journal of Automated Reasoning, 50(3), 279-315, 2013. © Creative-Commons
  7. H. Zankl and A. Middeldorp
    Increasing Interpretations (preprint)
    Annals of Mathematics and Artificial Intelligence, 56(1), 87-108, 2009. © Springer-Verlag
    The original publication is available at www.springerlink.com
    Invited to special issue of AISC 2008.
  8. H. Zankl, N. Hirokawa, and A. Middeldorp
    KBO Orientability (preprint)
    Journal of Automated Reasoning 43(2), 173-201, 2009. © Springer-Verlag
    The original publication is available at www.springerlink.com

Papers in Proceedings

  1. T. Aoto, M. Hamana, N. Hirokawa, A. Middeldorp, J. Nagele, N. Nishida, K. Shintani, and H. Zankl
    Confluence Competition 2018 open access
    In Proceedings of 3rd International Conference on Formal Structures for Computation and Deduction (FSCD 2018),
    Leibnitz International Proceedings in Informatics 21, pp 32:1-32:5, 2013. © Creative-Commons
  2. T. Aoto, N. Hirokawa, J. Nagele, N. Nishida, and H. Zankl
    Confluence Competition 2015
    In Proceedings of the 25th International Conference on Automated Deduction (CADE-25),
    Lecture Notes in Artificial Intelligence 9195, pp 101-104, 2015. © Springer-Verlag
  3. J. Nagele and H. Zankl
    Certified Rule Labeling open access
    In Proceedings of the 26th International Conference on Rewriting Techniques and Applications (RTA 2015),
    Leibnitz International Proceedings in Informatics 36, pp 269-284, 2015. © The Authors
  4. T. Sternagel, S. Winkler, and H. Zankl
    Recording Completion for Certificates in Equational Reasoning open access
    In Proceedings of the 4th ACM-SIGPLAN Conference on Certified Programs and Proofs (CPP 2015),
    ACM, pp 41-47, 2015. © The Authors
  5. H. Zankl
    Decreasing Diagrams – Formalized open access
    In Proceedings of the 24th International Conference on Rewriting Techniques and Applications (RTA 2013),
    Leibnitz International Proceedings in Informatics 21, pp 352-367, 2013. © Creative-Commons
    The formalization is available from the archive of formal proofs.
  6. S. Winkler, H. Zankl, and A. Middeldorp
    Beyond Peano Arithmetic – Automatically Proving Termination of the Goodstein Sequence open access
    In Proceedings of the 24th International Conference on Rewriting Techniques and Applications (RTA 2013),
    Leibnitz International Proceedings in Informatics 21, pp 335-351, 2013. © Creative-Commons
  7. T. Sternagel and H. Zankl
    KBCV - Knuth-Bendix Completion Visualizer
    In Proceedings of the 6th International Joint Conference on Automated Reasoning (IJCAR 2012),
    Lecture Notes in Artificial Intelligence 7364, pp 530-536, 2012. © Springer-Verlag
  8. S. Winkler, H. Zankl, and A. Middeldorp
    Ordinals and Knuth-Bendix Orders
    In Proceedings of the 18th International Conference on Logic for Programming, Artificial Intelligence, and Reasoning (LPAR-18),
    LNCS Advanced Research in Computing and Software Science 7180, pp 420-434, 2012. © Springer-Verlag
  9. B. Felgenhauer, H. Zankl, and A. Middeldorp
    Layer Systems for Proving Confluence open access
    In Proceedings of the 31st IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2011),
    Leibnitz International Proceedings in Informatics 13, pp 288-299, 2011. © Creative-Commons
  10. H. Zankl, B. Felgenhauer, and A. Middeldorp
    CSI – A Confluence Tool
    In Proceedings of the 23rd International Conference on Automated Deduction (CADE 2011),
    Lecture Notes in Artificial Intelligence 6803, pp 499-505, 2011. © Springer-Verlag
  11. A. Middeldorp, G. Moser, F. Neurauter, J. Waldmann, and H. Zankl
    Joint Spectral Radius Theory for Automated Complexity Analysis of Rewrite Systems
    In Proceedings of the 4th International Conference on Algebraic Informatics (CAI 2011),
    Lecture Notes in Computer Science 6742, pp 1-20, 2011. © Springer-Verlag
  12. H. Zankl, B. Felgenhauer, and A. Middeldorp
    Labelings for Decreasing Diagrams open access
    In Proceedings of the 22nd International Conference on Rewriting Techniques and Applications (RTA 2011),
    Leibnitz International Proceedings in Informatics 10, pp 377-392, 2011. © Creative-Commons
  13. H. Zankl, N. Hirokawa, and A. Middeldorp
    Uncurrying for Innermost Termination and Derivational Complexity open access
    In Proceedings of the 5th International Conference on Higher-Order Rewriting (HOR 2010),
    Electronic Proceedings in Theoretical Computer Science 49, pp 46-57, 2011. © Creative-Commons
  14. F. Neurauter, H. Zankl, and A. Middeldorp
    Revisiting Matrix Interpretations for Polynomial Derivational Complexity of Term Rewriting
    In Proceedings of the 17th International Conference on Logic for Programming, Artificial Intelligence, and Reasoning (LPAR-17),
    LNCS Advanced Research in Computing and Software Science 6397, pp 550-564, 2010. © Springer-Verlag
  15. H. Zankl and M. Korp
    Modular Complexity Analysis via Relative Complexity open access
    In Proceedings of the 21st International Conference on Rewriting Techniques and Applications (RTA 2010),
    Leibnitz International Proceedings in Informatics 6, pp 385-400, 2010. © Creative-Commons
  16. F. Neurauter, A. Middeldorp, and H. Zankl
    Monotonicity Criteria for Polynomial Interpretations over the Naturals
    In Proceedings of the 5th International Joint Conference on Automated Reasoning (IJCAR 2010),
    Lecture Notes in Artificial Intelligence 6173, pp 502-517, 2010. © Springer-Verlag
  17. H. Zankl and A. Middeldorp
    Satisfiability of Non-Linear (Ir)rational Arithmetic
    In Proceedings of the 16th International Conference on Logic for Programming, Artificial Intelligence, and Reasoning (LPAR-16), Lecture Notes in Artificial Intelligence 6355, pp. 481-500, 2010. © Springer-Verlag
  18. H. Zankl, C. Sternagel, D. Hofbauer, and A. Middeldorp
    Finding and Certifying Loops
    In 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. © Springer-Verlag
  19. H. Zankl, C. Sternagel, and A. Middeldorp
    Transforming SAT into Termination of Rewriting
    In 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. © Elsevier B.V.
  20. M. Korp, C. Sternagel, H. Zankl, and A. Middeldorp
    Tyrolean Termination Tool 2
    In Proceedings of the 20th International Conference on Rewriting Techniques and Applications (RTA 2009),
    Lecture Notes in Computer Science 5595, pp 295-304, 2009. © Springer-Verlag
  21. N. Hirokawa, A. Middeldorp, and H. Zankl
    Uncurrying for Termination
    In 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. © Springer-Verlag
  22. H. Zankl and A. Middeldorp
    Increasing Interpretations
    In Proceedings of the 9th International Conference on Artificial Intelligence and Symbolic Computation (AISC 2008),
    Lecture Notes in Artificial Intelligence 5144 pp 191-205, 2008. © Springer-Verlag
  23. C. Fuhs, J. Giesl, A. Middeldorp, P. Schneider-Kamp, R. Thiemann, and H. Zankl
    Maximal Termination
    In Proceedings of the 19th International Conference on Rewriting Techniques and Applications (RTA 2008),
    Lecture Notes in Computer Science 5117 pp 110-125, 2008. © Springer-Verlag
  24. H. Zankl and A. Middeldorp
    Satisfying KBO Constraints
    In Proceedings of the 18th International Conference on Rewriting Techniques and Applications (RTA 2007),
    Lecture Notes in Computer Science 4533, pp 389-403, 2007. © Springer-Verlag
  25. C. Fuhs, J. Giesl, A. Middeldorp, P. Schneider-Kamp, R. Thiemann, and H. Zankl
    SAT Solving for Termination Analysis with Polynomial Interpretations
    In Proceedings of the 10th International Conference on Theory and Applications of Satisfiability Testing (SAT 2007),
    Lecture Notes in Computer Science 4501, pp 340-354, 2007. © Springer-Verlag
  26. H. Zankl, N. Hirokawa, and A. Middeldorp
    Constraints for Argument Filterings
    In 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. © Springer-Verlag

Others

  1. H. Zankl
    Automating the Conversion Version of Decreasing Diagrams for First-Order Rewrite Systems
    Draft, 1 page, 17 April 2016.
  2. H. Zankl, S. Winkler, and A. Middeldorp
    Automating Elementary Interpretations
    In Proceedings of the 14th International Workshop on Termination (WST 2014),
    pp 90-94, 2014.
  3. N. Nagatsuka, M. Sakai, H. Zankl, and K. Kusakari
    Size complexity of BDD construction of Pseudo-Boolean constraints in binary/mixed-radix base form
    In Proceedings of the 28th Annual Conference of the Japan Society of Artificial Intelligence (JSAI 2014),
    1D4-OS-11a-3, 4 pages, 2014.
  4. C. Nemeth, H. Zankl and N. Hirokawa
    IaCOP — Interface for the Administration of Cops
    In Proceedings of the 1st International Workshop on Confluence (IWC 2012),
    pp 21-24, 2012.
  5. T. Sternagel, R. Thiemann, H. Zankl and C. Sternagel
    Recording Completion for Finding and Certifying Proofs in Equational Logic
    In Proceedings of the 1st International Workshop on Confluence (IWC 2012),
    pp 31-36, 2012.
  6. H. Zankl, B. Felgenhauer and A. Middeldorp
    CoCo 2012 Participant: CSI
    In Proceedings of the 1st International Workshop on Confluence (IWC 2012),
    p 47, 2012.
  7. H. Zankl, S. Winkler and A. Middeldorp
    Automating Ordinal Interpretations
    In Proceedings of the 12th International Workshop on Termination (WST 2012),
    pp 94-98, 2012.
  8. H. Zankl and M. Korp
    On Implementing Modular Complexity Analysis open access
    In Proceedings of the 8th International Workshop on the Implementation of Logics (IWIL 2010),
    Easychair Proceedings 2, pp 42-47, 2012. © Creative-Commons
  9. H. Zankl, R. Thiemann, and A. Middeldorp
    Satisfiability of Non-Linear Arithmetic over Algebraic Numbers
    In Proceedings of Symbolic Computation in Software Science (SCSS 2010),
    RISC-Linz Technical Report 10-10, University of Linz, pp 19-24, 2010.
  10. H. Zankl and M. Korp
    The Derivational Complexity of the Bits Function and the Derivation Gap Principle
    In Proceedings of the 11th International Workshop on Termination (WST 2010),
    2010.
  11. H. Zankl, N. Hirokawa, and A. Middeldorp
    Uncurrying for Innermost Termination and Derivational Complexity open access
    In Proceedings of the 5th International Workshop on Higher-Order Rewriting (HOR 2010),
    pp 9-13, 2010. © Creative-Commons
  12. H. Zankl and A. Middeldorp
    Equational Reasoning for Termination of Rewriting
    In Proceedings of the 10th International Workshop on Termination (WST 2009),
    pp 112-115, 2009.
  13. C. Sternagel, R. Thiemann, S. Winkler, and H. Zankl
    CeTA – A Tool for Certified Termination Analysis
    In Proceedings of the 10th International Workshop on Termination (WST 2009),
    pp 84-87, 2009.
  14. H. Zankl and A. Middeldorp
    Nontermination of String Rewriting using SAT
    In Proceedings of the 9th International Workshop on Termination (WST 2007),
    pp 52-55, 2007.
  15. C. Fuhs, J. Giesl, A. Middeldorp, P. Schneider-Kamp, R. Thiemann, and H. Zankl
    SAT Solving for Termination Analysis with Polynomial Interpretations
    In Proceedings of the 9th International Workshop on Termination (WST 2007),
    pp 56-59, 2007.
  16. H. Zankl, N. Hirokawa, and A. Middeldorp
    Constraints for Argument Filterings
    In Proceedings of the 8th International Workshop on Termination (WST 2006),
    pp 50-54, 2006.
  17. H. Zankl and A. Middeldorp
    KBO as a Satisfaction Problem
    In Proceedings of the 8th International Workshop on Termination (WST 2006),
    pp 55-59, 2006.