simon/sidekick
1
0
Fork 0
mirror of https://github.com/c-cube/sidekick.git synced 2026-01-28 04:14:50 -05:00
Code Issues Projects Releases Packages Wiki Activity Actions

Typos fix

Browse source
This commit is contained in:
Guillaume Bury 2017-09-04 16:08:51 +02:00
parent fb9c83aac9
commit 0bec9b7bec
2 changed files with 4 additions and 4 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

BIN
poster/poster.pdf
View file

Binary file not shown.

8
poster/poster.tex
View file

@ -113,11 +113,11 @@
\tblock{Problem Example}
{
\vspace{.2cm}
\vspace{.5cm}
\[
\begin{matrix}
\text{Are the following} & \quad & H1: & a = b & \quad & H2: & b = c \lor b = d \\
\text{hypotheses satisfible ?} & \quad & H3: & a <> d & \quad & H4: & a <> c \\
\text{hypotheses satisfiable ?} & \quad & H3: & a <> d & \quad & H4: & a <> c \\
\end{matrix}
\]
\includegraphics[height=33cm]{proof}
@ -128,7 +128,7 @@
\inputminted{ocaml}{theory_intf.ml}
}
\tblock{Proof generation}
\tblock{Proof Generation}
{
\begin{itemize}[label=\checkmark]
\item Each clause records its "history" which is the clauses
@ -141,7 +141,7 @@
\item Enables various proof outputs:
\begin{itemize}[label=$\bullet$]
\item Dot/Graphviz (see example above)
\item Coq (and soon dedukti) formal proofs
\item Coq (and soon Dedukti) formal proofs
\end{itemize}
\end{itemize}
}