Quotient-Paper-jv/document/root.tex
author Cezary Kaliszyk <cezarykaliszyk@gmail.com>
Fri, 17 Feb 2012 15:23:38 +0100 (2012-02-17)
changeset 3123 998978623654
parent 3092 ff377f9d030a
child 3136 d003938cc952
permissions -rw-r--r--
Update from Isabelle Wed Feb 15 23:19:30
\documentclass{svjour3}
\usepackage{amsmath}
\usepackage{amssymb}
\usepackage{isabelle}
\usepackage{isabellesym}
\usepackage{tikz}
\usepackage{verbdef}
\usepackage{mathpartir}
\usepackage{pdfsetup}
\usepackage{times}
\usepackage{stmaryrd}
%\newtheorem{definition}{Definition}
%\newtheorem{proposition}{Proposition}
%\newtheorem{lemma}{Lemma}

\urlstyle{rm}
\isabellestyle{it}
\renewcommand{\isastyleminor}{\it}%
\renewcommand{\isastyle}{\normalsize\it}%
\renewcommand{\isastylescript}{\it}
\def\dn{\,\triangleq\,}
\verbdef\singlearr|---->|
\verbdef\doublearr|===>|
\verbdef\tripple|###|

\renewcommand{\isasymequiv}{$\triangleq$}
\renewcommand{\isasymemptyset}{$\varnothing$}
%%\renewcommand{\isacharunderscore}{\mbox{$\_\!\_$}}
\renewcommand{\isasymUnion}{$\bigcup$}
\renewcommand{\isacharunderscore}{\text{$\_\!\_$}}

\newcommand{\isasymsinglearr}{$\mapsto$}
\newcommand{\isasymdoublearr}{$\Mapsto$}
\newcommand{\isasymtripple}{\tripple}

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

\begin{document}

\title{Quotients Revisited for Isabelle/HOL}
\author{Cezary Kaliszyk \and Christian Urban}
\institute{C.~Kaliszyk \at University of Tsukuba, Japan
     \and C.~Urban \at Technical University of Munich, Germany}
\date{Received: date / Accepted: date}

\maketitle

\begin{abstract}
Higher-Order Logic (HOL) is based on a small logic kernel, whose only
mechanism for extension is the introduction of safe definitions and of
non-empty types. Both extensions are often performed in quotient
constructions. To ease the work involved with such quotient constructions, we
re-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 formal
verifications, in order to be feasible, require a convenient reasoning infrastructure
for quotient constructions.
\end{abstract}

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

\bibliographystyle{abbrv}
\input{session}



\end{document}

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