\documentclass{sig-alternate} \pdfpagewidth=8.5truein \pdfpageheight=11truein\usepackage{times}\usepackage{isabelle}\usepackage{isabellesym}\usepackage{amsmath}\usepackage{amssymb}\usepackage{pdfsetup}\usepackage{tikz}\usepackage{pgf}\usepackage{stmaryrd}\usepackage{verbdef}\usepackage{longtable}\usepackage{mathpartir}\newtheorem{definition}{Definition}\newtheorem{proposition}{Proposition}\newtheorem{lemma}{Lemma}\urlstyle{rm}\isabellestyle{rm}\renewcommand{\isastyleminor}{\rm}%\renewcommand{\isastyle}{\normalsize\rm}%\renewcommand{\isastylescript}{\it}\def\dn{\,\triangleq\,}\verbdef\singlearr|---->|\verbdef\doublearr|===>|\verbdef\tripple|###|\renewcommand{\isasymequiv}{$\triangleq$}\renewcommand{\isasymemptyset}{$\varnothing$}%%\renewcommand{\isacharunderscore}{\mbox{$\_\!\_$}}\renewcommand{\isasymUnion}{$\bigcup$}\newcommand{\isasymsinglearr}{$\mapsto$}\newcommand{\isasymdoublearr}{$\Mapsto$}\newcommand{\isasymtripple}{\tripple}\newcommand{\numbered}[1]{\refstepcounter{equation}{\rm(\arabic{equation})}\label{#1}}\begin{document}\conferenceinfo{SAC'11}{March 21-25, 2011, TaiChung, Taiwan.}\CopyrightYear{2011}\crdata{978-1-4503-0113-8/11/03}\title{Quotients Revisited for Isabelle/HOL}\numberofauthors{2}\author{\alignauthorCezary Kaliszyk\\ \affaddr{University of Tsukuba, Japan}\\ \email{kaliszyk@cs.tsukuba.ac.jp}\alignauthorChristian Urban\\ \affaddr{Technical University of Munich, Germany}\\ \email{urbanc@in.tum.de}}\maketitle\begin{abstract}Higher-Order Logic (HOL) is based on a small logic kernel, whose onlymechanism for extension is the introduction of safe definitions and ofnon-empty types. Both extensions are often performed in quotientconstructions. To ease the work involved with such quotient constructions, were-implemented in the popular Isabelle/HOL theorem prover the quotient package by Homeier. In doing so we extended his work in order to deal with compositions of quotients and also specified completely the procedure of lifting theorems from the raw level to the quotient level.The importance for theorem proving is that many formalverifications, in order to be feasible, require a convenient reasoning infrastructure for quotient constructions.\end{abstract}%\category{D.??}{TODO}{TODO}\keywords{Quotients, Isabelle theorem prover, Higher-Order Logic}% generated text of all theories\input{session}% optional bibliography\bibliographystyle{abbrv}\bibliography{root}\end{document}%%% Local Variables:%%% mode: latex%%% TeX-master: t%%% End: