Talk:Event-B Language - Revision history

imported>Jens: /* Have you installed the provers ? */

2009-10-30T21:22:45Z

Have you installed the provers ?

← Older revision		Revision as of 21:22, 30 October 2009
Line 39:		Line 39:

	[[Image:HaiYun prove.png]]		[[Image:HaiYun prove.png]]




	[[Image:Install_Provers.png]]		[[Image:Install_Provers.png]]

imported>Jens: /* Have you installed the provers ? */

2009-10-30T21:22:26Z

Have you installed the provers ?

← Older revision		Revision as of 21:22, 30 October 2009
Line 37:		Line 37:
	Cheers		Cheers
	Jens		Jens

			[[Image:HaiYun prove.png]]

	[[Image:Install_Provers.png]]		[[Image:Install_Provers.png]]

imported>Jens: /* Have you installed the provers ? */

2009-10-30T21:21:04Z

Have you installed the provers ?

← Older revision		Revision as of 21:21, 30 October 2009
Line 30:		Line 30:
	== Have you installed the provers ?==		== Have you installed the provers ?==

	For legal reasons, Rodin does not contain the Atelier B Provers. You need to install them separately using the update site ~~(see screenshot)~~		For legal reasons, Rodin does not contain the Atelier B Provers. You need to install them separately using the update site

			If you have the provers installed, you can prove the theorem by clicking on the second ∈ in the goal and afterwards use ML.


	Cheers		Cheers

imported>Jens: /* Have you installed the provers */

2009-10-30T21:14:28Z

Have you installed the provers

← Older revision		Revision as of 21:14, 30 October 2009
Line 28:		Line 28:


	== Have you installed the provers ==		== Have you installed the provers ?==

	For legal reasons, Rodin does not contain the Atelier B Provers. You need to install them separately using the update site (see screenshot)		For legal reasons, Rodin does not contain the Atelier B Provers. You need to install them separately using the update site (see screenshot)

			Cheers
			Jens

	[[Image:Install_Provers.png]]		[[Image:Install_Provers.png]]

imported>Jens: /* It is not "parsed" but "passed" */

2009-10-30T21:13:53Z

It is not "parsed" but "passed"

← Older revision		Revision as of 21:13, 30 October 2009
Line 26:		Line 26:

	Futhermore, I have installed the newest version of Rodin (rodin-1.1RC1). I put "{x·x∈0‥4∣x↦0}∈0‥4⇸0‥4" in the AXIOMS and tick it as a theorem. However, the problem is the same as Rodin 0.9.1.		Futhermore, I have installed the newest version of Rodin (rodin-1.1RC1). I put "{x·x∈0‥4∣x↦0}∈0‥4⇸0‥4" in the AXIOMS and tick it as a theorem. However, the problem is the same as Rodin 0.9.1.


			== Have you installed the provers ==

			For legal reasons, Rodin does not contain the Atelier B Provers. You need to install them separately using the update site (see screenshot)
			[[Image:Install_Provers.png]]

imported>Tianhaiyun at 13:43, 27 October 2009

2009-10-27T13:43:57Z

← Older revision		Revision as of 13:43, 27 October 2009
Line 24:		Line 24:
	It means that the oblligation for this theorem is listed but remained red. The screen snapshot is		It means that the oblligation for this theorem is listed but remained red. The screen snapshot is
	"http://4.bp.blogspot.com/_GexLXHeTL7w/Sub0Xb8WoII/AAAAAAAAAD4/5u5XGKlTBTY/s1600/ebp.jpg"		"http://4.bp.blogspot.com/_GexLXHeTL7w/Sub0Xb8WoII/AAAAAAAAAD4/5u5XGKlTBTY/s1600/ebp.jpg"

			Futhermore, I have installed the newest version of Rodin (rodin-1.1RC1). I put "{x·x∈0‥4∣x↦0}∈0‥4⇸0‥4" in the AXIOMS and tick it as a theorem. However, the problem is the same as Rodin 0.9.1.

imported>Tianhaiyun at 13:28, 27 October 2009

2009-10-27T13:28:28Z

← Older revision		Revision as of 13:28, 27 October 2009
Line 18:		Line 18:

	Son		Son


			== It is not "parsed" but "passed" ==
			Much appreciation for that reply. Thanks.
			It means that the oblligation for this theorem is listed but remained red. The screen snapshot is
			"http://4.bp.blogspot.com/_GexLXHeTL7w/Sub0Xb8WoII/AAAAAAAAAD4/5u5XGKlTBTY/s1600/ebp.jpg"

imported>Tianhaiyun at 13:18, 27 October 2009

2009-10-27T13:18:12Z

← Older revision		Revision as of 13:18, 27 October 2009
Line 4:		Line 4:

	The problems is as follows.		The problems is as follows.
	I build one project, in which there is only one context. In this contest, there is only one theorem defined as {x·x∈0‥4∣x↦0}∈0‥4⇸0‥4. The obligation for it is generated by Rodin. However, it reports that the obligation ~~can~~ cannot be passed. It makes me quite confused. Please everyone knowing what the problem is and help me out.		I build one project, in which there is only one context. In this contest, there is only one theorem defined as {x·x∈0‥4∣x↦0}∈0‥4⇸0‥4. The obligation for it is generated by Rodin. However, it reports that the obligation cannot be passed. It makes me quite confused. Please everyone knowing what the problem is and help me out.

	Thank you so lot		Thank you so lot

imported>Son: /* What do you mean by "cannot be parsed"? */ new section

2009-10-27T13:10:44Z

What do you mean by "cannot be parsed"?: new section

← Older revision		Revision as of 13:10, 27 October 2009
Line 10:		Line 10:
	HaiYun tian		HaiYun tian
	SCM Teesside University		SCM Teesside University

			== What do you mean by "cannot be parsed"? ==

			I am a bit confused with the "obligation cannot be parsed". I tried to enter this in Rodin (1.1) and there is not such problem. It cannot be automatic proved though.

			Cheers,

			Son

imported>Tianhaiyun: The problem encountered when using Rodin.

2009-10-27T12:21:43Z

The problem encountered when using Rodin.

New page

'''Rodin Platform Version: 0.9.1'''

'''Sequent Prover Auto-tactic : all'''

The problems is as follows.
I build one project, in which there is only one context. In this contest, there is only one theorem defined as {x·x∈0‥4∣x↦0}∈0‥4⇸0‥4. The obligation for it is generated by Rodin. However, it reports that the obligation can cannot be passed. It makes me quite confused. Please everyone knowing what the problem is and help me out.

Thank you so lot

HaiYun tian
SCM Teesside University