Membership in Goal - Revision history

imported>Nicolas: /* Find a path */

2014-06-05T13:50:38Z

Find a path

← Older revision		Revision as of 13:50, 5 June 2014
Line 154:		Line 154:
	Now, the reasoner has to build the path, for each hypothesis into the list, a new rationale is built and saved into an array at the index of the list. If the hypothesis denotes a membership, the rationale is directly saved into the array. Else the reasoner retrieves from the array all rationales on which it depends and then from these rationales it builds a new rationale and saves it into the array.		Now, the reasoner has to build the path, for each hypothesis into the list, a new rationale is built and saved into an array at the index of the list. If the hypothesis denotes a membership, the rationale is directly saved into the array. Else the reasoner retrieves from the array all rationales on which it depends and then from these rationales it builds a new rationale and saves it into the array.

	However, the path building is ~~unidirectionnal~~, it works with a sat problem with clauses containing whith at most one positive literal. Indeed, the current version can't find a path with hypotheses in the following form :		However, the path building is unidirectional, it works with a sat problem with clauses containing whith at most one positive literal. Indeed, the current version can't find a path with hypotheses in the following form :
	* <math> x \in ... \binter / \bunion ... </math>		* <math> x \in ... \binter / \bunion ... </math>
	* <math> ... \subseteq ... \binter / \bunion ... </math>		* <math> ... \subseteq ... \binter / \bunion ... </math>

imported>Nicolas: /* Find a path */

2014-06-05T13:47:59Z

Find a path

← Older revision		Revision as of 13:47, 5 June 2014
Line 116:		Line 116:
	For instance, from the hypothesis "<math> f \ovl \{ x \mapsto y \} \in A \rel B </math>" the reasoner derives the predicates <math>x \in A</math> and <math>x \in dom(A \cprod B)</math>.		For instance, from the hypothesis "<math> f \ovl \{ x \mapsto y \} \in A \rel B </math>" the reasoner derives the predicates <math>x \in A</math> and <math>x \in dom(A \cprod B)</math>.

	Afterwards, the reasoner has to encode the new predicates in SAT clauses. For this purpose, it converts all new hypotheses in SAT proposition by extracting all set contained into the predicate. And then, ~~its~~ encodes the proposition SAT in Dimacs CNF format. Finally, the clauses encoded are inserted one by one into the SAT problem until the solver reports the problem as unsatisfiable in order to obtain a minimal solution to the SAT core.		Afterwards, the reasoner has to encode the new predicates in SAT clauses. For this purpose, it converts all new hypotheses in SAT proposition by extracting all set contained into the predicate. And then, it encodes the proposition SAT in Dimacs CNF format. Finally, the clauses encoded are inserted one by one into the SAT problem until the solver reports the problem as unsatisfiable in order to obtain a minimal solution to the SAT core.

	{\| class="wikitable" style="text-align:center; width:80%;"		{\| class="wikitable" style="text-align:center; width:80%;"

imported>Josselin: add inference rules

2013-11-22T12:45:39Z

add inference rules

Show changes

imported>Josselin at 17:07, 21 November 2013

2013-11-21T17:07:27Z

← Older revision		Revision as of 17:07, 21 November 2013
Line 112:		Line 112:
	From the hypothesis "<math> f \ovl \{ x \mapsto y \} \in A \rel B </math>" the reasoner derives the predicates <math>x \in A</math> and <math>x \in dom(A \cprod B)</math>.		From the hypothesis "<math> f \ovl \{ x \mapsto y \} \in A \rel B </math>" the reasoner derives the predicates <math>x \in A</math> and <math>x \in dom(A \cprod B)</math>.

	The ~~reasoner encodes the~~ new ~~hypotheses derived~~ from the hypotheses and the negation of the goal, to SAT clauses. For this purpose, it encodes all new hypotheses in SAT proposition by extracting all set contained into the predicate.		The new predicates deducted from the hypotheses and the negation of the goal have to been encoded in SAT clauses. For this purpose, it encodes all new hypotheses in SAT proposition by extracting all set contained into the predicate. And then, its encodes the proposition SAT in Dimacs CNF format. The clauses encoded are inserted one by one into the SAT problem until the solver reports the problem as unsatisfiable in order to obtain a minimal solution to the SAT core.
	And then, its encodes the proposition SAT in Dimacs CNF format. The clauses encoded are inserted one by one into the SAT problem until the solver reports the problem as unsatisfiable in order to obtain a minimal solution to the SAT core.

	{\| class="wikitable" style="text-align:center; width:80%;"		{\| class="wikitable" style="text-align:center; width:80%;"
Line 149:		Line 148:
	Afterwards, the clauses in the sat core sorted by their insertion order, are then reordered by using topological sorting. The reasonner traces each clause back to the corresponding hypotheses.		Afterwards, the clauses in the sat core sorted by their insertion order, are then reordered by using topological sorting. The reasonner traces each clause back to the corresponding hypotheses.

	For each hypothesis into the list, a rationale is built and saved into an array at the index of the list. If the hypothesis denotes a membership, the rationale is directly saved into the array. Else it retrevies the array all rationales wich allow to prove that the member is in each set contained into the intersection and then from these rationales it builds a new ~~Rationale~~ and saves it into the array. However, the path building is unidirectionnal, it works with a sat core wich contains ~~only clause~~ contains with at most one positive literals.		For each hypothesis into the list, a rationale is built and saved into an array at the index of the list. If the hypothesis denotes a membership, the rationale is directly saved into the array. Else it retrevies the array all rationales wich allow to prove that the member is in each set contained into the intersection and then from these rationales it builds a new rationale and saves it into the array. However, the path building is unidirectionnal, it works with a sat core wich only contains clauses that contains with at most one positive literals.

	Indeed, the current version finds a path with hypotheses in the following form :		Indeed, the current version finds a path with hypotheses in the following form :

imported>Laurent: /* Find a path */

2013-11-21T11:30:41Z

Find a path

← Older revision		Revision as of 11:30, 21 November 2013
Line 110:		Line 110:


	From the hypothesis "<math> f \ovl \{ x \mapsto y \} \in A \rel B </math>" the reasoner ~~deduct~~ the ~~following~~ predicates: <math> \{ x \in A ~~, \quad~~ x \in dom(A \cprod B) \} </math>		From the hypothesis "<math> f \ovl \{ x \mapsto y \} \in A \rel B </math>" the reasoner derives the predicates <math>x \in A</math> and <math>x \in dom(A \cprod B)</math>.

	The reasoner encodes the new hypotheses derived from the hypotheses and the negation of the goal, to SAT clauses. For this purpose, it encodes all new hypotheses in SAT proposition by extracting all set contained into the predicate.		The reasoner encodes the new hypotheses derived from the hypotheses and the negation of the goal, to SAT clauses. For this purpose, it encodes all new hypotheses in SAT proposition by extracting all set contained into the predicate.
Line 162:		Line 162:
	:<math>x\in dom(f\bunion g)\binter A,~A\subseteq B,~dom(f)\bunion dom(g)\subseteq B~\vdash~x\in B</math>		:<math>x\in dom(f\bunion g)\binter A,~A\subseteq B,~dom(f)\bunion dom(g)\subseteq B~\vdash~x\in B</math>
	Depending on whether the tactic returns <math>\left\{x\in dom(f\bunion g)\binter A,~dom(f)\bunion dom(g)\subseteq B\right\}</math> or <math>\left\{x\in dom(f\bunion g)\binter A,~A\subseteq B\right\}</math>, the reasoner will fail or succeed. To prevent such hazardous behavior, re-writing should be proceeded.		Depending on whether the tactic returns <math>\left\{x\in dom(f\bunion g)\binter A,~dom(f)\bunion dom(g)\subseteq B\right\}</math> or <math>\left\{x\in dom(f\bunion g)\binter A,~A\subseteq B\right\}</math>, the reasoner will fail or succeed. To prevent such hazardous behavior, re-writing should be proceeded.


	= Unimplemented cases =		= Unimplemented cases =

imported>Laurent: /* Find a path */

2013-11-21T11:27:56Z

Find a path

← Older revision		Revision as of 11:27, 21 November 2013
Line 48:		Line 48:

	=== Find a path ===		=== Find a path ===
	Now that we ~~recovered~~ all the hypotheses that could be useful ~~for~~ the reasoner, it remains to find a path among ~~the~~ hypotheses leading to discharge the sequent. Depending on the relations on each side of the inclusion, we will act differently. <math>f</math> always ~~represent~~ an expression (may be a domain, a range, etc.).		Now that we have found all the hypotheses that could be useful to the reasoner, it remains to find a path among these hypotheses leading to discharge the sequent. Depending on the relations on each side of the inclusion, we will act differently. <math>f</math> always denotes an expression (it may be a domain, a range, etc.).
	#The following sequent is provable because <math>f\subseteq \varphi (f)</math>.		#The following sequent is provable because <math>f\subseteq \varphi (f)</math>.
	#*<math>x\in f,\quad \varphi (f)\subseteq g\quad\vdash\quad x\in g</math>		#*<math>x\in f,\quad \varphi (f)\subseteq g\quad\vdash\quad x\in g</math>

imported>Laurent: /* Hypotheses */

2013-11-21T11:25:43Z

Hypotheses

← Older revision		Revision as of 11:25, 21 November 2013
Line 34:		Line 34:

	=== Hypotheses ===		=== Hypotheses ===
	Now we have to find hypotheses leading to discharge the sequent. To do so, the tactic ~~recovers~~ two kinds of ~~hypotheses~~ :		Now we have to find hypotheses leading to discharge the sequent. To do so, the tactic looks for two kinds of hypothesis :
	#the ones related to the left member of the goal <math>\left( x\in S\right)</math> (~~this is the start~~ point):		#the ones related to the left member of the goal <math>\left( x\in S\right)</math> (which will be used as a starting point):
	#*<math>x\in \cdots</math>		#*<math>x\in \cdots</math>
	#*<math>\cdots\mapsto x\mapsto\cdots\in\cdots</math>		#*<math>\cdots\mapsto x\mapsto\cdots\in\cdots</math>
Line 41:		Line 41:
	#*<math>\left\{\cdots, \cdots\mapsto x\mapsto\cdots,\cdots\right\}=/\subset/\subseteq\cdots</math>		#*<math>\left\{\cdots, \cdots\mapsto x\mapsto\cdots,\cdots\right\}=/\subset/\subseteq\cdots</math>
	#*<math>f\ovl\left\{\cdots, x, \cdots\right\}=/\subset/\subseteq\cdots</math>		#*<math>f\ovl\left\{\cdots, x, \cdots\right\}=/\subset/\subseteq\cdots</math>
	#the ones denoting inclusion (~~all but the ones matching the description of~~ the ~~first point~~) :		#the ones denoting inclusion (which will be used to find a path from a starting point to the goal) :
	#*<math>\cdots\subset\cdots</math>		#*<math>\cdots\subset\cdots</math>
	#*<math>\cdots\subseteq\cdots</math>		#*<math>\cdots\subseteq\cdots</math>
	#*<math>\cdots=\cdots</math>		#*<math>\cdots=\cdots</math>
	Then, it will search a link between ~~those~~ hypotheses so that the sequent can be discharged.		Then, it will search a link between these hypotheses so that the sequent can be discharged.

	=== Find a path ===		=== Find a path ===

imported>Laurent: /* Goal */

2013-11-21T11:23:46Z

Goal

← Older revision		Revision as of 11:23, 21 November 2013
Line 25:		Line 25:
	This part explains how the tactic (MembershipGoalTac) associated to the reasoner MembershipGoal is working.		This part explains how the tactic (MembershipGoalTac) associated to the reasoner MembershipGoal is working.
	=== Goal ===		=== Goal ===
	The tactic (as the reasoner) ~~should~~ works only on goals ~~such as~~ :		The tactic (as the reasoner) works only on goals of the form :
	*<math>\cdots~\in~\cdots</math>		*<math>\cdots~\in~\cdots</math>
	For ~~examples~~ :		For example:
	*<math>f(x)\in g\otimes h</math>		*<math>f(x)\in g\otimes h</math>
	*<math>x\in A\cprod\left(B\cup C\right)</math>		*<math>x\in A\cprod\left(B\cup C\right)</math>

imported>Laurent at 11:21, 21 November 2013

2013-11-21T11:21:41Z

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

imported>Josselin: More details given in find path section

2013-11-21T10:00:14Z

More details given in find path section

← Older revision		Revision as of 10:00, 21 November 2013
Line 111:		Line 111:
	From the hypothesis "<math> f \ovl \{ x \mapsto y \} \in A \rel B </math>" the reasoner deduct the following predicates: <math> \{ x \in A , \quad x \in dom(A \cprod B) \} </math>		From the hypothesis "<math> f \ovl \{ x \mapsto y \} \in A \rel B </math>" the reasoner deduct the following predicates: <math> \{ x \in A , \quad x \in dom(A \cprod B) \} </math>

	The reasoner encodes the new hypotheses derived from the hypotheses and the negation of the goal, to SAT clauses by ~~representing each inclusion of the form <math> A \subseteq B </math>~~ into the ~~clause <math>\{\lnot x\in A~~,~~\; x\in B\}</math> and then by encoding it~~ in CNF format ~~<math> \{-1, 2\}</math>~~. ~~In order to obtain a minimal solution, the~~ clauses are inserted one by one into the SAT problem until the solver reports the problem as unsatisfiable.		The reasoner encodes the new hypotheses derived from the hypotheses and the negation of the goal, to SAT clauses. For this purpose, it encodes all new hypotheses in SAT proposition by extracting all set contained into the predicate.
			And then, its encodes the proposition SAT in Dimacs CNF format. The clauses encoded are inserted one by one into the SAT problem until the solver reports the problem as unsatisfiable in order to obtain a minimal solution to the SAT core.

	{\| class="wikitable" style="text-align:center; width:80%;"		{\| class="wikitable" style="text-align:center; width:80%;"
	\|+ SAT problem encoding		\|+ SAT problem encoding
	\|-		\|-
	! scope=col \| ~~Hypothesis~~		! scope=col \| Sequent
	! scope=col \| ~~Clause~~		! scope=col \| SAT proposition
	! scope=col \| Dimacs format		! scope=col \| Dimacs CNF format
	\|-		\|-
	\|<math>x \in B</math>		\|<math>x \in B</math>
Line 147:		Line 148:
	Afterwards, the clauses in the sat core sorted by their insertion order, are then reordered by using topological sorting. The reasonner traces each clause back to the corresponding hypotheses.		Afterwards, the clauses in the sat core sorted by their insertion order, are then reordered by using topological sorting. The reasonner traces each clause back to the corresponding hypotheses.

	For each hypothesis into the list, a rationale is built and saved into an array at the index of the list. If the hypothesis denotes a membership, the rationale is directly saved into the array ~~else~~ it retrevies all ~~needed~~ rationales ~~(already seen)~~ and ~~contained~~ it into the array.		For each hypothesis into the list, a rationale is built and saved into an array at the index of the list. If the hypothesis denotes a membership, the rationale is directly saved into the array. Else it retrevies the array all rationales wich allow to prove that the member is in each set contained into the intersection and then from these rationales it builds a new Rationale and saves it into the array. However, the path building is unidirectionnal, it works with a sat core wich contains only clause contains with at most one positive literals.

			Indeed, the current version finds a path with hypotheses in the following form :
			* <math> x \in ... \binter / \bunion ... </math>
			* <math> ... \subseteq ... \binter / \bunion ... </math>


	Finally, the reasoner checks that the generated rule is equal to the goal. If so, the sequent is discharged. Else, a failure is returned		Finally, the reasoner checks that the generated rule is equal to the goal. If so, the sequent is discharged. Else, a failure is returned