\documentclass{article}
\usepackage{amssymb, amsmath, geometry, multicol, stmaryrd}

\geometry{tmargin=.7in, bmargin=.75in, lmargin=.75in, rmargin = .75in}

\begin{document}
\setlength{\parindent}{0mm}

\title{Logique}
\author{Aubin SIONVILLE}
\date{MPI Clemenceau - 2021-2023}
\maketitle

\begin{multicols}{2}
    \centering\section*{Syntaxe}
    Règles de la logique propositionnelle : \newline
    $\displaystyle\lnot{\Big|}^1 \quad \land{\Big|}^2 \quad \lor{\Big|}^2 \quad \longrightarrow{\Big|}^2 \quad \longleftrightarrow{\Big|}^2$\\
    $\displaystyle\top{\Big|}^0 \quad \bot{\Big|}^0 \quad v{\Big|}^0_\mathcal{P}$  


    \section*{Opérateurs booléens}
    $a\cdot b \sim $ $a$ et $b$ \\
    $a+b \sim $ $a$ ou $b$ \\
    $\bar{a} \sim $ non $a$

\end{multicols}
\hspace{1cm}
    \centering\section*{Fonctions booléennes}
    Environnement propositionnel : fonction $\rho : \mathcal{P} \rightarrow \mathbb{B}$
    Interprétation des formules :
    \[
        \begin{split}
        \llbracket\top\rrbracket^\rho = V & \quad\quad \llbracket\bot\rrbracket^\rho = F \\
        \llbracket p\rrbracket^\rho = \rho(p) & \quad\quad \llbracket\urcorner G\rrbracket^\rho = \overline{\llbracket G \rrbracket^\rho} \\
        \llbracket G \land H\rrbracket^\rho = \llbracket G \rrbracket^\rho \cdot \llbracket H \rrbracket^\rho & \quad\quad \llbracket G \lor H\rrbracket^\rho = \llbracket G \rrbracket^\rho + \llbracket H \rrbracket^\rho \\
        \llbracket G \longrightarrow H\rrbracket^\rho = \overline{\llbracket G \rrbracket^\rho} + \llbracket H \rrbracket^\rho & \quad\quad \llbracket G \longleftrightarrow H \rrbracket =  \Big(\overline{\llbracket G \rrbracket^\rho} + \llbracket H \rrbracket^\rho\Big) \cdot \Big(\llbracket G \rrbracket^\rho + \overline{\llbracket H \rrbracket^\rho}\Big)
        \end{split}
    \]

\hspace{1cm}

\begin{multicols}{2}
    \section*{Sémantique}
    \subsection*{Formules équivalentes}
    \[G \equiv H \iff \llbracket G \rrbracket = \llbracket H \rrbracket\]

    \subsection*{Conséquence sémantique}
    \[G \vDash H \iff \forall \rho \in \mathbb{B}^{\mathcal{P}}, (\llbracket G \rrbracket^\rho = V \Rightarrow \llbracket H \rrbracket^\rho = V)\]

    Une formule $G$ est
    \begin{itemize}
        \item valide si $\forall \rho \in \mathbb{B}^{\mathcal{P}}, \llbracket G \rrbracket^\rho = V$
        \item satisfiable si $\exists \rho \in \mathbb{B}^{\mathcal{P}}, \llbracket G \rrbracket^\rho = V$
        \item insatisfiable si $\nexists \rho \in \mathbb{B}^{\mathcal{P}}, \llbracket G \rrbracket^\rho = V$
    \end{itemize}
    On dit que $\rho$ est un modèle de $H$ $\iff$ $\llbracket H \rrbracket^\rho = V$

    \subsection*{Equivalence à un ensemble de formules $\Gamma$}
    \[H \equiv \Gamma \iff \forall \rho \in \mathbb{B}(\mathcal{P}), \Big(\forall G \in \Gamma, \llbracket G \rrbracket^\rho = V \Big) \Rightarrow \llbracket H \rrbracket^\rho = V\]

    \section*{Représentation des fonctions booléennes}
    \subsection*{Par des formules}
    Avec $f \in \mathbb{F}$ une fonction booléenne, $\exists H \in \mathcal{F}, \llbracket H \rrbracket = f$

    \subsection*{Par des formules sous forme normale}
    \begin{align*}
        l = p \lor \urcorner p :& \text{ littéral}\\
        C = \bigwedge_{i=1}^n l_i :& \text{ clause conjonctive}\\
        D = \bigvee_{i=1}^n C_i :& \text{ clause disjonctive}\\
        \bigwedge_{i=1}^n D_i :& \text{ formule normale conjonctive}\\
        \bigvee_{i=1}^n C_i :& \text{ formule normale disjonctive}\\
    \end{align*}
\end{multicols}
\end{document}