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