Proof Hints - Revision history

imported>Son: /* Proof Hints */

2010-03-05T22:17:20Z

Proof Hints

← Older revision		Revision as of 22:17, 5 March 2010
Line 3:		Line 3:
	This document does NOT provide a way to avoid doing interactive proofs or pointing out the weakness of existing provers. Rather this document shows how to use information from doing interactive proofs to improve the clarity of models. As a consequence of these improvement, more obligations can be discharged automatically. Below are our proposal for two kinds of improvements: [[#Hypothesis Selection \| hypothesis selection]] and [[#Case Distinction\|case distinction]].		This document does NOT provide a way to avoid doing interactive proofs or pointing out the weakness of existing provers. Rather this document shows how to use information from doing interactive proofs to improve the clarity of models. As a consequence of these improvement, more obligations can be discharged automatically. Below are our proposal for two kinds of improvements: [[#Hypothesis Selection \| hypothesis selection]] and [[#Case Distinction\|case distinction]].

	== ~~Proof Hints~~ ==		== Improvements ==

	The presentation for each kind of ~~proof hints~~ is as follows:		The presentation for each kind of improvement is as follows:

	1. '''Description''': A brief description of the proof hints with the situation where this can be helpful.		1. '''Description''': A brief description of the proof hints with the situation where this can be helpful.

imported>Son: /* Introduction */

2010-03-05T22:16:46Z

Introduction

← Older revision		Revision as of 22:16, 5 March 2010
Line 1:		Line 1:
	== Introduction ==		== Introduction ==

	This document does NOT provide a way to avoid doing interactive proofs or pointing out the weakness of existing provers. Rather this document shows how to use information from doing interactive proofs to improve the clarity of models. As a consequence of these improvement, more obligations can be discharged automatically~~. We call these added information to the model "proof hints".~~		This document does NOT provide a way to avoid doing interactive proofs or pointing out the weakness of existing provers. Rather this document shows how to use information from doing interactive proofs to improve the clarity of models. As a consequence of these improvement, more obligations can be discharged automatically. Below are our proposal for two kinds of improvements: [[#Hypothesis Selection \| hypothesis selection]] and [[#Case Distinction\|case distinction]].

	This concept of "proof hints" already exists in the form of "witness" or "theorem" in Event-B. These useful features are designed not only to help with proving the correctness of the model but also to give more information about the particular model.

	The question is how we can decide which "features" are useful to have in the model. In principle we can go to the extreme and include the whole proof strategy into the model in order to be able to have it being discharged automatically. But this is undesirable since it will make the model difficult to understand. Having taken this into account we specify our criteria here for "proof hints".

	~~1. It should help to understand the model better.~~

	~~2. It should improve the automatic proving rate of the model.~~

	~~In fact, we regard the first criterion as more important whereas the second criterion can be considered as a bonus for improving the clarity of the model~~. Below are our proposal for two kinds of ~~proof hints~~: [[#Hypothesis Selection \| hypothesis selection]] and [[#Case Distinction\|case distinction]].

	== Proof Hints ==		== Proof Hints ==

imported>Son at 22:15, 5 March 2010

2010-03-05T22:15:57Z

← Older revision		Revision as of 22:15, 5 March 2010
Line 11:		Line 11:
	2. It should improve the automatic proving rate of the model.		2. It should improve the automatic proving rate of the model.

	In fact, we regard the first criterion as more important whereas the second criterion can be considered as a bonus for improving the clarity of the model. Below are our proposal for two kinds of proof hints: [[#Hypothesis Selection \| hypothesis selection]] and ~~proof by cases~~.		In fact, we regard the first criterion as more important whereas the second criterion can be considered as a bonus for improving the clarity of the model. Below are our proposal for two kinds of proof hints: [[#Hypothesis Selection \| hypothesis selection]] and [[#Case Distinction\|case distinction]].

	== Proof Hints ==		== Proof Hints ==

imported>Son at 22:14, 5 March 2010

2010-03-05T22:14:53Z

← Older revision		Revision as of 22:14, 5 March 2010
Line 11:		Line 11:
	2. It should improve the automatic proving rate of the model.		2. It should improve the automatic proving rate of the model.

	In fact, we regard the first criterion as more important whereas the second criterion can be considered as a bonus for improving the clarity of the model. Below are our proposal for two kinds of proof hints: [[Hypothesis Selection \| hypothesis selection]] and proof by cases.		In fact, we regard the first criterion as more important whereas the second criterion can be considered as a bonus for improving the clarity of the model. Below are our proposal for two kinds of proof hints: [[#Hypothesis Selection \| hypothesis selection]] and proof by cases.

	== Proof Hints ==		== Proof Hints ==

imported>Son: /* Introduction */

2010-03-05T22:14:34Z

Introduction

← Older revision		Revision as of 22:14, 5 March 2010
Line 1:		Line 1:
	== Introduction ==		== Introduction ==

	This document does NOT provide a way to avoid doing interactive proofs or pointing out the weakness of existing provers. Rather this document shows how to use information from doing interactive proofs to improve the clarity of models. As a consequence of these improvement, ~~the~~ obligations can be discharged automatically. We call these added information to the model "proof hints".		This document does NOT provide a way to avoid doing interactive proofs or pointing out the weakness of existing provers. Rather this document shows how to use information from doing interactive proofs to improve the clarity of models. As a consequence of these improvement, more obligations can be discharged automatically. We call these added information to the model "proof hints".

	This concept of "proof hints" already exists in the form of "witness" or "theorem" in Event-B. These useful features are designed not only to help with proving the correctness of the model but also to give more information about the particular model.		This concept of "proof hints" already exists in the form of "witness" or "theorem" in Event-B. These useful features are designed not only to help with proving the correctness of the model but also to give more information about the particular model.

imported>Son: /* Case distinction */

2010-03-05T16:57:23Z

Case distinction

← Older revision		Revision as of 16:57, 5 March 2010
Line 65:		Line 65:

	[[Image:new-set-evts.png]]		[[Image:new-set-evts.png]]

			In the next refinement step, we can merge the above two new event to the original event as follows.

			[[Image:merged-set.png]]

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

imported>Son: /* Case distinction */

2010-03-05T16:54:01Z

Case distinction

← Older revision		Revision as of 16:54, 5 March 2010
Line 50:		Line 50:

	=== Case distinction ===		=== Case distinction ===
	'''Description''' In order to discharge a proof obligation, the developer makes a manual "proof by ~~case~~" based on some condition <math>P</math>. Afterwards, all branches of the proofs are discharged either by ML or AtelierB P0. The solution is to (somehow) give "hints" to the POG to generate different proof obligations for each case separately. ''~~proof~~ by ~~case~~'' is usually not applied automatically since this splits the proof tree which could lead to blows up in terms of the number of cases.		'''Description''' In order to discharge a proof obligation, the developer makes a manual "proof by cases" based on some condition <math>P</math>. Afterwards, all branches of the proofs are discharged either by ML or AtelierB P0. The solution is to (somehow) give "hints" to the POG to generate different proof obligations for each case separately. ''Proof by cases'' is usually not applied automatically since this splits the proof tree which could lead to blows up in terms of the number of cases.

	'''Example''' Consider the following Event-B model		'''Example''' Consider the following Event-B model
Line 60:		Line 60:
	[[Image:set-case0_1-INV.png]]		[[Image:set-case0_1-INV.png]]

	'''Workaround''' ~~TODO~~		In order to finish the proof, a correct "proof by cases" is done to consider <math>a = 1</math> or <math>a \neq 1</math>.

			'''Workaround''' To capture the effect of doing '''proof by cases''', we split the original event '''set''' into two different events as follows

			[[Image:new-set-evts.png]]

	~~'''Proposal''' TODO~~
	[[Category:Proof]]		[[Category:Proof]]
	[[Category:Work in progress]]		[[Category:Work in progress]]

imported>Son: /* Case distinction */

2010-03-05T16:46:18Z

Case distinction

← Older revision		Revision as of 16:46, 5 March 2010
Line 53:		Line 53:

	'''Example''' Consider the following Event-B model		'''Example''' Consider the following Event-B model

	[[Image:casesplit.png]]		[[Image:casesplit.png]]

			Consider the proof obligation '''set/case0_1/INV''' (Here all hypotheses, including those hidden are shown)

			[[Image:set-case0_1-INV.png]]

	'''Workaround''' TODO		'''Workaround''' TODO

imported>Son: /* Case distinction */

2010-03-05T16:40:42Z

Case distinction

← Older revision		Revision as of 16:40, 5 March 2010
Line 52:		Line 52:
	'''Description''' In order to discharge a proof obligation, the developer makes a manual "proof by case" based on some condition <math>P</math>. Afterwards, all branches of the proofs are discharged either by ML or AtelierB P0. The solution is to (somehow) give "hints" to the POG to generate different proof obligations for each case separately. ''proof by case'' is usually not applied automatically since this splits the proof tree which could lead to blows up in terms of the number of cases.		'''Description''' In order to discharge a proof obligation, the developer makes a manual "proof by case" based on some condition <math>P</math>. Afterwards, all branches of the proofs are discharged either by ML or AtelierB P0. The solution is to (somehow) give "hints" to the POG to generate different proof obligations for each case separately. ''proof by case'' is usually not applied automatically since this splits the proof tree which could lead to blows up in terms of the number of cases.

	'''Example''' ~~TODO~~		'''Example''' Consider the following Event-B model
			[[Image:casesplit.png]]

	'''Workaround''' TODO		'''Workaround''' TODO

imported>Son: /* Case distinction */

2010-03-05T16:35:40Z

Case distinction

← Older revision		Revision as of 16:35, 5 March 2010
Line 50:		Line 50:

	=== Case distinction ===		=== Case distinction ===
	'''Description''' ~~This section discuss about~~ a proof ~~hint related to~~ the ~~case where a~~ developer ~~has to do~~ a manual "proof by case"~~, after that~~, all branches of the proofs are discharged either by ML or AtelierB P0. The solution is to (somehow) give "hints" to the POG to generate different proof obligations for each case separately. ~~Proving~~ by ~~cases are~~ usually not ~~done~~ automatically since this splits the proof tree which could lead to blows up in terms of the number of cases.		'''Description''' In order to discharge a proof obligation, the developer makes a manual "proof by case" based on some condition <math>P</math>. Afterwards, all branches of the proofs are discharged either by ML or AtelierB P0. The solution is to (somehow) give "hints" to the POG to generate different proof obligations for each case separately. ''proof by case'' is usually not applied automatically since this splits the proof tree which could lead to blows up in terms of the number of cases.

	'''Example''' TODO		'''Example''' TODO