\begin{filecontents}{ftptalks.sty}
\parindent0pt
\newcommand\Duration{30}
\newcommand\invDuration{60}
\newcommand\posDuration{15}
\newcommand\disDuration{60}
\newcommand\lunchDuration{120}
\newcommand\coffeeDuration{30}

\newlength\sessionsep
\sessionsep 3ex plus 2ex minus 2ex
\newlength\daysep
\daysep 8ex plus 2ex minus 4ex

\newcommand\newtalk[3]%
   {\expandafter\def\csname authors@\romannumeral#1\endcsname{#2}%
    \expandafter\def\csname title@\romannumeral#1\endcsname{#3}%
   }
\newcommand\Authors[1]{\csname authors@\romannumeral#1\endcsname}
\newcommand\Title[1]{\csname title@\romannumeral#1\endcsname}

\newcommand\newinvitedtalk[3]%
   {\expandafter\def\csname invauthors@\romannumeral#1\endcsname{#2}%
    \expandafter\def\csname invtitle@\romannumeral#1\endcsname{#3}%
   }
\newcommand\invAuthors[1]{\csname invauthors@\romannumeral#1\endcsname}
\newcommand\invTitle[1]{\csname invtitle@\romannumeral#1\endcsname}

\newcommand\newpositiontalk[3]%
   {\expandafter\def\csname posauthors@\romannumeral#1\endcsname{#2}%
    \expandafter\def\csname postitle@\romannumeral#1\endcsname{#3}%
   }
\newcommand\posAuthors[1]{\csname posauthors@\romannumeral#1\endcsname}
\newcommand\posTitle[1]{\csname postitle@\romannumeral#1\endcsname}

\newcount\time
\newcount\@auxcnta
\newcount\@auxcntb
\newcommand\settime[1]{\global\time#1\relax}
\newcommand\advtime[1]{\global\advance\time#1\relax}
\newcommand\hour
   {\@auxcnta\time
    \divide\@auxcnta60\relax
    \ifnum\@auxcnta<10\relax\mbox{$\phantom{\mbox{0}}$}\fi
    \the\@auxcnta
   }
\newcommand\minutes
   {\@auxcnta\time
    \divide\@auxcnta60\relax
    \multiply\@auxcnta60\relax
    \@auxcntb\time
    \advance\@auxcntb-\@auxcnta
    \ifnum\@auxcntb<10\relax0\fi
    \the\@auxcntb
   }

\newenvironment{Day}[1]%
   {{\vspace\daysep\par
    \large\textsc{#1}}%
    \settime{540}%
   }%
   {}

\newcounter{session}
\setcounter{session}{0}
\newenvironment{Session}[1]%
   {\vspace\sessionsep\par
    \addtocounter{session}{1}%
    {\bfseries Session \Roman{session}: #1}\\[2ex]%
    \begin{tabular}{@{}lp{0.915\textwidth}@{}}%
   }%
   {\end{tabular}%
   }
\newcommand\talk[1]%
   {\hour:\minutes\advtime{\Duration}%
    & \Title{#1}\\
    & \textit{\Authors{#1}}\\
   }
\newcommand\invitedtalk[1]%
   {\hour:\minutes\advtime{\invDuration}%
    & \invTitle{#1}\\
    & \textit{\invAuthors{#1}}\\
   }
\newcommand\positiontalk[1]%
   {\hour:\minutes\advtime{\posDuration}%
    & \posTitle{#1}\\
    & \textit{\posAuthors{#1}}\\
   }
\newcommand\discussion[3]%
   {\hour:\minutes\advtime{\disDuration}%
    & #1\\
    & \textit{Chairs: #2}\\
    & \textit{Panelists: #3}
   }

\newcommand\extra[2]%
   {\vspace\sessionsep\par
    \begin{tabular}{@{}lp{0.915\textwidth}@{}}%
    \hour:\minutes\advtime{#1}%
    & #2%
    \end{tabular}%
   }

\newcommand\Extra[2]%
   {\vspace\sessionsep\par
    \begin{tabular}{@{}lp{0.915\textwidth}@{}}%
    \hour:\minutes\advtime{#1}%
    & {\bfseries #2}%
    \end{tabular}%
   }

\let\extra\Extra

\newcommand\Coffee{\extra{\coffeeDuration}{Coffee break}}
\newcommand\Lunch{\extra{\lunchDuration}{Lunch break}}
\end{filecontents}





\begin{filecontents}{ftp98talks.tex}
\newinvitedtalk
   {1}%
   {Gilles Dowek}%
   {Automated theorem proving in first-order logic modulo:
    on the difference between type theory and set theory}%
\newinvitedtalk
   {2}%
   {Melvin Fitting}%
   {Quantified modal logic}%
\newinvitedtalk
   {3}%
   {Alexander Leitsch}%
   {Decision procedures and model building,
    or How to improve logical information in ATP}%
\newtalk
   {1}%
   {Alessandro Armando and Silvio Ranise}%
   {Constraint contextual rewriting}%
\newtalk
   {2}%
   {Thierry Boy de la Tour}%
   {How complex is a finite first-order sorted interpretation?}%
\newtalk
   {3}%
   {Domenico Cantone and Marianna Nicolosi Asmundo}%
   {A further and effective liberalization of the $\delta$-rule in 
    free variable semantic tableaux}%
\newtalk
   {4}%
   {Domenico Cantone and Calogero G. Zarba}%
   {A new fast tableau-based decision procedure for an unquantified
    fragment of set theory}%
\newtalk
   {5}%
   {Ingo Dahn}%
   {Interpretation of a Mizar-like logic in first-order logic}%
\newtalk
   {6}%
   {Stephane Demri and Rajeev Gore}%
   {An ${\cal O}((n\cdot\log n)^3)$-time transformation from Grz into decidable
    fragments of classical first-order logic}%
\newtalk
   {7}%
   {Christian Ferm\"uller}%
   {Implicational completeness of signed resolution}%
\newtalk
   {8}%
   {Andrea Formisano and Eugenio Omodeo}%
   {An equational re-engineering of set theories}%
\newtalk
   {9}%
   {J.N. Hooker, G. Rago, Vijay Chandru, and Anjul Shrivastava}%
   {A partial instantiation based first order theorem prover}%
\newtalk
   {10}%
   {Ullrich Hustadt and Renate A. Schmidt}%
   {Issues of decidability for description logics in the framework
    of resolution}%
\newtalk
   {11}%
   {Boris Konev}%
   {Upper bound on the height of terms in proofs with cuts}%
\newtalk
   {12}%
   {Nicolas Peltier}%
   {Proof generalization and function introduction}%
\newtalk
   {13}%
   {Reinhard Pichler}%
   {Extending decidable clause classes via constraints}%
\newtalk
   {14}%
   {Reinhard Pichler}%
   {Completeness and redundancy in constrained clause logic}%
\newtalk
   {15}%
   {Aida Pliu\v skevi\v cien\.e}%
   {Effective properties for some first order
    intuitionistic modal logics}%
\newtalk
   {16}%
   {Grigore Rosu and Joseph Goguen}%
   {Hidden congruent deduction}%
\newtalk
   {17}%
   {Viorica Sofronie-Stokkermans}%
   {Resolution-based theorem proving for $SHn$-logics}%
\newtalk
   {18}%
   {Hubert Wagner}%
   {A new resolution calculus for the infinite-valued propositional
    logic of {\L}ukasiewicz}%
\newtalk
   {19}%
   {Claus-Peter Wirth}%
   {Full first-order sequent and tableau calculi with preservation of
    solutions and the liberalized $\delta$-rule but without skolemization}%
\newpositiontalk
   {1}%
   {Maria Paola Bonacina}%
   {Theorem proving strategies: a search oriented taxonomy}%
\newpositiontalk
   {2}%
   {Robert Matzinger}%
   {Computational representations of models of first-order formulas}%
\newpositiontalk
   {3}%
   {Claus Zinn}%
   {Verifying textbook proofs}%
\end{filecontents}







\documentclass[11pt]{article}
\usepackage{ftptalks}
%\pagestyle{empty}
\textheight24cm
\textwidth16cm
\oddsidemargin0cm
\evensidemargin\oddsidemargin
\topmargin 0cm
\headheight 0pt
\headsep 0pt 

\begin{document}
\input{ftp98talks}

\begin{center}
{\LARGE{\bfseries\sffamily FTP'98} -- {\scshape Final Program}}
\end{center}

\begin{Day}{Monday, 23 November 1998}

\extra{10}{Opening Address}

\begin{Session}{Invited talk}
   \invitedtalk{3}
\end{Session}

\Coffee

\begin{Session}{Constrained clause logic}
   \talk{12}
   \talk{14}
   \talk{13}
\end{Session}

\Lunch

\begin{Session}{Decision procedures}
   \talk{6}
   \talk{10}
   \talk{4}
\end{Session}

\Coffee

\begin{Session}{Interpretation \& Verification}
   \talk{2}
   \positiontalk{2}
   \talk{5}
   \positiontalk{3}
\end{Session}

\end{Day}

\pagebreak
\begin{Day}{Tuesday, 24 November 1998}

\begin{Session}{Invited talk}
   \def\invDuration{90}%
   \invitedtalk{2}
\end{Session}

\Coffee

\begin{Session}{Many-valued logics}
   \talk{7}
   \talk{17}
   \talk{18}
\end{Session}

\Lunch

\begin{Session}{Tableaux \& First-order theorem proving}
   \talk{3}
   \talk{19}
   \talk{9}
   \positiontalk{1}
\end{Session}

\Coffee

\begin{Session}{Panel discussion}
\discussion{Concepts, logics and research methodologies in automated deduction}%
           {Maria Paola Bonacina and Ricardo Caferra}%
           {Domenico Cantone, Gilles Dowek, Melvin Fitting, and Alexander Leitsch}
\end{Session}

\extra{30}{Business meeting}

\settime{1140}
\extra{120}{Dinner at a Viennese ``Heuriger''}

\end{Day}

\pagebreak
\begin{Day}{Wednesday, 25 November 1998}

\begin{Session}{Invited talk}
   \def\invDuration{90}%
   \invitedtalk{1}
\end{Session}

\Coffee

\begin{Session}{Equational reasoning}
   \talk{1}
   \talk{8}
   \talk{16}
\end{Session}

\Lunch

\begin{Session}{Proof theory}
   \talk{11}
   \talk{15}
\end{Session}

\Coffee

\extra{10}{Closing discussion}

\end{Day}

\end{document}