\documentclass[a4]{seminar}
\usepackage{advi}
\usepackage{advi-graphicx}
\usepackage{color}
\usepackage{amssymb}
%\usepackage[all]{xypic}
\usepackage{alltt}
\usepackage{url}

\slideframe{none}
\definecolor{slideblue}{rgb}{0,0,.5}
\definecolor{slidegreen}{rgb}{0,.5,0}
\definecolor{slidered}{rgb}{1,0,0}
\definecolor{slidegray}{rgb}{.6,.6,.6}
\definecolor{slidedarkgray}{rgb}{.4,.4,.4}
\definecolor{slidelightgray}{rgb}{.8,.8,.8}
\def\black#1{\textcolor{black}{#1}}
\def\white#1{\textcolor{white}{#1}}
\def\blue#1{\textcolor{slideblue}{#1}}
\def\green#1{\textcolor{slidegreen}{#1}}
\def\red#1{\textcolor{slidered}{#1}}
\def\gray#1{\textcolor{slidegray}{#1}}
\def\darkgray#1{\textcolor{slidedarkgray}{#1}}
\newpagestyle{fw}{}{\hfil\textcolor{slideblue}{\sf\thepage}\qquad\qquad}
\slidepagestyle{fw}
\newcommand{\sectiontitle}[1]{\centerline{\textcolor{slideblue}{\textbf{#1}}}
\par\medskip}
\newcommand{\slidetitle}[1]{{\textcolor{slideblue}{\strut #1}}\par
\vspace{-1.2em}{\color{slideblue}\rule{\linewidth}{0.04em}}}
\newcommand{\quadskip}{{\tiny\strut}\quad}
\newcommand{\dashskip}{{\tiny\strut}\enskip{ }}
\newcommand{\enskipp}{{\tiny\strut}\enskip}
\newcommand{\exclspace}{\hspace{.45pt}}
\newcommand{\notion}[1]{$\langle$#1$\rangle$}
\newcommand{\xnotion}[1]{#1}
\newcommand{\toolong}{$\hspace{-4em}$}

\begin{document}\sf
\renewcommand{\sliderightmargin}{0mm}
\renewcommand{\slideleftmargin}{20mm}
\renewcommand{\slidebottommargin}{6mm}

\setcounter{slide}{-1}
\begin{slide}
\slidetitle{\Large formalization \& decision procedures\toolong}

\red{Freek Wiedijk} \\
Radboud University Nijmegen

\green{`Diamant' day} \\
Radboud University Nijmegen \\
2005 10 28, 11:15
\end{slide}

\begin{slide}
\sectiontitle{intro}
\slidetitle{structure of the talk}
\begin{itemize}
\item[$\bullet$]
\textbf{formalization of mathematics}
\smallskip

\advirecord{a1}{
\green{Brouwer institute:}
\vspace{-\smallskipamount}
\begin{itemize}
\item
lambda calculus
\vspace{-\smallskipamount}

\item
\advirecord{a2}{formalization of mathematics}
\vspace{-\smallskipamount}

\item
intuitionistic mathematics

\end{itemize}
}
\medskip

\item[$\bullet$]
\textbf{decision procedures} \\
\textsl{procedures for automatically solving a well-defined class of problems\toolong}
\medskip

\advirecord{a3}{$\longrightarrow$\enskip talk by Jeremy Avigad}

\end{itemize}

\adviwait
\adviplay{a1}
\adviplay{a2}
\adviwait
\adviplay[slidered]{a2}
\adviwait
\adviplay[slidegreen]{a3}


\vspace{-1.5em}
\vfill
\end{slide}

\begin{slide}
\sectiontitle{formalization of mathematics}
\slidetitle{`formalization'}

\begin{center}
\medskip
\smallskip
\red{writing mathematics in a `computer language'}
\medskip

\adviwait
\strut computer checks the correctness \\
%\adviwait
\strut\phantom{computer} \rlap{keeps track of everything}\phantom{checks the correctness} \\
%\adviwait
\strut\phantom{computer} \rlap{bridges small gaps in the proofs}\phantom{checks the correctness}
\end{center}
\medskip
\smallskip
\adviwait

\blue{a very short history}

\begin{itemize}
\item[$\bullet$]
1910--1913\quad Russell \& Whitehead, Principia Mathematica
%\adviembed{xview -fullscreen pics/principia.jpg}
%\adviwait
%
%\item[$\bullet$]
%\strut 1967--1976\quad N.G.~de Bruijn, \green{Automath}
%
\end{itemize}

\newpagestyle{fw0}{}{}
\slidepagestyle{fw0}
\vfill
\break

\vbox to 0pt{
\vspace{-12.77em}
\centerline{\hspace{.85em}\includegraphics[width=40.1em]{pics/principia.eps}}
\vss
}

\end{slide}

\slidepagestyle{fw}
\setcounter{slide}{1}

\begin{slide}
\sectiontitle{formalization of mathematics}
\slidetitle{`formalization'}

\begin{center}
\medskip
\smallskip
\red{writing mathematics in a `computer language'}
\medskip

%\adviwait
\strut computer checks the correctness \\
%\adviwait
\strut\phantom{computer} \rlap{keeps track of everything}\phantom{checks the correctness} \\
%\adviwait
\strut\phantom{computer} \rlap{bridges small gaps in the proofs}\phantom{checks the correctness}
\end{center}
\medskip
\smallskip
%\adviwait

\blue{a very short history}

\begin{itemize}
\item[$\bullet$]
1910--1913\quad Russell \& Whitehead, Principia Mathematica
%\adviwait
%\adviembed{xview -fullscreen /home/freek/talks/dagen/pics/principia.jpg}
%\adviwait

\item[$\bullet$]
\strut 1967--1976\quad N.G.~de Bruijn, \green{Automath}

\end{itemize}

\vfill
\end{slide}

\begin{slide}
\slidetitle{four kinds of mathematics in the computer}

\begin{itemize}
\item[$\bullet$]
\textbf{numerical mathematics}\quad experimentation, visualization
$$\advirecord{b5}{\green{\phantom{\sqrt{x^2}}\llap{$\displaystyle {1\over 3}$} \;=\; \rlap{$0.3333333333$}\hspace{6em}}}$$
\item[$\bullet$]
\textbf{computer algebra systems}\quad CAS
$$\advirecord{b6}{\green{\sqrt{x^2} \;=\; \rlap{$x$}\hspace{6em}}}$$
\item[$\bullet$]
\textbf{automated theorem proving}\quad ATP 
\smallskip
\vspace{.5\smallskipamount}

\advirecord{b3}{currently mainly about solving logical puzzles}
\vspace{.5\smallskipamount}
\medskip

\item[\advirecord{b2}{$\bullet$}\adviplay{b2}]
\advirecord{b1}{\textbf{proof formalization}}\adviplay{b1}
\end{itemize}
\adviwait
\adviplay{b5}
\adviwait
\adviplay{b6}
\adviwait
\adviplay[slidegreen]{b3}
\adviwait
\adviplay[slidered]{b1}
\adviplay[slidered]{b2}

\vfill
\end{slide}

\begin{slide}
\slidetitle{state of the art: the most impressive that we can currently do}

\red{Fundamental Theorem of Algebra} \\
\begin{tabular}{ll}
Mizar & Robert Milewski, 2000 \\
\noalign{\vspace{-\smallskipamount}}
HOL Light$\quad$ & John Harrison, 2000 \\
\noalign{\vspace{-\smallskipamount}}
Coq & Herman Geuvers e.a., 2000
\end{tabular}
\smallskip
\adviwait

\red{Jordan Curve Theorem} \\
\begin{tabular}{ll}
HOL Light$\quad$ & Tom Hales, 2005 \\
\noalign{\vspace{-\smallskipamount}}
Mizar & \textsl{many people}, 2005
\end{tabular}
\smallskip
\adviwait

\red{Prime Number Theorem} \\
\begin{tabular}{ll}
\strut\rlap{Isabelle}\phantom{HOL Light$\quad$} & Jeremy Avigad, 2004
\end{tabular}
\smallskip
\adviwait

\red{Four Color Theorem} \\
\begin{tabular}{ll}
\strut\rlap{\advirecord{c}{Coq}\adviplay{c}}\phantom{HOL Light\quad} & Georges Gonthier, 2004
\end{tabular}
\smallskip
\adviwait
\adviplay[slidegreen]{c}

\vfill
\end{slide}

\begin{slide}
\slidetitle{de Bruijn criterion}

\red{can we \textbf{trust} formalized mathematics?}
\bigskip
\adviwait
\vbox to 0pt{
\vspace{-2.6em}
\hfill\includegraphics[width=6em]{pics/debruijn.eps}
\vss
}

\vspace{-\bigskipamount}
{de Bruijn criterion\enskip =}

\blue{correctness of \textbf{small} part of the program (`kernel') \\ guarantees the correctness of all the mathematics}

%`kernel' that checks the rules of the logic \\
%\adviwait
%possibility of independent checkers
\bigskip
\adviwait

\green{HOL Light kernel}

\begin{tabular}{rl}
643 & lines of program code \\
\noalign{\vspace{-\smallskipamount}}
10 & pages of program source listing (including comments)
\end{tabular}
\bigskip
\medskip
\adviwait

\blue{essential parts of this kernel proved correct using HOL Light itself}

\vspace{-1.5em}
\vfill
\end{slide}

\begin{slide}
\slidetitle{philosophical objections}

\begin{itemize}
\item[$\bullet$]
\textbf{irrelevant:}
%\adviwait

bugs in the checker \\
\adviwait
inconsistency of the logic \\
\adviwait
hardware malfunction
\medskip
\adviwait

\item[$\bullet$]
\textbf{relevant:}

correctness of the \red{definitions}
\bigskip
\medskip
\adviwait

\green{Isabelle's former definition of prime number}
\smallskip

$-p$ and $-1$ are also divisors of $p$ \\
with the former definition there were no prime numbers

\end{itemize}

\vfill
\end{slide}

\begin{slide}
\slidetitle{six systems for formalizing mathematics}
\vspace{-.2\bigskipamount}
\begin{center}
\begin{tabular}{ll}
\advirecord{d1}{HOL Light}\adviplay{d1}$\hspace{1em}$ & the most effective system of the moment \adviwait\\
Mizar & the most mathematical system of the moment \adviwait\\
\advirecord{d2}{Isabelle}\adviplay{d2} & the best of HOL and Mizar combined \adviwait\\
\advirecord{d3}{Coq}\adviplay{d3} & the most expressive system of the moment \adviwait\\
\advirecord{d4}{Nuprl}\adviplay{d4} & the US counterpart of Coq \adviwait\\
\advirecord{d5}{PVS}\adviplay{d5} & what most computer scientists use
\end{tabular}
\end{center}
\bigskip
\smallskip
\adviwait

\adviplay[slidered]{d1}
\adviplay[slidered]{d2}
\red{higher order logic}
\adviwait
%\adviplay[slidered]{d5}
%\adviwait

\adviplay[slidegreen]{d3}%
\adviplay[slidegreen]{d4}%
\green{type theory}

\vfill
\end{slide}

\begin{slide}
\slidetitle{three kinds of foundations}

\begin{itemize}
\item[$\bullet$]
\textbf{set theory}\quad \green{Mizar}

full ZFC set theory
(`everything is a set') \\
objects are untyped
\smallskip
\adviwait

\item[$\bullet$]
\textbf{higher order logic}\quad \green{HOL, Isabelle, PVS}

weak version of set theory \\
(only finitely many times a power set from the natural numbers) \\
objects are typed
\smallskip
\adviwait

\item[$\bullet$]
\textbf{type theory}\quad \green{Coq, Nuprl}

as expressive as full ZFC set theory, but intuitionistic \\
objects are typed \\
inductive types
(`free algebra' is a primitive) %\\
%calculating is primitive

\end{itemize}

\vspace{-1em}
\vfill
\end{slide}

\begin{slide}
\slidetitle{intuitionism!}
intuitionism encodes \red{computability} in the logic
\begin{center}
\green{$\exists\, x\, \dots$}\quad means\quad \green{there is an \textsl{algorithm} to compute $x$ such that \dots}
\end{center}
%\adviwait

%intuitionism popular in theoretical computer science
\bigskip
\medskip
\adviwait

\textbf{intermediate value theorem is not provable}

\vbox to 0pt{
\vspace{-2\bigskipamount}
\hfill
\includegraphics[width=13.5em]{pics/Tall96Fig10.eps}
\hspace{-6em}
\vss
}
\vspace{-\bigskipamount}
\adviwait

provable if the function is sufficiently often $\ne 0$ \\
\adviwait
provable if the function is a polynomial \\
\adviwait
provable that the value gets arbitrarily close to $0$
\bigskip
\adviwait

\blue{a very short history}
\begin{itemize}
\item[$\bullet$]
1907\quad L.E.J. Brouwer: intuitionism
\adviwait

\item[$\bullet$]
1967\quad Errett Bishop: \red{Bishop-style {constructivism}}

\end{itemize}

\vspace{-2em}
\vfill
\end{slide}

\begin{slide}
\slidetitle{state of the art: top 100 of theorems}

\begingroup
\setlength{\tabcolsep}{2pt}
\def\arraystretch{1}
\begin{tabular}{rl}
1. & \advirecord{g2}{The Irrationality of the Square Root of 2}\adviplay{g2} \advirecord{g3}{\enskip $\leftarrow$ \textsl{all systems}} \\
2. & Fundamental Theorem of Algebra \advirecord{g4}{\enskip $\leftarrow$ HOL, Mizar,
Coq} \\
3. & The Denumerability of the Rational Numbers \advirecord{g5}{\enskip $\leftarrow$ HOL, Mizar, Isabelle}\toolong \\
4. & Pythagorean Theorem \advirecord{g6}{\enskip $\leftarrow$ HOL, Mizar, Coq} \\
5. & Prime Number Theorem \advirecord{g7}{\enskip $\leftarrow$ Isabelle} \\
6. & G\"odel's Incompleteness Theorem \advirecord{g8}{\enskip $\leftarrow$ HOL,
Coq, nqthm} \\
7. & Law of Quadratic Reciprocity \advirecord{g9}{\enskip $\leftarrow$ Isabelle, nqthm} \\
8. & The Impossibility of Trisecting the Angle and Doubling the Cube \advirecord{g10}{\enskip $\leftarrow$ HOL}\toolong \\
9. & \rlap{\advirecord{g12}{The Area of a Circle}}\advirecord{g1}{\textsl{The Area of a Circle}}\adviplay{g12} \\
10. & Euler's Generalization of Fermat's Little Theorem \advirecord{g11}{\enskip $\leftarrow$ HOL, Mizar, Isabelle}\toolong \\
\dots & \dots
\end{tabular}
\endgroup
\adviwait

\begin{center}
\green{64\% formalized} \\
\adviplay[white]{g12}
\adviplay{g1}
\adviplay[slidered]{g3}
\adviplay[slidered]{g4}
\adviplay[slidered]{g5}
\adviplay[slidered]{g6}
\adviplay[slidered]{g7}
\adviplay[slidered]{g8}
\adviplay[slidered]{g9}
\adviplay[slidered]{g10}
\adviplay[slidered]{g11}
%\adviwait
\blue{\url{http://www.cs.ru.nl/~freek/100/}}
\end{center}

\vspace{-1pt}
\vfill
\end{slide}

\begin{slide}
\slidetitle{state of the art: what does it look like?}
formalization = human-computer symbiosis
\medskip

\red{two main proof styles}
%\adviwait
\begin{itemize}
\item[$\bullet$]
\textbf{procedural style}\quad \advirecord{e1a}{\rlap{HOL, Coq, Nuprl, PVS}}\advirecord{e1b}{HOL, \textbf{Coq}, Nuprl, PVS}\adviplay[slidegreen]{e1a}

computer is doing the proof under the direction of the human \\
proofs can be terse \\
proof looks like unreadable computer code
\smallskip
%\adviwait

\item[$\bullet$]
\textbf{declarative style}\quad \advirecord{e2a}{\rlap{Mizar, Isabelle}}\advirecord{e2b}{\textbf{Mizar}, Isabelle}\adviplay[slidegreen]{e2a}

the human is writing the proof checked by the computer \\
proofs more verbose \\
more writing from the human needed

\end{itemize}
\adviwait
\adviplay[white]{e1a}\adviplay[slidegreen]{e1b}
\adviplay[white]{e2a}\adviplay[slidegreen]{e2b}

\vfill
\end{slide}

\begin{slide}
\slidetitle{example of a Coq formalization}

\begin{alltt}\small
Lemma \green{sqrt_mult}:
 \red{forall x y:R, 0 <= x -> 0 <= y -> sqrt (x * y) = sqrt x * sqrt y.}\toolong
Proof.
 \blue{intros x y H1 H2;
 apply
  (Rsqr_inj (sqrt (x * y)) (sqrt x * sqrt y)
    (sqrt_positivity (x * y) (Rmult_le_pos x y H1 H2))
    (Rmult_le_pos (sqrt x) (sqrt y) (sqrt_positivity x H1)
      (sqrt_positivity y H2)));
 rewrite Rsqr_mult; 
 repeat rewrite Rsqr_sqrt;
 [ ring | assumption | assumption | apply (Rmult_le_pos x y H1 H2) ].}\toolong
Qed.
\end{alltt}

\vfill
\end{slide}

\begin{slide}
\slidetitle{example of a Mizar formalization}

\begin{alltt}\small
theorem \green{Th97}:
 \red{0 <= x & 0 <= y implies sqrt (x*y) = sqrt x * sqrt y}
proof
 \blue{assume \gray{A1:} 0 <= x & 0 <= y;
 then \gray{A2:} 0 <= x*y \gray{by Th19};
 then \gray{A3:} (sqrt(x*y))^2 = x*y \gray{by Def4}
   .= (sqrt x)^2*y \gray{by A1,Def4}
   .= (sqrt x)^2*(sqrt y)^2 \gray{by A1,Def4}
   .= (sqrt x*sqrt y)^2 \gray{by Th68};
 0 <= sqrt x & 0 <= sqrt y \gray{by A1,Def4};
 then \gray{A4:} 0 <= sqrt(x*y) & 0 <= sqrt x*sqrt y \gray{by A2,Def4,Th19};
 thus sqrt(x*y) = sqrt((sqrt x*sqrt y)^2) \gray{by A2,A3,Def4}
   .= sqrt x*sqrt y \gray{by A4,Lm5;}}
end;
\end{alltt}

\vfill
\end{slide}

\begin{slide}
\slidetitle{state of the art: how difficult is it?}

N.G. de Bruijn:
\begin{quote}
\green{
{A very important thing that can be concluded from all writing experiments is
the {constancy of the loss factor.}  The loss factor expresses what we loose in
shortness when translating very meticulous `ordinary' mathematics into
Automath.  %This factor may be quite big $\,$[$\,$\dots]$\,$ but it is
}%constant: it does not increase if we go further in the book.}
}
\end{quote}
\bigskip
\adviwait

the de Bruijn factor \advirecord{f}{in space:} \adviwait about \red{4 times} as long
\adviwait
\adviplay{f}
\adviwait

the de Bruijn factor in time: about \red{1 week/textbook page}

\vfill
\end{slide}

\begin{slide}
\slidetitle{why isn't formalization of mathematics bigger?}

\begin{itemize}
\item[\advirecord{g1a}{$\bullet$}]
\advirecord{g1b}{it does not have a good application}
\adviplay{g1a}\adviplay{g1b}
\adviwait
\adviplay[slidelightgray]{g1a}\adviplay[slidelightgray]{g1b}
\item[\advirecord{g2a}{$\bullet$}]
\advirecord{g2b}{it does not look like mathematics}
\adviplay{g2a}\adviplay{g2b}
\adviwait
\adviplay[slidelightgray]{g2a}\adviplay[slidelightgray]{g2b}
\item[$\bullet$]
formalizing trivialities is just too much work
\end{itemize}
\begin{eqnarray*}
x=i/n\;,\;\; n=m+1 &\red{\vdash}& n!\cdot x=i\cdot m! \\
\noalign{\smallskip}
{k\over n}\ge 0 &\red{\vdash}& \left|{n-k\over n}-1\right|={k\over n} \\
n\ge 2\;,\;\; x={1\over n+1} &\red{\vdash}& {x\over 1-x}<1 \adviwait\\
\noalign{\medskip\smallskip}
\quad 0 \le n \le \big({K \over 2}\big)\, x \;,\;\; C > 0 \;,\;\; 0 < \varepsilon < 1 &\red{\vdash}& \Big(1 + {\varepsilon \over 3(C + 3)}\Big)\, n < K x
\end{eqnarray*}

\vfill
\end{slide}

\begin{slide}
\sectiontitle{decision procedures}
\slidetitle{don't expect intelligent questions from computers}

\green{Paul J. Cohen, Arnold Neumaier, and probably many mathematicians:}
\bigskip

\begin{center}
\green{`}just have the computer read normal \textrm{\LaTeX}\phantom{'} \\
\strut\phantom{`}\red{it can ask questions if it does not understand}\green{'}
\medskip
\adviwait

{\small `also use this for ambiguities in formulas'}
\end{center}
\bigskip
\bigskip
\adviwait

\textbf{wrong mental model}, computers do not work like that
\adviwait

so what is it that computers \textbf{can} `understand'?

\vfill
\end{slide}

\begin{slide}
\slidetitle{three types of proof automation}

\begin{itemize}
\item[$\bullet$]
\textbf{basic automation} %\\
%`apply a bunch of lemmas as much as possible'
\medskip\smallskip %\bigskip
\adviwait

\item[$\bullet$]
\textbf{proof search} \\
\textsl{automated theorem proving}
\smallskip

general, \green{rather weak}
\medskip
\smallskip
\adviwait

\item[$\bullet$]
\textbf{decision procedures}
\smallskip

\green{specific}, {very useful}

\end{itemize}

\vfill
\end{slide}

\begin{slide}
\slidetitle{a first kind of automation: \textbf{basic automation}}
%formalizations always have the form of a long list of lemmas$\,+\,$proofs
%\medskip

systems often keep a \red{database of lemmas} with rules of a specific shape
\begin{itemize}
\item[$\bullet$]
\green{rewrite rules}\hfill \advirecord{n2}{\texttt{simp}}
$$\forall \vec{x}.\, \big(t_1(\vec{x}) = t_2(\vec{x})\big)$$
\item[$\bullet$]
\green{generalized implications (for backward chaining)}\hfill \advirecord{n1}{\texttt{auto}}
$$\forall \vec{x}.\, \big(\phi_1(\vec{x}) \land \dots \land \phi_n(\vec{x}) \to \psi(\vec{x})\big)$$
\end{itemize}
\smallskip

and have a {command} that `applies' those as much as possible\toolong
\bigskip
\adviwait

\blue{implementations in proof assistants}
\begin{center}
\begin{tabular}{lcl}
Isabelle &&  \green{\texttt{simp}} \\
\noalign{\vspace{-\smallskipamount}}
Coq && \green{\texttt{auto}} %, \green{\texttt{intuition}}
\end{tabular}
\end{center}
%\adviplay[slidegreen]{n1}
%\adviplay[slidegreen]{n2}

\vspace{-1.5em}
\vfill
\end{slide}

\begin{slide}
\slidetitle{a second kind of automation: \textbf{proof search}}

two \red{search strategies}
\smallskip
\begin{itemize}
\item[$\bullet$]
\textbf{resolution}

work from the assumptions towards the conclusion
\smallskip

\item[$\bullet$]
\textbf{tableaux methods}

work from the conclusion back to the assumptions

\end{itemize}
\bigskip
%\adviwait

\blue{implementations in proof assistants}
\begin{center}
\begin{tabular}{lcl}
HOL Light && \green{\texttt{MESON\char`\_TAC}} \\
\noalign{\vspace{-\smallskipamount}}
Isabelle && \green{\texttt{blast}}
\end{tabular}
\end{center}

\vfill
\end{slide}

\begin{slide}
\slidetitle{a third kind of automation: \textbf{decision procedures}}

{well-defined class of statements} \\
(explicit list of functions and predicates that can be used)
\medskip

\red{decidable} whether a statement in the class is provable or not
\bigskip
\adviwait

{decision procedure}:\enskip \green{command} in the system that implements this
%\adviwait
%and proves it if it is
\bigskip
\medskip
\adviwait

\blue{example}
$$f(f(x) - f(y)) \ne f(z) \;\land\; y \le x \;\land\; y \ge x + z \;\Rightarrow\; z < 0\adviwait$$

\green{proved at the push of a button}

\vfill
\end{slide}

\begin{slide}
\slidetitle{\textbf{decision procedures 1:} arithmetic in the real numbers}

first order statements involving $\advirecord{i1}{+}$ $-$ $\advirecord{i2}{\,\cdot\,}$ $\div$ $\,=\,$ $\le$ $<$
\medskip

\adviplay{i1}%
\adviplay{i2}%
%\adviwait
\adviplay[slidered]{i1}%
\adviplay[slidered]{i2}%
%\adviwait
\blue{theory of real-closed fields} \\
complete \& decidable theory
\medskip
\adviwait

first proved decidable by Alfred Tarski\adviwait\qquad \green{$\longrightarrow$\enskip decidability of geometry\toolong} \\
\adviwait
\red{cylindrical algebraic decomposition\quad CAD} \\
%\adviwait
complexity: doubly exponential
\bigskip
\adviwait

\green{kissing problem}:
{how many spheres fit around a sphere in $n$ dimensions?}\hfill
\vbox to 0pt{
\vspace{-.5em}
\hspace{24em}\includegraphics[width=6em]{pics/kissing.eps}
\vss
}

\vspace{-\bigskipamount}
\begin{tabular}{cll}
& $n=2\enskip$ & $6$ \\
\noalign{\vspace{-\smallskipamount}}
& $n=3$ & $12$ \\
\noalign{\vspace{-\smallskipamount}}
& $n=4$ & $24$ or $25$?
\end{tabular}

\vspace{-1em}
\vfill
\end{slide}

\begin{slide}
\slidetitle{quantifier elimination}
$$\begin{array}{c}
\advirecord{j1}{{\advirecord{j2}{\forall \advirecord{j3}{x}\in{\mathbb R}\,.\!}}}\,\; a\,\advirecord{j4}{x}^2 + b\,\advirecord{j5}{x} + c > 0
\adviplay{j2}
\adviplay{j3}
\adviplay{j4}
\adviplay{j5}
\adviwait\\
\noalign{\smallskip}
\Leftrightarrow \\
\noalign{\smallskip}
a > 0 \;\land\; b^2 - 4 a c < 0 \;\;\lor\;\; a = 0 \;\land\; b = 0 \;\land\; c > 0
\end{array}
$$
\adviwait
\adviplay[slidered]{j1}%
\adviplay[slidered]{j2}%
\adviplay[slidered]{j3}%
%\adviwait
%\adviplay[slidegreen]{j3}%
%\adviplay[slidegreen]{j4}%
%\adviplay[slidegreen]{j5}%

eliminates the \red{$\forall$} quantifier and its variable
from the formula \\
%\adviwait
this kind of \blue{quantifier elimination} is systematically possible
\bigskip
\adviwait

\green{iterated quantifier elimination} \\
{leads to formula without variables\enskip$\longrightarrow$\enskip just comparisons of numbers}

\vfill
\end{slide}

\begin{slide}
\slidetitle{\textbf{decision procedures 2:} linear arithmetic}

first order statements involving \red{$+$} $-$ $\,=\,$ $\le$ $<\,$ and \\
\strut\phantom{first order statements involving} multiplication by rational constants \\
{no arbitrary multiplication} \\
only {linear equalities and inequalities}
\medskip
\adviwait

\blue{example}
$$\exists\, x, y\in{\mathbb R}\;.\,\; 0 \le x \le y - 3 \;\land\; x + y \le 5 \;\land\; 2y - 3x \le 5\medskip\adviwait$$

\blue{implementations in proof assistants}
\begin{center}
\begin{tabular}{lcl}
HOL Light && \green{\texttt{ARITH\char`\_TAC}} \\
\noalign{\vspace{-\smallskipamount}}
Isabelle && \green{\texttt{arith}} \\
\noalign{\vspace{-\smallskipamount}}
Coq && \green{\texttt{omega}}
\end{tabular}
\end{center}

\vspace{-.5em}
\vfill
\end{slide}

\begin{slide}
\slidetitle{real numbers versus integers}

\begin{center}
\begin{tabular}{rccc}
& \large ${\mathbb R}$ && \large ${\mathbb N}$ \\
\noalign{\medskip}
& \green{real-closed fields} && \green{Peano arithmetic} \\
\noalign{\vspace{-\smallskipamount}}
\textbf{full theory}$\quad$ & \blue{decidable} && \blue{undecidable} \\
\noalign{\vspace{-\smallskipamount}}
& \red{CAD} && \\
\noalign{\medskip}
&&& \green{Presburger arithmetic} \\
\noalign{\vspace{-\smallskipamount}}
\textbf{linear arithmetic}$\quad$ & \blue{decidable} && \blue{decidable} \\
\noalign{\vspace{-\smallskipamount}}
& \red{Fourier-Motzkin} && \\
\end{tabular}
\end{center}

\vfill
\end{slide}

\begin{slide}
\slidetitle{Fourier-Motzkin, by example}

\blue{quantifier elimination} of
$$\red{\exists\, y.}\,\; 0 \le x \;\land\; x \le y - 3 \;\land\; x + y \le 5 \;\land\; 2y - 3x \le 5\adviwait$$

put variable $y$ everywhere all by itself on right or left hand side\adviwait
$$\exists\, y.\,\; \blue{0 \le x} \;\land\; \green{x + 3} \le \red{y} \;\land\; \red{y} \le \green{5 - x} \;\land\; \red{y} \le \green{{5\over 2} + {3\over 2} x}\adviwait$$

compare all lower bounds with all upper bounds\adviwait
$$\blue{0 \le x} \;\land\; \green{x + 3} \le \green{5 - x} \;\land\; \green{x + 3} \le \green{{5\over 2} + {3\over 2} x}\adviwait$$

we now have eliminated the variable \red{$y$}

\vfill
\end{slide}

\begin{slide}
\slidetitle{\textbf{decision procedures 3:} the universal formulas of real arithmetic}

\red{sum of squares decomposition}
\medskip
\adviwait
$${\forall x_1 \dots\, x_n.\; f(x_1,\dots,x_n) \ge 0}$$
follows from
$$f(x_1,\dots,x_n) = \sum_k \big(g_k(x_1,\dots,x_n)\big)^2$$ %\adviwait$$

such decompositions can be found by \red{semidefinite programming}
\medskip

$\longrightarrow$\enskip \green{decision procedure}
\bigskip
\medskip
\adviwait

\blue{implementations in proof assistants}
\begin{center}
\begin{tabular}{lcl}
HOL Light && \green{\texttt{REAL\char`\_SOS}}
\end{tabular}
\end{center}

\vspace{-2em}
\vfill
\end{slide}

\begin{slide}
\slidetitle{\textbf{decision procedures 4:} combining decision procedures}

separate decision procedures for universal statements about
\begin{quote}
\begin{quote}
\green{
arithmetic \\
%tuples \\
arrays \\
bit-vectors \\
uninterpreted functions \\
\dots
}
\end{quote}
\end{quote}
\medskip
\adviwait
integrate all of them in one master decision procedure
\smallskip

\begin{itemize}
\item[\advirecord{m1}{$\bullet$}]
\advirecord{m2}{\textbf{Nelson-Oppen}}
\adviplay{m1}
\adviplay{m2}

\item[$\bullet$]
\textbf{Shostak}
\medskip
\smallskip

\end{itemize}
\adviwait
{the story of PVS and ICS}
\adviwait
\adviplay[slideblue]{m1}
\adviplay[slideblue]{m2}

%signatures of the separate theories have to be \red{disjunct}
%\adviwait

\vspace{-1em}
\vfill
\end{slide}

\begin{slide}
\slidetitle{Craig's interpolation theorem}
$$\phi_1 \vdash \phi_2$$
implies that there is an \red{interpolant} $\psi$
with only symbols \green{both} in $\phi_1$ and $\phi_2$ such that
$$\phi_1 \vdash \psi \quad\mbox{and}\quad \psi \vdash \phi_2\bigskip\adviwait$$

\blue{Craig-Robinson variant}
\medskip
$$\phi_1, \phi_2 \vdash \bot\smallskip$$
implies that there is a $\psi$ with only symbols both in $\phi_1$ and $\phi_2$ such that
$$\phi_1 \vdash \psi \quad\mbox{and}\quad \phi_2 \vdash \neg\psi$$

\vspace{-2.5em}
\vfill
\end{slide}

\begin{slide}
\slidetitle{Nelson-Oppen, by example}
$$\green{f(v - 1) - 1 = v + 1 \;\land\; f(u) + 1 = u - 1 \;\land\; u + 1 = v \;\red{\;\Rightarrow\; \bot}}$$
combines decision procedures of arithmetic and uninterpreted functions
\smallskip
\adviwait
\begin{enumerate}
\item
introduce new variables plus equalities such that all conjuncts
only involve {one} of the component theories
\begin{quote}
\smallskip
$\green{\begin{array}{l}
\red{v_1} = v - 1 \;\land\; \red{v_2} = f(v_1) \;\land\; \red{v_3} = f(u) \;\land\;\\
v_2 = v + 1 \;\land\; v_3 + 1 = u - 1 \;\land\; u + 1 = v
\end{array}}\adviwait$
\smallskip
\end{quote}

\item
repeatedly infer equalities in each of the separate
component theories and add them to the set of conjuncts\adviwait
\begin{quote}
\smallskip
$\green{\begin{array}{l}
v_1 = v - 1 \;\land\; v_2 = v + 1 \;\land\; v_3 + 1 = u - 1 \;\land\; u + 1 = v \adviwait\\
\qquad\red{\Rightarrow u = v_1}
\end{array}}$
\smallskip
\end{quote}
\end{enumerate}

\vspace{-2em}
\vfill
\end{slide}

\begin{slide}
\slidetitle{Nelson-Oppen, by example (continued)}
\begin{itemize}
\item[]
\begin{quote}
\smallskip
$\green{\begin{array}{l}
v_2 = f(v_1) \;\land\; v_3 = f(u) \blue{\;\;\land\;\; u = v_1}\adviwait\\
\qquad\red{\Rightarrow v_2 = v_3}\adviwait
\end{array}}$
\medskip

$\green{\begin{array}{l}
v_1 = v - 1 \;\land\; v_2 = v + 1 \;\land\; v_3 + 1 = u - 1 \;\land\; u + 1 = v \\
\blue{\land\;\, u = v_1 \;\land\; v_2 = v_3}\adviwait\\
\qquad\red{\Rightarrow \bot}
\end{array}}$
\medskip
\smallskip
%\adviwait
\end{quote}
\qquad$\!${\small ($v_2 = v + 1 = u + 2$ and $v_3 = u - 2$, so they cannot be equal)}
\medskip
\adviwait

\item[3.]
if we manage to derive a contradiction in one of the theories then the original conjunction was contradictory; if not then it is satisfiable

\end{itemize}

\vfill
\end{slide}

\begin{slide}
\sectiontitle{extro}
\slidetitle{so when will mathematicians start formalizing their mathematics?}

\red{`killer app' for formalization has not yet been found}
\medskip\adviwait
\begin{itemize}
\item[$\bullet$]
the mathematics will be guaranteed to be fully \green{correct}
\adviwait
\item[$\bullet$]
the mathematics will be guaranteed to be fully \green{explicit}
\end{itemize}
\bigskip
\medskip
\smallskip
\adviwait

\blue{Jeremy Avigad:}
\medskip
\smallskip

things become interesting when
\begin{center}
\green{time for formalization {\large $\;<\;$} time for referee checking}
\end{center}

\vfill
\end{slide}

\end{document}