%==============
\begin{center}
{\LARGE \bf Automated Theorem Proving}
\end{center}
%==============
\bigskip

\noindent
{\bf Organizer}

\medskip
Bruno Buchberger (Bruno.Buchberger@risc.uni-linz.ac.at)
\bigskip

\noindent
{\bf Description}
\medskip

We envisage a merge of computer algebra and automated theorem proving systems in the near
future. The merge can be started from both ends: Either one may expand theorem proving systems
by adding more algebra or one may grade up algebra systems by adding proving potential. In this
session, we want to encourage researchers active in at least one of the two areas to get together and
discuss how this merge could be achieved most efficiently and soundly. 

\bigskip
\noindent
{\bf Talks}
\medskip

Date: July 17th (Wednesday) 


\begin{center}
{\Large \bf Automated Theorem Proving I
}
\end{center}

\begin{description}
\item[08:30-08:55 ] \ \\
  Bruno Buchberger \\
  {\bf An Overview on the Apply Math Project} 
\item[08:55-09:20] \ \\
  Henk Barendregt \\
  {\bf Efficient computations in formal proofs} 
\item[09:20-09:45] \ \\ 
  Bernd Ingo Dahn \\
  {\bf Computer Algebra Systems in an Environment of Cooperating
    Theorem Provers.} 
\item[09:45-10:20] \ \\
  \ \\
  {\bf Coffee Break}
\item[10:20-10:45] \ \\ 
  St\'ephane Dalmas, Marc Ga\"etano, Claude Huchet \\
  {\bf A Deductive Database for Mathematical formulas.} 
\item[10:45-11:10] \ \\ 
  Agostino Dovier, Andrea Formisano, Alberto Policriti\\
  {\bf Automated deduction scheme.}
\item[11:10-11:35] \ \\ 
  Michael Joswig\\
  {\bf Towards modelling the topology of homogeneous manifolds by
    means of symbolic computation.} 
\item[11:35-12:00] \ \\ 
  Eric Monfroy, Christophe Ringeissen\\
  {\bf Domain-Independent Scheme for Constraint Solver
  Extension.}
\end{description}

\newpage

\begin{center}
{\Large \bf Automated Theorem Proving II
}
\end{center}


\begin{description}
\item[14:00-14:25] \ \\ 
  J\"urgen Stuber\\
  {\bf Building abelian groups and commutative rings into first-order
    theorem proving.} 
\item[14:25-14:50] \ \\ 
  Volker Sorge\\
  {\bf Integrating a CAS as Proof Planer in the OMEGA Proof
    Development Environment.}  
\item[14:50-15:15] \ \\ 
  Wolfgang Gehrke\\
  {\bf A method to combine algebraic computations with related deductions.} 
\item[15:15-16:05] \ \\
  \ \\
  {\bf Coffe Break}
\item[16:05-16:30] \ \\ 
  Jacques Calmet, Karsten Homann\\
  {\bf The Role of Representation for Specification and Communication
    in Mathematical Assistants.}
\item[16:30-17:30] \ \\ 
  Helmut Thiele\\
  {\bf On an Algebraic Characterization of Default Reasoning.}
\end{description}

