Experiments

Comparison with Other Tools

• MaxComp & Slothrop
  comparison with MaxComp and Slothrop (2011-05-13)
• mkbTT & MaxComp run on TPDB
  comparison with MaxComp using different reduction orders, run on TPDB 7.0 (2011-06-20)
• mkbTT & MaxComp
  comparison with MaxComp using different reduction orders, run on standard database (2011-05-12)

Termination

• reduction orders
  using TTT2 with LPO, KBO, TKBO, and interpretations (2013-01-10)
• DP strategies
  using TTT2 with termination strategies using DPs, DP graphs, subterm criterion and some reduction order (2013-01-11)

Selection

• different strategies
  comparison of max, sum, size/age and other strategies (2013-01-05)

Term indexing

• term indexing for rewriting
  comparison of path indexing, discrimination and code trees (2013-01-09)

Critical Pair Criteria

• with max strategy
  comparison of criteria BCP, PCP, CCP and mixed criterion MCP (2013-01-02)
• with sum strategy
  comparison of criteria BCP, PCP, CCP and mixed criterion MCP using sum strategy (2013-01-15)

Isomorphisms

• different isomorphisms
  comparison of renamings and argument permutations (2013-01-05)

Certified Proofs

When called with the flag -cert, mkbTT outputs a completeness proof of the result in cpf format if the run succeeds. These proofs can then be certified by CeTa.

• certified proofs obtained with the standard strategy (for 115 systems of maxcomp database)

Novel Completions

Table 1 shows some novel completion results obtained with mkbTT. Here column (1) gives the total time in seconds, column (2) the number of control loop iterations, column (3) the number of processes and column (4) the number of termination checks. Column (5) specifies the process filtering percentage that was used, an option which allows to abandon too costly processes. The first three problems stem from [1], the last one was presented in [2].

Ordered Completion

• termination strategies
  comparison of different termination strategies inducing total termination ()

Normalized Completion

Results

• Table 1 from the paper Normalized Completion Revistited submitted to RTA 2013 (extended version)
• Table 8.13 from PhD thesis Termination Tools in Automated Reasoning
• comparison of ACRPO with ACKBO

1	A. Stump and B. Löchner. Knuth-Bendix completion of theories of commuting group endomorphisms. IPL, 98(5):195-198, 2006.
2	I. Wehrman and A. Stump. Mining propositional simplification proofs for small validating clauses. In Proc. 3rd PDPAR, volume 144 of ENTCS, pages 79-91, 2005.