CALCULEMUS Birmingham System for Integrated Computation and Deduction funded under the 5th Framework Programme of the European Commission Contract Reference HPRN-CT-2000-00102

Contents

• Project Coordinates
• People
• Research Activities
• Publications
• Collaborators and Other Related Research Groups

Project Coordinates

People

• Mateja Jamnik, staff (now at the University of Cambridge)
• Manfred Kerber, staff
• Martin Pollet, young visiting researcher (1/10/2001-28/02/2002, 1/6/2002-31/8/2002, and 1/7/2004-31/8/2004)
• Andreas Meier, young visiting researcher (1/05/2003-31/07/2003)
• Andreas Franke, young visiting researcher (1/12/2003-31/05/2004)
• Volker Sorge, staff

Research Activities

• Task 1.1: Construction of mathematical frameworks
• Task 2.3: Deduction systems with enhanced computational power
• Task 3.5: Challenging mathematical problems

• Learning of proof planning methods (Task 2.3): We implemented the prototypical system LEARNOMATIC that consists of a learning system for typical proof sequences and a module for the application of learned methods in the proof planner OMEGA. The deduction system was thereby enhanced in the sense that it can make use of learning techniques, which are usually outside of the scope of such a system.
• Representation for mathematics (Task 1.1/2.3): We investigate the differences in the representation of mathematical concepts in mathematical textbooks, the datastructure of computer algebra systems and the formal language used by deduction systems. We try to develop an object-centred and hierarchical representation of concepts by frames that approximates mathematical practice. An enhanced representation should enable a deduction system to store computational knowledge to concepts and help to identify proof situation in which computer algebra techniques could be applied.
• Challenging mathematical problems (Task 3.5): Together with Christoph Benzmüller from the University of Saarbrücken a challenging problem by Boolos was investigated. See ``A Challenge for Mechanized Deduction'' in the list of publications.

Publications

• Manfred Kerber and Martin Pollet.
  
On the Design of Mathematical Concepts.
(gzipped PostScript, pdf)
Technical Report, CSRP-02-06, School of Computer Science, The University of Birmingham. 2002. 22pp. Short version in Calculemus 2002, Work in Progress Papers, Seki-Report SR-02-04, edited by Olga Caprotti and Volker Sorge. One page abstract to appear at AI-02, Canberra.
• Mateja Jamnik, Manfred Kerber and Martin Pollet.
  
LearnOmatic: System Description - Learning of Proof Methods in Proof Planning.
(gzipped PostScript, pdf)
In "Automated Deduction - CADE-18", 18th International Conference on Automated Deduction, Copenhagen, Denmark, July 2002, LNAI 2392, editor: A. Voronkov, pages 150-155.
• Mateja Jamnik, Manfred Kerber, Martin Pollet.
  
Automatic Learning in Proof Planning.
(gzipped PostScript, pdf)
In "European Conference on Artificial Intelligence", editor: F. van Harmelen, 2002, IOS Press, pages 282-286, also available as Technical Report, see next item.
• Mateja Jamnik, Manfred Kerber, Martin Pollet.
  
Automatic Learning in Proof Planning.
(gzipped PostScript, pdf)
Technical Report, CSRP-02-03, School of Computer Science, The University of Birmingham. 2002. 13pp.
• Andreas Franke, Markus Moschner, Martin Pollet.
  
Cooperation between the Mathematical Knowledge Base MBase and the Theorem Prover Omega.
(gzipped PostScript, pdf)
Calculemus 2002, Work in Progress Papers, p.68-70, Marseille, July 2002.
• Christoph Benzmüller, Manfred Kerber.
  
A Challenge for Mechanized Deduction.
(gzipped PostScript, pdf)
Proceedings of IJCAR Workshop on Future Directions in Automated Reasoning; p. 13-24, Siena, 18 June 2001.
• Andreas Meier, Martin Pollet, Volker Sorge.
  
Comparing Approaches to Explore the Domain of Residue Classes.
(gzipped PostScript, pdf)
Journal of Symbolic Computation 34(4), p. 287-306, September 2002.
• Andreas Meier, Volker Sorge, Simon Colton.
  
Employing Theory Formation to Guide Proof Planning.
(gzipped PostScript, pdf)
In Proceedings of Calculemus-2002, LNAI 2385, editors: Olga Caprotti and Volker Sorge, p. 275-289..
• Jacques Calmet, Belaid Benhamou, Olga Caprotti, Laurent Henocque, Volker Sorge.
  
Artificial Intelligence, Automated Reasoning, and Symbolic Computation --- Joint International Conference, AISC 2002 and Calculemus 2002.
LNAI 2385, Springer Verlag..
• Olga Caprotti, Volker Sorge.
  
Calculemus 2002 --- 10th Symposium on the Integration of Symbolic Computation and Mechanized Reasoning --- Work in Progress Papers.
Seki-Report SR-02-04..
• Frank Theiß, Volker Sorge.
  
Automatic Generation of Algorithms and Tactics.
(gzipped PostScript, pdf)
In Calculemus 2002, Work in Progress Papers, Seki-Report SR-02-04, edited by Olga Caprotti and Volker Sorge..

Talks

• Martin Pollet with Mateja Jamnik, Manfred Kerber and Christoph Benzmüller.
  
LearnOmatic: System Description - Learning of Proof Methods in Proof Planning.
(gzipped PostScript, pdf)
CADE 2002, Copenhagen, July 2002.
• Manfred Kerber with Mateja Jamnik and Martin Pollet.
  
Automatic Learning in Proof Planning.
(gzipped PostScript, pdf)
ECAI 2002, Lyon, July 2002.
• Martin Pollet with Andreas Franke and Markus Moschner.
  
Cooperation between the Mathematical Knowledge Base MBase and the Theorem Prover Omega.
(gzipped PostScript, pdf)
Calculemus 2002, Marseille, July 2002.
• Manfred Kerber with Martin Pollet.
  
On the Design of Mathematical Concepts.
(gzipped PostScript, pdf)
Calculemus 2002, Marseille, July 2002.
• Manfred Kerber with Martin Pollet.
  
On the Design of Mathematical Concepts.
(gzipped PostScript, pdf)
Automath-Workshop, Edinburgh, April 2002.
• Martin Pollet.
  
Towards the Application of Frame Representation For Mathematical Concepts In Proof Planning.
(gzipped PostScript, pdf)
CIAO Workshop, Edinburgh, April 2002.
• Manfred Kerber.
  
Extendible Reasoning.
(gzipped PostScript, pdf)
CIAO Workshop, Edinburgh, April 2002.
• Martin Pollet with Manfred Kerber.
  
On the Representation of Mathematical Objects.
(gzipped PostScript, pdf)
Calculemus Task Force Meeting, University of Genova, February 2002.
• Martin Pollet.
  
A Mathematical Representation for Mathematics?.
(gzipped PostScript, pdf)
Cake Talks, University of Birmingham, November 2001.

Collaborators and Other Related Research Groups

Collaborators

• Alan Bundy, University of Edinburgh
• Arjeh Cohen, Eindhoven University of Technology
• Simon Colton, Imperial College of Science, Technology and Medicine, London
• Michael Kohlhase, Carnegie Mellon University, Pittsburgh
• Roy McCasland, University of Edinburgh

Research Groups and Projects

• Mathematical Reasoning Group, University of Edinburgh, Scotland, UK
• Mechanised Reasoning Group, Istituto Ricerca Scientifica e Tecnologica (IRST), Trento, Italy
• Omega Group, Universität des Saarlandes, Saarbrücken, Germany
• Mathweb project, Universität des Saarlandes, Saarbrücken, Germany
• Research Institute for Applications of Computer Algebra, Eindhoven University of Technology