add build manifest, update title page, fix svg files names
This commit is contained in:
parent
690ddb42f0
commit
ac0a90c0b1
19
.build.yml
Normal file
19
.build.yml
Normal file
@ -0,0 +1,19 @@
|
||||
image: debian/unstable
|
||||
packages:
|
||||
- biber
|
||||
- fonts-linuxlibertine
|
||||
- graphviz
|
||||
- inkscape
|
||||
- python3-pygments
|
||||
- texlive-extra-utils
|
||||
- texlive-fonts-extra
|
||||
- texlive-lang-french
|
||||
- texlive-pstricks
|
||||
- texlive-xetex
|
||||
sources:
|
||||
- https://git.zapashcanon.fr/zapashcanon/ter-report
|
||||
tasks:
|
||||
- build: |
|
||||
cd ter-report
|
||||
make
|
||||
ls main.pdf
|
3
.gitignore
vendored
3
.gitignore
vendored
@ -10,4 +10,5 @@
|
||||
*.cmx
|
||||
*.o
|
||||
src/svg-inkscape/
|
||||
*.dot.svg
|
||||
*_dot.svg
|
||||
*.toc
|
||||
|
4
Makefile
4
Makefile
@ -1,11 +1,11 @@
|
||||
IMG_DIR := img
|
||||
|
||||
DOT_FILES := $(wildcard $(IMG_DIR)/*.dot)
|
||||
SVG_FILES := $(DOT_FILES:$(IMG_DIR)/%.dot=$(IMG_DIR)/%.dot.svg)
|
||||
SVG_FILES := $(DOT_FILES:$(IMG_DIR)/%.dot=$(IMG_DIR)/%_dot.svg)
|
||||
|
||||
default: build clean
|
||||
|
||||
$(IMG_DIR)/%.dot.svg: $(IMG_DIR)/%.dot
|
||||
$(IMG_DIR)/%_dot.svg: $(IMG_DIR)/%.dot
|
||||
dot -Tsvg $< -o $@
|
||||
|
||||
build: $(SVG_FILES)
|
||||
|
1
README.md
Normal file
1
README.md
Normal file
@ -0,0 +1 @@
|
||||
# TER Report [](https://builds.sr.ht/~zapashcanon/ter-report?)
|
16
src/bdd.tex
16
src/bdd.tex
@ -22,7 +22,7 @@
|
||||
\paragraph{}
|
||||
Représentons tout d'abord la formule $P$:
|
||||
\begin{center}
|
||||
\includesvg[width=100pt]{simple_bdd.dot.svg}
|
||||
\includesvg[width=100pt]{simple_bdd_dot.svg}
|
||||
\end{center}
|
||||
\paragraph{}
|
||||
Un diagramme de décision binaire a donc un sommet \enquote{de départ}, $P$ ici. Un sommet a soit deux arcs sortants, soit aucun. S'il en a deux, alors, il contient une \emph{variable propositionnelle} et dans ce cas, le \enquote{chemin à suivre} dépend de la valeur de vérité de la variable. Si la variable vaut $\bot$, on prend l'arc en pointillés, sinon, on prend l'autre. Si le sommet n'a aucun arc sortant, alors, il contient soit $\top$ soit $\bot$, ce qui correspond à la valeur de vérité de la formule représentée par ce diagramme dans le cas où on assigne aux variables les mêmes valeurs de vérités que celles que l'on a prises sur ce chemin.
|
||||
@ -30,12 +30,12 @@
|
||||
\paragraph{}
|
||||
Prenons un autre exemple, voilà un diagramme représentant la proposition $P \lor Q$:
|
||||
\begin{center}
|
||||
\includesvg[width=100pt]{simple_bdd2.dot.svg}
|
||||
\includesvg[width=100pt]{simple_bdd2_dot.svg}
|
||||
\end{center}
|
||||
\paragraph{}
|
||||
Il aurait aussi été possible de la représenter par celui-ci:
|
||||
\begin{center}
|
||||
\includesvg[width=100pt]{simple_bdd3.dot.svg}
|
||||
\includesvg[width=100pt]{simple_bdd3_dot.svg}
|
||||
\end{center}
|
||||
\paragraph{}
|
||||
On va en fait se donner un \emph{ordre} sur les variables et dès que l'on \enquote{aura le choix} entre deux variables, on prendra la plus petite des deux selon cet ordre. Par exemple, si l'on décide d'utiliser l'ordre lexicographique, alors, on aura le premier des deux diagrammes ci-dessus.
|
||||
@ -43,17 +43,17 @@
|
||||
\paragraph{}
|
||||
Une seconde chose à prendre en compte est le fait que l'on va éviter toute redondance dans nos diagrammes. Si deux sommets mènent au même résultat dans tous les cas, on va les fusionner. Sur notre exemple précédent, on peut par exemple fusionner les deux sommets $\top$:
|
||||
\begin{center}
|
||||
\includesvg[width=100pt]{simple_bdd4.dot.svg}
|
||||
\includesvg[width=100pt]{simple_bdd4_dot.svg}
|
||||
\end{center}
|
||||
\subsubsection{Simplification}
|
||||
\paragraph{}
|
||||
Enfin, si les deux arcs sortants d'un sommet mènent à la même chose, on va tout simplement supprimer ce sommet. Par exemple, la proposition $P \lor \neg P$ ne sera pas représentée comme ceci:
|
||||
\begin{center}
|
||||
\includesvg[width=50pt]{simple_bdd5.dot.svg}
|
||||
\includesvg[width=50pt]{simple_bdd5_dot.svg}
|
||||
\end{center}
|
||||
Mais comme cela:
|
||||
\begin{center}
|
||||
\includesvg[width=50pt]{simple_bdd6.dot.svg}
|
||||
\includesvg[width=50pt]{simple_bdd6_dot.svg}
|
||||
\end{center}
|
||||
En fait, on a en quelque sorte développé la fonction, elle est \enquote{partiellement calculée}. Dans le cas d'une tautologie ou d'une contradiction, on aurait même complètement calculé la valeur de la proposition.
|
||||
\subsection{Représentation formelle}
|
||||
@ -85,13 +85,13 @@
|
||||
\paragraph{}
|
||||
Une proposition sous FNI peut être représentée comme un arbre binaire, sur notre exemple précédent, cela donnerait le résultat suivant:
|
||||
\begin{center}
|
||||
\includesvg[width=150pt]{simple_bdd7.dot.svg}
|
||||
\includesvg[width=150pt]{simple_bdd7_dot.svg}
|
||||
\end{center}
|
||||
\paragraph{}
|
||||
% TODO oe
|
||||
On peut alors réduire l'arbre, c'est-à-dire que tout noeud ayant deux sous-arbres identiques sera supprimé:
|
||||
\begin{center}
|
||||
\includesvg[width=150pt]{simple_bdd8.dot.svg}
|
||||
\includesvg[width=150pt]{simple_bdd8_dot.svg}
|
||||
\end{center}
|
||||
\paragraph{}
|
||||
% TODO: déf. d'isomorphisme de graphes dans ce cas
|
||||
|
@ -1,27 +1,30 @@
|
||||
\begin{titlepage}
|
||||
\begin{center}
|
||||
\begin{center}
|
||||
|
||||
%\vspace*{0.1\textheight}
|
||||
\fontsize{25}{25}\scshape Partage d'implémentation, implémentation du partage:\\
|
||||
une bibliothèque fonctorisée de diagrammes de décision binaires
|
||||
\vspace*{0.1\textheight}
|
||||
\newcommand\important{\huge \scshape }
|
||||
\newcommand\notimportant{\Large}
|
||||
\newcommand\vspa[1]{\vspace*{#1\textheight}}
|
||||
|
||||
{\fontsize{18}{18}\calligra{Rapport de travaux de recherche par\\}}
|
||||
{\fontsize{28}{28}\scshape Léo \bsc{Andrès}\\}
|
||||
\vspace*{0.01\textheight}
|
||||
{\fontsize{18}{18}\calligra{\today\\}}
|
||||
\vspace*{0.03\textheight}
|
||||
{\fontsize{18}{18}\calligra{Master 1 Informatique\\}}
|
||||
\vspace*{0.03\textheight}
|
||||
{\includesvg{universite-paris-saclay.svg}}\\
|
||||
\vspace*{0.1\textheight}
|
||||
\important{} Partage d'implémentation, implémentation du partage:\\
|
||||
une bibliothèque fonctorisée de diagrammes de décision binaires
|
||||
|
||||
\begin{tikzpicture}[start chain=main going right]
|
||||
\vspa{0.1}
|
||||
|
||||
\node[on chain,align=center,draw=none](a1)
|
||||
{{\fontsize{18}{18}\calligra Sous la direction de} \\
|
||||
{\Large {Jean-Christophe~\bsc{Filliâtre}}}};
|
||||
\notimportant{} Rapport de travaux de recherche par\\
|
||||
\important{} Léo \bsc{Andrès}\\
|
||||
\vspa{0.02}
|
||||
\notimportant{} 6 mai 2019\\
|
||||
|
||||
\end{tikzpicture}
|
||||
\end{center}
|
||||
\vspa{0.1}
|
||||
|
||||
\notimportant{} Master 1 Informatique\\
|
||||
\vspa{0.05}
|
||||
\includesvg[width=100pt]{universite-paris-saclay.svg}\\
|
||||
|
||||
\vspa{0.1}
|
||||
|
||||
\notimportant{} Sous la direction de\\
|
||||
\important{} Jean-Christophe~\bsc{Filliâtre}
|
||||
|
||||
\end{center}
|
||||
\end{titlepage}
|
||||
|
Loading…
x
Reference in New Issue
Block a user