%Some LaTeX checking: no bad pratices
%\RequirePackage[l2tabu, orthodox]{nag}
%\RequirePackage[all,error]{onlyamsmath}
\RequirePackage{fixltx2e}

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

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

% lualatex
%\usepackage{spelling}
\usepackage{fullpage}
\usepackage{graphicx}
\usepackage{comment}


\usepackage{mdframed}
\usepackage{subcaption}

%% Pour composer des mathématiques
\usepackage{amsmath,amssymb, amsthm}
\usepackage{nicefrac}
\usepackage{tikz}
\usetikzlibrary{decorations, arrows, shapes, automata, mindmap, trees}
  %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{wasysym}

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

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

\usepackage[english]{babel}
% this should be the last package used
\usepackage{pdfsetup}

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

\hyphenation{Schlicht-krull}

\begin{document}

\title{Extensions to the Comprehensive Framework for Saturation Theorem Proving}
\author{Jasmin Blanchette \and Sophie Tourret}
\maketitle

\begin{abstract}
\noindent
This Isabelle/HOL formalization extends the \verb|Saturation_Framework| entry of
the \emph{Archive of Formal Proofs} with the following contributions:

\begin{itemize}
\item an application of the framework to prove Bachmair and Ganzinger's
  resolution prover \textsf{RP} refutationally complete, which was formalized
  in a more ad hoc fashion by Schlichtkrull et al.\ in the \emph{AFP} entry
  \verb|Ordered_Resultion_Prover|;

\item generalizations of various basic concepts formalized by Schlichtkrull et
  al., which were needed to verify \textsf{RP} and could be useful to formalize
  other calculi, such as superposition;

\item alternative proofs of fairness (and hence saturation and ultimately
  refutational completeness) for the eager and lazy given clause procedures
  (\textsf{GC} and \textsf{LGC}) based on invariance.
\end{itemize}
\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:
