Description

On this page we compare Small Polynomial Path Orders to various similar techniques. The employed testbed contains a subset of 757 examples from the termination problem database, version 8.0. This subset was obtained by restricting the runtime complexity problem set to constructor TRSs, additionally removing TRSs that are not wellformed. The employed testbed can be downloaded from here.

The tests rendered below cover following techniques:

LMPO	Lightweight Multiset Path Orders over quasi precedences
MPO	Multiset Multiset Path Orders over quasi precedences
POP*	Polynomial Path Orders over quasi precedences
POP* (PS)	Polynomial Path Orders with parameter substitution, over quasi precedences
Small POP*	Small Polynomial Path Orders over quasi precedences
Small POP* (PS)	Small Polynomial Path Orders with parameter substitution, over quasi precedences

Setup

All Experiments were conducted on a laptop with 4Gb of RAM and Intel® Core™ i7-2620M CPU (2.7GHz). The experiments were generated using this test file and this TCT configuration file.

Overview

Execution Times (in seconds)

Details