Dr Manfred Kerber

School of Computer Science
Honorary Senior Lecturer

Contact details

Email: m.kerber@cs.bham.ac.uk

Address: School of Computer Science
University of Birmingham
Edgbaston
Birmingham
B15 2TT
UK

Manfred Kerber's research focuses on automated reasoning and mathematical knowledge representation. In 1992, he earned a PhD for research on representing mathematical knowledge and translations of higher order logic into first order logic for automatic use by first order theorem provers. As part of this work he formalised and formally proved many theorems from a mathematical textbook. After his PhD he led 1992-1996 the Omega group which built an interactive proof development environment. After taking up a lectureship at the University of Birmingham in 1996, Kerber led projects related to automated reasoning (funded by the EPSRC and the EU) and (co-)organised a number of events in related fields. Kerber remains an honorary member of staff in the School of Computer Science at the University of Birmingham.

For more information, please see Manfred's Computer Science Profile

Qualifications

PhD (Dr. rer. nat.) in Computer Science, 1992
Teacher Examination (1.Staatsexamen) in Mathematics and Physics, 1985
MSc (Dipl. Math.) in Mathematics, 1983

Biography

Manfred Kerber studied as an undergraduate Mathematics at the University of Kaiserslautern, Germany, and received an MSc there in 1983. In 1985 he passed the first Teacher Examination in Mathematics and Physics. He then did a PhD in Computer Science, also at the University of Kaiserslautern. After the PhD he was a Senior Research Fellow at the University of the Saarland in Saarbruecken (1992-1995). Since 1996 he has been a lecturer at the University of Birmingham (Senior Lecturer since 2001).

Teaching

Manfred Kerber has taught widely in Artificial Intelligence (Introduction to Artificial Intelligence, AI Techniques, Machine Learning, Planning, Automated Reasoning) and Computer Science (Logic, Data Structures, Verification, Professional Issues). He is currently teaching the introductory Software Workshop for students on the MSc in Computer Science programme.

Postgraduate supervision

Manfred Kerber does not take on any Doctoral Research Students any more.

Research

In his work Kerber has explored (in collaboration with others) the strengths and weaknesses of different formal systems, established the robustness of agent-oriented theorem proving, studied the value of machine learning for the formation of proof planning methods (his interest in machine learning goes beyond theorem proving). Further interests involve the study of partiality in reasoning, model-based approaches, and the integration of reasoning and computation. A long standing interest is about the relationship between formal and informal representations and the consequences for formalising mathematical reasoning. In his work on why the Lucas-Penrose argument is invalid, he explored the consequences of Goedel's incompleteness theorem. Recently he started to investigate properties of heuristic search in propositional logic. A major focus of his research is the application of formal techniques in the field of economics, in particular, in auction theory and risk analysis.

Publications

Recent publications

Book

Kerber, M, Carette, J, Kaliszyk, C, Rabe, F & Sorge, V (eds) 2015, Intelligent computer mathematics: International conference, CICM 2015 Washington, DC, USA, july 13–17, 2015 proceedings. Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), vol. 9150, vol. 9150, Springer. https://doi.org/10.1007/978-3-319-20615-8

Article

Kammueller, F, Kerber, M & Probst, CW 2017, 'Insider threats and auctions: formalization, mechanized proof, and code generation', Journal of Wireless Mobile Networks, Ubiquitous Computing, and Dependable Applications, vol. 8, no. 1, pp. 44-78. https://doi.org/10.22667/JOWUA.2017.03.31.044

Kerber, M, Lange-Bever, C & Rowat, C 2016, 'An introduction to mechanized reasoning', Journal of Mathematical Economics, vol. 66, pp. 26-39. https://doi.org/10.1016/j.jmateco.2016.06.005

Mackenzie, S, Kerber, M & Rowat, C 2015, 'Pillage games with multiple stable sets', International Journal of Game Theory, vol. 44, no. 4, pp. 993-1013. https://doi.org/10.1007/s00182-015-0462-1

Caminati, MB, Kerber, M, Lange-Bever, C & Rowat, C 2015, 'VCG - Combinatorial Vickrey-Clarke-Groves Auctions', Archive of Formal Proofs, pp. 1-134. <http://afp.sourceforge.net/entries/Vickrey_Clarke_Groves.shtml>

Rowat, C & Kerber, M 2014, 'Sufficient conditions for unique stable sets in three agent pillage games', Mathematical Social Sciences, vol. 69, pp. 69-80. https://doi.org/10.1016/j.mathsocsci.2014.02.003

Chapter

Kerber, M 2014, A Proof and Some Representations. in JL Wyatt, DD Petters & D Hogg (eds), From Animals to Robots and Back: Reflections on Hard Problems in the Study of Cognition : A Collection in Honour of Aaron Sloman. Cognitive Systems Monographs, vol. 22, Springer, pp. 65-73. https://doi.org/10.1007/978-3-319-06614-1_5

Abstract

Caminati, MB, Kerber, M & Rowat, C 2015, 'Reasoning about Dynamic Auctions', Automated Reasoning Workshop (ARW), Birmingham, United Kingdom, 9/04/15 - 10/04/15 pp. 15-16. <http://events.cs.bham.ac.uk/arw15/ARW15_proceedings.pdf>

Caminati, MB, Kerber, M, Lange-Bever, C & Rowat, C 2014, 'Reasoning about Auctions', Joint Automated Reasoning Workshop and Deduktionstreffen, Vienna, United Kingdom, 23/07/14 - 24/07/14 pp. 10-11. <http://istina.msu.ru/media/publications/article/a43/a58/6436063/proceedings.pdf#page=10>

Conference contribution

Caminati, MB, Kerber, M, Lange-Bever, C & Rowat, C 2015, Sound auction specification and implementation. in T Roughgarden, M Feldman & M Schwarz (eds), EC '15 Proceedings of the Sixteenth ACM Conference on Economics and Computation . Association for Computing Machinery , New York, NY, USA, pp. 547-564, 16th ACM Conference on Economics and Computation, Portland, United States, 15/06/15. https://doi.org/10.1145/2764468.2764511

Caminati, MB, Kerber, M, Lange, C & Rowat, C 2014, Set Theory or Higher Order Logic to Represent Auction Concepts in Isabelle? in SM Watt, JH Davenport, AP Sexton, P Sojka & J Urban (eds), Intelligent Computer Mathematics: International Conference, CICM 2014, Coimbra, Portugal, July 7-11, 2014. Proceedings. vol. 8543 LNCS, Lecture Notes in Computer Science, vol. 8543, Springer, pp. 236-251, Conference on Intelligent Computer Mathematics, Coimbra, United Kingdom, 7/07/14. https://doi.org/10.1007/978-3-319-08434-3_18

Data set/Database

Caminati, MB, Kerber, M & Rowat, C, Problem set for first order theorem provers in the TPTP format, 2015, Data set/Database. <https://github.com/formare/auctions/blob/master/tptp>

Editorial

Kerber, M, Lange, C & Rowat, C 2014, 'Foreword', Mathematics in Computer Science, vol. 8, no. 1, pp. 1-4. https://doi.org/10.1007/s11786-014-0178-9

Paper

Kammueller, F & Kerber, M 2016, 'Investigating airplane safety and security against insider threats using logical modeling', Paper presented at IEEE Symposium on Security and Privacy, 37th, San Jose, CA, United States, 23/05/16 - 25/05/16. https://doi.org/10.1109/SPW.2016.47

Caminati, MB, Kerber, M & Rowat, C 2014, 'Budget imbalance criteria for auctions: A formalized theorem', Paper presented at Trends in Contemporary Computer Science, Białystok, Poland, 1/07/14 - 4/07/14 pp. 35-44. <http://alioth.uwb.edu.pl/~mml/6pcm/ComputerScience/Monograph-ComputerSciencePodlasie2014.pdf>

View all publications in research portal