## CALCULEMUS BirminghamSystem for Integrated Computation and Deductionfunded under the 5th Framework Programme of the European Commission Contract Reference HPRN-CT-2000-00102 |
---|

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

Start Date: | 1 September 2000 |

End Date: | 31 August 2004 |

Total Grant Value: | Euro 80,063 |

Funding Agency: | European Commission |

Grant: | HPRN-CT-2000-00102 |

Project Central Web Page: | http://www.eurice.de/calculemus/ |

Calculemus Interest Group: | www.calculemus.net |

- 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

- 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.

- Manfred Kerber and Martin Pollet.
- Mateja Jamnik, Manfred Kerber and Martin Pollet.
- Mateja Jamnik, Manfred Kerber, Martin Pollet.
- Mateja Jamnik, Manfred Kerber, Martin Pollet.
- Andreas Franke, Markus Moschner, Martin Pollet.
- Christoph Benzmüller, Manfred Kerber.
- Andreas Meier, Martin Pollet, Volker Sorge.
- Andreas Meier, Volker Sorge, Simon Colton.
- Jacques Calmet, Belaid Benhamou, Olga Caprotti, Laurent Henocque, Volker Sorge.
- Olga Caprotti, Volker Sorge.
- Frank Theiß, Volker Sorge.

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.

In "Automated Deduction - CADE-18", 18th International Conference on Automated Deduction, Copenhagen, Denmark, July 2002, LNAI 2392, editor: A. Voronkov, pages 150-155.

In "European Conference on Artificial Intelligence", editor: F. van Harmelen, 2002, IOS Press, pages 282-286, also available as Technical Report, see next item.

Technical Report, CSRP-02-03, School of Computer Science, The University of Birmingham. 2002. 13pp.

Calculemus 2002, Work in Progress Papers, p.68-70, Marseille, July 2002.

Proceedings of IJCAR Workshop on Future Directions in Automated Reasoning; p. 13-24, Siena, 18 June 2001.

Journal of Symbolic Computation 34(4), p. 287-306, September 2002.

In Proceedings of Calculemus-2002, LNAI 2385, editors: Olga Caprotti and Volker Sorge, p. 275-289..

LNAI 2385, Springer Verlag..

Seki-Report SR-02-04..

In Calculemus 2002, Work in Progress Papers, Seki-Report SR-02-04, edited by Olga Caprotti and Volker Sorge..

- Martin Pollet with Mateja Jamnik, Manfred Kerber and Christoph Benzmüller.
- Manfred Kerber with Mateja Jamnik and Martin Pollet.
- Martin Pollet with Andreas Franke and Markus Moschner.
- Manfred Kerber with Martin Pollet.
- Manfred Kerber with Martin Pollet.
- Martin Pollet.
- Manfred Kerber.
- Martin Pollet with Manfred Kerber.
- Martin Pollet.

CADE 2002, Copenhagen, July 2002.

ECAI 2002, Lyon, July 2002.

Calculemus 2002, Marseille, July 2002.

Calculemus 2002, Marseille, July 2002.

Automath-Workshop, Edinburgh, April 2002.

CIAO Workshop, Edinburgh, April 2002.

CIAO Workshop, Edinburgh, April 2002.

Calculemus Task Force Meeting, University of Genova, February 2002.

Cake Talks, University of Birmingham, November 2001.

- 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

- 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

Last update: 15 Oct 2002

School of Computer Science, The University of Birmingham