Extending the Proof Manager - Revision history

imported>Ladenberger at 10:27, 27 October 2011

2011-10-27T10:27:29Z

← Older revision		Revision as of 10:27, 27 October 2011
Line 4:		Line 4:
	There are two ways for extending the Proof Manager:		There are two ways for extending the Proof Manager:

	# adding a new [~~[Reasoners\|~~reasoner]].		# adding a new [http://handbook.cobra.cs.uni-duesseldorf.de/current/html/reasoners.html reasoner].

	# adding a new [~~[Tactics\|~~tactic]].		# adding a new [http://handbook.cobra.cs.uni-duesseldorf.de/current/html/proof_tactics.html tactic].

	== Adding a New Reasoner ==		== Adding a New Reasoner ==

imported>Nicolas: /* Adding a New Reasoner */

2010-11-24T17:32:48Z

Adding a New Reasoner

← Older revision		Revision as of 17:32, 24 November 2010
Line 36:		Line 36:

	* [[Adding General Purpose Reasoners \|General purpose]] Reasoners that do not fall into the four previous categories.		* [[Adding General Purpose Reasoners \|General purpose]] Reasoners that do not fall into the four previous categories.

			''Please also have a look at'' [[How_To_Evolve_Reasoners\| How To Evolve Reasoners]].

	== Adding a New Tactic ==		== Adding a New Tactic ==

imported>Mathieu: Category:Proof

2009-08-12T12:52:50Z

Category:Proof

← Older revision		Revision as of 12:52, 12 August 2009
Line 50:		Line 50:
	[[Category:Developer documentation]]		[[Category:Developer documentation]]
	[[Category:Rodin Platform]]		[[Category:Rodin Platform]]
			[[Category:Proof]]

imported>Mathieu: cat

2008-09-17T16:53:23Z

cat

← Older revision		Revision as of 16:53, 17 September 2008
Line 45:		Line 45:

	* [[Adding Manual Tactics \| Manual Tactics ]]: Tactics that need to be invoke manually during interactive proofs.		* [[Adding Manual Tactics \| Manual Tactics ]]: Tactics that need to be invoke manually during interactive proofs.



			[[Category:Developer documentation]]
			[[Category:Rodin Platform]]

imported>Son: /* Adding a New Tactic */

2008-09-16T17:53:11Z

Adding a New Tactic

← Older revision		Revision as of 17:53, 16 September 2008
Line 39:		Line 39:
	== Adding a New Tactic ==		== Adding a New Tactic ==
	Adding a reasoner is only a first step in extending the Proof Manager. Reasoners need to be wrapped by Tactics for the Proof Manager to use. Similar to reasoners, there are different types of tactics for implementation purpose.		Adding a reasoner is only a first step in extending the Proof Manager. Reasoners need to be wrapped by Tactics for the Proof Manager to use. Similar to reasoners, there are different types of tactics for implementation purpose.

			=== Implementing a Tactic ===

	* [[Adding Automatic Tactics \| Automatic Tactics]]: Tactics that can be run automatically either as POM Tactics or Post Tactics.		* [[Adding Automatic Tactics \| Automatic Tactics]]: Tactics that can be run automatically either as POM Tactics or Post Tactics.

	* [[Adding Manual Tactics \| Manual Tactics ]]: Tactics that need to be invoke manually during interactive proofs.		* [[Adding Manual Tactics \| Manual Tactics ]]: Tactics that need to be invoke manually during interactive proofs.

imported>Son at 17:43, 16 September 2008

2008-09-16T17:43:40Z

← Older revision		Revision as of 17:43, 16 September 2008
Line 35:		Line 35:
	* [[Adding Manual Inference Reasoners \| Manual inference]] Reasoner of this type apply an inference rule manually.		* [[Adding Manual Inference Reasoners \| Manual inference]] Reasoner of this type apply an inference rule manually.

	* [[~~Extending the Proof Manager#~~General Purpose Reasoners\|General purpose]] Reasoners that do not fall into the four previous categories.		* [[Adding General Purpose Reasoners \|General purpose]] Reasoners that do not fall into the four previous categories.

			== Adding a New Tactic ==
			Adding a reasoner is only a first step in extending the Proof Manager. Reasoners need to be wrapped by Tactics for the Proof Manager to use. Similar to reasoners, there are different types of tactics for implementation purpose.

	~~=== General Purpose Reasoners ===~~		* [[Adding Automatic Tactics \| Automatic Tactics]]: Tactics that can be run automatically either as POM Tactics or Post Tactics.

	== Adding ~~a New Tactic ==~~		* [[Adding Manual Tactics \| Manual Tactics ]]: Tactics that need to be invoke manually during interactive proofs.

imported>Son: /* Adding a New Reasoner */

2008-09-16T12:43:30Z

Adding a New Reasoner

← Older revision		Revision as of 12:43, 16 September 2008
Line 33:		Line 33:
	* [[Adding Automatic Inference Reasoners \| Automatic inference]] Reasoners of this type apply an inference rule automatically.		* [[Adding Automatic Inference Reasoners \| Automatic inference]] Reasoners of this type apply an inference rule automatically.

	* [[~~Extending the Proof Manager#~~Manual Inference Reasoners\|Manual inference]] Reasoner of this type apply ~~and~~ inference rule manually.		* [[Adding Manual Inference Reasoners \| Manual inference]] Reasoner of this type apply an inference rule manually.

	* [[Extending the Proof Manager#General Purpose Reasoners\|General purpose]] Reasoners that do not fall into the four previous categories.		* [[Extending the Proof Manager#General Purpose Reasoners\|General purpose]] Reasoners that do not fall into the four previous categories.

	~~=== Manual Inference Reasoners ===~~

	=== General Purpose Reasoners ===		=== General Purpose Reasoners ===

	== Adding a New Tactic ==		== Adding a New Tactic ==

imported>Son at 13:52, 15 September 2008

2008-09-15T13:52:48Z

← Older revision		Revision as of 13:52, 15 September 2008
Line 31:		Line 31:
	* [[Adding Manual Rewrite Reasoners \| Manual rewrite]] Reasoners of this type apply a rewriting rule for a given formula (or sub-formula) in the goal or in one of the hypotheses.		* [[Adding Manual Rewrite Reasoners \| Manual rewrite]] Reasoners of this type apply a rewriting rule for a given formula (or sub-formula) in the goal or in one of the hypotheses.

	* [[~~Extending the Proof Manager#~~Automatic Inference Reasoners\|Automatic inference]] Reasoners of this type apply an inference rule automatically.		* [[Adding Automatic Inference Reasoners \| Automatic inference]] Reasoners of this type apply an inference rule automatically.

	* [[Extending the Proof Manager#Manual Inference Reasoners\|Manual inference]] Reasoner of this type apply and inference rule manually.		* [[Extending the Proof Manager#Manual Inference Reasoners\|Manual inference]] Reasoner of this type apply and inference rule manually.

	* [[Extending the Proof Manager#General Purpose Reasoners\|General purpose]] Reasoners that do not fall into the four previous categories.		* [[Extending the Proof Manager#General Purpose Reasoners\|General purpose]] Reasoners that do not fall into the four previous categories.

	~~=== Automatic Inference Reasoners ===~~

	=== Manual Inference Reasoners ===		=== Manual Inference Reasoners ===

imported>Son at 16:01, 13 September 2008

2008-09-13T16:01:58Z

← Older revision		Revision as of 16:01, 13 September 2008
Line 28:		Line 28:

	* [[Adding Automatic Rewrite Reasoners \| Automatic rewrite]] Reasoners of this type apply some rewriting rules automatically to simplify the input sequent.		* [[Adding Automatic Rewrite Reasoners \| Automatic rewrite]] Reasoners of this type apply some rewriting rules automatically to simplify the input sequent.

			* [[Adding Manual Rewrite Reasoners \| Manual rewrite]] Reasoners of this type apply a rewriting rule for a given formula (or sub-formula) in the goal or in one of the hypotheses.

	* [[Extending the Proof Manager#Automatic Inference Reasoners\|Automatic inference]] Reasoners of this type apply an inference rule automatically.		* [[Extending the Proof Manager#Automatic Inference Reasoners\|Automatic inference]] Reasoners of this type apply an inference rule automatically.

	* [[Extending the Proof Manager#Manual Rewrite Reasoners\|Manual rewrite]] Reasoner of this type apply a rewriting rule for a given formula (or sub-formula) in the goal or in one of the hypotheses.

	* [[Extending the Proof Manager#Manual Inference Reasoners\|Manual inference]] Reasoner of this type apply and inference rule manually.		* [[Extending the Proof Manager#Manual Inference Reasoners\|Manual inference]] Reasoner of this type apply and inference rule manually.
Line 37:		Line 37:
	* [[Extending the Proof Manager#General Purpose Reasoners\|General purpose]] Reasoners that do not fall into the four previous categories.		* [[Extending the Proof Manager#General Purpose Reasoners\|General purpose]] Reasoners that do not fall into the four previous categories.

	~~=== Automatic Rewrite Reasoners ===~~
	=== Automatic Inference Reasoners ===		=== Automatic Inference Reasoners ===

	~~=== Manual Rewrite Reasoners ===~~

	=== Manual Inference Reasoners ===		=== Manual Inference Reasoners ===

imported>Son at 08:18, 12 September 2008

2008-09-12T08:18:10Z

← Older revision		Revision as of 08:18, 12 September 2008
Line 38:		Line 38:

	=== Automatic Rewrite Reasoners ===		=== Automatic Rewrite Reasoners ===
	Beside the input sequent, reasoners of this type does not have any extra input and automatically rewrites all the occurrences of certain formulas. An example of this is the rewriter which rewrites according to the following rules:

	~~<math>~~
	~~\begin{array}{rcl}~~
	~~\top \limp P & \Rightarrow & P \\~~
	~~P \limp \top & \Rightarrow & \top \\~~
	~~\bot \limp P & \Rightarrow & \top \\~~
	~~P \limp \bot & \Rightarrow & \neg P~~
	~~\end{array}~~
	~~</math>~~

	~~Below are the step by step instructions to create an automatic rewrite reasoner:~~

	* Create a new plug-in project, e.g. ''org.eventb.contributors.seqprover.autorewrites''. Deselect the plug-in options for "Generating an activator" and "Contribution to the UI".

	* Add dependency on the project ''org.eventb.core.seqprover''

	* Add an extension for ''org.eventb.core.seqprover.reasoners'', e.g.

	~~<extension point="org.eventb.core.seqprover.reasoners">~~
	~~<reasoner~~
	~~class="org.eventb.contributors.seqprover.autorewrite.AutoRewrites"~~
	~~id="autoRewrites"~~
	~~name="%autoRewritesName"/>~~
	~~</extension>~~

	~~(add the key autoRewritesName to the plugin.properties accordingly).~~

	* Click on the class attribute of the newly created extension. A dialog appears for new class wizard.

	* The abstract implementation of this class is ''org.eventb.internal.core.seqprover.eventbExtensions.rewriters.AbstractAutoRewrites''. Choose this as the Superclass in the new class wizard. (For the moment, the class is internal within the project and subjected to be changed. Clients can make a copy of this class to develop their own implementation).

	* Finish the wizard and a new implementation for AutoRewrite class is created.

	* The implementation can be as follows:

	~~import org.eventb.core.ast.IFormulaRewriter;~~
	~~import org.eventb.internal.core.seqprover.eventbExtensions.rewriters.AbstractAutoRewrites;~~
	~~public class AutoRewrites extends AbstractAutoRewrites {~~

	~~public AutoRewrites() {~~
	~~super(new AutoRewriterImpl(), true);~~
	}

	~~public static String REASONER_ID = "org.evenb.contributors.seqprover.autoRewrites";~~

	~~public String getReasonerID() {~~
	~~return REASONER_ID;~~
	}

	~~@Override~~
	~~protected String getDisplayName() {~~
	~~return "simplification rewrites";~~
	}

	}

	The constructor must call the super constructor method ''super(IFormulaRewriter, boolean)'' to specify the formula rewriter to use and the resulting reasoner should hide the source of the rewritten hypothesis or not. Clients need to implement two methods. The first one, namely ''getReasonerID()'', return the string ID of this reasoner. This must be the same ID as declared in the ''plugin.xml'' file (do not forget the project name prefix). The second method is ''getDisplayName()'' which return the display name of the reasoner, which will be used for displaying in the UI.

	~~What left is to implement the formula rewriter which is used in the constructor of the reasoner. This is very convenient by using [http://tom.loria.fr/ Tom].~~

	* Create a file named ''build-tom.xml'' within your project. The best way to do this is to copy from ''org.eventb.core.seqprover'', and modify this accordingly.
	* Right click on the name of your project and choose Properties.
	* Choose "Builders", then click on "New" and choose "Ant Build" and click OK. A dialog will open for new builder wizard.
	* At the "Main" tab:
	** Enter the name of the builder, e.g. ''Tom Builder''.
	** Buildfile: ''Browse Workspace'' to your ''build-tom.xml''.
	** Base Directory: ''Variables'' and choose ''build_project''.
	* At the "Targets" tab:
	** Auto Build: Click ''Set Targets'' and choose "tom" from the list.
	** During a "clean": Click "Set Targets" and choose ''clean'' (unchecked ''tom'').

	~~Creating the~~
	=== Automatic Inference Reasoners ===		=== Automatic Inference Reasoners ===

← Older revision		Revision as of 13:52, 15 September 2008
Line 31:		Line 31:
	* [[Adding Manual Rewrite Reasoners \| Manual rewrite]] Reasoners of this type apply a rewriting rule for a given formula (or sub-formula) in the goal or in one of the hypotheses.		* [[Adding Manual Rewrite Reasoners \| Manual rewrite]] Reasoners of this type apply a rewriting rule for a given formula (or sub-formula) in the goal or in one of the hypotheses.

	* [[~~Extending the Proof Manager#~~Automatic Inference Reasoners\|Automatic inference]] Reasoners of this type apply an inference rule automatically.		* [[Adding Automatic Inference Reasoners \| Automatic inference]] Reasoners of this type apply an inference rule automatically.

	* [[Extending the Proof Manager#Manual Inference Reasoners\|Manual inference]] Reasoner of this type apply and inference rule manually.		* [[Extending the Proof Manager#Manual Inference Reasoners\|Manual inference]] Reasoner of this type apply and inference rule manually.

	* [[Extending the Proof Manager#General Purpose Reasoners\|General purpose]] Reasoners that do not fall into the four previous categories.		* [[Extending the Proof Manager#General Purpose Reasoners\|General purpose]] Reasoners that do not fall into the four previous categories.

	~~=== Automatic Inference Reasoners ===~~

	=== Manual Inference Reasoners ===		=== Manual Inference Reasoners ===