Quellcode-Bibliothek

^© Kompilation durch diese Firma

[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]

Datei: root.tex Sprache: Latech

Original von: Isabelle^©

\documentclass[11pt,a4paper]{article}
\usepackage{isabelle,isabellesym,pdfsetup}
\usepackage[only,bigsqcap]{stmaryrd}

\urlstyle{rm}\isabellestyle{it}
\pagestyle{headings}

\hyphenation{Isabelle}
\hyphenation{Isar}

\begin{document}

\title{Lattices and Orders in Isabelle/HOL}
\author{Markus Wenzel \\ TU M\"unchen}
\maketitle

\begin{abstract}
  We consider abstract structures of orders and lattices.  Many fundamental
  concepts of lattice theory are developed, including dual structures,
  properties of bounds versus algebraic laws, lattice operations versus
  set-theoretic ones etc.  We also give example instantiations of lattices and
  orders, such as direct products and function spaces.  Well-known properties
  are demonstrated, like the Knaster-Tarski Theorem for complete lattices.

  This formal theory development may serve as an example of applying
  Isabelle/HOL to the domain of mathematical reasoning about ``axiomatic''
  structures.  Apart from the simply-typed classical set-theory of HOL, we
  employ Isabelle's system of axiomatic type classes for expressing structures
  and functors in a light-weight manner.  Proofs are expressed in the Isar
  language for readable formal proof, while aiming at its ``best-style'' of
  representing formal reasoning.
\end{abstract}

\tableofcontents

\newpage
{
  \parindent 0pt\parskip 0.7ex
  \pagestyle{myheadings}
  \renewcommand{\setisabellecontext}[1]{\markright{THEORY~``#1''}}
  \input{session}
}

\nocite{Wenzel:1999:TPHOL}
\nocite{Wenzel:2000:isar-ref}
\nocite{Wenzel:2000:axclass}
\nocite{Bauer-Wenzel:2000:HB}

\bibliographystyle{abbrv}
\bibliography{root}

\end{document}

¤ Dauer der Verarbeitung: 0.24 Sekunden (vorverarbeitet) ¤

Download des Quellennavigators
Download des sprechenden Kalenders
in der Quellcodebibliothek suchen

Haftungshinweis

Die Informationen auf dieser Webseite wurden nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit, noch Qualität der bereit gestellten Informationen zugesichert.

Bemerkung:

Die farbliche Syntaxdarstellung ist noch experimentell.