Certification of Relative Termination and Termination modulo Theories

From Termination-Portal.org
Revision as of 10:46, 24 April 2009 by UlrichSG (talk | contribs) (Submitted proposal. Sorry for the long page title :))
(diff) ← Older revision | Latest revision (diff) | Newer revision → (diff)
Jump to navigationJump to search

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

Retrieved from "http://termination-portal.org/mediawiki/index.php?title=Certification_of_Relative_Termination_and_Termination_modulo_Theories&oldid=730"