Proof Simplification - Revision history

imported>Mathieu: Category:design proposal

2009-08-12T12:58:03Z

← Older revision		Revision as of 12:58, 12 August 2009
Line 32:		Line 32:


	[[Category:design]]		[[Category:design proposal]]
	[[Category:Work in progress]]		[[Category:Work in progress]]
	[[Category:Proof]]		[[Category:Proof]]

imported>Mathieu: Category:Proof

2009-08-12T12:55:53Z

Category:Proof

← Older revision		Revision as of 12:55, 12 August 2009
Line 34:		Line 34:
	[[Category:design]]		[[Category:design]]
	[[Category:Work in progress]]		[[Category:Work in progress]]
			[[Category:Proof]]

imported>Mathieu: Category:design Category:Work in progress

2009-08-12T12:12:33Z

Category:design Category:Work in progress

← Older revision		Revision as of 12:12, 12 August 2009
Line 30:		Line 30:
	Since we have to determine for each node if the predicates it refers to are used in its subtree, it is necessary to gather informations about the subtree before processing a node.		Since we have to determine for each node if the predicates it refers to are used in its subtree, it is necessary to gather informations about the subtree before processing a node.
	The approach consists in a depth-first postorder traversal of the closed proof tree, remembering in each branch which predicates are needed. It is then possible to simplify the nodes according to the above stated principles.		The approach consists in a depth-first postorder traversal of the closed proof tree, remembering in each branch which predicates are needed. It is then possible to simplify the nodes according to the above stated principles.


			[[Category:design]]
			[[Category:Work in progress]]

imported>Laurent at 15:19, 9 June 2009

2009-06-09T15:19:05Z

← Older revision		Revision as of 15:19, 9 June 2009
Line 1:		Line 1:
	Proofs stored in xml text files are sometimes quite large (70 MB proof files exist). We know that some information contained in these files is not needed. For instance, rewriting a predicate p1 into p2 when p2 is never used afterwards, is a needless step. This development aims at getting rid of ~~that~~ kind of needless data contained in proof files.		Proofs stored in xml text files are sometimes quite large (70 MB proof files exist). We know that some information contained in these files is not needed. For instance, rewriting a predicate p1 into p2 when p2 is never used afterwards, is a needless step. This development aims at getting rid of this kind of needless data contained in proof files.

	== Useless data ==		== Useless data ==

	As a reminder about the structure of proof trees, one can have a look at the [[Proof_Manager\|Proof Manager]] page.		As a reminder about the structure of proof trees, one can have a look at the [[Proof_Manager\|Proof Manager]] page.
	The idea here is to remove actions on ~~unneeded predicates~~. These include:		The idea here is to remove unnecessary actions on hypotheses. These include:
	* 'forward' on a ~~hypothese~~ when the inferred predicate is never ~~referred to~~ afterwards		* 'forward' on a hypothesis when the inferred predicate is never used afterwards
	* 'hide' of an ~~unneeded forwarded hypothese~~		* 'hide' of an unused forward-generated hypothesis
	* 'select' of an ~~hypothese~~ that is never used afterwards		* 'select' of an hypothesis that is never used afterwards

	~~Those~~ actions are stored in antecedents. After removing unneeded actions of an antecedent, it may become empty and can thus be removed ~~itself~~.		These actions are stored in antecedents. After removing unneeded actions of an antecedent, it may become empty and can thus be itself removed.
	~~Those~~ antecedents are stored in rules. After removing unneeded antecedents ~~of a~~ rule~~, it~~ may become empty. But the rule is linked to the node it is applied to, so we cannot remove the rule without removing the corresponding proof tree node.		These antecedents are stored in rules. After removing unneeded antecedents, the rule may become empty. But the rule is linked to the node it is applied to, so we cannot remove the rule without removing the corresponding proof tree node.
	Here, we have to distinguish 3 cases, depending on the number of children a proof tree node has:		Here, we have to distinguish 3 cases, depending on the number of children a proof tree node has:
	* 0 child: it is a leaf of the proof tree, we cannot remove it without obtaining a pending node		* 0 child: it is a leaf of the proof tree, we cannot remove it without obtaining a pending node
Line 24:		Line 24:
	Therefore, the simplification has to take place at proof saving, when the proof is committed.		Therefore, the simplification has to take place at proof saving, when the proof is committed.

	But when a project is imported, it may also contain proofs with useless data. So a new user action ~~is implemented~~, ~~with a right click on a PO, context,~~		But when a project is imported, it may also contain proofs with useless data. So a new user action has been added to the contextual menu of proof obligations, event-B components and projects: "Simplify Proof(s)". It allows to manually trigger proof simplification.
	~~machine or project~~: "Simplify Proof(s)". It allows to manually trigger proof simplification.

	== Implementation approach ==		== Implementation approach ==

imported>Nicolas at 14:34, 5 June 2009

2009-06-05T14:34:15Z

← Older revision		Revision as of 14:34, 5 June 2009
Line 1:		Line 1:
	Proofs stored in xml text files are sometimes quite large (70 MB proof files exist). We know that some information contained in these files is not needed. For instance, rewriting a predicate p1 into p2 when p2 is never used afterwards, is a needless step. This development aims at getting rid of that kind of needless data contained in proof files.		Proofs stored in xml text files are sometimes quite large (70 MB proof files exist). We know that some information contained in these files is not needed. For instance, rewriting a predicate p1 into p2 when p2 is never used afterwards, is a needless step. This development aims at getting rid of that kind of needless data contained in proof files.

			== Useless data ==

	~~{{TODO~~\|complete}}		As a reminder about the structure of proof trees, one can have a look at the [[Proof_Manager\|Proof Manager]] page.
			The idea here is to remove actions on unneeded predicates. These include:
			* 'forward' on a hypothese when the inferred predicate is never referred to afterwards
			* 'hide' of an unneeded forwarded hypothese
			* 'select' of an hypothese that is never used afterwards

			Those actions are stored in antecedents. After removing unneeded actions of an antecedent, it may become empty and can thus be removed itself.
			Those antecedents are stored in rules. After removing unneeded antecedents of a rule, it may become empty. But the rule is linked to the node it is applied to, so we cannot remove the rule without removing the corresponding proof tree node.
			Here, we have to distinguish 3 cases, depending on the number of children a proof tree node has:
			* 0 child: it is a leaf of the proof tree, we cannot remove it without obtaining a pending node
			* 2 or more children: it is a branching node, we cannot remove it because the children could not be 'plugged' anywhere else
			* 1 child: if the rule is empty, the step is unnecessary and can be skipped, 'plugging' its only child node to its parent node

			== Automatic and manual simplification ==

			In order to simplify a proof, it is necessary to determine for each of its nodes if some data is needless. But, when the proof is not complete, some data that is not yet used might become valuable in a further step. Thus, only discharged proofs are simplifiable.

			The main goal is to reduce the size of the proof file, so the simplification should take place before the storage of the proof.
			But before the user saves its proof, he or she is modifying it, so the proof is unstable and undischarged.
			Therefore, the simplification has to take place at proof saving, when the proof is committed.

			But when a project is imported, it may also contain proofs with useless data. So a new user action is implemented, with a right click on a PO, context,
			machine or project: "Simplify Proof(s)". It allows to manually trigger proof simplification.

			== Implementation approach ==

			Since we have to determine for each node if the predicates it refers to are used in its subtree, it is necessary to gather informations about the subtree before processing a node.
			The approach consists in a depth-first postorder traversal of the closed proof tree, remembering in each branch which predicates are needed. It is then possible to simplify the nodes according to the above stated principles.

imported>Nicolas: New page: Proofs stored in xml text files are sometimes quite large (70 MB proof files exist). We know that some information contained in these files is not needed. For instance, rewriting a predica...

2009-06-04T17:38:30Z

New page: Proofs stored in xml text files are sometimes quite large (70 MB proof files exist). We know that some information contained in these files is not needed. For instance, rewriting a predica...

New page

Proofs stored in xml text files are sometimes quite large (70 MB proof files exist). We know that some information contained in these files is not needed. For instance, rewriting a predicate p1 into p2 when p2 is never used afterwards, is a needless step. This development aims at getting rid of that kind of needless data contained in proof files.

{{TODO|complete}}