Session 1
   9:20--9:30     OPENING
  
   9:30--10:00 K.Aboul-Hosn, D.Kozen.   Kat-ML: An Interactive Theorem Prover for
                                        Kleene Algebra with Tests
  
  10:00--10:30 S.Colin, V.Poirriez,     Thoughts about the implementation of
               G.Mariano.               the Duration Calculus with Coq
  
  
  
  10:30--11:00    COFFEE BREAK
  
  
  Invited talk
  11:00--12:00 Stephan Schulz.          Invited talk
  
  
  12:00--14:00    LUNCH
  
  
Session 2
  14:00--14:30 M.Baaz, C.Fermueller,    MUltlog and MUltset Reanimated and 
               A.Gil, G.Salzer,         Married
  	       N.Preining.
  
  14:30--15:00 M.Marin, T.Kutsia        On the Implementation of a Rule-Based
                                        Programming System and Some of its 
  				        Applications
  
  
  15:00--15:30    COFFEE BREAK
  
  
Session 3 
  15:30--16:00 J.Giesl, R.Thiemann,     The Termination Prover AProVE
               P.Schneider-Kamp, 
  	       S.Falke.
  
  16:00--16:30 H.de Nivelle.            Implementing the Clausal Normal Form 
                                        Transformation with Proof Generation

  16:30--17:00 G.Bittencourt, J.Marchi, A Syntactic Approach to Satisfaction
               R.Padilha.