Handling DG and SCCs

From Termination-Portal.org
Revision as of 14:09, 17 May 2008 by Griff (talk | contribs) (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...)
(diff) ← Older revision | Latest revision (diff) | Newer revision → (diff)
Jump to navigationJump to search

(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.

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