Matrix Interpretations on Polyhedral Domains

Experiments on star-exec generally, using 5 min wallclock, 20 min CPU timeout.

New (after submission of paper)

NOTE (Sun Mar 29 12:06:16 CEST 2015): I changed the urls here (termcomp => termcomp-devel) because a server went down. This just concerns presentation. Original data are fetched from starexec, and have not been altered.

Bulk experiments (matchbox-with-constraints vs. termcomp2014)

Termination of Term Rewriting

TRS Standard | SRS Standard
Complexity Analysis of Term Rewriting

Derivational Complexity - Full Rewriting

On each page, click through to “flexible query” to see differences between minisat (satchmo) and boolector back-end. (because of Issue #75)

Anti-cheating provision: check that job numbers in these URLs coincide with those from original termcomp2014 data

Bulk experiments (matchbox vs. itself)

with constraints or without, dp with usable rules or without, back-end boolector or minisat.

Termination of Term Rewriting

TRS Standard | SRS Standard
Complexity Analysis of Term Rewriting

Derivational Complexity - Full Rewriting

Old (at time of submission of paper)

Individual examples mentioned (or omitted) in the paper

Example 19 (Ex16_Luc06_C)
Example 22 (TRS/secret06/jambox/5)
SK90/4.27
Example 23 (ExProp7_Luc06_GM)
Example 24 (TRS_Standard/Various_04/11)
Example 25 (TRS_Standard/Endrullis_06/pair2simple2)
test9 Note: actually not terminating.

Bulk experiments (different versions of matchbox-with-constraints)

Constraints vs. No Constraints (for TRS Standard) (using DP method with natural and arctic matrices) first two columns of this comparison
Satchmo+Minisat vs. Boolector (for full derivational complexity) comparison

Software