1 \documentclass{sig-alternate}

     2   \pdfpagewidth=8.5truein

     3   \pdfpageheight=11truein

     4 \usepackage{times}

     5 \usepackage{isabelle}

     6 \usepackage{isabellesym}

     7 \usepackage{amsmath}

     8 \usepackage{amssymb}

     9 \usepackage{pdfsetup}

    10 \usepackage{tikz}

    11 \usepackage{pgf}

    12 \usepackage{stmaryrd}

    13 \usepackage{verbdef}

    14 \usepackage{longtable}

    15 \usepackage{mathpartir}

    16 \newtheorem{definition}{Definition}

    17 \newtheorem{proposition}{Proposition}

    18 \newtheorem{lemma}{Lemma}

    19 

    20 \urlstyle{rm}

    21 \isabellestyle{rm}

    22 \renewcommand{\isastyleminor}{\rm}%

    23 \renewcommand{\isastyle}{\normalsize\rm}%

    24 \renewcommand{\isastylescript}{\it}

    25 \def\dn{\,\triangleq\,}

    26 \verbdef\singlearr|---->|

    27 \verbdef\doublearr|===>|

    28 \verbdef\tripple|###|

    29 

    30 \renewcommand{\isasymequiv}{$\triangleq$}

    31 \renewcommand{\isasymemptyset}{$\varnothing$}

    32 %%\renewcommand{\isacharunderscore}{\mbox{$\_\!\_$}}

    33 \renewcommand{\isasymUnion}{$\bigcup$}

    34 

    35 \newcommand{\isasymsinglearr}{$\mapsto$}

    36 \newcommand{\isasymdoublearr}{$\Mapsto$}

    37 \newcommand{\isasymtripple}{\tripple}

    38 

    39 \newcommand{\numbered}[1]{\refstepcounter{equation}{\rm(\arabic{equation})}\label{#1}}

    40 

    41 \begin{document}

    42 

    43 \conferenceinfo{SAC'11}{March 21-25, 2011, TaiChung, Taiwan.}

    44 \CopyrightYear{2011}

    45 \crdata{978-1-4503-0113-8/11/03}

    46 

    47 \title{Quotients Revisited for Isabelle/HOL}

    48 \numberofauthors{2}

    49 \author{

    50 \alignauthor

    51 Cezary Kaliszyk\\

    52   \affaddr{University of Tsukuba, Japan}\\

    53   \email{kaliszyk@cs.tsukuba.ac.jp}

    54 \alignauthor

    55 Christian Urban\\

    56   \affaddr{Technical University of Munich, Germany}\\

    57   \email{urbanc@in.tum.de}

    58 }

    59 

    60 \maketitle

    61 

    62 \begin{abstract}

    63 Higher-Order Logic (HOL) is based on a small logic kernel, whose only

    64 mechanism for extension is the introduction of safe definitions and of

    65 non-empty types. Both extensions are often performed in quotient

    66 constructions. To ease the work involved with such quotient constructions, we

    67 re-implemented in the %popular 

    68 Isabelle/HOL theorem prover the quotient 

    69 package by Homeier. In doing so we extended his work in order to deal with 

    70 compositions of quotients and also specified completely the procedure 

    71 of lifting theorems from the raw level to the quotient level.

    72 The importance for theorem proving is that many formal

    73 verifications, in order to be feasible, require a convenient reasoning infrastructure 

    74 for quotient constructions.

    75 \end{abstract}

    76 

    77 %\category{D.??}{TODO}{TODO}

    78 

    79 \keywords{Quotients, Isabelle theorem prover, Higher-Order Logic}

    80 

    81 % generated text of all theories

    82 \bibliographystyle{abbrv}

    83 \input{session}

    84 

    85 

    86 

    87 \end{document}

    88 

    89 %%% Local Variables:

    90 %%% mode: latex

    91 %%% TeX-master: t

    92 %%% End: