Experimental Data
About This Page
This page reports experimental data for
Nao Hirokawa,
``Completion and Reduction Orders'',
Proceedings of the 5th International Conference on Formal Structures
on Computation and Deduction, Leibniz International Proceedings in Informatics, 2021.
Test Set
problems.zip contains 115 equational systems
from the distribution of mkbTT.
Environment
We used Maxcomp v1.5 and
tested on a system equipped with an Intel Core i7-1065G7 CPU with 1.3 GHz
and 32 GB of RAM using a timeout of 600 seconds. Z3 version 4.8.9 was
employed for solving order constraints.
Results
Table
See here.
Note that ERROR indicates run-out of memory.
Abbreviations
- lpo
- LPO with total precedence
- elpo
- ELPO with total precedence and linear interpretations over 0,1-coefficients
- kbo
- KBO with total precedence
- ekbo
- EKBO with total precedence and linear interpretations over 0,1-coefficients
- elpoekbo
- union of ELPO and EKBO
- kbcv
- KBCV v2.1.0.6 with TTT2 1.20: kbcv -a -s 600 -m "./ttt2 -cpf -ext xml - 1"
- MaxcompDP
- MaxcompDP