Experimental Data
About This Page
This page reports experimental data for the article of Nao Hirokawa and Aart Middeldorp, ``Decreasing Diagrams and Relative Termination'', Journal of Automated Reasoning.
Test Set
Environment
We used Saigawa v1.1. The tool requires a QF-NIA SMT solver and a termination tool. We employed MiniSmt v0.3 and TTT2 v1.06 equipped with the configuration file comp.conf (used in the international termination competition 2010). The tests were performed with the next command:
$ saigawa -smt minismt -tt 'ttt2 -c comp.conf -s COMP' <option> <filename.trs>
We tested on a PC with Intel Atom CPU Z550 (2.00 GHz) and 2 GB memory.
Results
Tables
- Table 1 (for summary, including properties of TRSs)
- Table 2 (for rule labeling)
- results.csv (CSV file of all results)
Abbreviations
| name | confluence criterion |
|---|---|
| kb | Knuth and Bendix' criterion |
| orthogonal | orthogonality |
| dc-5 | Theorem 2 |
| dc2-5 | Theorem 3 |
| rl-n | Theorem 4 (k = n) |
| rlv-n | Theorem 5 (k = n) |
| name | property / result by other tool |
|---|---|
| left_linear | left-linear TRS |
| linear | linear TRS |
| locally_confluent-n | locally confluent TRS (proved by at most n step rewriting) |
| terminating | R is terminating |
| cpssn | CPS(R)/R is terminating |
| cps2sn | CPS'(R)/R is terminating |
Note that all abbreviations except "terminating" correspond to options of the confluence tool.