Certification of Relative Termination and Termination modulo Theories

Proposal

Add certified counterparts to the following categories:

• SRS Relative
• TRS Relative
• TRS Termination modulo Theory

Rationale

In the 2008 competition, only full termination (of TRSs and SRSs) could be certified. Since then, CoLoR has added support for relative and modulo-theory termination proofs. There are already non-certified categories for these types of proofs, so it would make sense to have certified ones, too. This should be possible with very little effort and encourage developers of both provers and certification tools to consider these and other forms of non-standard termination problems.

Tools interested in participating

• AProVE