Homepage of Manfred Kerber

Address

Research Interests

Funded Projects

Talks

Software Workshop

Project Prosals

Adv. Msc Project Prosals

Previously taught modules

Departmental Seminar

Project Coordinator

Manfred Kerber

Publications on Proof Planning and Related Work

Combined reasoning by automated cooperation
Journal of Applied Logic, 6, pages 318-342 Christoph Benzmüller, Volker Sorge, Mateja Jamnik, Manfred Kerber, 2008
Informal and Formal Representations in Mathematics
From Insight to Proof: Festschrift in Honour of Andrzej Trybulec; editor: Roman Matuszewski and Anna Zalewska, pages 75-94 Manfred Kerber, Martin Pollet, 2007
Available: pdf © University of Białystok
Can a Higher-Order and a First-Order Theorem Prover Cooperate?
Proceedings of the 11th International Conference on Logic for Programming Artificial Intelligence and Reasoning (LPAR); editor: Franz Baader and Andrei Voronkov, pages 415-431, Springer, LNAI 3452 Christoph Benzmüller, Volker Sorge, Mateja Jamnik, Manfred Kerber, 2005
Available: html BiBTeX pdf PostScript © Springer Verlag
Automatic Learning of Proof Methods in Proof Planning
Logic Journal of the IGPL, 11, pages 647-673 Mateja Jamnik, Manfred Kerber, Martin Pollet, Christoph Benzmüller, 2003
Available: html BiBTeX pdf PostScript © Oxford University Press
On the Design of Mathematical Concepts
Norman Foo's Festschrift, Abhaya Nayak and Maurice Pagnucco, eds. Manfred Kerber, Martin Pollet, 2003
Available: html BiBTeX pdf PostScript © Manfred Kerber, Martin Pollet
Model-Guided Proof Planning
Logical and Computational Aspects of Model-Based Reasoning; editor: Lorenzo Magnani and Nancy J. Nersessian and Claudio Pizzi, pages 143-162 Seungyeob Choi, Manfred Kerber, 2002
Available: html BiBTeX pdf PostScript © Kluwer Academic
On the Design of Mathematical Concepts
AI-2002: 15th Australian Joint Conference on Artificial Intelligence; editor: Bob McKay and John Slaney, pages 716, Springer, LNAI 2557 Manfred Kerber, Martin Pollet, 2002
Available: html BiBTeX pdf PostScript © Springer Verlag
LearnOmatic: System Description
CADE-2002: Conference on Automated Deduction; editor: Andrei Voronkov, pages 150-155, Springer, LNAI 2392 Mateja Jamnik, Manfred Kerber, Martin Pollet, 2002
Available: html BiBTeX pdf PostScript © Springer Verlag
Automatic Learning in Proof Planning
ECAI-2002: European Conference on Artificial Intelligence; editor: Frank van Harmelen, pages 282-286, IOS Press Mateja Jamnik, Manfred Kerber, Martin Pollet, 2002
Available: html BiBTeX pdf PostScript © IOS Press
On the Design of Mathematical Concepts
Calculemus Work-in-Progress-Papers; editor: Olga Caprotti and Volker Sorge Manfred Kerber, Martin Pollet, 2002
Available: html BiBTeX pdf PostScript © Manfred Kerber, Martin Pollet
On the Design of Mathematical Concepts
The University of Birmingham, School of Computer Science. Cognitive Science Research Papers, CSRP-02-06 Manfred Kerber, Martin Pollet, 2002
Available: html BiBTeX pdf PostScript © Manfred Kerber, Martin Pollet
Automatic Learning in Proof Planning
The University of Birmingham, School of Computer Science. Cognitive Science Research Papers, CSRP-02-03 Mateja Jamnik, Manfred Kerber, Martin Pollet, 2002
Available: html BiBTeX pdf PostScript © Mateja Jamnik, Manfred Kerber, Martin Pollet
Automatic Learning of Proof Methods in Proof Planning
The University of Birmingham, School of Computer Science. Cognitive Science Research Papers, CSRP-02-05 Mateja Jamnik, Manfred Kerber, Martin Pollet, Christoph Benzmüller, 2002
Available: html BiBTeX pdf PostScript © Mateja Jamnik, Manfred Kerber, Martin Pollet, Christoph Benzmüller
Experiments with an Agent-oriented Reasoning System
KI-2001 Symposium; editor: F. Baader and G. Brewka and T. Eiter, pages 409-424, Springer, LNAI 2174 Christoph Benzmüller, Mateja Jamnik, Manfred Kerber, Volker Sorge, 2001
Available: html BiBTeX pdf PostScript © Springer Verlag
Resource Guided Concurrent Deduction
Symbolic Calculation and Automated Reasoning: The CALCULEMUS-2000 Symposium; editor: Manfred Kerber and Michael Kohlhase, pages 243-244, A K Peters Mateja Jamnik, Manfred Kerber, Christoph Benzmüller, Volker Sorge, 2001
Available: html BiBTeX pdf PostScript © A K Peters
Towards Learning New Methods in Proof Planning
Symbolic Calculation and Automated Reasoning: The CALCULEMUS-2000 Symposium; editor: Manfred Kerber and Michael Kohlhase, pages 141-156, A K Peters Mateja Jamnik, Manfred Kerber, Christoph Benzmüller, 2001
Available: html BiBTeX pdf PostScript © A K Peters
Learning Methods Outlines in Proof Planning
The University of Birmingham, School of Computer Science. Cognitive Science Research Papers, CSRP-01-08 Mateja Jamnik, Manfred Kerber, Christoph Benzmüller, 2001
Available: html BiBTeX pdf PostScript © Mateja Jamnik, Christoph Benzmüller, Manfred Kerber
Towards Learning New Methods in Proof Planning
Workshop-Proceedings of the CADE-Workshop on The Role of Automated Deduction in Mathematics; editor: Simon Colton and Ursula Martin and Volker Sorge, pages 1-11, CADE Mateja Jamnik, Manfred Kerber, Christoph Benzmüller, 2000
Available: html BiBTeX pdf PostScript © Mateja Jamnik, Manfred Kerber, Christoph Benzmüller
Resource Guided Concurrent Deduction
Workshop-Proceedings of the AISB-2000 Workshop: How to Design a Functioning Mind; editor: Aaron Sloman, pages 137-138, AISB Christoph Benzmüller, Mateja Jamnik, Manfred Kerber, Volker Sorge, 2000
Available: html BiBTeX pdf PostScript © Christoph Benzmüller, Mateja Jamnik, Manfred Kerber, Volker Sorge
Towards Learning New Methods in Proof Planning
The University of Birmingham, School of Computer Science. Cognitive Science Research Papers, CSRP-00-09 Mateja Jamnik, Manfred Kerber, Christoph Benzmüller, 2000
Available: html BiBTeX pdf PostScript © Mateja Jamnik, Manfred Kerber, Christoph Benzmüller
Agent Based Mathematical Reasoning
Workshop-Proceedings of the CADE-Calculemus Workshop; editor: Alessandro Armando and Tudor Jebelean, CADE Christoph Benzmüller, Mateja Jamnik, Manfred Kerber, Volker Sorge, 1999
Towards Concurrent Resource Managed Deduction
The University of Birmingham, School of Computer Science. Cognitive Science Research Papers, CSRP-99-17 Christoph Benzmüller, Mateja Jamnik, Manfred Kerber, Volker Sorge, 1999
Available: BiBTeX pdf PostScript
Proof Planning - A Practical Approach to Mechanised Reasoning in Mathematics
Automated Deduction - A Basis for Applications; editor: Wolfgang Bibel and Peter H.~Schmitt, pages 77-95 Manfred Kerber, 1998
Available: BiBTeX pdf PostScript
Integrating Computer Algebra into Proof Planning
Journal of Automated Reasoning, 21, pages 327-355 Manfred Kerber, Michael Kohlhase, Volker Sorge, 1998
Available: BiBTeX pdf PostScript
Adaptation of Declaratively Represented Methods in Proof Planning
Annals of Mathematics and Artificial Intelligence, 23, pages 299-320 Xiaorong Huang, Manfred Kerber, Lassaad Cheikhrouhou, 1998
Available: BiBTeX pdf PostScript © Springer Verlag, http://dx.doi.org/10.1023/A:1018980611571
Proving Ground Completeness of Resolution by Proof Planning
FLAIRS-97, Proceedings of the 10th International Florida Artificial Intelligence Research Symposium; editor: Dankel II, Douglas D., pages 372-376, Florida AI Research Society, St.~Petersburg, Florida, USA Manfred Kerber, Arthur C. Sehn, 1997
Available: BiBTeX pdf PostScript
Proof Planning: A Practical Approach to Mechanised Reasoning in Mathematics
The University of Birmingham, School of Computer Science. Cognitive Science Research Papers, CSRP-97-24 Manfred Kerber, 1997
Available: BiBTeX pdf PostScript
Mechanising Partiality without Re-Implementation
The University of Birmingham, School of Computer Science. Cognitive Science Research Papers, CSRP-97-10 Manfred Kerber, Michael Kohlhase, 1997
Available: BiBTeX pdf PostScript
Integrating Computer Algebra with Proof Planning
Proceedings of DISCO, Conference on Design and Implementation of Symbolic Computation Systems; editor: Jaques Calmet and Carla Limongelli, pages 204-215, Springer, LNCS 1128 Manfred Kerber, Michael Kohlhase, Volker Sorge, 1996
Available: BiBTeX pdf PostScript © Springer Verlag
The Adaptation of Proof Methods by Reformulation
Proceedings of the First Workshop on Abstraction, Analogy and Metareasoning; editor: Alessandro Armando and Erica Melis, pages 40-48 Xiaorong Huang, Manfred Kerber, Lassaad Cheikhrouhou, 1996
Available: BiBTeX pdf PostScript
The Adaption of Proof Methods by Reformulations
Proceedings of the Fourth International Symposium on ``Artificial Intelligence and Mathematics''; editor: Henry Kautz and Bart Selman Xiaorong Huang, Manfred Kerber, Lassaad Cheikhrouhou, 1996
Available: BiBTeX pdf PostScript
Proving Ground Completeness of Resolution by Proof Planning
The University of Birmingham, School of Computer Science. Cognitive Science Research Papers, CSRP-96-16 Manfred Kerber, Arthur C. Sehn, 1996
Available: BiBTeX pdf PostScript
An Integration of Mechanised Reasoning and Computer Algebra that Respects Explicit Proofs
The University of Birmingham, School of Computer Science. Cognitive Science Research Papers, CSRP-96-09 Manfred Kerber, Michael Kohlhase, Volker Sorge, 1996
Available: BiBTeX pdf PostScript
Adapting the Diagonalization Method by Reformulations
Proceedings of the Symposium on Abstraction, Reformulation, and Approximation, SARA-95; editor: Alon Levy and Pandu Nayak Xiaorong Huang, Manfred Kerber, Lassaad Cheikhrouhou, 1995
Available: BiBTeX pdf PostScript
Reuse of Proofs by Meta-Methods
Proceedings of the IJCAI-Workshop on Formal Approaches to the Reuse of Plans, Proofs, and Programs; editor: Jana Köhler and Fausto Giunchiglia and Cordell Green and Christoph Walther, pages 46-50 Xiaorong Huang, Manfred Kerber, 1995
Available: BiBTeX pdf PostScript
Adaptation of Declaratively Represented Methods in Proof Planning
Fachbereich Informatik, Universität des Saarlandes, Saarbrücken, Germany. SEKI Report, SR-95-12 Xiaorong Huang, Manfred Kerber, Lassaad Cheikhrouhou, 1995
Available: BiBTeX pdf PostScript
Planning Mathematical Proofs with Methods
Journal of Information Processing and Cybernetics, EIK, 30, pages 277-291 Xiaorong Huang, Manfred Kerber, Jörn Richts, Arthur Sehn, 1994
Available: BiBTeX pdf PostScript
Adapting Methods to Novel Tasks in Proof Planning
KI-94: Advances in Artificial Intelligence; editor: Bernhard Nebel and Leonie Dreschler-Fischer, pages 379-390, Springer Verlag, Berlin, Germany Xiaorong Huang, Manfred Kerber, Michael Kohlhase, Jörn Richts, 1994
Available: BiBTeX pdf PostScript © Springer Verlag
A declarative language for formulating methods
Workshop-Proceedings der KI-94; editor: Jürgen Kunze and Herbert Stoyan, pages 277-278, GI, Bonn Xiaorong Huang, Manfred Kerber, Jörn Richts, Arthur Sehn, 1994
Available: BiBTeX pdf PostScript
Representing the Diagonalization Methods
Workshop-Proceedings der KI-94; editor: Jürgen Kunze and Herbert Stoyan, pages 279-280, GI, Bonn Xiaorong Huang, Manfred Kerber, Erica Melis, Jörn Richts, 1994
Available: BiBTeX pdf PostScript
Planning Mathematical Proofs with Methods
Fachbereich Informatik, Universität des Saarlandes, Saarbrücken, Germany. SEKI Report, SR-94-08 Xiaorong Huang, Manfred Kerber, Jörn Richts, Arthur Sehn, 1994
Available: BiBTeX pdf PostScript
Using Tactics to Reformulate Formulae for Resolution Theorem Proving
Second International Symposium on Artificial Intelligence and Mathematics Manfred Kerber, Axel Präcklein, 1992
Methods - The Basic Units for Planning and Verifying Proofs
Fachbereich Informatik, Universität des Saarlandes, Saarbrücken, Germany. SEKI Report, SR-92-20 Xiaorong Huang, Manfred Kerber, Michael Kohlhase, 1992
Available: BiBTeX pdf PostScript
Some Aspects of Analogy in Mathematical Reasoning
Analogical and Inductive Inference; International Workshop AII '89; editor: Klaus P. Jantke, pages 231-242, Springer-Verlag, Berlin, Germany Manfred Kerber, 1989
Available: BiBTeX pdf PostScript © Springer Verlag

© and maintained by Manfred Kerber, School of Computer Science, The University of Birmingham
Last update: 15.2.2010. The URL of this page is http://www.cs.bham.ac.uk/~mmk/publications/proofplanning.php.