Natural Algorithms in the TPDB

The TPDB contains many TRSs that implement realistic functions. For example, here is a (non-exhaustive) list of such examples. This demonstrates that our experiments are indeed useful to evaluate the performance of our approach on typical algorithms.

• directory AG01
  • minsort (#3.10)
  • average (#3.15)
  • multiplication (#3.16)
  • summing up list-elements (#3.17)
  • double (#3.18)
• directory AProVE_04
  • factorial (fac)
  • division (IJCAR_12)
  • prime-test (IJCAR_18)
  • incrementing the elements of a list (LPAR_intlist)
  • ackermann (rta1)
• directory AProVE_06
  • logarithm
  • modulo
  • quicksort
  • (repeated) exponentiation (tower, tower_sizeChange)
• directory AProVE_07
  • gcd (kabasci04)
  • take, list length (otto01)
  • fibonacci (otto04)
  • subtraction (otto07)
• directory AProVE_08
  • logarithm (log)
  • list-reverse (parting01_reverse)
  • doubling the elements of a list (parting02_doublelist)
  • minsort (parting03_minsort)
  • maxsort (parting05_maxsort)
• directory AProVE_09
  • division (divhard, div)
  • gcd (gcd, gcd2, gcdhard)
  • logarithm (log)
  • maxsort (maxsort, maxsortcondition)
  • minsort
  • modulo (mod)
  • quicksort (qsort, qsortlast, qsortmiddle)
• directory Beerendonk_07
  • even (10)
  • greater than, neq (11)
  • addition (15)
  • eq (17)
  • or (18)
• directory CiME_04
  • factorial (fact-hard)
  • intersection of sets represented as lists (intersect)
  • ackermann (ack_prolog)
  • list-append (append)
  • logarithm (log2)