Experiments
Comparison with Other Tools

MaxComp & Slothrop
comparison with MaxComp and Slothrop (20110513) 
mkbTT & MaxComp run on TPDB
comparison with MaxComp using different reduction orders, run on TPDB 7.0 (20110620) 
mkbTT & MaxComp
comparison with MaxComp using different reduction orders, run on standard database (20110512)
Termination
 reduction orders
using TTT2 with LPO, KBO, TKBO, and interpretations (20130110)  DP strategies
using TTT2 with termination strategies using DPs, DP graphs, subterm criterion and some reduction order (20130111)
Selection
 different strategies
comparison of max, sum, size/age and other strategies (20130105)
Term indexing
 term indexing for rewriting
comparison of path indexing, discrimination and code trees (20130109)
Critical Pair Criteria
 with max strategy
comparison of criteria BCP, PCP, CCP and mixed criterion MCP (20130102)  with sum strategy
comparison of criteria BCP, PCP, CCP and mixed criterion MCP using sum strategy (20130115)
Isomorphisms
 different isomorphisms
comparison of renamings and argument permutations (20130105)
Certified Proofs
When called with the flagcert
, mkbTT outputs a
completeness proof of the result in cpf format if the run succeeds.
These proofs can then be certified by
CeTa.
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].(1)  (2)  (3)  (4)  (5)  
CGE3  15.78  37  1  276  20 
CGE4  145.68  50  1  1392  20 
CGE5  35796.48  90  155  56235  70 
proof reduction system  104.94  87  31  401  70 
Table 1: New completions
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. KnuthBendix completion of theories of commuting group endomorphisms. IPL, 98(5):195198, 2006. 
2 
I. Wehrman and A. Stump. Mining propositional simplification proofs for small validating clauses. In Proc. 3rd PDPAR, volume 144 of ENTCS, pages 7991, 2005. 