Certified Termination

From Termination-Portal.org
Revision as of 14:40, 21 December 2009 by C-Otto (talk | contribs)
(diff) ← Older revision | Latest revision (diff) | Newer revision → (diff)
Jump to navigationJump to search

From the rules of the 2009 competition: The certified categories will be run as follows:

  • After the corresponding uncertified category of the competition has finished, the problems that have been solved (yes or no) are collected and form the initial selection for the certified category.
  • Termination tools that can produce output in the new format and that participate in the certified competition are then run on the collection of 1, resulting in a collection of termination proofs. (Termination provers may use a different strategy from the uncertified competition, to increase chances of the proof being certified.)
  • The certifiers are then run on the collection produced by 2.

see also: