\documentclass{article}

%{{{ Preamble
% ========================================
\usepackage[T1]{fontenc}
\usepackage{geometry}
\geometry{top=0.5in,bottom=0.5in,left=1in,right=0.75in}
\pagestyle{empty}

% ========================================
\newcommand{\day}[1]{\vspace*{5ex}\framebox{\textsc{\Large #1}}\vspace*{2ex}}
\newenvironment{session}[1]{%
  \begin{tabular}{ll}%
  \multicolumn{2}{l}{\textsf{\bfseries #1}}\\}{\end{tabular}\vspace{1ex}}
\newcommand{\event}[2]{{#1} & {#2} \\}

% ========================================
\renewcommand{\arraystretch}{1.5}

\newcommand{\italka}{\begin{minipage}[t]{0.9\textwidth}
    \textbf{Bruno Buchberger}: \\
    \emph{The Theorema Project: An Overview}
    \end{minipage}}

\newcommand{\talka}{\begin{minipage}[t]{0.9\textwidth}
    \textbf{Matthias Baaz and Alexander Leitsch}: \\
    \emph{Cut Elimination by Resolution}
    \end{minipage}}
\newcommand{\talkb}{\begin{minipage}[t]{0.9\textwidth}
    \textbf{Ricardo Caferra and Nicolas Peltier}: \\
    \emph{Model building in the
    cross-roads of consequence and non-consequence relations}
    \end{minipage}}
\newcommand{\talkc}{\begin{minipage}[t]{0.9\textwidth}
    \textbf{Carsten Bierwald and Thomas K\"aufl}: \\
    \emph{Tableau Prover Tatzelwurm:
    Hyper-Links and UR-Resolution}
    \end{minipage}}
\newcommand{\talkd}{\begin{minipage}[t]{0.9\textwidth}
    \textbf{Uwe Petermann}: \\
    \emph{Building-In Hybrid Theories}
    \end{minipage}}
\newcommand{\talke}{\begin{minipage}[t]{0.9\textwidth}
    \textbf{John Harrison}: \\
    \emph{First Order Logic in Practice}
    \end{minipage}}
\newcommand{\talkf}{\begin{minipage}[t]{0.9\textwidth}
    \textbf{Ingo Dahn and Christoph Wernhard}: \\
    \emph{First Order Proof Problems
    Extracted from an Article in the MIZAR Mathematical Library}
    \end{minipage}}
\newcommand{\talkg}{\begin{minipage}[t]{0.9\textwidth}
    \textbf{Alfons Geser and Wolfgang K\"uchlin}: \\
    \emph{Structured Formal Verification of a Fragment of the IBM 390
    Clock Chip}
    \end{minipage}}
\newcommand{\talkh}{\begin{minipage}[t]{0.9\textwidth}
    \textbf{Wolfgang Reif and Gerhard Schellhorn}: \\
    \emph{Theorem Proving in Large Theories}
    \end{minipage}}
\newcommand{\talki}{\begin{minipage}[t]{0.9\textwidth}
    \textbf{Maria Paola Bonacina}: \\
    \emph{On the representation of parallel search in theorem proving}
    \end{minipage}}
\newcommand{\talkj}{\begin{minipage}[t]{0.9\textwidth}
    \textbf{Thierry Boy de la Tour}: \\
    \emph{Up-to-Isomorphism Enumeration of Finite Models - The Monadic Case}
    \end{minipage}}
\newcommand{\talkk}{\begin{minipage}[t]{0.9\textwidth}
    \textbf{Albert Brandl, Christian G. Ferm\"uller, and Gernot Salzer}: \\
    \emph{Testing for Renamability to Classes of Clause Sets}
    \end{minipage}}
\newcommand{\talkl}{\begin{minipage}[t]{0.9\textwidth}
    \textbf{Domenico Cantone, Alessandra Cavarra, and Eugenio Omodeo}: \\
    \emph{On existential quantified conjunctions of atomic formulae of
          $\mathcal{L}^+$}
    \end{minipage}}
\newcommand{\talkm}{\begin{minipage}[t]{0.9\textwidth}
    \textbf{Eric Gascard and Laurence Pierre}: \\
    \emph{Two Approaches to the Formal Proof of Replicated Hardware
    Systems using the Boyer-Moore Theorem Prover}
    \end{minipage}}
\newcommand{\talkn}{\begin{minipage}[t]{0.9\textwidth}
    \textbf{Olga Caprotti}: \\
    \emph{Symbolic Pattern Solving for Equational Reasoning}
    \end{minipage}}
\newcommand{\talko}{\begin{minipage}[t]{0.9\textwidth}
    \textbf{Joseph A. Goguen}: \\
    \emph{Stretching First Order Equational Logic: Proofs
    with Partiality, Subtypes and Retracts}
    \end{minipage}}
\newcommand{\talkp}{\begin{minipage}[t]{0.9\textwidth}
    \textbf{Peter Baumgartner and Ulrich Furbach}: \\
    \emph{Refinements for Restart Model Elimination}
    \end{minipage}}
\newcommand{\talkq}{\begin{minipage}[t]{0.9\textwidth}
    \textbf{Marc Fuchs}: \\
    \emph{Similarity-Based Lemma Generation for Model Elimination}
    \end{minipage}}
\newcommand{\talkr}{\begin{minipage}[t]{0.9\textwidth}
    \textbf{Pierre Ostier}: \\
    \emph{A Complete Deduction System for Reasoning with Temporary
    Assumptions}
    \end{minipage}}
\newcommand{\talks}{\begin{minipage}[t]{0.9\textwidth}
    \textbf{Serge Autexier and Dieter Hutter}: \\
    \emph{Equational Proof-Planning by Dynamic Abstraction}
    \end{minipage}}
\newcommand{\talkt}{\begin{minipage}[t]{0.9\textwidth}
    \textbf{Robert Matzinger}: \\
    \emph{Using Grammars for Finite Domain Evaluation}
    \end{minipage}}
\newcommand{\talku}{\begin{minipage}[t]{0.9\textwidth}
    \textbf{Georg Moser}: \\
    \emph{Some Remarks on Transfinite E-Semantic Trees and Superposition}
    \end{minipage}}
\newcommand{\talkv}{\begin{minipage}[t]{0.9\textwidth}
    \textbf{J\"urgen Stuber}: \\
    \emph{Strong Symmetrization and Semi-Compatibility of
    Normalized Rewriting and First-Order Theorem Proving}
    \end{minipage}}
\newcommand{\talkw}{\begin{minipage}[t]{0.9\textwidth}
    \textbf{Reinhard Pichler}: \\
    \emph{Testing the Equivalence of Models given through
    Linear Atomic Representations}
    \end{minipage}}
\newcommand{\talkx}{\begin{minipage}[t]{0.9\textwidth}
    \textbf{Uwe Waldmann}: \\
    \emph{A Superposition Calculus for Divisible Torsion-Free Abelian Groups}
    \end{minipage}}
\newcommand{\talky}{\begin{minipage}[t]{0.9\textwidth}
    \textbf{Nic Wilson and Jerome Mengin}: \\
    \emph{Logical Deduction using the Local Computation Framework}
    \end{minipage}}
% ========================================
\title{FTP '97 \\ Schedule}
\author{Schloss Hagenberg, Austria}
\date{October 27 -- 28, 1997}


% ========================================
%}}}

\begin{document}
\begin{center}
{\Large\sc  FTP97 -- Schedule}\\[2.5ex]
{\large  Schloss\ Hagenberg, Austria, October 27--28, 1997}\\[5ex]
\end{center}


%{{{ Monday
\day{Monday 27 October 1997}

\begin{session}{08:45 -- 09:00~~~Opening Remarks}
\end{session}

\begin{session}{09:00 -- 10:00~~~Invited Talk I}
  \event{}{\italka} % Bruno Buchberger
\end{session}

\begin{session}{10:00 -- 10:30~~~Break}
\end{session}

\begin{session}{10:30 -- 12:10~~~Session I}
  \event{}{\talka}
  \event{}{\talkb}
  \event{}{\talkc}
  \event{}{\talkd}
\end{session}

\begin{session}{12:10 -- 14:00~~~Lunch Break}
\end{session}

\begin{session}{14:00 -- 15:40~~~Session II}
  \event{}{\talke}
  \event{}{\talkf}
  \event{}{\talkg}
  \event{}{\talkh}
\end{session}

\begin{session}{15:40 -- 16:10~~~Break}
\end{session}

\begin{session}{16:10 -- 17:50~~~Session III}
  \event{}{\talki}
  \event{}{\talkj}
  \event{}{\talkk}
  \event{}{\talkl}
\end{session}
%}}}

%{{{ Tuesday
\day{Tuesday 28 October 1997}

\begin{session}{09:00 -- 10:15~~~Session IV}
  \event{}{\talkm}
  \event{}{\talkn}
  \event{}{\talko}
\end{session}

\begin{session}{10:15 -- 10:45~~~Break}
\end{session}

\begin{session}{10:45 -- 12:00~~~Session V}
  \event{}{\talkp}
  \event{}{\talkq}
  \event{}{\talkr}
\end{session}

\begin{session}{12:00 -- 14:00~~~Lunch Break}
\end{session}

\begin{session}{14:00 -- 15:40~~~Session VI}
  \event{}{\talks}
  \event{}{\talkt}
  \event{}{\talku}
  \event{}{\talkv}
\end{session}

\begin{session}{15:40 -- 16:10~~~Break}
\end{session}

\begin{session}{16:10 -- 17:25~~~Session VII}
  \event{}{\talkw}
  \event{}{\talkx}
  \event{}{\talky}
\end{session}

\begin{session}{17:25 -- 17:50~~~Closing Discussion}
\end{session}
%}}}


\end{document}

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