Handling DG and SCCs: Difference between revisions

Revision as of 14:10, 17 May 2008

(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 in this ordering.

Revision as of 14:09, 17 May 2008 view source Griff (talk \| contribs) 47 edits 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...		Revision as of 14:10, 17 May 2008 view source Griff (talk \| contribs) 47 edits No edit summary Newer edit →
Line 1:		Line 1:
	(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~~.		(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 in this ordering.