Handling DG and SCCs: Difference between revisions
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... |
No edit summary |
||
| (2 intermediate revisions by the same user not shown) | |||
| Line 1: | Line 1: | ||
( | (draft, please extend) | ||
= Dependency Graphs = | |||
how to handle approximations? for every missing edge, indicate why it is not necessary? | |||
= Strongly Connected Components = | |||
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. | |||
Latest revision as of 14:20, 17 May 2008
(draft, please extend)
Dependency Graphs
how to handle approximations? for every missing edge, indicate why it is not necessary?
Strongly Connected Components
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.