Automated Theorem Proving

Organizer

Bruno Buchberger (Bruno.Buchberger@risc.uni-linz.ac.at)
RISC-Linz
Schloß Hagenberg
A-4232 Hagenberg
Austria/Europe
Tel: +43 7236 3231 41
Fax: +43 7236 3231 30

Description

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.

Talks

Date: July 17th (Wednesday)

08:30-08:55: Bruno Buchberger
An Overview on the Apply Math Project
Abstract
08:55-09:20: Henk Barendregt
Efficient computations in formal proofs
Abstract
09:20-09:45: Bernd, Ingo Dahn
Computer Algebra Systems in an Environment of Cooperating Theorem Provers
Abstract

09:45-10:20: Coffee Break

10:20-10:45: Stéphane Dalmas, Marc Gaëtano, Claude Huchet
A Deductive Database for Mathematical formulas
Abstract
10:45-11:10: Agostino Dovier, Andrea Formisano, Alberto Policriti
Automated deduction scheme
Abstract
11:10-11:35: Michael Joswig
Towards modelling the topology of homogeneous manifolds by means of symbolic computation
Abstract
11:35-12:00: Eric Monfroy, Christophe Ringeissen
Domain-Independent Scheme for Constraint Solver Extension
Abstract

14:00-14:25: Jürgen Stuber
Building abelian groups and commutative rings into first-order theorem proving
Abstract
14:25-14:50: Volker Sorge
Integrating a CAS as Proof Planer in the OMEGA Proof Development Environment
Abstract
14:50-15:15: Wolfgang Gehrke
A method to combine algebraic computations with related deductions
Abstract

15:15-16:05: Coffee Break

16:05-16:30: Jacques Calmet, Karsten Homann
The Role of Representation for Specification and Communication in Mathematical Assistants.
Abstract
16:30-17:30: Helmut Thiele
On an Algebraic Characterization of Default Reasoning
Abstract

________________________________________________________