\documentclass[11pt,a4paper]{article}
\usepackage[T1]{fontenc}
\usepackage{isabelle,isabellesym}
\usepackage{amsmath}
\usepackage{amssymb} 

% this should be the last package used
\usepackage{pdfsetup}

% urls in roman style, theory text in math-similar italics
\urlstyle{rm}
\isabellestyle{it}


\begin{document}

\title{The Sturm--Tarski Theorem}
\author{Wenda Li}
\maketitle

\begin{abstract}
  We have formalised the Sturm--Tarski theorem (also referred as the Tarski theorem): Given polynomials $p, q \in \mathbb{R}[x]$, the Sturm--Tarski theorem computes the sum of the signs of $q$ over the roots of $p$ by calculating some remainder sequences. Note, the better-known Sturm theorem is an instance of the Sturm--Tarski theorem when $q=1$. The proof follows the classic book by Basu et al. \cite{Basu:2006:ARA:1197095} and Cyril Cohen's work in Coq \cite{cohen_phd}. With the Sturm--Tarski theorem proved, it is possible to further build a quantifier elimination procedure for real numbers as Cohen did in Coq.
  Another application of the Sturm--Tarski theorem is to build sign determination procedures for polynomials at real algebraic points, as described in our formalisation of real algebraic numbers \cite{Li_CPP_16}.
\end{abstract}

%\tableofcontents

% include generated text of all theories
\input{session}

\bibliographystyle{abbrv}
\bibliography{root}

\end{document}
