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