http://termination-portal.org/mediawiki/index.php?action=history&feed=atom&title=Handling_DG_and_SCCs 2026-11-10T02:24:56Z Revision history for this page on the wiki MediaWiki 1.43.11 http://termination-portal.org/mediawiki/index.php?title=Handling_DG_and_SCCs&diff=447&oldid=prev 2008-05-17T14:20:19Z

<p></p> <table style="background-color: #fff; color: #202122;" 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: #202122; text-align: center;">← Older revision</td> <td colspan="2" style="background-color: #fff; color: #202122; text-align: center;">Revision as of 14:20, 17 May 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 class="diff-marker" data-marker="−"></td><td style="color: #202122; font-size: 88%; border-style: solid; border-width: 1px 1px 1px 4px; border-radius: 0.33em; border-color: #ffe49c; vertical-align: top; white-space: pre-wrap;"><div>(<del style="font-weight: bold; text-decoration: none;">Idea</del>, please extend) Termination Prover computes SCCs and outputs them. Proof assistant does not have to recompute SCCs (which is costly). Prover has to indicate topological ordering on SCCs. Assistant checks that there are no backward edges between components in this ordering.</div></td><td class="diff-marker" data-marker="+"></td><td style="color: #202122; 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;">draft</ins>, please extend)</div></td></tr> <tr><td colspan="2" class="diff-side-deleted"></td><td class="diff-marker" data-marker="+"></td><td style="color: #202122; 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;">= Dependency Graphs =</ins></div></td></tr> <tr><td colspan="2" class="diff-side-deleted"></td><td class="diff-marker" data-marker="+"></td><td style="color: #202122; 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;">how to handle approximations? for every missing edge, indicate why it is not necessary?</ins></div></td></tr> <tr><td colspan="2" class="diff-side-deleted"></td><td class="diff-marker" data-marker="+"></td><td style="color: #202122; 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;">= Strongly Connected Components =</ins></div></td></tr> <tr><td colspan="2" class="diff-side-deleted"></td><td class="diff-marker" data-marker="+"></td><td style="color: #202122; 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>Termination Prover computes SCCs and outputs them. Proof assistant does not have to recompute SCCs (which is costly). Prover has to indicate topological ordering on SCCs. Assistant checks that there are no backward edges between components in this ordering.</div></td></tr> </table>

Griff http://termination-portal.org/mediawiki/index.php?title=Handling_DG_and_SCCs&diff=445&oldid=prev 2008-05-17T14:18:19Z

<p><a href="/wiki/Handling_SCCs" class="mw-redirect" title="Handling SCCs">Handling SCCs</a> moved to <a href="/wiki/Handling_DG_and_SCCs" title="Handling DG and SCCs">Handling DG and SCCs</a></p> <table style="background-color: #fff; color: #202122;" data-mw="interface"> <tr class="diff-title" lang="en"> <td colspan="1" style="background-color: #fff; color: #202122; text-align: center;">← Older revision</td> <td colspan="1" style="background-color: #fff; color: #202122; text-align: center;">Revision as of 14:18, 17 May 2008</td> </tr><tr><td colspan="2" class="diff-notice" lang="en"><div class="mw-diff-empty">(No difference)</div> </td></tr></table>

Griff http://termination-portal.org/mediawiki/index.php?title=Handling_DG_and_SCCs&diff=443&oldid=prev 2008-05-17T14:10:59Z

<p></p> <table style="background-color: #fff; color: #202122;" 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: #202122; text-align: center;">← Older revision</td> <td colspan="2" style="background-color: #fff; color: #202122; text-align: center;">Revision as of 14:10, 17 May 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 class="diff-marker" data-marker="−"></td><td style="color: #202122; font-size: 88%; border-style: solid; border-width: 1px 1px 1px 4px; border-radius: 0.33em; border-color: #ffe49c; vertical-align: top; white-space: pre-wrap;"><div>(Idea, please extend) Termination Prover computes SCCs and outputs them. Proof assistant does not have to recompute SCCs (which is costly). Prover has to indicate topological ordering on SCCs. Assistant checks that there are no backward edges between components <del style="font-weight: bold; text-decoration: none;">of </del>this <del style="font-weight: bold; text-decoration: none;">order</del>.</div></td><td class="diff-marker" data-marker="+"></td><td style="color: #202122; 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>(Idea, please extend) Termination Prover computes SCCs and outputs them. Proof assistant does not have to recompute SCCs (which is costly). Prover has to indicate topological ordering on SCCs. Assistant checks that there are no backward edges between components <ins style="font-weight: bold; text-decoration: none;">in </ins>this <ins style="font-weight: bold; text-decoration: none;">ordering</ins>.</div></td></tr> </table>

Griff http://termination-portal.org/mediawiki/index.php?title=Handling_DG_and_SCCs&diff=440&oldid=prev 2008-05-17T14:09:26Z

<p>New page: (Idea, please extend) Termination Prover computes SCCs and outputs them. Proof assistant does not have to recompute SCCs (which is costly). Prover has to indicate topological ordering on S...</p> <p><b>New page</b></p><div>(Idea, please extend) Termination Prover computes SCCs and outputs them. Proof assistant does not have to recompute SCCs (which is costly). Prover has to indicate topological ordering on SCCs. Assistant checks that there are no backward edges between components of this order.</div>

Griff