### Derivational Complexity Analysis

In the area of term rewriting powerful methods have been introduced to establish termination of a given term rewrite system. Modern termination provers can often establish termination or nontermination of the input rewrite system in a couple of seconds. However, termination of a rewrite system is only one property of interest. Another interesting property is the complexity of the rewrite system. Here complexity is measured as the maximal length of derivations. This notion of complexity is usually called derivational complexity in the literature. The goal of this project is to make derivational complexity analysis

- modern by studying the derivational complexities induced by modern termination techniques,

- useful by establishing refinements of existing termination techniques guaranteeing that the induced derivational complexity is bounded by a function of low computational complexity, for example a polytime computable function,

- broad by analysing the derivational complexities of higher-order rewrite systems and for rewrite systems based on particular rewrite strategies.

Further we want to ensure that the results that we develop in these three parts provide computable and precise bounds. Thus guaranteeing that we can establish instructive upper bounds automatically. We have incorporated obtained results into a complexity analyser: the Tyrolean Complexity Tool (TCT for short). TCT is open source and and licensed under the GNU Lesser General Public License.

#### Members

#### FWF project number

P20133#### Contact

georg moser at uibk dot ac dot at#### Publications

Verifying Polytime Computability Automatically

Martin Avanzini

PhD thesis, University of Innsbruck, 2013.

Derivational Complexity Analysis Revisited

Andreas Schnabl

PhD thesis, University of Innsbruck, 2012.

On Transfinite Knuth-Bendix Orders

Laura Kovács, Georg Moser, and Andrei Voronkov

Proceedings of the 23rd International Conference on Automated Deduction (CADE 2011),
Lecture Notes in Artificial Intelligence 6803,
pp. 384 – 399,
2011.

The Derivational Complexity Induced by the Dependency Pair Method

Georg Moser and Andreas Schnabl

Logical Methods in Computer Science 7(3:1),
pp. 1 – 38,
2011.

Joint Spectral Radius Theory for Automated Complexity Analysis of Rewrite Systems

Aart Middeldorp, Georg Moser, Friedrich Neurauter, Johannes Waldmann, and Harald Zankl

Proceedings of the 4th International Conference on Algebraic Informatics (CAI 2011),
Lecture Notes in Computer Science 6742,
pp. 1 – 20,
2011.

Termination Proofs in the Dependency Pair Framework May Induce Multiple Recursive Derivational Complexity

Georg Moser and Andreas Schnabl

Proceedings of the 22nd International Conference on Rewriting Techniques and Applications (RTA 2011),
Leibniz International Proceedings in Informatics 10,
pp. 235 – 250,
2011.

A Path Order for Rewrite Systems that Compute Exponential Time Functions

Martin Avanzini, Naohi Eguchi, and Georg Moser

Proceedings of the 22nd International Conference on Rewriting Techniques and Applications (RTA 2011),
Leibniz International Proceedings in Informatics 10,
pp. 123 – 138,
2011.

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.

Cdiprover3: A Tool for Proving Derivational Complexities of Term Rewriting Systems

Andreas Schnabl

Interfaces: Explorations in Logic, Language and Computation,
Lecture Notes in Artificial Intelligence 6211,
pp. 142 – 154,
2010.

Closing the Gap Between Runtime Complexity and Polytime Complexity

Martin Avanzini and Georg Moser

Proceedings of the 21st International Conference on Rewriting Techniques and Applications (RTA 2010),
Leibniz International Proceedings in Informatics 6,
pp. 33 – 48,
2010.

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.

Proof Theory at Work: Complexity Analysis of Term Rewrite Systems

Georg Moser

Habilitation thesis, University of Innsbruck,
2009.

The Hydra Battle and Cichon’s Principle

Georg Moser

Applicable Algebra in Engineering, Communication and Computing 20(2),
pp. 133 – 158,
2009.

Dependency Pairs and Polynomial Path Orders

Martin Avanzini and Georg Moser

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

The Derivational Complexity Induced by the Dependency Pair Method

Georg Moser and Andreas Schnabl

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

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

Georg Moser, Andreas Schnabl, and Johannes Waldmann

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

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.

Automated Implicit Computational Complexity Analysis (System Description)

Martin Avanzini, Georg Moser, and Andreas Schnabl

Proceedings of the 4th International Joint Conference on Automated Reasoning (IJCAR 2008),
Lecture Notes in Artificial Intelligence 5195,
pp. 132 – 139,
2008.

Automated Complexity Analysis Based on the Dependency Pair Method

Nao Hirokawa and Georg Moser

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

Proving Quadratic Derivational Complexities using Context Dependent Interpretations

Georg Moser and Andreas Schnabl

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

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.