cl-banner

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

P20133

  Contact

georg.moser@uibk.ac.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.
Nach oben scrollen