imported>Billaude: New section added (in order to replace the Membership Goal section)

2013-02-26T11:50:22Z

New section added (in order to replace the Membership Goal section)

← Older revision		Revision as of 11:50, 26 February 2013
Line 276:		Line 276:

	This describe the rule that I implemented in the first version of MembershipGoal. Others should also be taken into account (they will be written later). Even if those rule have been checked, they may not be implemented in the reasoner since some can explode the time research.		This describe the rule that I implemented in the first version of MembershipGoal. Others should also be taken into account (they will be written later). Even if those rule have been checked, they may not be implemented in the reasoner since some can explode the time research.

			= Membership Goal Exhaustive rules =

			To be completed ...

	= Autorewriter =		= Autorewriter =

imported>Billaude: This page is to be completed soon. Nevertheless, it contains more important informations.

2011-09-30T16:39:03Z

This page is to be completed soon. Nevertheless, it contains more important informations.

New page

This page is here to describe the work that I started, but which is yet to be finished.

= MembershipGoal =

Here the rules that could be useful for the reasoner MembershipGoal.

{| class="wikitable" style="text-align:center; width:80%;"
|+ Inference rules for the reasoner MembershipGoal
|-
! scope=col | Inference Rule
! scope=col | Side condition
! scope=col | Implemented in the new version
! scope=col | Implemented in the first version
|-
|align="left"|<math> x\in A,\;\; A\subseteq B\vdash x\in B </math>
|align="left"|
|<math></math>
|<math>\checkmark</math>
|-
|align="left"|<math> A\subset B\vdash A\subseteq B </math>
|align="left"|
|<math>\checkmark</math>
|<math>\checkmark</math>
|-
|align="left"|<math> A=B\vdash A\subseteq B</math>
|align="left"|
|<math>\checkmark</math>
|<math>\checkmark</math>
|-
|align="left"|<math> A=B\vdash B\subseteq A</math>
|align="left"|
|<math>\checkmark</math>
|<math>\checkmark</math>
|-
|align="left"|<math> A\subseteq B\vdash \dom(A)\subseteq\dom(B)</math>
|align="left"|
|<math>\checkmark</math>
|<math>\checkmark</math>
|-
|align="left"|<math> A\subseteq B\vdash \ran(A)\subseteq\ran(B)</math>
|align="left"|
|<math>\checkmark</math>
|<math>\checkmark</math>
|-
|align="left"|<math> x\in\dom(A\cprod B)\vdash x\in A</math>
|align="left"|
|<math>\checkmark</math>
|<math>\checkmark</math>
|-
|align="left"|<math> y\in\ran(A\cprod B)\vdash y\in B</math>
|align="left"|
|<math>\checkmark</math>
|<math>\checkmark</math>
|-
|align="left"|<math> x\mapsto y\in f\vdash x\in\dom(f)</math>
|align="left"|
|<math>\checkmark</math>
|<math>\checkmark</math>
|-
|align="left"|<math> x\mapsto y\in f\vdash y\in\ran(f)</math>
|align="left"|
|<math>\checkmark</math>
|<math>\checkmark</math>
|-
|align="left"|<math> \left\{a,\cdots,x,\cdots, z\right\}\subseteq A\vdash x\in A</math>
|align="left"|
|<math>\checkmark</math>
|<math>\checkmark</math>
|-
|align="left"|<math> f\ovl\cdots\ovl g\ovl\cdots\ovl h\subseteq A\vdash g\ovl\cdots\ovl h\subseteq A</math>
|align="left"|
|<math>\checkmark</math>
|<math>\checkmark</math>
|-
|align="left"|<math> f\in A\;op\;B\vdash f\subseteq A\cprod B</math>
|align="left"|where <math>\mathit{op}</math> is one of <math>\rel</math>, <math>\trel</math>, <math>\srel</math>, <math>\strel</math>, <math>\pfun</math>, <math>\tfun</math>, <math>\pinj</math>, <math>\tinj</math>, <math>\psur</math>, <math>\tsur</math>, <math>\tbij</math>
|<math>\checkmark</math>
|<math>\checkmark</math>
|-
|align="left"|<math>e\subseteq f,\;\; f\setminus g\subseteq h\quad\vdash\quad e\setminus g\subseteq h</math>
|align="left"|
|<math></math>
|<math>\checkmark</math>
|-
|align="left"|<math>g\subseteq k,\;\; f\setminus g\subseteq h \quad\vdash\quad f\setminus k\subseteq h</math>
|align="left"|
|<math></math>
|<math>\checkmark</math>
|-
|align="left"|<math>e\subseteq f\setminus g,\;\; f\subseteq h\quad\vdash\quad e\subseteq h\setminus g</math>
|align="left"|
|<math></math>
|<math>\checkmark</math>
|-
|align="left"|<math>e\subseteq f\setminus g,\;\; k\subseteq g \quad\vdash\quad e\subseteq f\setminus k</math>
|align="left"|
|<math></math>
|<math>\checkmark</math>
|-
|align="left"|<math>e\subseteq f,\;\; f\ranres B\subseteq g \quad\vdash\quad e\ranres B\subseteq g</math>
|align="left"|
|<math></math>
|<math>\checkmark</math>
|-
|align="left"|<math>A\subseteq B ,\;\; f\ranres B\subseteq g \quad\vdash\quad f\ranres A\subseteq g</math>
|align="left"|
|<math></math>
|<math>\checkmark</math>
|-
|align="left"|<math>f\subseteq g\ranres A ,\;\; g\subseteq h \quad\vdash\quad f\subseteq h\ranres A</math>
|align="left"|
|<math></math>
|<math>\checkmark</math>
|-
|align="left"|<math>f\subseteq g\ranres A ,\;\; A\subseteq B \quad\vdash\quad f\subseteq g\ranres B</math>
|align="left"|
|<math></math>
|<math>\checkmark</math>
|-
|align="left"|<math>A\subseteq B ,\;\; B\domres f\subseteq g \quad\vdash\quad A\domres f\subseteq g</math>
|align="left"|
|<math></math>
|<math>\checkmark</math>
|-
|align="left"|<math>e\subseteq f ,\;\; B\domres f\subseteq g \quad\vdash\quad B\domres e\subseteq g</math>
|align="left"|
|<math></math>
|<math>\checkmark</math>
|-
|align="left"|<math>f\subseteq A\domres g ,\;\; A\subseteq B \quad\vdash\quad f\subseteq B\domres g</math>
|align="left"|
|<math></math>
|<math>\checkmark</math>
|-
|align="left"|<math>f\subseteq A\domres g ,\;\; g\subseteq h \quad\vdash\quad f\subseteq A\domres h</math>
|align="left"|
|<math></math>
|<math>\checkmark</math>
|-
|align="left"|<math>e\subseteq f ,\;\; f\ransub A\subseteq g \quad\vdash\quad e\ransub A\subseteq g</math>
|align="left"|
|<math></math>
|<math>\checkmark</math>
|-
|align="left"|<math>f\ransub A\subseteq g ,\;\; A\subseteq B \quad\vdash\quad f\ransub B\subseteq g</math>
|align="left"|
|<math></math>
|<math>\checkmark</math>
|-
|align="left"|<math>f\subseteq g\ransub A ,\;\; g\subseteq h \quad\vdash\quad f\subseteq h\ransub A</math>
|align="left"|
|<math></math>
|<math>\checkmark</math>
|-
|align="left"|<math>f\subseteq g\ransub B ,\;\; A\subseteq B \quad\vdash\quad f\subseteq g\ransub A</math>
|align="left"|
|<math></math>
|<math>\checkmark</math>
|-
|align="left"|<math>A\domsub f\subseteq g ,\;\; A\subseteq B \quad\vdash\quad B\domsub f\subseteq g</math>
|align="left"|
|<math></math>
|<math>\checkmark</math>
|-
|align="left"|<math>e\subseteq f ,\;\; A\domsub f\subseteq g \quad\vdash\quad A\domsub e\subseteq g</math>
|align="left"|
|<math></math>
|<math>\checkmark</math>
|-
|align="left"|<math>A\subseteq B ,\;\; f\subseteq B\domsub g \quad\vdash\quad f\subseteq A\domsub g</math>
|align="left"|
|<math></math>
|<math>\checkmark</math>
|-
|align="left"|<math>f\subseteq A\domsub g ,\;\; g\subseteq h \quad\vdash\quad f\subseteq A\domsub h</math>
|align="left"|
|<math></math>
|<math>\checkmark</math>
|-
|align="left"|<math>e\subseteq f ,\;\; f\ovl g\ovl\cdots\ovl h\subseteq k \quad\vdash\quad e\ovl g\ovl\cdots\ovl h\subseteq k</math>
|align="left"|
|<math></math>
|<math>\checkmark</math>
|-
|align="left"|<math>f\subseteq g\ovl h\ovl\cdots\ovl k ,\;\; e\subseteq g \quad\vdash\quad f\subseteq e\ovl h\ovl\cdots\ovl k</math>
|align="left"|
|<math></math>
|<math>\checkmark</math>
|-
|align="left"|<math>Z\subseteq B,\;\; A\bunion\cdots\bunion B\bunion\cdots\bunion C\subseteq D\quad\vdash\quad A\bunion\cdots\bunion Z\bunion\cdots\bunion C\subseteq D</math>
|align="left"|
|<math></math>
|<math>\checkmark</math>
|-
|align="left"|<math>B\subseteq Z ,\;\; D\subseteq A\bunion\cdots\bunion B\bunion\cdots\bunion C \quad\vdash\quad D\subseteq A\bunion\cdots\bunion Z\bunion\cdots\bunion C</math>
|align="left"|
|<math></math>
|<math>\checkmark</math>
|-
|align="left"|<math>Z\subseteq B,\;\; A\binter\cdots\binter B\binter\cdots\binter C\subseteq D\quad\vdash\quad A\binter\cdots\binter Z\binter\cdots\binter C\subseteq D</math>
|align="left"|
|<math></math>
|<math>\checkmark</math>
|-
|align="left"|<math>B\subseteq Z ,\;\; D\subseteq A\binter\cdots\binter B\binter\cdots\binter C \quad\vdash\quad D\subseteq A\binter\cdots\binter Z\binter\cdots\binter C</math>
|align="left"|
|<math></math>
|<math>\checkmark</math>
|-
|align="left"|<math>A\subseteq B,\;\; B\cprod D\subseteq E \quad\vdash\quad A\cprod D\subseteq E</math>
|align="left"|
|<math></math>
|<math>\checkmark</math>
|-
|align="left"|<math>C\subseteq D,\;\; B\cprod D\subseteq E \quad\vdash\quad B\cprod C\subseteq E</math>
|align="left"|
|<math></math>
|<math>\checkmark</math>
|-
|align="left"|<math>A\subseteq B\cprod D,\;\; B\subseteq C \quad\vdash\quad A\subseteq C\cprod D</math>
|align="left"|
|<math></math>
|<math>\checkmark</math>
|-
|align="left"|<math>A\subseteq B\cprod D,\;\; D\subseteq E\quad\vdash\quad A\subseteq B\cprod E</math>
|align="left"|
|<math></math>
|<math>\checkmark</math>
|-
|align="left"|<math>\dom(f\domres\prjone)\defi f</math>
|align="left"|
|<math></math>
|<math>\checkmark</math>
|-
|align="left"|<math>\dom(f\domres\prjtwo)\defi f</math>
|align="left"|
|<math></math>
|<math>\checkmark</math>
|-
|align="left"|<math>\dom(f\domres\id)\defi f</math>
|align="left"|
|<math></math>
|<math>\checkmark</math>
|-
|align="left"|<math>\ran(\prjone\ranres f)\defi f</math>
|align="left"|
|<math></math>
|<math>\checkmark</math>
|-
|align="left"|<math>\ran(\prjtwo\ranres f)\defi f</math>
|align="left"|
|<math></math>
|<math>\checkmark</math>
|-
|align="left"|<math>\ran(\id\ranres f)\defi f</math>
|align="left"|
|<math></math>
|<math>\checkmark</math>
|-
|align="left"|<math>\ran(f\domres\prjone)\defi\dom(f)</math>
|align="left"|
|<math></math>
|<math>\checkmark</math>
|-
|align="left"|<math>\ran(f\domres\prjtwo)\defi\ran(f)</math>
|align="left"|
|<math></math>
|<math>\checkmark</math>
|-
|align="left"|<math>\ran(f\domres\id)\defi f</math>
|align="left"|
|<math></math>
|<math>\checkmark</math>
|-
|}

This describe the rule that I implemented in the first version of MembershipGoal. Others should also be taken into account (they will be written later). Even if those rule have been checked, they may not be implemented in the reasoner since some can explode the time research.

= Autorewriter =

In the AutorewriterL3, some re-writing about <math>\usucc</math> and <math>\upred</math> are proceeded. But, more re-writing should be done. Unfortunately, I did not take too much time to analyze all the possibilities about this two functions <math>\left(\finite(\usucc) = \bfalse,\;\cdots\right)</math>.

Nevertheless, one trail has been explored : instead of re-writing <math>\usucc(x) = x+1</math>, we may should better re-write : <math>\left(\lambda x\qdot\btrue\mid x+1\right)</math>.

Moreover, since <math>\upred\defi\usucc^{-1}</math>, instead of re-writing <math>\usucc^{-1}\defi\left(\lambda x\qdot\btrue\mid x+1\right)^{-1}\defi\left\{a\qdot\btrue\mid a-1\mapsto a\right\}</math> (the last re-writing is proceeded by the auto-rewriter, and is not really easy to read), I think that we should re-write <math>\usucc^{-1}\defi\left(\lambda x\qdot\btrue\mid x-1\right)</math>.

= Others Feature Requests =

The feature request #2887264 should also be treated.

[[Category:Design proposal]]

Billaude's work to finish - Revision history

imported>Billaude: New section added (in order to replace the Membership Goal section)

imported>Billaude: This page is to be completed soon. Nevertheless, it contains more important informations.