Edinburgh Research Explorer
Profile photo
Phone: +44 131 650 9342Fax: +44 131 651 1426

Willingness to take Ph.D. students: Yes

Research Interests

Mechanical geometry theorem proving, mechanization of standard and nonstandard analysis, interactive and automatic proofs.


1995-1999PhD in Automated Reasoning, University of Cambridge
 Thesis title: A combination of geometry theorem proving and nonstandard analysis, with application to Newton's Principia
1991-1995MEng Computing, Imperial College of Science, Technology and Medicine, University of London


Dr. Jacques Fleuriot received a  First Class Honours MEng Computing degree in Artificial Intelligence from Imperial College, London (1995) and a PhD in Automated Reasoning from the University of Cambridge (May 1999).  He received scholarships from the Government of Mauritius, Imperial College, The University of Cambridge and the Overseas Research Students Awards Scheme in support of his studies.  His PhD focused on the mechanization of proofs from Newton's Principia using the proof assistant Isabelle.  He received a British Computer Society Distinguished Dissertation Award for this work in 2000.  In 1999, after completing his PhD, he was appointed to the post of Lecturer in Automated Reasoning at the School of Informatics at the University of Edinburgh.

Dr. Fleuriot has been principal investigator on recent grants involving diverse areas such as collaborative theorem proving and computer-based modelling for healthcare.  He has been co-investigator on several grants on mathematical reasoning including a current EPSRC platform grant.  He is currently the principal supervisor for several PhD students and. over the years, has acted as principal or co-supervisor for over 10 successful PhD students.  He currenlty teaches courses in automated reasoning and formal verification to both undergraduates and masters students.

Research outputs

  1. Machine Learning for Automated Inductive Theorem Proving

    Research output: Chapter in Book/Report/Conference proceedingConference contribution

  2. Computer-Assisted Theorem Proving in Synthetic Geometry

    Research output: Chapter in Book/Report/Conference proceedingChapter (peer-reviewed)

  3. Correct-by-construction Process Composition Using Classical Linear Logic Inference

    Research output: Chapter in Book/Report/Conference proceedingConference contribution

View all (49) »

Research activities & awards

  1. IJCAR 2012 - The 6th International Joint Conference on Automated Reasoning

    Activity: Participating in or organising an event typesParticipation in conference

  2. The 9th International Workshop on Automated Deduction in Geometry

    Activity: Participating in or organising an event typesParticipation in workshop, seminar, course

View all (2) »

ID: 11500