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

• Martin Avanzini
• Georg Moser
• Andreas Schnabl

FWF project number

Contact

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.