Variations in HYP, CNTR and GenMP - Revision history

imported>Josselin: Fix results

2014-07-08T07:08:29Z

Fix results

← Older revision		Revision as of 07:08, 8 July 2014
Line 464:		Line 464:
	\|-		\|-
	\| '''Total'''		\| '''Total'''
	\| '''~~7683~~'''		\| '''8161'''
	\| '''~~3564~~'''		\| '''3786'''
	\| '''~~3914~~'''		\| '''4518'''
	\|}		\|}

Line 484:		Line 484:

	== Conclusion ==		== Conclusion ==
	We measured that we had an overall 9,8 % increase in number of POs discharged compared to the previous version.		We measured that we had an overall 19,3 % increase in number of POs discharged compared to the previous version.
	A less time of few minutes has been observed for discharge the POs. Only one time measurement has been taken into account because the others are too short. Moreover, this result is not really significiant because even if the new version discharges more sequent than the previous, it decharges earlier than the previous version.		A less time of few minutes has been observed for discharge the POs. Only one time measurement has been taken into account because the others are too short. Moreover, this result is not really significiant because even if the new version discharges more sequent than the previous, it decharges earlier than the previous version.

imported>Josselin at 13:14, 22 November 2013

2013-11-22T13:14:41Z

@@ Line 28: / Line 28: @@
 These functions have been defined as follows:
-* StongerPositive(P) = <math>\{Q \mid Q \limp P\} \;\; (\lnot P \limp \lnot Q)</math>
+{| style="border: width:80%;"
-* WeakerPositive(P) = <math>\{Q \mid P \limp Q\} \;\; (\lnot Q \limp \lnot P )</math>
+|+
-* StongerNegative(P) = <math>\{Q \mid Q \limp \lnot P\}  \;\; (P \limp \lnot Q)</math>
+|-
-* WeakerNegative(P) = <math>\{Q \mid \lnot P \limp Q\} \;\; (\lnot Q \limp P )</math>
+! scope=col |
 A rule can be written in 2 implications, one for each sign of the predicate P.

imported>Josselin at 11:10, 22 November 2013

2013-11-22T11:10:34Z

← Older revision		Revision as of 11:10, 22 November 2013
Line 21:		Line 21:
	= Implementation =		= Implementation =

	This section explains how the variation ~~have~~ been implemented.		This section explains how the generation of variation of the sought predicate has been implemented.

	== Variation Implementation ==		== Variation Implementation ==
Line 466:		Line 466:
	== Conclusion ==		== Conclusion ==
	We measured that we had an overall 9,8 % increase in number of POs discharged compared to the previous version.		We measured that we had an overall 9,8 % increase in number of POs discharged compared to the previous version.
	A less time of few minutes has been observed for discharge the POs. Only one time measurement ~~have~~ been taken into account because the others are too short. Moreover, this result is not really significiant because even if the new version discharges more sequent than the previous, it decharges earlier than the previous version.		A less time of few minutes has been observed for discharge the POs. Only one time measurement has been taken into account because the others are too short. Moreover, this result is not really significiant because even if the new version discharges more sequent than the previous, it decharges earlier than the previous version.

imported>Josselin at 16:26, 21 November 2013

2013-11-21T16:26:21Z

imported>Josselin: fix misleading descriptions

2013-11-21T14:30:43Z

fix misleading descriptions

imported>Laurent: /* Results */

2013-11-21T11:18:42Z

Results

← Older revision		Revision as of 11:18, 21 November 2013
Line 130:		Line 130:
	* New version : commit 2ea1cf6ffe		* New version : commit 2ea1cf6ffe
	== Results ==		== Results ==
	The following results are ~~means~~ of measures on the Auto-prover		The following results are averages of measures on the Auto-prover

	{\| class="wikitable" style="text-align:center; width:80%;"		{\| class="wikitable" style="text-align:center; width:80%;"
Line 466:		Line 466:
	\| 1811,398 s (~30 min)		\| 1811,398 s (~30 min)
	\|}		\|}

	== Conclusion ==		== Conclusion ==
	We measured that we had an overall 9,8 % increase in number of POs discharged compared to the previous version.		We measured that we had an overall 9,8 % increase in number of POs discharged compared to the previous version.
	A extra time of more than few minutes has been observed for discharge the POs. This result should be interpret with caution, probably some provers discharged the sequent simplified by the new version of the GenMP reasoner.		A extra time of more than few minutes has been observed for discharge the POs. This result should be interpret with caution, probably some provers discharged the sequent simplified by the new version of the GenMP reasoner.

imported>Laurent: /* Benchmark Projects */

2013-11-21T11:17:46Z

Benchmark Projects

← Older revision		Revision as of 11:17, 21 November 2013
Line 103:		Line 103:
	== Benchmark Projects ==		== Benchmark Projects ==

	The Rodin projects ~~are available at~~ [http://deploy-eprints.ecs.soton.ac.uk/cgi/search/archive/advanced?exp=0\|1\|-date%2Fcreators_name%2Ftitle\|archive\|-\|documents.format%3Adocuments.format%3AANY%3AEQ%3Aapplication%2Fzip\|-\|eprint_status%3Aeprint_status%3AANY%3AEQ%3Aarchive\|metadata_visibility%3Ametadata_visibility%3AANY%3AEQ%3Ashow&_action_search=1&order=-date%2Fcreators_name%2Ftitle&screen=Search&cache=321270&search_offset=0].		The Rodin projects have been taken from the [http://deploy-eprints.ecs.soton.ac.uk/cgi/search/archive/advanced?exp=0\|1\|-date%2Fcreators_name%2Ftitle\|archive\|-\|documents.format%3Adocuments.format%3AANY%3AEQ%3Aapplication%2Fzip\|-\|eprint_status%3Aeprint_status%3AANY%3AEQ%3Aarchive\|metadata_visibility%3Ametadata_visibility%3AANY%3AEQ%3Ashow&_action_search=1&order=-date%2Fcreators_name%2Ftitle&screen=Search&cache=321270&search_offset=0 Deploy archives].

	== Protocol ==		== Protocol ==

imported>Laurent: /* Implementation */

2013-11-21T11:05:50Z

Implementation

← Older revision		Revision as of 11:05, 21 November 2013
Line 21:		Line 21:
	= Implementation =		= Implementation =

	This section explains how the variation ~~has~~ been implemented.		This section explains how the variation have been implemented.

	== Variation Implementation ==		== Variation Implementation ==
Line 78:		Line 78:

	'''Note''': This improvement corresponds to the level 2 of GenMP.		'''Note''': This improvement corresponds to the level 2 of GenMP.

	= Performances =		= Performances =

imported>Laurent at 11:04, 21 November 2013

2013-11-21T11:04:10Z

← Older revision		Revision as of 11:04, 21 November 2013
Line 1:		Line 1:
			{{TOCright}}

	This page describes the introduction of variations in the HYP, HYP_OR, CNTR and GENMP reasoners.		This page describes the introduction of variations in the HYP, HYP_OR, CNTR and GENMP reasoners.

imported>Josselin: Describe the implementation and present the results

2013-11-19T17:05:59Z

Describe the implementation and present the results

Show changes

← Older revision		Revision as of 16:26, 21 November 2013
Line 43:		Line 43:
	== Reasoners Implementation ==		== Reasoners Implementation ==
	=== HYP, HYP_OR ===		=== HYP, HYP_OR ===
	The HYP reasoner calls to StongerPositive function in order to ~~generates~~ a list of predicates that infer the goal ~~(or disjunct)~~. Thus, the sequent is discharged ~~iff~~ at least one hypothesis is contained into this list.		The HYP reasoner calls to StongerPositive function in order to generate a list of predicates that infer the goal. Thus, the sequent is discharged if and only if at least one hypothesis is contained into this list.

	The HYP_OR reasoner proceeds the same, for each disjunct a list of stronger predicates is generated and then the sequent is dicharged if at least one hypothesis is contained into these lists.		The HYP_OR reasoner proceeds the same, for each disjunct a list of stronger predicates is generated and then the sequent is dicharged if at least one hypothesis is contained into these lists.
Line 50:		Line 50:
	Checks if the predicate, that we would contradict, is not null and it is contained into the hypotheses.		Checks if the predicate, that we would contradict, is not null and it is contained into the hypotheses.

	If the given ~~predicate is a positive predicate~~, ~~it generates~~ a list of predicates ~~which infer~~ the predicate. Else, it splits a conjunctive hypothesis ~~if necessary~~ into its conjuncts and ~~compute~~ for each conjunct a list of predicates ~~wich infer~~ the negation of the predicate (or conjunct). Finally, ~~it saves into~~ the ~~list named neededHyps the hypotheses~~ contained into the ~~lists previously computed (~~hypotheses ~~which contradict~~ the ~~given hypothesis)~~.		To generate the predicates contradicting the given hypothesis, a list of predicates inferring the predicate is generated if the given hypothesis is a positive predicate. Else, the reasoner splits a possible conjunctive hypothesis, into its conjuncts and computes for each conjunct a list of predicates inferring the negation of the predicate (or conjunct). Finally, the sequent is dicharged if at least one predicate computed is contained into the hypotheses. If so, all hypotheses needed to achieve it are stored in the list named neededHyps.

	=== GEN_MP ===		=== GEN_MP ===
	~~First, it extracts all predicates~~ (unless predicates <math> \btrue ~~and~~ \bfalse</math>) from the hypotheses~~. For each hypothesis its~~ computes:		For each predicate extracted (unless predicates <math> \btrue / \bfalse </math>) from the hypotheses the reasoner computes:
	* a list of predicates which could be remplaced by <math> \btrue </math> and which are weaker than the hypothesis.		* a list of predicates which could be remplaced by <math> \btrue </math> and which are weaker than the hypothesis.
	* a list of predicates which could be remplaced by <math> \bfalse </math> and which are stronger than the negation of the hypothesis.		* a list of predicates which could be remplaced by <math> \bfalse </math> and which are stronger than the negation of the hypothesis.

	Then, it extracts the goal or the disjuncts if the sequent contain a goal in a disjunctive form. For each predicate its computes:		Then, it extracts the goal or the disjuncts if the sequent contain a goal in a disjunctive form. For each predicate extracted its computes:
	* a list of predicates which could be remplaced by <math> \bfalse </math> and which are stronger than the hypothesis.		* a list of predicates which could be remplaced by <math> \bfalse </math> and which are stronger than the hypothesis.
	* a list of predicates which could be remplaced by <math> \btrue </math> and which are weaker than the negation of the hypothesis.		* a list of predicates which could be remplaced by <math> \btrue </math> and which are weaker than the negation of the hypothesis.


	For each substitution computed the following informations are stored:		For each possible substitution computed the following informations are stored:
	* predicate original (hypothesis or goal)		* predicate original (hypothesis or goal)
	* a boolean tells if the substitution comes from the goal		* a boolean tells if the substitution comes from the goal
Line 68:		Line 68:
	* the substitue <math> ( \btrue / \bfalse ) </math>		* the substitue <math> ( \btrue / \bfalse ) </math>

	In order to simplify predicate ~~searching~~ algorithm ~~(avoid sign distinction)~~, the sub-predicate should be positive.		Note: In order to simplify and avoid to make a distinction about the predicate sign in the reasoner algorithm, the sub-predicate should be positive.

	Afterwards, ~~each predicate extracted from~~ hypotheses or the goal is traversed to get the list of possible applications of substitutes ~~while ensuring~~ that a given predicate ~~could~~'nt be ~~rewritten~~ by himself.		Afterwards, the hypotheses and the goal are traversed in order to get the list of possible applications of substitutes. Indeed, for each predicate traversed, we retrieve the corresponding substitute previously computed and we ensure that the given predicate won't be rewrite by himself. We store the substitute and the position in the predicate which corresponding to an application of substitutes into the list.
	~~A possible applications~~ of substitutes ~~corresponds to a position~~ into the ~~predicate to rewrite and a sustitute~~.

	Finally, the goal is re-written ~~using the applications of substitutes computed. Thus~~, the re-written goal and the hypotheses needed to achieve it are stored. ~~Then~~ the hypotheses are re-written ~~by producing~~ new hypothesis actions.		Finally, all applications of substitutes are applied into the sequent, first on the goal and then on the hypotheses. Thus, if the goal is re-written, the re-written goal and the hypotheses needed to achieve it are stored. If the hypotheses are re-written we produce new hypothesis actions.

	'''Note''': This improvement corresponds to the level 2 of GenMP.		'''Note''': This improvement corresponds to the level 2 of GenMP.

← Older revision		Revision as of 14:30, 21 November 2013
Line 24:		Line 24:

	== Variation Implementation ==		== Variation Implementation ==
	In order to simplify and optimize the generation of variation of the sought predicate, 4 functions (common to HYP, HYP_OR, CNTR and GenMP reasoners) have been implemented.		In order to simplify and optimize the generation of variation of the sought predicate, 4 functions (common to HYP, HYP_OR, CNTR and GenMP reasoners) have been implemented. Each function takes as input a predicate and returns a list of predicates generated by applying their corresponding rule.

	These functions have been defined as follows:		These functions have been defined as follows:

	* StongerPositive(P) = <math>\{Q, Q \limp P\} \;\; (\lnot P \limp \lnot Q)</math>		* StongerPositive(P) = <math>\{Q \mid Q \limp P\} \;\; (\lnot P \limp \lnot Q)</math>
	* WeakerPositive(P) = <math>\{Q, P \limp Q\} \;\; (\lnot Q \limp \lnot P )</math>		* WeakerPositive(P) = <math>\{Q \mid P \limp Q\} \;\; (\lnot Q \limp \lnot P )</math>
	* StongerNegative(P) = <math>\{Q, Q \limp \lnot P\} \;\; (P \limp \lnot Q)</math>		* StongerNegative(P) = <math>\{Q \mid Q \limp \lnot P\} \;\; (P \limp \lnot Q)</math>
	* WeakerNegative(P) = <math>\{Q, \lnot P \limp Q\} \;\; (\lnot Q \limp P )</math>		* WeakerNegative(P) = <math>\{Q \mid \lnot P \limp Q\} \;\; (\lnot Q \limp P )</math>

	~~The above functions can be read as follows: The function returns the set of predicates Q from the predicate P by applying the corresponding rule. Each~~ rule can be written in 2 ~~implication~~, one for each sign of the predicate P.		A rule can be written in 2 implications, one for each sign of the predicate P.


	Some optimisations, to reduce the number of implication to implement, have been implemented. Indeed, only the implications <math>(Q \limp P, P \limp Q, P \limp \lnot Q, \lnot Q \limp P)</math> have been implemented because they cover all cases. For instance, if the function StongerPositive takes a negative predicate as an input, the function returns a list of predicates stronger (e.g which infer) than the input. But it's also performed by the function StongerNegative. So this function applies the predicate negation and call to StongerNegative function.

			Some optimisations, to reduce the number of implication to implement, have been implemented. Indeed, only the implications <math>(Q \limp P, P \limp Q, P \limp \lnot Q, \lnot Q \limp P)</math> have been implemented because they cover all cases. For instance, if the function StongerPositive takes a negative predicate as an input, the function returns a list of predicates stronger (e.g which infer) than the input. But it's also performed by the function StongerNegative. So this function applies the predicate negation and call to StongerNegative function.

	Note:		Note:
	These functions assume the operators such as '<math>\neq</math>' have been removed by the normalization. Moreover, as explained in the convention part, the list of predicates returned contains only ~~predicate~~ in a normal form.		These functions assume the operators such as '<math>\neq</math>' have been removed by the normalization. Moreover, as explained in the convention part, the list of predicates returned contains only predicates in a normal form.


	== Reasoners Implementation ==		== Reasoners Implementation ==
	=== HYP, HYP_OR ===		=== HYP, HYP_OR ===
	The HYP reasoner generates a list of ~~predicate wich are stronger than~~ the goal (or disjunct). Thus, the sequent is discharged iff at least one hypothesis is contained into this list.		The HYP reasoner calls to StongerPositive function in order to generates a list of predicates that infer the goal (or disjunct). Thus, the sequent is discharged iff at least one hypothesis is contained into this list.

	The HYP_OR reasoner ~~proceed~~ the same, for each disjunct a list of stronger ~~predicate~~ is generated if at least one hypothesis is contained into these lists ~~the sequent is dicharged~~.		The HYP_OR reasoner proceeds the same, for each disjunct a list of stronger predicates is generated and then the sequent is dicharged if at least one hypothesis is contained into these lists.

	=== CNTR ===		=== CNTR ===
	Checks if the predicate to contradict is not null and it is contained into the hypotheses.		Checks if the predicate, that we would contradict, is not null and it is contained into the hypotheses.

	If the ~~hypothesis to contradict~~ is a positive predicate, it generates a list of predicates ~~wich inferr~~ the predicate. Else, it splits a conjunctive hypothesis if necessary into its conjuncts and compute for each ~~conjuncts~~ a list of ~~predicate~~ wich ~~inferr~~ the negation of the predicate (or conjunct). Finally, it saves into the list named neededHyps the hypotheses contained into the lists previously computed (hypotheses which contradict the given hypothesis).		If the given predicate is a positive predicate, it generates a list of predicates which infer the predicate. Else, it splits a conjunctive hypothesis if necessary into its conjuncts and compute for each conjunct a list of predicates wich infer the negation of the predicate (or conjunct). Finally, it saves into the list named neededHyps the hypotheses contained into the lists previously computed (hypotheses which contradict the given hypothesis).

	=== GEN_MP ===		=== GEN_MP ===
	First, it extracts all predicates (unless predicates <math> \btrue and \bfalse</math>) from the hypotheses. For each hypothesis its computes:		First, it extracts all predicates (unless predicates <math> \btrue and \bfalse</math>) from the hypotheses. For each hypothesis its computes:
	* a list of ~~predicate~~ which could be ~~remplace~~ by <math> \btrue </math> and which are weaker than the hypothesis.		* a list of predicates which could be remplaced by <math> \btrue </math> and which are weaker than the hypothesis.
	* a list of ~~predicate~~ which could be ~~remplace~~ by <math> \bfalse </math> and which are stronger than the negation of the hypothesis.		* a list of predicates which could be remplaced by <math> \bfalse </math> and which are stronger than the negation of the hypothesis.

	Then, it extracts the goal or the disjuncts if the sequent contain a goal in a disjunctive form. For each predicate its computes:		Then, it extracts the goal or the disjuncts if the sequent contain a goal in a disjunctive form. For each predicate its computes:
	* a list of ~~predicate~~ which could be ~~remplace~~ by <math> \bfalse </math> and which are stronger than the hypothesis.		* a list of predicates which could be remplaced by <math> \bfalse </math> and which are stronger than the hypothesis.
	* a list of ~~predicate~~ which could be ~~remplace~~ by <math> \btrue </math> and which are weaker than the negation of the hypothesis.		* a list of predicates which could be remplaced by <math> \btrue </math> and which are weaker than the negation of the hypothesis.


Line 70:		Line 68:
	* the substitue <math> ( \btrue / \bfalse ) </math>		* the substitue <math> ( \btrue / \bfalse ) </math>

	In order to simplify predicate ~~search~~ algorithm (avoid sign distinction), the sub-predicate should be ~~postive~~.		In order to simplify predicate searching algorithm (avoid sign distinction), the sub-predicate should be positive.

	Afterwards, each predicate extracted from hypotheses or the goal is traversed to get the list of possible applications of substitutes while ensuring that a given predicate could'nt be rewritten by himself.		Afterwards, each predicate extracted from hypotheses or the goal is traversed to get the list of possible applications of substitutes while ensuring that a given predicate could'nt be rewritten by himself.
	A possible applications of substitutes corresponds to a position into the predicate to rewrite and a sustitute.		A possible applications of substitutes corresponds to a position into the predicate to rewrite and a sustitute.

	Finally, the goal is re-written using the applications of substitutes computed ~~and Then~~, the re-written goal and the hypotheses needed to achieve it are stored. Then the ~~hypothese~~ are re-written by producing new hypothesis actions.		Finally, the goal is re-written using the applications of substitutes computed. Thus, the re-written goal and the hypotheses needed to achieve it are stored. Then the hypotheses are re-written by producing new hypothesis actions.

	'''Note''': This improvement corresponds to the level 2 of GenMP.		'''Note''': This improvement corresponds to the level 2 of GenMP.
Line 124:		Line 122:


	First, it checks that the program argument is a directory and then it imports all Rodin projects from the directory into a workspace. The Auto-prover is applied on all Rodin ~~Projects~~. For each Rodin project the following informations are displayed : "Project: Number of POs discharged/Number of POs". Finally, the proof files are strored into a directory named "Results" at the same level as the directory ~~which contain~~ the Rodin ~~Project~~.		First, it checks that the program argument is a directory and then it imports all Rodin projects from the directory into a workspace. The Auto-prover is applied on all Rodin projects. For each Rodin project the following informations are displayed : "Project: Number of POs discharged/Number of POs". Finally, the proof files are strored into a directory named "Results" at the same level as the directory where is contained the Rodin projects.

	== Tests ==		== Tests ==
Line 469:		Line 467:
	== Conclusion ==		== Conclusion ==
	We measured that we had an overall 9,8 % increase in number of POs discharged compared to the previous version.		We measured that we had an overall 9,8 % increase in number of POs discharged compared to the previous version.
	A ~~extra~~ time of ~~more than~~ few minutes has been observed for discharge the POs. ~~This~~ result ~~should be interpret with caution, probably some provers discharged~~ the sequent ~~simplified by~~ the ~~new~~ version ~~of the GenMP reasoner~~.		A less time of few minutes has been observed for discharge the POs. Only one time measurement have been taken into account because the others are too short. Moreover, this result is not really significiant because even if the new version discharges more sequent than the previous, it decharges earlier than the previous version.