mkbTT

Experiments

Comparison with Other Tools
Termination
Selection
Term indexing
Critical Pair Criteria
Isomorphisms
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.

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

Normalized Completion

Results
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.