Billaude's work to finish

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.

Inference rules for the reasoner MembershipGoal

Inference Rule	Side condition	Implemented in the new version	Implemented in the first version
$x\in A,\;\; A\subseteq B\vdash x\in B$			$\checkmark$
$A\subset B\vdash A\subseteq B$		$\checkmark$	$\checkmark$
$A=B\vdash A\subseteq B$		$\checkmark$	$\checkmark$
$A=B\vdash B\subseteq A$		$\checkmark$	$\checkmark$
$A\subseteq B\vdash \dom(A)\subseteq\dom(B)$		$\checkmark$	$\checkmark$
$A\subseteq B\vdash \ran(A)\subseteq\ran(B)$		$\checkmark$	$\checkmark$
$x\in\dom(A\cprod B)\vdash x\in A$		$\checkmark$	$\checkmark$
$y\in\ran(A\cprod B)\vdash y\in B$		$\checkmark$	$\checkmark$
$x\mapsto y\in f\vdash x\in\dom(f)$		$\checkmark$	$\checkmark$
$x\mapsto y\in f\vdash y\in\ran(f)$		$\checkmark$	$\checkmark$
$\left\{a,\cdots,x,\cdots, z\right\}\subseteq A\vdash x\in A$		$\checkmark$	$\checkmark$
$f\ovl\cdots\ovl g\ovl\cdots\ovl h\subseteq A\vdash g\ovl\cdots\ovl h\subseteq A$		$\checkmark$	$\checkmark$
$f\in A\;op\;B\vdash f\subseteq A\cprod B$	where $\mathit{op}$ is one of $\rel$, $\trel$, $\srel$, $\strel$, $\pfun$, $\tfun$, $\pinj$, $\tinj$, $\psur$, $\tsur$, $\tbij$	$\checkmark$	$\checkmark$
$e\subseteq f,\;\; f\setminus g\subseteq h\quad\vdash\quad e\setminus g\subseteq h$			$\checkmark$
$g\subseteq k,\;\; f\setminus g\subseteq h \quad\vdash\quad f\setminus k\subseteq h$			$\checkmark$
$e\subseteq f\setminus g,\;\; f\subseteq h\quad\vdash\quad e\subseteq h\setminus g$			$\checkmark$
$e\subseteq f\setminus g,\;\; k\subseteq g \quad\vdash\quad e\subseteq f\setminus k$			$\checkmark$
$e\subseteq f,\;\; f\ranres B\subseteq g \quad\vdash\quad e\ranres B\subseteq g$			$\checkmark$
$A\subseteq B ,\;\; f\ranres B\subseteq g \quad\vdash\quad f\ranres A\subseteq g$			$\checkmark$
$f\subseteq g\ranres A ,\;\; g\subseteq h \quad\vdash\quad f\subseteq h\ranres A$			$\checkmark$
$f\subseteq g\ranres A ,\;\; A\subseteq B \quad\vdash\quad f\subseteq g\ranres B$			$\checkmark$
$A\subseteq B ,\;\; B\domres f\subseteq g \quad\vdash\quad A\domres f\subseteq g$			$\checkmark$
$e\subseteq f ,\;\; B\domres f\subseteq g \quad\vdash\quad B\domres e\subseteq g$			$\checkmark$
$f\subseteq A\domres g ,\;\; A\subseteq B \quad\vdash\quad f\subseteq B\domres g$			$\checkmark$
$f\subseteq A\domres g ,\;\; g\subseteq h \quad\vdash\quad f\subseteq A\domres h$			$\checkmark$
$e\subseteq f ,\;\; f\ransub A\subseteq g \quad\vdash\quad e\ransub A\subseteq g$			$\checkmark$
$f\ransub A\subseteq g ,\;\; A\subseteq B \quad\vdash\quad f\ransub B\subseteq g$			$\checkmark$
$f\subseteq g\ransub A ,\;\; g\subseteq h \quad\vdash\quad f\subseteq h\ransub A$			$\checkmark$
$f\subseteq g\ransub B ,\;\; A\subseteq B \quad\vdash\quad f\subseteq g\ransub A$			$\checkmark$
$A\domsub f\subseteq g ,\;\; A\subseteq B \quad\vdash\quad B\domsub f\subseteq g$			$\checkmark$
$e\subseteq f ,\;\; A\domsub f\subseteq g \quad\vdash\quad A\domsub e\subseteq g$			$\checkmark$
$A\subseteq B ,\;\; f\subseteq B\domsub g \quad\vdash\quad f\subseteq A\domsub g$			$\checkmark$
$f\subseteq A\domsub g ,\;\; g\subseteq h \quad\vdash\quad f\subseteq A\domsub h$			$\checkmark$
$e\subseteq f ,\;\; f\ovl g\ovl\cdots\ovl h\subseteq k \quad\vdash\quad e\ovl g\ovl\cdots\ovl h\subseteq k$			$\checkmark$
$f\subseteq g\ovl h\ovl\cdots\ovl k ,\;\; e\subseteq g \quad\vdash\quad f\subseteq e\ovl h\ovl\cdots\ovl k$			$\checkmark$
$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$			$\checkmark$
$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$			$\checkmark$
$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$			$\checkmark$
$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$			$\checkmark$
$A\subseteq B,\;\; B\cprod D\subseteq E \quad\vdash\quad A\cprod D\subseteq E$			$\checkmark$
$C\subseteq D,\;\; B\cprod D\subseteq E \quad\vdash\quad B\cprod C\subseteq E$			$\checkmark$
$A\subseteq B\cprod D,\;\; B\subseteq C \quad\vdash\quad A\subseteq C\cprod D$			$\checkmark$
$A\subseteq B\cprod D,\;\; D\subseteq E\quad\vdash\quad A\subseteq B\cprod E$			$\checkmark$
$\dom(f\domres\prjone)\defi f$			$\checkmark$
$\dom(f\domres\prjtwo)\defi f$			$\checkmark$
$\dom(f\domres\id)\defi f$			$\checkmark$
$\ran(\prjone\ranres f)\defi f$			$\checkmark$
$\ran(\prjtwo\ranres f)\defi f$			$\checkmark$
$\ran(\id\ranres f)\defi f$			$\checkmark$
$\ran(f\domres\prjone)\defi\dom(f)$			$\checkmark$
$\ran(f\domres\prjtwo)\defi\ran(f)$			$\checkmark$
$\ran(f\domres\id)\defi f$			$\checkmark$

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

In the AutorewriterL3, some re-writing about $\usucc$ and $\upred$ 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 $\left(\finite(\usucc) = \bfalse,\;\cdots\right)$.

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

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

Others Feature Requests

The feature request #2887264 should also be treated.