TCT - TRS (termcomp2018)

The Tyrolean Complexity Tool (TCT for short) is a tool for automatically proving polynomial upper bounds on the derivational complexity and runtime complexity of term rewriting systems. TCT is open source and licensed under the GNU Lesser General Public License.

Examples

Select example Jones1 Jones2 Jones4 Jones5 Jones6 Flatten Reverse Shuffle Shuffleshuffle Clique Dcquad Egypt Eratosthenes Lcs Mmult-nat Qbf Sat Z86 Bits Div Mult Mult2 Quad Square AppendAll.raml Bfs.raml Bft mmult.raml Bitonic.raml Bitvectors.raml Clevermmult.raml Duplicates.raml Dyade.raml Eratosthenes.raml Flatten.raml Insertionsort.raml Listsort.raml LongestCommonSubsequence.raml Matrix.raml Mergesort.raml Minsort.raml Queue.raml Quicksort.raml RationalPotential.raml Splitandsort.raml Subtrees.raml Tctres Tuples.raml Fold Map Bubblesort-nat Isort Mergesort-nat Mergesort Quicksort-nat Quicksort

Load own example

Syntax highlighting

Plain text FP

Tool input

(VAR a k ls x) (RULES rev(ls) -> r1(ls,empty) r1(empty,a) -> a r1(cons(x,k),a) -> r1(k,cons(x,a)) )

Complexity Measure

Runtime Complexity - full rewriting

Runtime Complexity - innermost rewriting

Derivational Complexity - full rewriting

Derivational Complexity - innermost rewriting

Search Strategy

Automatic

Certify

Customised by user

Base Techniques

matchbounds

matrices - use usable arguments

matrices - orient only usable rules

polynomials - use usable arguments

polynomials - orient only usable rules

Transformations

to innermost

relative decompose

Weak Dependency Pairs

use dependency tuples

employ simplifications

dependency graph decomposition

Search for upper bound

Linear

Quadratic

Cubic

O(n^4)

O(n^5)

Any

Timeout

Certify output with CeTA

No Yes