General
On this page we provide detailed links to our formalization and experimental evidence concerning our paper Certification of Complexity Proofs using CeTA.Links
Theories mentioned in the papers
- Complexity
- Matchbounds and Matchbounds_Impl
- DT_Transformation and DT_Transformation_Impl
- WDP_Transformation and WDP_Transformation_Impl
- Usable_Rules_Complexity and Usable_Rules_Complexity_Impl
- Usable_Replacement_Map and Usable_Replacement_Map_Impl
Definitions and theorems of the paper
- Theorem 2: deriv_bound_relto_class_union
- Theorem 4: match_raise_bounded_SN_on
- Lemma 5: rstep_imp_raise_step
- Theorem 6: match_raise_bounded_linear_complexity
- Theorem 7: match_raise_bounded_linear_complexity_rel
- Definition 9: is_WDP_of
- Definition 10: good_for
- Lemma 11: le_sharp_dmax_singleton and le_sharp_dmax_subst
- Lemma 12: NF_terms_Q’
- Lemma 13: qrstep_good_for
- Corollary 14: rel_qrsteps_good_for
- Theorem 15: WDPs_sound
- Definition 16: is_DT_of
- Definition 17: goodFor
- Lemma 19: one_step_generic
- Corollary 20: many_relative_steps
- Theorem 21: dependency_tuples_sound
- Definition 22: usable_symbols_closed and U_usable
- Theorem 24: usable_rules_complexity
- Theorem 25: usable_rules_innermost_complexity_urm_redpair
Experiments
As testbed we used the runtime complexity testsuite from the termination problem data base, version 9.0.2, which also served as testbed for the complexity category of the FLoC Olympic Games of 2014. All tests were conducted on a machine with a 8 dual core AMD Opteron 885 processors running at 2.60GHz with 64Gb of RAM, within a timeout of 60 seconds per test.
We have conducted the following tests:
- Innermost Runtime Complexity Analysis with the tool AProVE
- Innermost Runtime Complexity Analysis with the tool TcT.
- Runtime Complexity Analysis with the tool TcT.