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

% further packages required for unusual symbols (see also
% isabellesym.sty), use only when needed

%\usepackage{amssymb}
  %for \<leadsto>, \<box>, \<diamond>, \<sqsupset>, \<mho>, \<Join>,
  %\<lhd>, \<lesssim>, \<greatersim>, \<lessapprox>, \<greaterapprox>,
  %\<triangleq>, \<yen>, \<lozenge>

%\usepackage{eurosym}
  %for \<euro>

%\usepackage[only,bigsqcap]{stmaryrd}
  %for \<Sqinter>

%\usepackage{eufrak}
  %for \<AA> ... \<ZZ>, \<aa> ... \<zz> (also included in amssymb)

%\usepackage{textcomp}
  %for \<onequarter>, \<onehalf>, \<threequarters>, \<degree>, \<cent>,
  %\<currency>

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

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

% for uniform font size
%\renewcommand{\isastyle}{\isastyleminor}


\begin{document}

\title{PSL: Proof Strategy Language for Isabelle/HOL}
\author{Yutaka Nagashima \\
  Data61, CSIRO / NICTA
  \footnote{NICTA is funded by the Australian Government through the Department
  of Communications and the Australian Research Council through the
  ICT Centre of Excellence Program.}
}
\maketitle

\begin{abstract}
Isabelle includes various automatic tools for finding proofs under certain conditions. 
However, for each conjecture, knowing which automation to use, and how to tweak its parameters, 
is currently labour intensive. 
We have developed a language, PSL \cite{DBLP:journals/corr/NagashimaK16},
designed to capture high level proof strategies.
PSL offloads the construction of human-readable fast-to-replay proof scripts to automatic search, 
making use of search-time information about each conjecture. 
Our preliminary evaluations show that 
PSL reduces the labour cost of interactive theorem proving.
This submission contains the implementation of PSL and an example theory file,
Example.thy, showing how to write poof strategies in PSL.
\end{abstract}

%\tableofcontents

% sane default for proof documents
\parindent 0pt\parskip 0.5ex

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

% optional bibliography
\bibliographystyle{abbrv}
\bibliography{root}

\end{document}

%%% Local Variables:
%%% mode: latex
%%% TeX-master: t
%%% End:
