ADVANCE D3.2 Improvement of automated proof - Revision history

imported>Laurent: /* Planning */

2012-07-18T13:21:31Z

Planning

← Older revision		Revision as of 13:21, 18 July 2012
Line 15:		Line 15:

	= Planning =		= Planning =
	Enhancement to automated proof will continue during the ADVANCE project. ~~This will be mainly achieved by the implementation of~~ the remaining missing rewriting<ref>http://wiki.event-b.org/index.php/All_Rewrite_Rules</ref> and inference rules<ref>http://wiki.event-b.org/index.php/Inference_Rules</ref> that have already been documented, ~~and by the addition of~~ new ~~ones~~.		Enhancement to automated proof will continue during the ADVANCE project. Notably, the remaining missing rewriting<ref>http://wiki.event-b.org/index.php/All_Rewrite_Rules</ref> and inference rules<ref>http://wiki.event-b.org/index.php/Inference_Rules</ref>, that have already been documented, will be implemented together with new rules.

	Maintenance of the SMT solver integration plug-in will be ensured within the time frame of ADVANCE. In particular, the translation to SMT-LIB will be completed by adding some support for mathematical extensions.		Maintenance of the SMT solver integration plug-in will be ensured within the time frame of ADVANCE. In particular, the translation to SMT-LIB will be completed by adding some support for mathematical extensions.

imported>Laurent: /* Planning */

2012-07-18T13:20:05Z

Planning

← Older revision		Revision as of 13:20, 18 July 2012
Line 18:		Line 18:

	Maintenance of the SMT solver integration plug-in will be ensured within the time frame of ADVANCE. In particular, the translation to SMT-LIB will be completed by adding some support for mathematical extensions.		Maintenance of the SMT solver integration plug-in will be ensured within the time frame of ADVANCE. In particular, the translation to SMT-LIB will be completed by adding some support for mathematical extensions.

			Finally, connecting other provers (such as Super Zenon and iProver) to the platform will be investigated.

	= References =		= References =

imported>Tommy: /* Planning */

2012-07-16T13:24:56Z

Planning

← Older revision		Revision as of 13:24, 16 July 2012
Line 15:		Line 15:

	= Planning =		= Planning =
	Enhancement to automated proof will continue ~~as long as Rodin is maintained~~. This will be mainly achieved by the implementation of the remaining missing rewriting<ref>http://wiki.event-b.org/index.php/All_Rewrite_Rules</ref> and inference rules<ref>http://wiki.event-b.org/index.php/Inference_Rules</ref> that have already been documented, and by the addition of new ones.		Enhancement to automated proof will continue during the ADVANCE project. This will be mainly achieved by the implementation of the remaining missing rewriting<ref>http://wiki.event-b.org/index.php/All_Rewrite_Rules</ref> and inference rules<ref>http://wiki.event-b.org/index.php/Inference_Rules</ref> that have already been documented, and by the addition of new ones.

	Maintenance of the SMT solver integration plug-in will be ensured within the time frame of ADVANCE. In particular, the translation to SMT-LIB will be completed by adding some support for mathematical extensions.		Maintenance of the SMT solver integration plug-in will be ensured within the time frame of ADVANCE. In particular, the translation to SMT-LIB will be completed by adding some support for mathematical extensions.

imported>Laurent: /* Planning */

2012-06-28T15:18:32Z

Planning

← Older revision		Revision as of 15:18, 28 June 2012
Line 15:		Line 15:

	= Planning =		= Planning =
	Enhancement ~~of the~~ automated proof will continue as long as Rodin is maintained. This will be mainly be achieved by the implementation of the remaining missing rewriting<ref>http://wiki.event-b.org/index.php/All_Rewrite_Rules</ref> and inference rules<ref>http://wiki.event-b.org/index.php/Inference_Rules</ref> that have already been documented, and by the addition of new ones.		Enhancement to automated proof will continue as long as Rodin is maintained. This will be mainly achieved by the implementation of the remaining missing rewriting<ref>http://wiki.event-b.org/index.php/All_Rewrite_Rules</ref> and inference rules<ref>http://wiki.event-b.org/index.php/Inference_Rules</ref> that have already been documented, and by the addition of new ones.

	Maintenance of the SMT solver integration plug-in will be ensured within the time frame of ADVANCE.		Maintenance of the SMT solver integration plug-in will be ensured within the time frame of ADVANCE. In particular, the translation to SMT-LIB will be completed by adding some support for mathematical extensions.

	= References =		= References =

imported>Laurent: /* Motivations / Decisions */

2012-06-28T15:16:59Z

Motivations / Decisions

← Older revision		Revision as of 15:16, 28 June 2012
Line 6:		Line 6:

	= Motivations / Decisions =		= Motivations / Decisions =
	The proportion of automatically discharged proof obligations heavily depends on Auto-Tactic configuration. Sometimes, the automatic prover fails because the tactics are applied in a unappropriate order. Since Rodin 2.4, a new tactic combinator 'Attempt after Lasso' is available in ~~auto~~ tactic profile editor as well as an import/export feature. Indeed, a user that elaborates a good profile for a certain proof pattern is now able to share or backup this profile thus increasing the number of automatic proofs for a given proof pattern.		The proportion of automatically discharged proof obligations heavily depends on Auto-Tactic configuration. Sometimes, the automatic prover fails because the tactics are applied in an unappropriate order. Since Rodin 2.4, a new tactic combinator 'Attempt after Lasso' is available in the tactic profile editor as well as an import/export feature. Indeed, a user that elaborates a good profile for a certain proof pattern is now able to share or backup this profile thus increasing the number of automatic proofs for a given proof pattern.

	Two main reasons mainly motivated the integration of SMT solvers into the Rodin platform. Firstly, to allow Rodin to benefit from the ~~know~~ capacity of such solvers in the field of arithmetics. Secondly, to extract some useful ~~informations~~ from the proofs that these solvers produce such as unsatisfiable cores, in order to significantly decrease the proving time of a modified model. The translation of Event-B language into the SMT-LIB language is the main issue of this integration. Two approaches were developed for this. The more efficient one is based on the translation capabilities of the integrated predicate prover of the Rodin platform (PP). It is completed by translating membership using an uninterpreted predicate symbol, refined with an axiom of the set theory.		Two main reasons mainly motivated the integration of SMT solvers into the Rodin platform. Firstly, to allow Rodin to benefit from the known capacity of such solvers in the field of arithmetics. Secondly, to extract some useful information from the proofs that these solvers produce such as unsatisfiable cores, in order to significantly decrease the proving time of a modified model. The translation of Event-B language into the SMT-LIB language is the main issue of this integration. Two approaches were developed for this. The more efficient one is based on the translation capabilities of the integrated predicate prover of the Rodin platform (PP). It is completed by translating membership using an uninterpreted predicate symbol, refined with an axiom of the set theory.

	= Available Documentation =		= Available Documentation =

imported>Laurent: /* Overview */

2012-06-28T15:14:48Z

Overview

← Older revision		Revision as of 15:14, 28 June 2012
Line 1:		Line 1:
	= Overview =		= Overview =
	In an Event-B development, more than 60% of the time is spent on proofs. That explains why all users are naturally keen for the proofs to be as automatic as possible and why the automated prover enhancement was a continuous task since the birth of the Rodin platform.		In an Event-B development, more than 60% of the time is spent on proofs. That explains why all users are naturally keen for the proofs to be as automatic as possible and why the automated prover enhancement was a continuous task since the birth of the Rodin platform.
	Enhancing the automated prover can be achieved by core platform refactorings and additions to it, such as the addition of integrated reasoners and tactics, but also by the integration of some external reasoning ability such as external provers (e.g. ~~the~~ SMT solvers).<br>		Enhancing the automated prover can be achieved by core platform refactorings and additions to it, such as the addition of integrated reasoners and tactics, but also by the integration of some external reasoning ability such as external provers (e.g., SMT solvers).<br>
	From the core platform point of view, and within the ten first month of ADVANCE, it consisted into two tasks: the addition of rewriting and inference rules, and the addition of a mechanism to allow the customization and the parametrization or combination of tactics. The user is now able to define various types of tactics called 'profiles' which could be customized and parameterized tactics to discharge some specific proof obligations. The user can furthermore share and backup these defined tactics using the provided import/export mechanism.<br>		From the core platform point of view, and within the ten first month of ADVANCE, it consisted into two tasks: the addition of rewriting and inference rules, and the addition of a mechanism to allow the customization and the parametrization or combination of tactics. The user is now able to define various types of tactics called 'profiles' which could be customized and parameterized tactics to discharge some specific proof obligations. The user can furthermore share and backup these defined tactics using the provided import/export mechanism.<br>
	From an external point of view, the SMT Solver Integration plug-in allowing to use the SMT solvers within Rodin is an effective alternative to the Atelier-B provers, particularly when reasoning on linear arithmetic. It is maintained in the time frame of ADVANCE, and increases the rate of automatically discharged proof obligations.		From an external point of view, the SMT Solver Integration plug-in allowing to use the SMT solvers within Rodin as an effective alternative to the Atelier-B provers, particularly when reasoning on linear arithmetic. It is maintained in the time frame of ADVANCE, and increases the rate of automatically discharged proof obligations.

	= Motivations / Decisions =		= Motivations / Decisions =

imported>Tommy at 15:41, 25 June 2012

2012-06-25T15:41:11Z

← Older revision		Revision as of 15:41, 25 June 2012
Line 1:		Line 1:
	== Overview ==		= Overview =
	In an Event-B development, more than 60% of the time is spent on proofs. That explains why all users are naturally keen for the proofs to be as automatic as possible and why the automated prover enhancement was a continuous task since the birth of the Rodin platform.		In an Event-B development, more than 60% of the time is spent on proofs. That explains why all users are naturally keen for the proofs to be as automatic as possible and why the automated prover enhancement was a continuous task since the birth of the Rodin platform.
	Enhancing the automated prover can be achieved by core platform refactorings and additions to it, such as the addition of integrated reasoners and tactics, but also by the integration of some external reasoning ability such as external provers (e.g. the SMT solvers).<br>		Enhancing the automated prover can be achieved by core platform refactorings and additions to it, such as the addition of integrated reasoners and tactics, but also by the integration of some external reasoning ability such as external provers (e.g. the SMT solvers).<br>
Line 5:		Line 5:
	From an external point of view, the SMT Solver Integration plug-in allowing to use the SMT solvers within Rodin is an effective alternative to the Atelier-B provers, particularly when reasoning on linear arithmetic. It is maintained in the time frame of ADVANCE, and increases the rate of automatically discharged proof obligations.		From an external point of view, the SMT Solver Integration plug-in allowing to use the SMT solvers within Rodin is an effective alternative to the Atelier-B provers, particularly when reasoning on linear arithmetic. It is maintained in the time frame of ADVANCE, and increases the rate of automatically discharged proof obligations.

	== Motivations / Decisions ==		= Motivations / Decisions =
	The proportion of automatically discharged proof obligations heavily depends on Auto-Tactic configuration. Sometimes, the automatic prover fails because the tactics are applied in a unappropriate order. Since Rodin 2.4, a new tactic combinator 'Attempt after Lasso' is available in auto tactic profile editor as well as an import/export feature. Indeed, a user that elaborates a good profile for a certain proof pattern is now able to share or backup this profile thus increasing the number of automatic proofs for a given proof pattern.		The proportion of automatically discharged proof obligations heavily depends on Auto-Tactic configuration. Sometimes, the automatic prover fails because the tactics are applied in a unappropriate order. Since Rodin 2.4, a new tactic combinator 'Attempt after Lasso' is available in auto tactic profile editor as well as an import/export feature. Indeed, a user that elaborates a good profile for a certain proof pattern is now able to share or backup this profile thus increasing the number of automatic proofs for a given proof pattern.

	Two main reasons mainly motivated the integration of SMT solvers into the Rodin platform. Firstly, to allow Rodin to benefit from the know capacity of such solvers in the field of arithmetics. Secondly, to extract some useful informations from the proofs that these solvers produce such as unsatisfiable cores, in order to significantly decrease the proving time of a modified model. The translation of Event-B language into the SMT-LIB language is the main issue of this integration. Two approaches were developed for this. The more efficient one is based on the translation capabilities of the integrated predicate prover of the Rodin platform (PP). It is completed by translating membership using an uninterpreted predicate symbol, refined with an axiom of the set theory.		Two main reasons mainly motivated the integration of SMT solvers into the Rodin platform. Firstly, to allow Rodin to benefit from the know capacity of such solvers in the field of arithmetics. Secondly, to extract some useful informations from the proofs that these solvers produce such as unsatisfiable cores, in order to significantly decrease the proving time of a modified model. The translation of Event-B language into the SMT-LIB language is the main issue of this integration. Two approaches were developed for this. The more efficient one is based on the translation capabilities of the integrated predicate prover of the Rodin platform (PP). It is completed by translating membership using an uninterpreted predicate symbol, refined with an axiom of the set theory.

	== Available Documentation ==		= Available Documentation =
	A page<ref>http://handbook.event-b.org/current/html/preferences.html#ref_01_preferences_auto_post_tactic</ref> concerning tactic profiles is available in the user manual.<br>		A page<ref>http://handbook.event-b.org/current/html/preferences.html#ref_01_preferences_auto_post_tactic</ref> concerning tactic profiles is available in the user manual.<br>
	A page<ref>http://wiki.event-b.org/index.php/SMT_Solvers_Plug-in</ref> is dedicated to the SMT Solver integration plug-in on the Event-B wiki.		A page<ref>http://wiki.event-b.org/index.php/SMT_Solvers_Plug-in</ref> is dedicated to the SMT Solver integration plug-in on the Event-B wiki.

	== Planning ==		= Planning =
	Enhancement of the automated proof will continue as long as Rodin is maintained. This will be mainly be achieved by the implementation of the remaining missing rewriting<ref>http://wiki.event-b.org/index.php/All_Rewrite_Rules</ref> and inference rules<ref>http://wiki.event-b.org/index.php/Inference_Rules</ref> that have already been documented, and by the addition of new ones.		Enhancement of the automated proof will continue as long as Rodin is maintained. This will be mainly be achieved by the implementation of the remaining missing rewriting<ref>http://wiki.event-b.org/index.php/All_Rewrite_Rules</ref> and inference rules<ref>http://wiki.event-b.org/index.php/Inference_Rules</ref> that have already been documented, and by the addition of new ones.

	Maintenance of the SMT solver integration plug-in will be ensured within the time frame of ADVANCE.		Maintenance of the SMT solver integration plug-in will be ensured within the time frame of ADVANCE.

	== References ==		= References =
	<references/>		<references/>

	[[Category:ADVANCE D3.2 Deliverable]]		[[Category:ADVANCE D3.2 Deliverable]]

imported>Tommy: /* Overview */

2012-06-25T14:27:19Z

Overview

← Older revision		Revision as of 14:27, 25 June 2012
Line 3:		Line 3:
	Enhancing the automated prover can be achieved by core platform refactorings and additions to it, such as the addition of integrated reasoners and tactics, but also by the integration of some external reasoning ability such as external provers (e.g. the SMT solvers).<br>		Enhancing the automated prover can be achieved by core platform refactorings and additions to it, such as the addition of integrated reasoners and tactics, but also by the integration of some external reasoning ability such as external provers (e.g. the SMT solvers).<br>
	From the core platform point of view, and within the ten first month of ADVANCE, it consisted into two tasks: the addition of rewriting and inference rules, and the addition of a mechanism to allow the customization and the parametrization or combination of tactics. The user is now able to define various types of tactics called 'profiles' which could be customized and parameterized tactics to discharge some specific proof obligations. The user can furthermore share and backup these defined tactics using the provided import/export mechanism.<br>		From the core platform point of view, and within the ten first month of ADVANCE, it consisted into two tasks: the addition of rewriting and inference rules, and the addition of a mechanism to allow the customization and the parametrization or combination of tactics. The user is now able to define various types of tactics called 'profiles' which could be customized and parameterized tactics to discharge some specific proof obligations. The user can furthermore share and backup these defined tactics using the provided import/export mechanism.<br>
	From an external point of view, the SMT ~~Solvers~~ plug-in allowing to use the SMT solvers within Rodin is an effective alternative to the Atelier-B provers, particularly when reasoning on linear arithmetic. It is maintained in the time frame of ADVANCE, and increases the rate of automatically discharged proof obligations.		From an external point of view, the SMT Solver Integration plug-in allowing to use the SMT solvers within Rodin is an effective alternative to the Atelier-B provers, particularly when reasoning on linear arithmetic. It is maintained in the time frame of ADVANCE, and increases the rate of automatically discharged proof obligations.

	== Motivations / Decisions ==		== Motivations / Decisions ==

imported>Tommy: /* Planning */

2012-06-25T14:26:59Z

Planning

← Older revision		Revision as of 14:26, 25 June 2012
Line 17:		Line 17:
	Enhancement of the automated proof will continue as long as Rodin is maintained. This will be mainly be achieved by the implementation of the remaining missing rewriting<ref>http://wiki.event-b.org/index.php/All_Rewrite_Rules</ref> and inference rules<ref>http://wiki.event-b.org/index.php/Inference_Rules</ref> that have already been documented, and by the addition of new ones.		Enhancement of the automated proof will continue as long as Rodin is maintained. This will be mainly be achieved by the implementation of the remaining missing rewriting<ref>http://wiki.event-b.org/index.php/All_Rewrite_Rules</ref> and inference rules<ref>http://wiki.event-b.org/index.php/Inference_Rules</ref> that have already been documented, and by the addition of new ones.

	Maintenance of the SMT ~~Solver~~ integration plug-in will be ensured within the time frame of ADVANCE.		Maintenance of the SMT solver integration plug-in will be ensured within the time frame of ADVANCE.

	== References ==		== References ==

imported>Tommy: /* Available Documentation */

2012-06-25T14:26:07Z

Available Documentation

← Older revision		Revision as of 14:26, 25 June 2012
Line 11:		Line 11:

	== Available Documentation ==		== Available Documentation ==
	A page ~~concerning tactic profiles is available in the user manual~~<ref>http://handbook.event-b.org/current/html/preferences.html#ref_01_preferences_auto_post_tactic</ref>.<br>		A page<ref>http://handbook.event-b.org/current/html/preferences.html#ref_01_preferences_auto_post_tactic</ref> concerning tactic profiles is available in the user manual.<br>
	A page ~~is dedicated to the SMT Solver integration plug-in on the Event-B wiki~~<ref>http://wiki.event-b.org/index.php/SMT_Solvers_Plug-in</ref>.		A page<ref>http://wiki.event-b.org/index.php/SMT_Solvers_Plug-in</ref> is dedicated to the SMT Solver integration plug-in on the Event-B wiki.

	== Planning ==		== Planning ==