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



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.




nameconfluence criterion
kbKnuth and Bendix' criterion
dc-5Theorem 2
dc2-5Theorem 3
rl-nTheorem 4 (k = n)
rlv-nTheorem 5 (k = n)

nameproperty / result by other tool
left_linearleft-linear TRS
linearlinear TRS
locally_confluent-nlocally confluent TRS (proved by at most n step rewriting)
terminatingR is terminating
cpssnCPS(R)/R is terminating
cps2snCPS'(R)/R is terminating

Note that all abbreviations except "terminating" correspond to options of the confluence tool.