Après relecture
Cette révision appartient à :
Florian Hatat
@@ -77,7 +77,7 @@ Dans tout le sujet, pour tout entier $n$ positif, on notera $\Sigma_n$ l'alphabe
|
|||||||
\Sigma_2=\left\{\binom{0}{0},\binom{1}{0},\binom{0}{1},\binom{1}{1}\right\}
|
\Sigma_2=\left\{\binom{0}{0},\binom{1}{0},\binom{0}{1},\binom{1}{1}\right\}
|
||||||
\]
|
\]
|
||||||
|
|
||||||
Pour tout entier $i$ dans $\llbracket 1, n \rrbracket$, et pour tout mot $m$ sur $\Sigma_n$, on note $\pi_i(m)$ la projection de $m$ sur la composante $i$, c'est-à-dire, le mot sur $\{0,1\}$ composé du terme à la $i$-ème ligne sur chaque lettre de $m$.
|
Pour tout entier $i$ dans $\llbracket 1, n \rrbracket$, et pour tout mot $m$ sur $\Sigma_n$, on note $\pi_i(m)$ la projection de $m$ sur la composante $i$, c'est-à-dire, le mot sur $\{0,1\}$ composé du terme à la $i$\ieme{} ligne sur chaque lettre de $m$.
|
||||||
|
|
||||||
Par abus de notation, on s'autorise à confondre la lettre $0$ et $1$ de l'alphabet $\{0,1\}$ avec les entiers $0$ et $1$. Pour tout mot $u$ de taille $|u|=k$ sur $\{0,1\}$ tel que $u=u_0 \ldots u_{k-1}$, on va noter $v(u)$ la valeur suivante :
|
Par abus de notation, on s'autorise à confondre la lettre $0$ et $1$ de l'alphabet $\{0,1\}$ avec les entiers $0$ et $1$. Pour tout mot $u$ de taille $|u|=k$ sur $\{0,1\}$ tel que $u=u_0 \ldots u_{k-1}$, on va noter $v(u)$ la valeur suivante :
|
||||||
|
|
||||||
@@ -87,7 +87,7 @@ v(u)=\sum_{j=0}^{k-1} 2^{j} u_j
|
|||||||
|
|
||||||
Autrement dit, $v(u)$ est l'entier dont $u$ en est une de ses représentations en binaire telles que le bit de poids faible soit à gauche, donc à l'inverse du sens habituel.
|
Autrement dit, $v(u)$ est l'entier dont $u$ en est une de ses représentations en binaire telles que le bit de poids faible soit à gauche, donc à l'inverse du sens habituel.
|
||||||
|
|
||||||
Pour un mot $m$ sur $\Sigma_n$ et un entier $i$ entre 1 et $n$, on note $v_i(m)=v\left(\pi_(m)\right)$.
|
Pour un mot $m$ sur $\Sigma_n$ et un entier $i$ entre 1 et $n$, on note $v_i(m)=v(\pi_i(m))$.
|
||||||
|
|
||||||
Considérons par exemple le mot $m$ suivant :
|
Considérons par exemple le mot $m$ suivant :
|
||||||
|
|
||||||
@@ -148,9 +148,9 @@ On représente en OCaml les lettres de $\Sigma_n$ à l'aide du type \mintinline{
|
|||||||
|
|
||||||
\section{\label{sec:automates-finis}Automates finis sur $\sum_n$}
|
\section{\label{sec:automates-finis}Automates finis sur $\sum_n$}
|
||||||
|
|
||||||
Considérons les automates $\mathcal{A}_1$ et $\mathcal{A}_2$ suivants :
|
Considérons les automates $\mathcal{A}_1$ et $\mathcal{A}_2$ dont les représentations sont données sur les figures \ref{fig:automate-a1} et \ref{fig:automate-a2}.
|
||||||
|
|
||||||
\begin{figure}[h]
|
\begin{figure}[ht]
|
||||||
\begin{center}
|
\begin{center}
|
||||||
\begin{tikzpicture}[initial text = {}]
|
\begin{tikzpicture}[initial text = {}]
|
||||||
\node[state, initial] (q0) {$q_0$};
|
\node[state, initial] (q0) {$q_0$};
|
||||||
@@ -165,10 +165,11 @@ Considérons les automates $\mathcal{A}_1$ et $\mathcal{A}_2$ suivants :
|
|||||||
;
|
;
|
||||||
\end{tikzpicture}
|
\end{tikzpicture}
|
||||||
\caption{Représentation de l'automate $\mathcal{A}_1$}
|
\caption{Représentation de l'automate $\mathcal{A}_1$}
|
||||||
|
\label{fig:automate-a1}
|
||||||
\end{center}
|
\end{center}
|
||||||
\end{figure}
|
\end{figure}
|
||||||
|
|
||||||
\begin{figure}[h]
|
\begin{figure}[ht]
|
||||||
\begin{center}
|
\begin{center}
|
||||||
\begin{tikzpicture}[initial text = {}]
|
\begin{tikzpicture}[initial text = {}]
|
||||||
\node[state, initial] (q0) {$q_0$};
|
\node[state, initial] (q0) {$q_0$};
|
||||||
@@ -181,31 +182,32 @@ Considérons les automates $\mathcal{A}_1$ et $\mathcal{A}_2$ suivants :
|
|||||||
;
|
;
|
||||||
\end{tikzpicture}
|
\end{tikzpicture}
|
||||||
\caption{Représentation de l'automate $\mathcal{A}_2$}
|
\caption{Représentation de l'automate $\mathcal{A}_2$}
|
||||||
|
\label{fig:automate-a2}
|
||||||
\end{center}
|
\end{center}
|
||||||
\end{figure}
|
\end{figure}
|
||||||
|
|
||||||
Soit $E$ l'ensemble des mots $m$ sur $\Sigma_2$ tels que $v_2(m)$ est la plus grande puissance de 2 qui divise $v_1(m)$.
|
Soit $E$ l'ensemble des mots $m$ sur $\Sigma_2$ tels que $v_2(m)$ est la plus grande puissance de 2 qui divise $v_1(m)$.
|
||||||
|
|
||||||
\begin{question}
|
\begin{question}
|
||||||
Démontrer que $\mathcal{L}\left(\mathcal{A}_1\right)=E$.
|
Démontrer que $\mathcal{L}(\mathcal{A}_1)=E$.
|
||||||
\end{question}
|
\end{question}
|
||||||
|
|
||||||
\begin{question}
|
\begin{question}
|
||||||
Montrer que pour tout $m \in \mathcal{L}\left(\mathcal{A}_1\right), v_1(m) \equiv v_2(m)\left[2 \times v_2(m)\right]$.
|
Montrer que pour tout $m \in \mathcal{L}(\mathcal{A}_1), v_1(m) \equiv v_2(m) \quad [2 \times v_2(m)]$.
|
||||||
\end{question}
|
\end{question}
|
||||||
|
|
||||||
\begin{question}
|
\begin{question}
|
||||||
Décrire sans justifier le langage $\mathcal{L}\left(\mathcal{A}_2\right)$ en donnant une condition nécessaire et suffisante pour qu'un mot $m$ sur $\Sigma_2$ soit dans le langage qui fait intervenir $v_1(m)$ et $v_2(m)$.
|
Décrire sans justifier le langage $\mathcal{L}(\mathcal{A}_2)$ en donnant une condition nécessaire et suffisante pour qu'un mot $m$ sur $\Sigma_2$ soit dans le langage qui fait intervenir $v_1(m)$ et $v_2(m)$.
|
||||||
\end{question}
|
\end{question}
|
||||||
|
|
||||||
\begin{question}
|
\begin{question}
|
||||||
Proposer sans justifier un automate à 3 états qui reconnaît le langage $L$ défini par :
|
Proposer sans justifier un automate à 3 états qui reconnaît le langage $L$ défini par :
|
||||||
\[
|
\[
|
||||||
L=\left\{m \in \Sigma_3^{*} \mid v_1(m)=v_3(m) \text { ou } v_2(m)=v_3(m)\right\}
|
L=\{m \in \Sigma_3^{*} \mid v_1(m)=v_3(m) \text { ou } v_2(m)=v_3(m)\}
|
||||||
\]
|
\]
|
||||||
\end{question}
|
\end{question}
|
||||||
|
|
||||||
Pour implémenter les automates, on utilise le type automate suivant en OCaml. Un automate sur $\Sigma_n$ à $k$ états est représenté en utilisant un entier différent dans $\llbracket 0, k-1 \rrbracket$ pour chaque état. L'état initial est toujours l'état $0$.
|
Pour implémenter les automates, on utilise le type \mintinline{ocaml}{automate} suivant en OCaml. Un automate sur $\Sigma_n$ à $k$ états est représenté en utilisant un entier différent dans $\llbracket 0, k-1 \rrbracket$ pour chaque état. L'état initial est toujours l'état $0$.
|
||||||
|
|
||||||
\begin{minted}{ocaml}
|
\begin{minted}{ocaml}
|
||||||
type automate = {
|
type automate = {
|
||||||
@@ -301,7 +303,7 @@ Dans la formule $\exists x . \forall y .(z=t+y \wedge z=x) \vee(\exists w . z=t+
|
|||||||
|
|
||||||
Pour $\bar{x}$ un vecteur de variables, on notera souvent $\varphi(\bar{x})$ pour signifier que $\bar{x}$ est l'ensemble des variables libres de $\varphi$. Une assignation est une fonction des variables libres de $\varphi$ vers $\mathbb{N}$. Pour $\varphi$ une formule de Presburger et $a$ une assignation de ses variables libres, on note $\llbracket \varphi \rrbracket_a$ la valeur de vérité de $\varphi$ dans l'assignation $a$.
|
Pour $\bar{x}$ un vecteur de variables, on notera souvent $\varphi(\bar{x})$ pour signifier que $\bar{x}$ est l'ensemble des variables libres de $\varphi$. Une assignation est une fonction des variables libres de $\varphi$ vers $\mathbb{N}$. Pour $\varphi$ une formule de Presburger et $a$ une assignation de ses variables libres, on note $\llbracket \varphi \rrbracket_a$ la valeur de vérité de $\varphi$ dans l'assignation $a$.
|
||||||
|
|
||||||
Par exemple, considérons la formule $\varphi_{\leqslant}(x, y):=\exists z . y=x+z$, où : $=$ est un opérateur de définition. Ici, $z$ est une variable liée, et $y$ et $x$ sont des variables libres. Pour un $x$ et un $y$ donnés, cette formule est vraie si et seulement s'il existe un entier $z$ dans $\mathbb{N}$ tel que $y=x+z$, donc si et seulement si $x \leqslant y$.
|
Par exemple, considérons la formule $\varphi_{\leqslant}(x, y):=\exists z . y=x+z$, où $:=$ est un opérateur de définition. Ici, $z$ est une variable liée, et $y$ et $x$ sont des variables libres. Pour un $x$ et un $y$ donnés, cette formule est vraie si et seulement s'il existe un entier $z$ dans $\mathbb{N}$ tel que $y=x+z$, donc si et seulement si $x \leqslant y$.
|
||||||
|
|
||||||
Pour deux formules $\varphi$ et $\varphi^{\prime}$ ayant le même ensemble de variables libres, on dit qu'elles sont équivalentes, si pour toute assignation de ces variables libres, elles ont la même valeur de vérité.
|
Pour deux formules $\varphi$ et $\varphi^{\prime}$ ayant le même ensemble de variables libres, on dit qu'elles sont équivalentes, si pour toute assignation de ces variables libres, elles ont la même valeur de vérité.
|
||||||
|
|
||||||
@@ -317,7 +319,7 @@ Pour deux formules $\varphi$ et $\varphi^{\prime}$ ayant le même ensemble de va
|
|||||||
|
|
||||||
On dit qu'une formule est sous forme simple si elle vérifie les propriétés suivantes :
|
On dit qu'une formule est sous forme simple si elle vérifie les propriétés suivantes :
|
||||||
\begin{enumerate}[(i)]
|
\begin{enumerate}[(i)]
|
||||||
\item elle ne contient pas les opérateurs $\vee$ et $→$ ;
|
\item elle ne contient pas les opérateurs $\vee$ et $\rightarrow$ ;
|
||||||
\item elle ne contient pas le quantificateur $\forall$ ;
|
\item elle ne contient pas le quantificateur $\forall$ ;
|
||||||
\item pour toute sous-formule de la forme $t_1=t_2$, $t_1$ est une variable dans $\mathcal{V}$ et
|
\item pour toute sous-formule de la forme $t_1=t_2$, $t_1$ est une variable dans $\mathcal{V}$ et
|
||||||
\begin{itemize}
|
\begin{itemize}
|
||||||
@@ -339,7 +341,7 @@ On veut à présent montrer que certaines formules sont des tautologies à l'aid
|
|||||||
|
|
||||||
Pour $\varphi$ une formule, $x$ une variable, et $t$ un terme, on note $\varphi[t / x]$ la formule $\varphi$ où toutes les occurrences libres de $x$ ont été remplacées par le terme $t$. Pour pouvoir effectuer des preuves sur des formules plus complexes, on introduit les règles suivantes sur l'égalité pour $x$ une variable, $\varphi$ une formule et $t$ un terme :
|
Pour $\varphi$ une formule, $x$ une variable, et $t$ un terme, on note $\varphi[t / x]$ la formule $\varphi$ où toutes les occurrences libres de $x$ ont été remplacées par le terme $t$. Pour pouvoir effectuer des preuves sur des formules plus complexes, on introduit les règles suivantes sur l'égalité pour $x$ une variable, $\varphi$ une formule et $t$ un terme :
|
||||||
\begin{mathpar}
|
\begin{mathpar}
|
||||||
\inferrule{}{\Gamma \vdash t=t} \quad {\operatorname{ax}_{=}}
|
\inferrule{ }{\Gamma \vdash t=t} \quad {\operatorname{ax}_{=}}
|
||||||
\and
|
\and
|
||||||
\inferrule{\Gamma, x=t \vdash \varphi[t / x]}{\Gamma, x=t \vdash \varphi} \quad {\operatorname{sub}_{=}}
|
\inferrule{\Gamma, x=t \vdash \varphi[t / x]}{\Gamma, x=t \vdash \varphi} \quad {\operatorname{sub}_{=}}
|
||||||
\end{mathpar}
|
\end{mathpar}
|
||||||
@@ -353,7 +355,7 @@ De plus, on sait que l'addition est associative et pour simplifier les preuves,
|
|||||||
\section{\label{sec:retour-automates}Retour sur les automates}
|
\section{\label{sec:retour-automates}Retour sur les automates}
|
||||||
|
|
||||||
\begin{question}
|
\begin{question}
|
||||||
Écrire une fonction \mintinline{ocaml}{sans_zero : automate -> automate} qui prend en entrée un automate et qui renvoie une copie de cet automate ayant pour états finaux tout état permettant d'accéder à un état final par une suite de transitions étiquetées par la lettre $\begin{pmatrix}0 \\ \ldots \\ 0\end{pmatrix}$ dans l'automate initial.
|
Écrire une fonction \mintinline{ocaml}{sans_zero : automate -> automate} qui prend en entrée un automate et qui renvoie une copie de cet automate ayant pour états finaux tout état permettant d'accéder à un état final par une suite de transitions étiquetées par la lettre $\begin{pmatrix}0 \\ \vdots \\ 0\end{pmatrix}$ dans l'automate initial.
|
||||||
\end{question}
|
\end{question}
|
||||||
|
|
||||||
Avant de faire le lien entre automate et formules, on doit d'abord s'intéresser au problème des différentes représentations des entiers dues aux zéros non significatifs.
|
Avant de faire le lien entre automate et formules, on doit d'abord s'intéresser au problème des différentes représentations des entiers dues aux zéros non significatifs.
|
||||||
@@ -375,13 +377,13 @@ Autrement dit, il s'agit de l'ensemble des mots égaux à un mot de $L$ sauf pos
|
|||||||
|
|
||||||
Soit $n$ un entier supérieur ou égal à $3$. Soit, $i$, $j$ et $k$ des entiers de $\llbracket 1, n \rrbracket$.
|
Soit $n$ un entier supérieur ou égal à $3$. Soit, $i$, $j$ et $k$ des entiers de $\llbracket 1, n \rrbracket$.
|
||||||
|
|
||||||
On note $L_{i, j, k}$ le langage $\{m \in \Sigma_n^{*} \mid v_(m)+v_(m)=v_k(m)\}$. On suppose disposer d'une fonction \mintinline{ocaml}{automate_somme : int -> int -> int -> int -> automate} telle que \mintinline{ocaml}{automate_somme n i j k} renvoie un automate reconnaissant $L_{i, j, k}$.
|
On note $L_{i, j, k}$ le langage $\{m \in \Sigma_n^{*} \mid v_i(m)+v_j(m)=v_k(m)\}$. On suppose disposer d'une fonction \mintinline{ocaml}{automate_somme : int -> int -> int -> int -> automate} telle que \mintinline{ocaml}{automate_somme n i j k} renvoie un automate reconnaissant $L_{i, j, k}$.
|
||||||
|
|
||||||
On note $L_{=i, j}$ le langage $\{m \in \Sigma_n^{*} \mid v_(m)=v_(m)\}$. On suppose disposer d'une fonction \mintinline{ocaml}{automate_egalite : int -> int -> int -> automate} telle que \mintinline{ocaml}{automate_egalite n i j} renvoie un automate reconnaissant $L_{=i, j}$.
|
On note $L_{=i, j}$ le langage $\{m \in \Sigma_n^{*} \mid v_i(m)=v_j(m)\}$. On suppose disposer d'une fonction\\ \mintinline{ocaml}{automate_egalite : int -> int -> int -> automate} telle que \mintinline{ocaml}{automate_egalite n i j} renvoie un automate reconnaissant $L_{=i, j}$.
|
||||||
|
|
||||||
Considérons une formule sous forme simple $\varphi$ utilisant $n$ variables qu'on note $\{x_1, \ldots, x_n\}$. Soit $k$ le nombre de variables libres de $\varphi$. Soit une fonction $f$ strictement croissante de $\llbracket 1, k \rrbracket$ dans $\llbracket 1, n \rrbracket$ telle que les $\{x_{f(1)}, \ldots, x_{f(k)}\}$ est l'ensemble des variables libres de $\varphi$. Pour tout mot $m$ de $\Sigma_n$, on note $a^{m}$ l'assignation des variables libres de $\varphi$ définie pour $i$ dans $\llbracket 1, k \rrbracket$ par $a^{m}(x_{f(i)})=v_{f(i)}(m)$. On note $L_{\varphi}$ le langage
|
Considérons une formule sous forme simple $\varphi$ utilisant $n$ variables qu'on note $\{x_1, \ldots, x_n\}$. Soit $k$ le nombre de variables libres de $\varphi$. Soit une fonction $f$ strictement croissante de $\llbracket 1, k \rrbracket$ dans $\llbracket 1, n \rrbracket$ telle que les $\{x_{f(1)}, \ldots, x_{f(k)}\}$ est l'ensemble des variables libres de $\varphi$. Pour tout mot $m$ de $\Sigma_n$, on note $a^{m}$ l'assignation des variables libres de $\varphi$ définie pour $i$ dans $\llbracket 1, k \rrbracket$ par $a^{m}(x_{f(i)})=v_{f(i)}(m)$. On note $L_{\varphi}$ le langage
|
||||||
\[
|
\[
|
||||||
L_{\varphi}=\{m \in \Sigma_n^{*} \mid \llbracket \varphi \rrbracket_{a^{m}} \text { est vrai }\}
|
L_{\varphi}=\{m \in \Sigma_n^{*} \mid \llbracket \varphi \rrbracket_{a^{m}} \text { est vrai}\}
|
||||||
\]
|
\]
|
||||||
|
|
||||||
Intéressons nous à l'implémentation des formules de Presburger sous forme simple. On représente les variables par des entiers. On utilise les types OCaml suivants :
|
Intéressons nous à l'implémentation des formules de Presburger sous forme simple. On représente les variables par des entiers. On utilise les types OCaml suivants :
|
||||||
@@ -424,49 +426,48 @@ On présente les règles de la déduction naturelle suivantes.
|
|||||||
Les arbres de preuves doivent être effectués à partir de l'ensemble de règles fourni ci-dessous.
|
Les arbres de preuves doivent être effectués à partir de l'ensemble de règles fourni ci-dessous.
|
||||||
|
|
||||||
\begin{mathpar}
|
\begin{mathpar}
|
||||||
\inferrule{\Gamma \vdash}{\Gamma, A \vdash A} \quad \text{ax}
|
\inferrule{ }{\Gamma, A \vdash A} \quad \text{ax}
|
||||||
\and
|
\and
|
||||||
\inferrule{\Gamma \vdash B}{\Gamma, A \vdash B} \quad \text{aff}
|
\inferrule{\Gamma \vdash B}{\Gamma, A \vdash B} \quad \text{aff}
|
||||||
\and
|
\and
|
||||||
\inferrule{\Gamma \vdash \bot}{\Gamma \vdash A} \quad \bot
|
\inferrule{\Gamma \vdash \bot}{\Gamma \vdash A} \quad \bot
|
||||||
\\
|
\\
|
||||||
\inferrule{}{\Gamma \vdash A \vee \neg A} \quad \text {t.e.}
|
\inferrule{ }{\Gamma \vdash A \vee \neg A} \quad \text {t.e.}
|
||||||
\and
|
\and
|
||||||
\inferrule{\Gamma, \neg A \vdash \bot}{\Gamma \vdash A} \quad \text{RAA}
|
\inferrule{\Gamma, \neg A \vdash \bot}{\Gamma \vdash A} \quad \text{RAA}
|
||||||
\\
|
\\
|
||||||
\inferrule{\Gamma, A \vdash B}{\Gamma \vdash A \rightarrow B} \quad \rightarrow_i
|
\inferrule{\Gamma, A \vdash B}{\Gamma \vdash A \rightarrow B} \quad \rightarrow_i
|
||||||
\quad
|
|
||||||
\inferrule{\Gamma \vdash A \rightarrow B \\ \Gamma \vdash A}{\Gamma \vdash B} \rightarrow_e
|
|
||||||
\\
|
|
||||||
\inferrule{\Gamma \vdash A \\ \Gamma \vdash B}{\Gamma \vdash A \wedge B} \wedge_i
|
|
||||||
\and
|
\and
|
||||||
\inferrule{\Gamma \vdash A \wedge B}{\Gamma \vdash A} \wedge_e^{g}
|
\inferrule{\Gamma \vdash A \rightarrow B \\ \Gamma \vdash A}{\Gamma \vdash B} \quad \rightarrow_e
|
||||||
\and
|
|
||||||
\inferrule{\Gamma \vdash A \wedge B}{\Gamma \vdash B} \wedge_e^{d}
|
|
||||||
\\
|
\\
|
||||||
\inferrule{\Gamma \vdash A}{\Gamma \vdash A \vee B} \vee_i^{g}
|
\inferrule{\Gamma \vdash A \\ \Gamma \vdash B}{\Gamma \vdash A \wedge B} \quad \wedge_i
|
||||||
\and
|
\and
|
||||||
\inferrule{\Gamma \vdash B}{\Gamma \vdash A \vee B} \vee_i^{d}
|
\inferrule{\Gamma \vdash A \wedge B}{\Gamma \vdash A} \quad \wedge_e^{g}
|
||||||
\and
|
\and
|
||||||
\inferrule{\Gamma \vdash A \vee B \\ \Gamma, A \vdash C \\ \Gamma, B \vdash C}{\Gamma \vdash C} \vee_e
|
\inferrule{\Gamma \vdash A \wedge B}{\Gamma \vdash B} \quad \wedge_e^{d}
|
||||||
\\
|
\\
|
||||||
\inferrule{\Gamma, A \vdash \perp}{\Gamma \vdash \neg A} \neg_i
|
\inferrule{\Gamma \vdash A}{\Gamma \vdash A \vee B} \quad \vee_i^{g}
|
||||||
\and
|
\and
|
||||||
\inferrule{\Gamma \vdash \neg A \\ \Gamma \vdash A}{\Gamma \vdash \bot} \neg_e
|
\inferrule{\Gamma \vdash B}{\Gamma \vdash A \vee B} \quad \vee_i^{d}
|
||||||
\\
|
|
||||||
\inferrule{\Gamma, A, B \vdash C}{\Gamma, A \wedge B \vdash C} \text{cut}
|
|
||||||
\\
|
|
||||||
\inferrule{\Gamma \vdash A \\ x \not\in \operatorname{FV}(\Gamma)}{\Gamma \vdash \forall x. A} \forall_i
|
|
||||||
\and
|
\and
|
||||||
\inferrule{\Gamma \vdash \forall x. A}{\Gamma \vdash A[t/x]} \forall_e
|
\inferrule{\Gamma \vdash A \vee B \\ \Gamma, A \vdash C \\ \Gamma, B \vdash C}{\Gamma \vdash C} \quad \vee_e
|
||||||
\\
|
\\
|
||||||
\inferrule{\Gamma \vdash A[t/x]}{\Gamma \vdash \exists x. A} \exists_i
|
\inferrule{\Gamma, A \vdash \perp}{\Gamma \vdash \neg A} \quad \neg_i
|
||||||
\and
|
\and
|
||||||
\inferrule{\Gamma \vdash \exists x. A \\ \Gamma, A \vdash B \\ x \not\in \operatorname{FV}(\Gamma) \cup \operatorname{FV}(B)}{\Gamma \vdash B} \exists_e
|
\inferrule{\Gamma \vdash \neg A \\ \Gamma \vdash A}{\Gamma \vdash \bot} \quad \neg_e
|
||||||
\\
|
\\
|
||||||
\inferrule{\Gamma, A \vdash B \\ x \not\in \operatorname{FV}(\Gamma) \cup \operatorname{FV}(B)}{\Gamma, \exists x. A \vdash B} \exists'_e
|
\inferrule{\Gamma, A, B \vdash C}{\Gamma, A \wedge B \vdash C} \quad \text{cut}
|
||||||
|
\\
|
||||||
|
\inferrule{\Gamma \vdash A \\ x \not\in \operatorname{FV}(\Gamma)}{\Gamma \vdash \forall x. A} \quad \forall_i
|
||||||
|
\and
|
||||||
|
\inferrule{\Gamma \vdash \forall x. A}{\Gamma \vdash A[t/x]} \quad \forall_e
|
||||||
|
\\
|
||||||
|
\inferrule{\Gamma \vdash A[t/x]}{\Gamma \vdash \exists x. A} \quad \exists_i
|
||||||
|
\and
|
||||||
|
\inferrule{\Gamma \vdash \exists x. A \\ \Gamma, A \vdash B \\ x \not\in \operatorname{FV}(\Gamma) \cup \operatorname{FV}(B)}{\Gamma \vdash B} \quad \exists_e
|
||||||
|
\\
|
||||||
|
\inferrule{\Gamma, A \vdash B \\ x \not\in \operatorname{FV}(\Gamma) \cup \operatorname{FV}(B)}{\Gamma, \exists x. A \vdash B} \quad \exists'_e
|
||||||
\end{mathpar}
|
\end{mathpar}
|
||||||
|
où $\operatorname{FV}(A)$ désigne l'ensemble des variables libres dans une formule $A$ et $\operatorname{FV}(\Gamma)$ l'ensemble des variables libres dans un ensemble de formules $\Gamma$. De plus, $A[t / x]$ correspond à la formule $A$ où les occurrences d'une variable libre $x$ ont été remplacées par $t$.
|
||||||
Où $\operatorname{FV}(A)$ désigne l'ensemble des variables libres dans une formule $A$ et $\operatorname{FV}(\Gamma)$ l'ensemble des variables libres dans un ensemble de formules $\Gamma$. De plus, $A[t / x]$ correspond à la formule $A$ où les occurrences d'une variable libre $x$ ont été remplacées par $t$.
|
|
||||||
|
|
||||||
\end{document}
|
\end{document}
|
||||||
|
|||||||
Référencer dans un nouveau ticket
Bloquer un utilisateur