WScT08-Minutes-Competition
From Termination-Portal.org
Revision as of 13:38, 2 June 2008 by J.waldmann (talk | contribs)
(These are minutes of the meeting. Please do not edit this page except for correcting obvious mistakes. Make links to separate pages for further discussions.)
- Unique IDs for problems in database
- Idea: short IDs that can be used in papers
- Different suggested formats (nrs are relative, e.g., 2008-1 and 2009-1 possible):
- nameOfAuthor-year-nr (problem of uniqueness)
- abbreviatedNameOfAuthor-year-nr (problem of uniqueness)
- login-year-nr
- year-archiveNr-fileNr
- year-fileNr
- nr
- Question: Who decides format? Would be nice to have decision soon
- Annotation of termination problems
- Comments can be added by user
- Status at time of submission (open in theory, solved on paper, solved, solved certified, ...)
- Presentation will show above points and computed information (like date of submission, solved by xx tools, ...)
- Submission of many problems
- Zip-files which contain xml-file for adding initial comments, etc.
- Format of xml-file has to be fixed
- Should be same format for adding and for retrieving examples
- To discuss: relation to system-part of XTC-format
- Wishlist for termination competition platform
- Testing should be frequently possible
- Extract challenging problems and letting them run with higher time-limit
- Quotas for experiments? Accessing non-approved examples? Using non-approved tools? Mainly Innsbruck is in charge and makes rules public
- SQL-variant for selection problems and evaluate results, where several properties can be used within queries
- Scoring should be flexible
- Categories as queries (incl. randomSubsetOf(..)) + timeout(s) + scoring
- New category: XML-proofs given, certifiers compete
- Possibility to manually attach proofs for problem (difficult to find/human assisted, or large and put it as challenge for certificating category)
- Open source (Obergurgl 2007 this was stated)
- https
- Discussion whether TRSs should be removed from standard categories which do not satisfy variable condition
- Timeouts for verified competition
- Discussion whether there are separate timeouts on proof-finding and checking, or one global timeout
- Majority was for separate timeouts
Proposed XML Format for Import/Export to the termination database
See here: TPDB_XML_Format