T H E O R E M A   W O R K S H O P
 
                         9-10 June, 1997 

                 RISC, Hagenberg by Linz, Austria

The "Theorema" project at RISC aims at extending current computer
algebra systems by facilities for supporting mathematical proving.
In cooperation with RISC, related research is going on at SCORE, 
University of Tsukuba, Japan.

The purpose of the workshop is to present the current status of these
projects and to stimulate further interaction between the two groups.
Guests from the international research community are cordially invited 
to participate.
 
The proceedings will be published in the RISC Technical Report Series.

PRELIMINARY PROGRAM (further details will be announced at
 http://www.risc.uni-linz.ac.at/conferences/Theorema)


 Mo, June 9:
  
Overview and Language
09:00-09:15     Opening
09:15-09:45     B. Buchberger ``Overview on Theorema''
09:45-10:15     B. Buchberger, F. Kriftner ``Theorema: The Language''

10:15-10:45     Coffee Break

Equational Solving and Narrowing
10:45-11:15     T. Suzuki, K. Nakagawa, T. Ida, `` Higher-Order Lazy
                Narrowing Calculus: A Computation Model for a Higher-order Functional
                Logic Language.''
11:15-11:45     M. Hamada, "Lazy Conditional Narrowing Calculus and 
                Its Implementation"

11:45-14:00     Lunch
14:00-15:00     Tour through RISC and SWP

Provers 
15:00-15:30     B. Buchberger, T. Jebelean ``Theorema: The Predicate Prover''.
15:30-16:00     B. Buchberger, D. Vasaru ``Theorema: The Induction Prover for
                Lists''.

16:00-16:15     Coffee Break


16:15-16:45     J. Matsuda, A Prover for Propositional Logic
                in Natural (Deduction) Style: Implementation in C
16:45-17:15     E. Tomuta ``Using Functors in Organizing Proofs''


Dinner in Linz


Tue, June 10:  

Rewriting  I
09:30-10:00     A. Middeldorp, Decidable Call by Need Computations
                in Term Rewriting
10:00-10:30     B. Buchberger, M. Marin ``Proving by Simplification''

10:30-11:00     Coffee Break

Rewriting II
11:00-11:30     M. Hamana, Term Rewriting with Sequences
11:30-12:00     T. Yamada, Logicality of Conditional Rewrite Systems

12:00-14:00     Lunch

Guests Section
14:00-14:30     D. Wang "Clifford Algebraic Calculus for Geometric Reasoning"
14:30-15:00     D. Shand  "Investigating some Embedded Verification
                          Techniques for Computer Algebra Systems" 

15:00-15:30     Coffee Break

15:30-          Demo + Discussion   


Dinner in Hagenberg


  
For registration info, please contact Daniela Vasaru at
dvasaru@risc.uni-linz.ac.at .