AC-KBO
Home
AC-KBO
experiments downloads

Completion Experiments

AC-KBO Experiments

The following table collects results obtained with mkbtt running normalized completion with different versions of AC-KBO. A tarball containing all input systems can be found here.

Results in one row were obtained in parallel and run on a server equipped with eight dual-core AMD Opteron processors 885 running at a clock rate of 2.6GHz with 64GB of main memory, for each setting with a timeout of 200 seconds. Each termination call had a timeout of 1.5 seconds, and the primality critical pair criterion was used.

The columns correspond to the following settings. Column 1 applies AC-RPO directly, and column 0 applies AC-KBO directly, with subterm coefficients and possibly partial precedences. Columns 2 and 3 compare these plain orders to the settings where AC-dependency pairs are computed and AC-KBO and AC-RPO are used as reduction pairs, respectively, in both cases with argument filterings. Column 4 applies a strategy dependency pairs, a dependency graph approximation followed by a computation of strongly connected components. Afterwards reduction pairs based on AC-RPO, AC-KBO and matrix interpretations remove rules as long as possible, incorporating argument filterings and usable rules. AC-KBO always used 2 input and 3 output bits to represent weights and subterm coefficients.

 01234
A95_bincoeff 0.18 ∞ 0.23 ⊥ 0.62
A95_finite_comm_monoid 0.12 0.49 1.62 3.27 0.95
A95_homomorphism 0.07 0.08 0.08 0.15 0.15
A95_integers 0.37 0.81 0.72 3.86 3.04
A95_listaddition 0.69 2.30 2.31 12.26 10.81
A95_listaddition2 0.77 1.59 2.24 9.22 12.67
A95_naturals 0.26 0.38 0.84 2.36 1.52
A95_proplogic 0.10 0.09 0.02 0.02 0.02
A95_proplogic2 0.08 0.12 0.10 0.27 0.22
DP93_d2 0.75 1.39 3.57 11.67 11.78
DP93_d3 1.77 4.17 24.84 85.40 74.81
GK01_eqtheory_add ∞ ∞ ∞ ⊥ ⊥
ICS 0.04 0.03 0.01 0.01 0.01
K00_ex5_4_2 0.15 0.23 0.24 0.66 0.93
K00_max ⊥ ∞ ⊥ ⊥ 1.10
LS94_G0 0.21 0.26 0.22 1.55 1.40
LS94_G2 0.22 1.09 0.17 1.72 1.79
MU98_balanced_ternary_add ⊥ ∞ ∞ ⊥ 63.00
MU98_binarith1 ⊥ 1.28 ⊥ 5.85 6.56
MU98_binarith1b ⊥ 3.02 ∞ ⊥ 16.56
MU98_binarith2 ∞ ∞ ∞ ∞ ∞
MU98_multisets 0.47 ∞ 1.51 ∞ 2.19
MU98_ternary_add ⊥ 10.55 ⊥ ⊥ 65.12
MU98_ternary_arith ∞ ∞ ∞ ∞ ∞
abelian_groups 0.05 0.05 0.01 0.01 0.01
abelian_groups_action 0.37 0.98 1.74 9.17 9.36
abelian_groups_comm_action ⊥ ⊥ ∞ ∞ ∞
abelian_groups_homomorphism 0.13 0.17 0.19 0.45 0.42
anf ∞ ∞ ∞ ∞ ∞
arithmetic ⊥ ⊥ ⊥ ⊥ ∞
arithmetic_exp ∞ ∞ ∞ ∞ ∞
assoc_comm_ring_unit 0.10 0.12 0.13 0.21 0.17
assoc_ring_unit ∞ ⊥ ⊥ ⊥ ∞
bimodule ∞ ∞ ∞ ∞ ∞
bimodule_comm_ring ∞ ∞ ∞ ∞ ∞
bool_ring ∞ ∞ ∞ ∞ ∞
comm_assoc_ring_homomorphism ∞ ∞ ∞ ∞ ∞
comm_monoid 0.02 0.02 0.01 0.01 0.01
distr_lattice ∞ ∞ ∞ ∞ ∞
example10 ⊥ ⊥ 0.04 0.07 0.06
field 1.77 3.93 ∞ 11.86 30.63
finite_group 0.16 0.33 0.12 0.45 0.53
height ∞ 0.59 ⊥ 2.07 1.17
inverse_property 0.07 0.07 0.07 0.13 0.15
lattice 0.06 0.06 0.01 0.01 0.01
lie_ring ∞ ∞ ∞ ∞ ∞
max ⊥ ∞ ⊥ ⊥ 1.12
max2 ∞ ∞ ⊥ ⊥ 1.30
module ∞ ∞ ∞ ∞ ∞
module_comm_ring ∞ ∞ ∞ ∞ ∞
multisets 0.44 ∞ 1.44 ∞ 2.19
multisets_binary 1.03 ∞ 2.85 ∞ 5.83
nondeterministic_machines ∞ ∞ ∞ ⊥ ∞
popplestone_robot ∞ ∞ ∞ ∞ ∞
ring ∞ ⊥ ⊥ ⊥ ∞
ring_unit ∞ ⊥ ⊥ ⊥ ∞
ring_unit_chomo ∞ ⊥ ⊥ ∞ ∞
ring_unit_homo ∞ ⊥ ⊥ ⊥ ∞
semilattice 0.02 0.02 0.01 0.01 0.01
semiring ⊥ ⊥ ⊥ ⊥ ∞
semiring_unit_chomo ∞ ⊥ ⊥ ∞ ∞
semiring_unit_homo1 ∞ ⊥ ⊥ ⊥ ∞
semiring_unit_homo5 ∞ ⊥ ⊥ ⊥ ∞
slothrop_equiv_proofs ⊥ ∞ ⊥ ⊥ ∞
slothrop_equiv_proofs2 ⊥ ⊥ ⊥ ⊥ ⊥
strange_addition ∞ ∞ ∞ ⊥ 0.84
sum ⊥ ∞ ⊥ ⊥ 1.17
successes28 28 28 27 39
total time234010.47 234034.22 234045.34 240162.72 168330.23
∅ time 0.37 1.22 1.62 6.03 8.47

Legend
0./mkbtt -ct -st -cp prime -T 1.5 -t 200 -s acrpo
1./mkbtt -ct -st -cp prime -T 1.5 -t 200 -s 'ackbo -ib 2 -ob 3 -direct -sc -nt'
2./mkbtt -ct -st -cp prime -T 1.5 -t 200 -s 'dp; (acrpo -af)*'
3./mkbtt -ct -st -cp prime -T 1.5 -t 200 -s 'dp; (ackbo -af -ib 2 -ob 3 -sc -nt)*'
4./mkbtt -ct -st -cp prime -T 1.5 -t 200 -s 'dp; acdg?; sccs?; ({ur?; matrix -ib 2 -ob 3 -dp -dim 1 -ur[2]}restore || acrpo -af || ackbo -af -ib 2 -ob 3 -sc -nt || {ur?; matrix -ib 2 -ob 3 -dp -dim 2 -ur[2]}restore)*'