-->
Harald Zankl
Theses
H. Zankl,
Challenges in Automation of Rewriting ,
Habilitation thesis,
University of Innsbruck ,
October 2014. Final defense on April 21, 2015.
H. Zankl,
Lazy Termination Analysis , PhD thesis,
University of Innsbruck ,
September 2009. Final defense on November 27, 2009.
Journal Articles
J. Nagele, B. Felgenhauer, and H. Zankl
Certifying Confluence Proofs via Relative Termination and Rule Labeling
Logical Methods in Computer Science ,
13(2), 1-27, 2017.
©
Creative-Commons
B. Felgenhauer, A. Middeldorp, H. Zankl, and V. van Oostrom
Layer Systems for Proving Confluence
ACM Transactions on Computational Logic ,
16(2:14), 1-32, 2015.
©
Creative-Commons
H. Zankl, B. Felgenhauer, and A. Middeldorp
Labelings for Decreasing Diagrams
Journal of Automated Resoning
54(2), 101-133, 2015.
© Creative-Commons
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
H. Zankl and M. Korp
Modular
Complexity Analysis for Term Rewriting
Logical Methods in Computer Science
10(1:19), 1-33, 2014.
©
Creative-Commons
Invited to special issue of RTA 2010.
N. Hirokawa, A. Middeldorp, and H. Zankl
Uncurrying
for Termination and Complexity
Journal of Automated Reasoning ,
50(3), 279-315, 2013.
© Creative-Commons
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.
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
T. Aoto, M. Hamana, N. Hirokawa, A. Middeldorp, J. Nagele, N. Nishida, K. Shintani, and H. Zankl
Confluence Competition 2018
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
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
J. Nagele and H. Zankl
Certified Rule Labeling
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
T. Sternagel, S. Winkler, and H. Zankl
Recording Completion for Certificates in Equational Reasoning
In Proceedings of the 4th ACM-SIGPLAN Conference on Certified Programs and Proofs
(CPP 2015 ) ,
ACM, pp 41-47, 2015.
© The Authors
H. Zankl
Decreasing Diagrams – Formalized
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 .
S. Winkler, H. Zankl, and A. Middeldorp
Beyond Peano Arithmetic –
Automatically Proving Termination of the Goodstein Sequence
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
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
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
B. Felgenhauer, H. Zankl, and A. Middeldorp
Layer Systems for Proving Confluence
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
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
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
H. Zankl, B. Felgenhauer, and A. Middeldorp
Labelings for Decreasing Diagrams
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
H. Zankl, N. Hirokawa, and A. Middeldorp
Uncurrying for Innermost Termination and Derivational Complexity
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
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
H. Zankl and M. Korp
Modular Complexity Analysis via Relative Complexity
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
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
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
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
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.
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
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
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
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
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
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
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
H. Zankl
Automating the Conversion Version of Decreasing Diagrams for First-Order Rewrite Systems
Draft, 1 page, 17 April 2016.
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.
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.
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.
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.
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.
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.
H. Zankl and M. Korp
On Implementing Modular Complexity Analysis
In Proceedings of the 8th International Workshop on the Implementation of Logics
(IWIL 2010 ) ,
Easychair Proceedings 2, pp 42-47, 2012.
© Creative-Commons
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.
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.
H. Zankl, N. Hirokawa, and A. Middeldorp
Uncurrying for Innermost Termination and Derivational Complexity
In Proceedings of the 5th International Workshop on Higher-Order Rewriting
(HOR 2010 ) ,
pp 9-13, 2010.
© Creative-Commons
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.
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.
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.
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.
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.
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.