http://termination-portal.org/mediawiki/index.php?action=history&feed=atom&title=WScT08-Minutes-Certification 2026-05-03T15:59:14Z Revision history for this page on the wiki MediaWiki 1.34.2 http://termination-portal.org/mediawiki/index.php?title=WScT08-Minutes-Certification&diff=512&oldid=prev 2008-06-02T13:37:42Z

<p></p> <table class="diff diff-contentalign-left" data-mw="interface"> <col class="diff-marker" /> <col class="diff-content" /> <col class="diff-marker" /> <col class="diff-content" /> <tr class="diff-title" lang="en"> <td colspan="2" style="background-color: #fff; color: #222; text-align: center;">← Older revision</td> <td colspan="2" style="background-color: #fff; color: #222; text-align: center;">Revision as of 13:37, 2 June 2008</td> </tr><tr><td colspan="2" class="diff-lineno" id="mw-diff-left-l1" >Line 1:</td> <td colspan="2" class="diff-lineno">Line 1:</td></tr> <tr><td colspan="2"> </td><td class='diff-marker'>+</td><td style="color: #222; font-size: 88%; border-style: solid; border-width: 1px 1px 1px 4px; border-radius: 0.33em; border-color: #a3d3ff; vertical-align: top; white-space: pre-wrap;"><div><ins style="font-weight: bold; text-decoration: none;">(These are minutes of the meeting. Please do not edit this page except for correcting obvious mistakes.</ins></div></td></tr> <tr><td colspan="2"> </td><td class='diff-marker'>+</td><td style="color: #222; font-size: 88%; border-style: solid; border-width: 1px 1px 1px 4px; border-radius: 0.33em; border-color: #a3d3ff; vertical-align: top; white-space: pre-wrap;"><div><ins style="font-weight: bold; text-decoration: none;">Make links to separate pages for further discussions.)</ins></div></td></tr> <tr><td class='diff-marker'> </td><td style="background-color: #f8f9fa; color: #222; font-size: 88%; border-style: solid; border-width: 1px 1px 1px 4px; border-radius: 0.33em; border-color: #eaecf0; vertical-align: top; white-space: pre-wrap;"></td><td class='diff-marker'> </td><td style="background-color: #f8f9fa; color: #222; font-size: 88%; border-style: solid; border-width: 1px 1px 1px 4px; border-radius: 0.33em; border-color: #eaecf0; vertical-align: top; white-space: pre-wrap;"></td></tr> <tr><td class='diff-marker'> </td><td style="background-color: #f8f9fa; color: #222; font-size: 88%; border-style: solid; border-width: 1px 1px 1px 4px; border-radius: 0.33em; border-color: #eaecf0; vertical-align: top; white-space: pre-wrap;"><div>* Notation:</div></td><td class='diff-marker'> </td><td style="background-color: #f8f9fa; color: #222; font-size: 88%; border-style: solid; border-width: 1px 1px 1px 4px; border-radius: 0.33em; border-color: #eaecf0; vertical-align: top; white-space: pre-wrap;"><div>* Notation:</div></td></tr> </table>

J.waldmann http://termination-portal.org/mediawiki/index.php?title=WScT08-Minutes-Certification&diff=498&oldid=prev 2008-06-02T13:30:36Z

<p>New page: * Notation: ** TCG is Termination Certificate Grammar ** Rainbow is the translator from TCG, with several backends (one for Color, one for Isabelle) ** Another format and another translat...</p> <p><b>New page</b></p><div><br /> * Notation:<br /> ** TCG is Termination Certificate Grammar<br /> ** Rainbow is the translator from TCG, with several backends (one for Color, one for Isabelle)<br /> ** Another format and another translator is CiME from A3PAT<br /> ** what's the file extension (.tc, .tcg, .tcf, .xml?)<br /> *** .xtc (xml termination certificate)<br /> ** introduce version names/numbers for the format and for the translator(s) (in the .xtc, versioning is by using the proper namespace)<br /> <br /> <br /> * extend TCG format towards common format:<br /> ** make nodes (more) self-contained <br /> ** have system (termination problem) in each node<br /> <br /> * DG Approx, SCC analysis<br /> ** give topologically sorted list of SCCs (A3PAT handles graphs and requests this list)<br /> ** have certificate for each missing edge (allow different kinds of certificates)<br /> <br /> * want to certify non-termination <br /> ** proposal: new top element: disproof<br /> ** certify loops (is leaf in proof tree)<br /> *** loop has: start term, sequence of steps, final position (and substitution?)<br /> *** step has: position, rule (and substitution?) <br /> ** later: other nodes in non-termination-proof trees?<br /> <br /> * extend polynomial and (standard) matrix interpretations to rational domain (new XML node types rational-polynomial-interp and rational-matrix-interp)<br /> ** a rational number is an XML node (enum, denom)<br /> ** need to provide the delta for the ordering<br /> <br /> * apply argument filtering on ordering <br /> ** currently, manna-ness has ordering, we want to allow argument-filtering-of-ordering there<br /> <br /> * direct checking of TPG trees (no formal verification) might be useful for testing extensions (Christian has a prototype ([[microTTT]]) but not exactly for Rainbow)<br /> <br /> * re-use in Color some theorems proved in Coccinelle <br /> ** e.g. prover termination by innermost termination (if nonoverlapping)<br /> ** modular termination (?) <br /> ** perhaps have a general transformation (back and forth)<br /> <br /> * plan: generate Isabelle proof from TPG tree</div>

J.waldmann