« Reseau inverse » : différence entre les versions

Version du 20 octobre 2008 à 15:02

Formula : $A:=X(t_{1},\dots ,t_{n})\mid \neg A\mid A\vee B\mid A\wedge B\mid \forall xA\mid \exists xA$

Clause (à démontrer) : $\Gamma :=1\mid A.\Gamma$ (le point est une conjonction)

Séquent : $\Delta :=0\mid \Gamma ,\Delta$ (la virgule est une dicjoncyion)

Règle logique : ${\frac {A.B.\Gamma ,\Delta }{A\wedge B.\Gamma ,\Delta }}\wedge _{i}$

@@ Ligne 1 : / Ligne 1 : @@
 Formula : <math>A := X(t_1,\dots,t_n) \mid \neg A \mid A \vee B \mid A \wedge B \mid \forall x A \mid \exists x A</math>
@@ Ligne 5 : / Ligne 4 : @@
 Séquent : <math>\Delta := 0 \mid \Gamma , \Delta</math> (la virgule est une dicjoncyion)
+Règle logique :
+<math>
+\frac{A . B . \Gamma , \Delta}{A \wedge B . \Gamma , \Delta}\wedge_i
+</math>