This page contains details of experiments reported in the following paper:

Takahito Aoto, Automated confluence proof by decreasing diagrams based on rule-labelling, In Proc. of RTA 2010, pp.7-16, LIPIcs, Vol.6, Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik, 2010.

Below is a table that presents a summary of experiments (Table 1 of the paper above). Click the corresponding link to jump to the detailed output of the program.

  R1 R2 R3 R4 Col. (msec)
Decreasing diagrams technique based on rule-labelling          
   (1) basic version (Thm. 3.7) Fail Fail Fail Fail 35 (200)
   (2) counting designated function symbol's occurrences Success Fail Fail Fail 41 (486)
   (3) with context weight (Thm. 5.4) Success Success Fail Fail 41 (481)
   (4) (3) + extended comparison (Subsect. 6.1) Success Success Success Fail 41 (695)
   (5) (4) + extended context weight (Subsect. 6.2) Success Success Success Success 42 (692)
Other techniques for left-linear TRSs          
   Huet-Toyama-van Oostrom criterion [van Oostrom,1997] Fail Fail Fail Fail 16 (52)
   Huet's strongly-closed criterion [Huet,1980] Fail Fail Fail Fail 24 (52)
   Parallel-critical-pairs criterion [Toyama,1981] Fail Fail Fail Fail 31 (58)
   Simultaneous-critical-pairs criterion [Okui,1998] Fail Fail Fail Fail 36 (91)
   Oyamaguchi-Ohta's criterion [Oyamaguchi&Ohta,2004] Fail Fail Fail Fail 19 (53)
All techniques Success Success Success Success 48 (593)
All techniques except the decreasing diagrams technique Fail Fail Fail Fail 40 (84)


Please send any requests and comments to webmaster