Reseau inverse - Historique des versions

Raffalli : /* Simplification (structural) rules */

2008-10-21T13:00:04Z

Simplification (structural) rules

← Version précédente		Version du 21 octobre 2008 à 13:00
Ligne 137 :		Ligne 137 :

	<math>		<math>
	\frac{\gamma \vdash t : A^x . \neg A^x . \Gamma, \Delta}{\gamma \vdash t : \Delta}\hbox{reversed tautology elimination}		\frac{x:A, \gamma \vdash t : A^x . \neg A^x . \Gamma, \Delta}{x:A, \gamma \vdash t : \Delta}\hbox{reversed tautology elimination}
	</math>		</math>

	<math>		<math>
	\frac{\gamma \vdash t : A^x . \Gamma , \Delta}{\vdash t : \Gamma , \Delta}\hbox{coweakening}		\frac{x:A, \gamma \vdash t : A^x . \Gamma , \Delta}{x:A, \gamma \vdash t : \Gamma , \Delta}\hbox{coweakening}
	</math>		</math>

	<math>		<math>
	\frac{\gamma \vdash t : A^x . \Gamma , \Delta}{\vdash t : A^x . A^x . \Gamma , \Delta}\hbox{cocontraction}		\frac{x:A, \gamma \vdash t : A^x . \Gamma , \Delta}{x:A, \gamma \vdash t : A^x . A^x . \Gamma , \Delta}\hbox{cocontraction}
	</math>		</math>

Raffalli : /* Logical rules */

2008-10-21T12:59:27Z

Logical rules

← Version précédente		Version du 21 octobre 2008 à 12:59
Ligne 123 :		Ligne 123 :

	<math>		<math>
	\frac{\gamma \vdash t : \Gamma . \Gamma', \Delta}{\gamma \vdash t : A^x . \Gamma, \neg A^x . \Gamma', \Delta}\hbox{resolution}		\frac{x: A, \gamma \vdash t : \Gamma . \Gamma', \Delta}{x: A, \gamma \vdash t : A^x . \Gamma, \neg A^x . \Gamma', \Delta}\hbox{resolution}
	</math>		</math>

Raffalli : /* Logical rules */

2008-10-21T12:58:02Z

Logical rules

← Version précédente		Version du 21 octobre 2008 à 12:58
Ligne 98 :		Ligne 98 :

	<math>		<math>
	\frac{}{z : A \vee B, x:A, \gamma \vdash !z\leftarrow L(x) : (A \vee B)^z, \neg A^x}~~+_i~~^L		\frac{}{z : A \vee B, x:A, \gamma \vdash !z\leftarrow L(x) : (A \vee B)^z, \neg A^x}\vee_i^L
	</math>		</math>

	<math>		<math>
	\frac{}{z : A \vee B, y:B, \gamma \vdash !z\leftarrow R(y) : (A \vee B)^z, \neg B^y}~~+_i~~^R		\frac{}{z : A \vee B, y:B, \gamma \vdash !z\leftarrow R(y) : (A \vee B)^z, \neg B^y}\vee_i^R
	</math>		</math>

Raffalli : /* Simplification (structural) rules */

2008-10-21T12:56:19Z

Simplification (structural) rules

← Version précédente		Version du 21 octobre 2008 à 12:56
Ligne 135 :		Ligne 135 :

	===Simplification (structural) rules===		===Simplification (structural) rules===

	<math>
	\frac{\gamma \vdash t : \Delta}{\vdash t : A^x . \neg A^x . \Gamma, \Delta}\hbox{tautology elimination}
	</math>

	<math>		<math>
Ligne 149 :		Ligne 145 :

	<math>		<math>
	\frac{\gamma \vdash t : A^x . \Gamma , \Delta}{\vdash t : A^x . A^x . \Gamma , \Delta}\hbox{~~reversed~~ cocontraction}		\frac{\gamma \vdash t : A^x . \Gamma , \Delta}{\vdash t : A^x . A^x . \Gamma , \Delta}\hbox{cocontraction}
	</math>

	<math>
	\frac{\gamma \vdash t : A^x . A^x . \Gamma , \Delta}{\gamma \vdash t : A^x . \Gamma , \Delta}\hbox{cocontraction}
	</math>		</math>

Raffalli : /* Simplification (structural) rules */

2008-10-21T12:55:00Z

Simplification (structural) rules

← Version précédente		Version du 21 octobre 2008 à 12:55
Ligne 158 :		Ligne 158 :
	<math>		<math>
	\frac{\gamma \vdash t : \Gamma , \Gamma, \Delta}{\gamma \vdash t : \Gamma , \Delta}\hbox{contraction}		\frac{\gamma \vdash t : \Gamma , \Gamma, \Delta}{\gamma \vdash t : \Gamma , \Delta}\hbox{contraction}
	</math>

	<math>
	\frac{\gamma \vdash t : \Gamma , \Delta}{\gamma \vdash t : \Gamma.\Gamma' , \Gamma , \Delta}\hbox{subsumption}
	</math>		</math>

Thirs : /* Logical rules */

2008-10-21T12:23:29Z

Logical rules

← Version précédente		Version du 21 octobre 2008 à 12:23
Ligne 111 :		Ligne 111 :

	<math>		<math>
	\frac{x: A, \gamma \vdash t : \Delta}{z: \forall x,A, \gamma \vdash ?z\rightarrow(x,\alpha).t : \Delta[A^x := (\forall \alpha A)^z]}\forall_i\;\;\; (\alpha \hbox{ non libre dans la conclusion})		\frac{x: A, \gamma \vdash t : \Delta}{z: \forall x A, \gamma \vdash ?z\rightarrow(x,\alpha).t : \Delta[A^x := (\forall \alpha A)^z]}\forall_i\;\;\; (\alpha \hbox{ non libre dans la conclusion})
	</math>		</math>

	<math>		<math>
	\frac{}{z : \exists x A, x : A[x:=t], \gamma \vdash \exists x A^z, \neg A[x:=t]^x}\exists_i		\frac{}{z : \exists x A, x : A[x:=t], \gamma \vdash ! z \leftarrow (x, t) : \exists x A^z, \neg A[x:=t]^x}\exists_i
	</math>		</math>

Thirs : /* Logical rules */

2008-10-21T12:12:45Z

Logical rules

← Version précédente		Version du 21 octobre 2008 à 12:12
Ligne 107 :		Ligne 107 :
	<math>		<math>
	\frac{x: A, \gamma \vdash t : \Delta \;\;\;\;\; y: B, \gamma \vdash u : \Delta'}		\frac{x: A, \gamma \vdash t : \Delta \;\;\;\;\; y: B, \gamma \vdash u : \Delta'}
	{z: A \wedge B, \gamma\vdash ?z\rightarrow(x.t + y.u) : \Delta[A^x := (A \wedge B)^z] \otimes \Delta[B^y := (A \wedge B)^z]}\wedge_i		{z: A \wedge B, \gamma\vdash ?z\rightarrow(x.t + y.u) : \Delta[A^x := (A \wedge B)^z] \otimes \Delta'[B^y := (A \wedge B)^z]}\wedge_i
	</math>		</math>

Raffalli : /* Simplification (structural) rules */

2008-10-21T12:09:04Z

Simplification (structural) rules

← Version précédente		Version du 21 octobre 2008 à 12:09
Ligne 157 :		Ligne 157 :

	<math>		<math>
	\frac{\gamma \vdash t : \Gamma , \Gamma, \Delta}{\gamma t : ~~\vdash~~ \Gamma , \Delta}\hbox{contraction}		\frac{\gamma \vdash t : \Gamma , \Gamma, \Delta}{\gamma \vdash t : \Gamma , \Delta}\hbox{contraction}
	</math>		</math>

Raffalli : /* Logical rules */

2008-10-21T12:05:09Z

Logical rules

← Version précédente		Version du 21 octobre 2008 à 12:05
Ligne 98 :		Ligne 98 :

	<math>		<math>
	\frac{}{z : A \vee B, x:A, \gamma \vdash !z\leftarrow L(x) : (A + B)^z, \neg A^x}+_i^L		\frac{}{z : A \vee B, x:A, \gamma \vdash !z\leftarrow L(x) : (A \vee B)^z, \neg A^x}+_i^L
	</math>		</math>

	<math>		<math>
	\frac{}{z : A \vee B, y:B, \gamma \vdash !z\leftarrow R(y) : (A + B)^z, \neg B^y}+_i^R		\frac{}{z : A \vee B, y:B, \gamma \vdash !z\leftarrow R(y) : (A \vee B)^z, \neg B^y}+_i^R
	</math>		</math>

Raffalli : /* Tentative de Calcul */

2008-10-21T12:04:45Z

Tentative de Calcul

← Version précédente		Version du 21 octobre 2008 à 12:04
Ligne 81 :		Ligne 81 :
	== Tentative de Calcul ==		== Tentative de Calcul ==

	Formules : <math>A := X(t_1,\dots,t_n) \mid \neg A ~~\mid A + B~~ \mid A \wedge B ~~\mid A \times B~~ \mid A \vee B \mid \forall x A \mid \exists x A</math>		Formules : <math>A := X(t_1,\dots,t_n) \mid \neg A \mid A \wedge B \mid A \vee B \mid \forall x A \mid \exists x A</math>


Ligne 98 :		Ligne 98 :

	<math>		<math>
	\frac{}{z : A \~~times~~ B, x:A~~, y : B~~, \gamma\vdash !z\leftarrow(x,y) : (A ~~\times~~ B)^z, \neg A^x~~, \neg B~~^~~y}\times_i~~		\frac{}{z : A \vee B, x:A, \gamma \vdash !z\leftarrow L(x) : (A + B)^z, \neg A^x}+_i^L
	</math>		</math>

	<math>		<math>
	\frac{x: A, y: B, \gamma \vdash t : \~~Delta~~}		\frac{}{z : A \vee B, y:B, \gamma \vdash !z\leftarrow R(y) : (A + B)^z, \neg B^y}+_i^R
	{z: A \vee B, \gamma \vdash ?z\rightarrow(x,y).t : \Delta[A^x := (A \vee B)^z, B^y := (A \vee B)^z]}\vee_i
	</math>

	<math>
	\frac{}{z : A + B, x:A, \gamma \vdash !z\leftarrow L(x) : (A + B)^z, \neg A^x}+_i^L
	</math>

	<math>
	\frac{}{z : A + B, y:B, \gamma \vdash !z\leftarrow R(y) : (A + B)^z, \neg B^y}+_i^R
	</math>		</math>

Reseau inverse - Historique des versions

Raffalli : /* Simplification (structural) rules */

Raffalli : /* Logical rules */

Raffalli : /* Logical rules */

Raffalli : /* Simplification (structural) rules */

Raffalli : /* Simplification (structural) rules */

Thirs : /* Logical rules */

Thirs : /* Logical rules */

Raffalli : /* Simplification (structural) rules */

Raffalli : /* Logical rules */

Raffalli : /* Tentative de Calcul */

Raffalli : /* Simplification (structural) rules */

Raffalli : /* Logical rules */

Raffalli : /* Logical rules */

Raffalli : /* Simplification (structural) rules */

Raffalli : /* Simplification (structural) rules */

Thirs : /* Logical rules */

Thirs : /* Logical rules */

Raffalli : /* Simplification (structural) rules */

Raffalli : /* Logical rules */

Raffalli : /* Tentative de Calcul */