Formation of Methods for Proof Planning in Mathematics EPSRC Grant GR/M22031/01

Contents

• Project Coordinates
• People
• Grant Proposal
• Final Report
• Publications
• Talks
• System Demo
• Related Persons and Research Groups

Project Coordinates

People

• Mateja Jamnik, research fellow
• Manfred Kerber, principal investigator
• Seungyeob Choi, PhD student (start: September 1999)
• Christoph Benzmüller, collaborator
• Martin Pollet, collaborator
• Volker Sorge, collaborator

Grant Proposal

Final Report

Publications

• Mateja Jamnik, Manfred Kerber, Martin Pollet, Christoph Benzmüller.
  
Automatic Learning of Proof Methods in Proof Planning.
(gzipped PostScript, pdf)
Technical Report, CSRP-02-05, School of Computer Science, The University of Birmingham. 2002, submitted.
• 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.
• Mateja Jamnik, Manfred Kerber, Martin Pollet.
  
LearnOmatic: System Description.
(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.
• Seungyeob Choi, Manfred Kerber.
  
Model-Guided Proof Planning.
(gzipped PostScript, pdf)
In "Logical and Computational Aspects of Model-Based Reasoning", editors: L. Magnani and N.J. Nersessian, 2002, forthcoming.
• Daniel Winterstein, Alan Bundy, Corin Gurr, Mateja Jamnik.
  
Using animation in diagrammatic theorem proving.
(gzipped PostScript, pdf)
In "Theory and Application of Diagrams: Second International Conference, Diagrams 2002", editors: M. Hegarty, B. Meyer, and H. Narayanan, LNAI 2317. Springer Verlag. 2002.
• Seungyeob Choi, Andreas Meier.
  
Proof Planning in Omega with Semantic Guidance.
(gzipped PostScript, pdf)
Technical Report, CSRP-01-11, School of Computer Science, The University of Birmingham. 2001. 29pp.
• Mateja Jamnik.
  
Mathematical Reasoning with Diagrams: From Intuition to Automation.
Published by CSLI Press, Stanford University, Stanford, CA, USA, Distributed by Chicago University Press. December, 2001.
• Christoph Benzmüller, Mateja Jamnik, Manfred Kerber, Volker Sorge.
  
Experiments with an agent-oriented reasoning system.
(gzipped PostScript, pdf)
In Proceeding of the KI 2001: Advances in Artificial Intelligence, editors: F. Baader, G. Brewka, and T. Eiter, LNAI 2174, Springer, 2001, pages 409--424.
• Mateja Jamnik, Manfred Kerber, Christoph Benzmüller.
  
Towards Learning New Methods in Proof Planning.
(gzipped PostScript, pdf)
In "Proceedings of the 2000 Calculemus Symposium: Systems for Integrated Computation and Deduction". St. Andrews, Scotland, UK. August, 2000, A.K.Peters, 2001. Also presented at CADE 2000 Workshop: "The Role of Automated Deduction in Mathematics", Pittsburgh, USA. 11pp.
• Mateja Jamnik, Manfred Kerber, Christoph Benzmüller.
  
Learning Methods Outlines in Proof Planning.
(gzipped PostScript, pdf)
Technical Report CSRP-01-08, School of Computer Science, The University of Birmingham. 2001. 14pp.
• Daniel Winterstein, Alan Bundy, Mateja Jamnik.
  
A proposal for automatic diagrammatic reasoning in continuous domains.
(gzipped PostScript, pdf)
In "Theory and Application of Diagrams: First International Conference, Diagrams 2000", editors: M. Anderson, P. Cheng and V. Haarslev (eds.), LNAI 1889, Springer, 2000, pages 286--299.
• Manfred Kerber, Seungyeob Choi.
  
The Semantic Clause Graph Procedure.
(gzipped PostScript, pdf)
In "Proceeding of the CADE 2000 Workshop: Model Computation - Principles, Algorithms, and Applications", Pittsburgh, USA. 9pp.
• Christoph Benzmüller, Mateja Jamnik, Manfred Kerber, Volker Sorge.
  
Towards Concurrent Resource Managed Deduction.
(gzipped PostScript, pdf)
Technical Report CSRP-99-17, School of Computer Science, The University of Birmingham. 1999. 33pp.
• Mateja Jamnik.
  
Analogy and automated reasoning.
(gzipped PostScript, pdf)
Technical Report CSRP-99-14, School of Computer Science, The University of Birmingham. 1999. 18pp.

Talks - Posters - Lectures

• Mateja Jamnik with Manfred Kerber, Martin Pollet, Christoph Benzmüller.
  
Automatic Learning of Proof Methods in Proof Planning.
(gzipped PostScript, pdf)
CIAO-Workshop, Edinburgh, April 2002.
• Manfred Kerber with Mateja Jamnik, Martin Pollet.
  
Extendible Reasoning.
(gzipped PostScript, pdf)
CIAO-Workshop, Edinburgh, April 2002.
• Mateja Jamnik with Manfred Kerber, Martin Pollet, Christoph Benzmüller.
  
Automatic Learning of Proof Methods in Proof Planning.
(gzipped PostScript, pdf)
Seminar, University of Saarbrücken, March 2002.
• Seungyeob Choi with Manfred Kerber.
  
Semantically Guided Proof Planning.
(gzipped PostScript, pdf)
MBR'02 conference, Pavia, Italy, May 2001.
• Manfred Kerber with Christoph Benzmüller, Mateja Jamnik, Martin Pollet.
  
Automatic Learning of Proof Methods in Proof Planning.
(gzipped PostScript, pdf)
Poster, Automated Reasoning Workshop, Imperial College, London, 2002.
• Manfred Kerber with Christoph Benzmüller, Mateja Jamnik.
  
Learning Methods to Prove Theorems.
(gzipped PostScript, pdf)
Dagstuhl Seminar, Deduction, March 2001. Seminar 9 March 2001, University of Saarbrücken.
• Mateja Jamnik with Manfred Kerber, Christoph Benzmüller.
  
Learning Proof Methods in Proof Planning.
(gzipped PostScript, pdf)
Poster, Automated Reasoning Workshop, York, 2001.
• Manfred Kerber, Seungyeob Choi.
  
The Semantic Clause Graph Procedure.
(gzipped PostScript, pdf)
CADE-Workshop: "Model Computation - Principles, Algorithms, and Applications", Pittsburgh, USA, 2000.
• Manfred Kerber with Christoph Benzmüller, Seungyeob Choi, Mateja Jamnik.
  
Proof Planning - Case Studies and Future Directions.
(gzipped PostScript, pdf)
Seminar 24 November 2000, University of Essex. 2 October 2001, University of Koblenz.
• Mateja Jamnik, Manfred Kerber.
  
Human-Oriented Mechanised Mathematical Reasoning.
(gzipped PostScript, pdf)
European Summer School on Logic, Language, Information, The University of Birmingham, Birmingham, England, 2000, 159pp.

System Demo

• Mateja Jamnik, Manfred Kerber, Martin Pollet, Christoph Benzmüller.
  
LearnOmatic.

Related Persons and Research Groups

Advisors, Contacts, Visitors, Friends

• Alan Bundy
• Andrew Ireland
• Predrag Janicic
• Achim Jung
• Andreas Meier
• Stephen H. Muggleton
• Julian Richardson

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
• MBase Project: A mathematical Knowledge Base, Universität des Saarlandes, Saarbrücken, Germany

Related Work in the School of Computer Science