D23 Rule-based Prover - Revision history

imported>Pascal: /* Planning */

2010-01-08T11:44:40Z

Planning

← Older revision		Revision as of 11:44, 8 January 2010
Line 55:		Line 55:

	The rule-based prover plug-in is available as an external plug-in for Rodin release 1.1 and above.		The rule-based prover plug-in is available as an external plug-in for Rodin release 1.1 and above.
	:See [http://wiki.event-b.org/index.php/Rodin_Platform_1.1_Release_Notes Rodin Platform 1.1 Release_Notes]		:See [http://wiki.event-b.org/index.php/Rodin_Platform_1.1_Release_Notes Rodin Platform 1.1 Release_Notes] and [http://wiki.event-b.org/index.php/Rodin_Platform_1.2_Release_Notes Rodin Platform 1.2 Release_Notes].
	:and [http://wiki.event-b.org/index.php/Rodin_Platform_1.2_Release_Notes Rodin Platform 1.2 Release_Notes].
	[[Category:D23 Deliverable]]		[[Category:D23 Deliverable]]

imported>Pascal: /* Choices/Decisions */

2010-01-08T11:34:13Z

Choices/Decisions

← Older revision		Revision as of 11:34, 8 January 2010
Line 36:		Line 36:

	*Contexts describe the static properties of models, and they are used to parameterise machines. Adding the capability of defining proof rules within contexts would allow the co-existence of modelling elements and meta-logical elements with no clear relationship between the two. This may require significant changes to the core architecture, and will unnecessarily overload the functionality of contexts with elements not directly relevant to modelling. As such, a clear separation of modelling and meta-reasoning was adopted. This resulted in a theory construct that acts as a placeholder for prover extensions.		*Contexts describe the static properties of models, and they are used to parameterise machines. Adding the capability of defining proof rules within contexts would allow the co-existence of modelling elements and meta-logical elements with no clear relationship between the two. This may require significant changes to the core architecture, and will unnecessarily overload the functionality of contexts with elements not directly relevant to modelling. As such, a clear separation of modelling and meta-reasoning was adopted. This resulted in a theory construct that acts as a placeholder for prover extensions.
	*Rodin has a collection of rewrite and inference rules. Most inference rules as found in:		*Rodin has a collection of rewrite and inference rules. Most inference rules as found in [http://wiki.event-b.org/index.php/Inference_Rules] require predicate variables to be defined. This is not the case for most rewrite rules as found in [http://wiki.event-b.org/index.php/All_Rewrite_Rules].

	:[http://wiki.event-b.org/index.php/Inference_Rules ~~Inference Rules~~]

	:require predicate variables to be defined. This is not the case for most rewrite rules as found in:

	:[http://wiki.event-b.org/index.php/All_Rewrite_Rules ~~All Rewrite Rules~~]

	:Since predicate variables were not available when the development started, it was decided to cover rewrite rules first.		:Since predicate variables were not available when the development started, it was decided to cover rewrite rules first.

imported>Pascal: /* Motivations */

2010-01-08T11:33:40Z

Motivations

← Older revision		Revision as of 11:33, 8 January 2010
Line 18:		Line 18:
	*After a new rule is added, soundness of the prover augmented with the new rule has to be established. It is not clear how this can be achieved at the level of Java code.		*After a new rule is added, soundness of the prover augmented with the new rule has to be established. It is not clear how this can be achieved at the level of Java code.

	The rule-based prover is an attempt to address the aforementioned limitations in a uniform and effective fashion. It is uniform because it offers the user (we shall call a theory developer) the possibility to develop and validate theories in a similar way to developing and validating models. It is also effective since it relieves the theory developer from writing Java code, and covers most of the rewrite rules available ~~at:~~		The rule-based prover is an attempt to address the aforementioned limitations in a uniform and effective fashion. It is uniform because it offers the user (we shall call a theory developer) the possibility to develop and validate theories in a similar way to developing and validating models. It is also effective since it relieves the theory developer from writing Java code, and covers most of the rewrite rules available in [http://wiki.event-b.org/index.php/All_Rewrite_Rules]

	:[http://wiki.event-b.org/index.php/All_Rewrite_Rules ~~All Rewrite Rules~~]

	The advantages of the rule-based prover include:		The advantages of the rule-based prover include:

imported>Pascal: /* Planning */

2010-01-08T11:32:51Z

Planning

← Older revision		Revision as of 11:32, 8 January 2010
Line 63:		Line 63:

	The rule-based prover plug-in is available as an external plug-in for Rodin release 1.1 and above.		The rule-based prover plug-in is available as an external plug-in for Rodin release 1.1 and above.
	:See [http://wiki.event-b.org/index.php/Rodin_Platform_1.1_Release_Notes Rodin Platform 1.1 Release_Notes].		:See [http://wiki.event-b.org/index.php/Rodin_Platform_1.1_Release_Notes Rodin Platform 1.1 Release_Notes]
	:and [http://wiki.event-b.org/index.php/Rodin_Platform_1.2_Release_Notes Rodin Platform 1.2 Release_Notes].		:and [http://wiki.event-b.org/index.php/Rodin_Platform_1.2_Release_Notes Rodin Platform 1.2 Release_Notes].
	[[Category:D23 Deliverable]]		[[Category:D23 Deliverable]]

imported>Pascal: /* Planning */

2010-01-08T11:32:40Z

Planning

← Older revision		Revision as of 11:32, 8 January 2010
Line 63:		Line 63:

	The rule-based prover plug-in is available as an external plug-in for Rodin release 1.1 and above.		The rule-based prover plug-in is available as an external plug-in for Rodin release 1.1 and above.
	:See [http://wiki.event-b.org/index.php/Rodin_Platform_1.1_Release_Notes ~~http://wiki.event-b~~.~~org/index.php/Rodin_Platform_1.1_Release_Notes~~].		:See [http://wiki.event-b.org/index.php/Rodin_Platform_1.1_Release_Notes Rodin Platform 1.1 Release_Notes].
	:and [http://wiki.event-b.org/index.php/Rodin_Platform_1.2_Release_Notes ~~http://wiki~~.~~event-b.org/index.php/Rodin_Platform_1.2_Release_Notes~~].		:and [http://wiki.event-b.org/index.php/Rodin_Platform_1.2_Release_Notes Rodin Platform 1.2 Release_Notes].
	[[Category:D23 Deliverable]]		[[Category:D23 Deliverable]]

imported>Pascal: /* Available Documentation */

2010-01-08T11:31:41Z

Available Documentation

← Older revision		Revision as of 11:31, 8 January 2010
Line 53:		Line 53:
	There is a dedicated wiki page covering the plug-in functionality:		There is a dedicated wiki page covering the plug-in functionality:

	* [[Rule-~~based Prover Plug~~-in\|Rule-based Prover]]		* [http://wiki.event-b.org/index.php/Rule-based_Prover_Plug-in Rule-based Prover]

	==Papers & Technical Reports==		==Papers & Technical Reports==

imported>Pascal: /* Choices/Decisions */

2010-01-08T11:30:22Z

Choices/Decisions

← Older revision		Revision as of 11:30, 8 January 2010
Line 40:		Line 40:
	*Rodin has a collection of rewrite and inference rules. Most inference rules as found in:		*Rodin has a collection of rewrite and inference rules. Most inference rules as found in:

	:http://wiki.event-b.org/index.php/Inference_Rules		:[http://wiki.event-b.org/index.php/Inference_Rules Inference Rules]

	:require predicate variables to be defined. This is not the case for most rewrite rules as found in:		:require predicate variables to be defined. This is not the case for most rewrite rules as found in:

	:http://wiki.event-b.org/index.php/All_Rewrite_Rules .		:[http://wiki.event-b.org/index.php/All_Rewrite_Rules All Rewrite Rules]

	:Since predicate variables were not available when the development started, it was decided to cover rewrite rules first.		:Since predicate variables were not available when the development started, it was decided to cover rewrite rules first.

imported>Pascal: /* Motivations */

2010-01-08T11:29:53Z

Motivations

← Older revision		Revision as of 11:29, 8 January 2010
Line 20:		Line 20:
	The rule-based prover is an attempt to address the aforementioned limitations in a uniform and effective fashion. It is uniform because it offers the user (we shall call a theory developer) the possibility to develop and validate theories in a similar way to developing and validating models. It is also effective since it relieves the theory developer from writing Java code, and covers most of the rewrite rules available at:		The rule-based prover is an attempt to address the aforementioned limitations in a uniform and effective fashion. It is uniform because it offers the user (we shall call a theory developer) the possibility to develop and validate theories in a similar way to developing and validating models. It is also effective since it relieves the theory developer from writing Java code, and covers most of the rewrite rules available at:

	:http://wiki.event-b.org/index.php/All_Rewrite_Rules		:[http://wiki.event-b.org/index.php/All_Rewrite_Rules All Rewrite Rules]

	The advantages of the rule-based prover include:		The advantages of the rule-based prover include:

imported>Pascal: /* Available Documentation */

2009-12-04T11:08:38Z

Available Documentation

← Older revision		Revision as of 11:08, 4 December 2009
Line 53:		Line 53:
	There is a dedicated wiki page covering the plug-in functionality:		There is a dedicated wiki page covering the plug-in functionality:

	* [[Rule-based Prover Plug-in\|Rule-based Prover ~~wiki~~]]		* [[Rule-based Prover Plug-in\|Rule-based Prover]]

	==Papers & Technical Reports==		==Papers & Technical Reports==

imported>Pascal: /* Papers & Technical Reports */

2009-12-04T11:08:15Z

Papers & Technical Reports

← Older revision		Revision as of 11:08, 4 December 2009
Line 57:		Line 57:
	==Papers & Technical Reports==		==Papers & Technical Reports==

	:[http://eprints.ecs.soton.ac.uk/18269/ Issam Maamria, Michael Butler, Andrew Edmunds, and Abdolbaghi Rezazadeh. On an Extensible Rule-based Prover for Event-B, ABZ'2010.]		*[http://eprints.ecs.soton.ac.uk/18269/ Issam Maamria, Michael Butler, Andrew Edmunds, and Abdolbaghi Rezazadeh. On an Extensible Rule-based Prover for Event-B, ABZ'2010.]
	:[http://eprints.ecs.soton.ac.uk/18273/ Issam Maamria, Michael Butler, Andrew Edmunds, and Abdolbaghi Rezazadeh. On an Extensible Rule-based Prover for Event-B, Technical Report.]		*[http://eprints.ecs.soton.ac.uk/18273/ Issam Maamria, Michael Butler, Andrew Edmunds, and Abdolbaghi Rezazadeh. On an Extensible Rule-based Prover for Event-B, Technical Report.]

	= Planning =		= Planning =