9-10 June, 1997
RISC, Hagenberg near 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.
|
Contents of the Proceedings |
| Overview and Language |
| Bruno Buchberger |
Overview on Theorema |
| Bruno Buchberger,
Franz Kriftner |
Theorema: The Language |
| |
| Equational Solving and Narrowing |
| T. Suzuki, K. Nakagawa, Tetsuo Ida |
Higher-Order
Lazy Narrowing Calculus: A Computation Model for a
Higher-order Functional Logic Language |
| Mohamed Hamada, Tetsuo Ida |
A Deterministic Lazy Conditional Narrowing and its Implementation in Mathematica |
| |
| Tour through RISC and SWP |
| |
| Provers |
| Bruno Buchberger,
Tudor Jebelean |
Theorema: The Predicate Prover |
| Bruno Buchberger,
Daniela Vãsaru |
Theorema: The Induction Prover for Lists |
| |
| Jun Matsuda |
A Prover for Propositional Logic in Natural (Deduction) Style:
Implementation in C |
| Elena Tomuta |
Using Functors in Organizing Proofs |
| |
| |
| Rewriting 1 |
| Irène Durant, Aart Middeldorp |
Decidable Call by Need Computations in Term Rewriting |
| Bruno Buchberger, Mircea Marin |
Proving by Simplification |
| Coffee Break |
| |
| Rewriting 2 |
| Makoto Hamana |
Term Rewriting with Sequences |
| Toshiyuki Yamada, Jürgen Avenhaus,
Carlos Loría-Sáenz, Aart Middeldorp |
Logicality of Conditional Rewrite Systems |
| |
| Guests Section |
| U. Martin, D. Shand |
Investigating some Embedded
Verification Techniques for Computer Algebra Systems |
| M. Matsumoto |
Algebraic Specification Language ``CafeOBJ'' |
|
|
For more info, please contact
Daniela.Vasaru@risc.uni-linz.ac.at.
|