Experimental Data
About This Page
This page reports experimental data for Kiraku Shintani and Nao Hirokawa, ``CoLL: A Confluence Tool for Left-Linear TRSs''
Test Set
- testset1.tar.gz contains 188 left-linear TRSs in Cops
- testset2.tar.gz additional problems
Environment
We used CoLL v1.0 and tested on a PC with Intel Core i7-4500U CPU (1.8 GHz) and 3.8 GB memory
Results
Tables
- left table in Figure 1 (for criteria and confluence tools )
- right table in Figure 1 (for Church-Rosser modulo E)
- results.csv (CSV file of Table 1 and 2)
- results for testset2 (CSV file: commuting.csv)
Abbreviations
| name | commutation criterion |
|---|---|
| kb | Knuth and Bendix' criterion |
| dc | development closedness |
| rl | weighted rule-labeling |
| jk | Church-Rosser modulo (summation of jk series) |
| jka | with associativity |
| jkc | with commutativity |
| jkac | with associativity and commutativity |
| jkacc | with associativity and/or commutativity |
| all_three | summation of jk, dc and rl |
| all_with_elim | same as all_three but elimination is enabled |
| coll1.0_nd | coll1.0 without composability decomposition |