Publications

Books

• Fleuriot, J. (2001). A Combination of Geometry Theorem Proving and Nonstandard Analysis, with Application to Newton’s Principia. Distinguished Dissertations Series, Springer.
• Ida T. and Fleuriot J. (Eds., 2013). Automated Deduction in Geometry, Lecture Notes in Artificial Intelligence, Volume 7993, Springer.
• Fleuriot J. and Ida T. (Eds., 2015). Geometric Reasoning. Special issue of the Annals of Mathematics and Artificial Intelligence, Volume 74, Issue 3-4, Springer.
• Fleuriot J., Wang D. and Calmet J. (Eds. 2018). Artificial Intelligence and Symbolic Computation. Lecture Notes in Artificial Intelligence, Volume 1110, Springer.

Edited Proceedings

• Fleuriot, J., Horner P., McIver A., and Smaill A. (2013).  ATx’12/WInG’12: Joint Proceedings of the Workshops on Automated Theory eXploration and on Invariant Generation , 6th International Joint Conference on Automated Reasoning 2012, EasyChair Proceedings (EPiC volume 17).
• Ida. T. and Fleuriot J. (2012). The 9th International Workshop on Automated Deduction in Geometry, Informatics Research Report, Edinburgh.

Refereed Articles (Not complete or up-to-date)
See also our AI Modelling Lab publication webpage

• Smola F., Fleuriot J. D. (2024). Linear Resources in Isabelle/HOL. To appear in the Journal of Automated Reasoning.
• Ho L., Pugh C., Seth S., Arakelyan S., Lone N., Lyall M. J., Anand A., Fleuriot J. D., Galdi P., Guthrie B. (2024). Predicting short- to medium-term care home admission risk in older adults: a systematic review of externally validated models. To appear in Age and Ageing.
• Moreno G. R., Restocchi R., Fleuriot J. D., Anand A., Mercer S., Guthrie B. (2024). Multimorbidity analysis with low condition counts: A robust Bayesian approach for small but important subgroups.  eBioMedicine, Volume 102, https://doi.org/10.1016/j.ebiom.2024.105081.
• Burton J. K.,  McMinn M., Vaughan J. E.,  Nightingale G., Fleuriot J., Guthrie B. (2024). Analysis of the impact of COVID-19 on Scotland’s care-homes from March 2020 to October 2021: national linked data cohort analysis. Age and Ageing, Volume 53, Issue 2,  https://doi.org/10.1093/ageing/afae015.
• Ho L., Pugh C., Seth S., Arakelyan S., Lone N., Lyall M. J., Anand A., Fleuriot J. D., Galdi P., Guthrie B. (2024). Performance of models for predicting one to three year mortality in older adults: a systematic review of externally validated models. Lancet Healthy Longevity.
• Zheng J., Papapanagiotou P., Fleuriot J. D. (2024). Alignment-based conformance checking over probabilistic events. Proceedings of the 57th Hawaii International Conference on System Sciences (HICSS-57).
• DeLong L. N., Gadiya Y., Fleuriot J. D., Domingo-Fernandez D. (2023). Neurosymbolic AI Reveals Biases and Limitations in ML-Driven Drug Discovery.  In New Frontiers of AI for Drug Discovery and Development, NeurIPS.
• DeLong L. N., Fernández Mir R, Ji Z., Smith F. N. C., Fleuriot J. D. (2023). Neurosymbolic AI for Reasoning on Biomedical Knowledge Graphs. Proceedings of Knowledge and Logical Reasoning in the Era of Data-driven Learning, ICML. See also arXiv:2307.0841.
• Livingstone S., Morales D. R., Fleuriot J., Donnan P. T., Guthrie B. (2023). External validation of the QLifetime cardiovascular risk prediction tool: population cohort study. BMC Cardiovasc Disord 23, 194.
• Charlton E. C., Poon M. T. C., Brennan P. and Fleuriot J. D. (2023). Development of prediction models for one-year brain tumour survival using machine learning: a comparison of accuracy and interpretability. Computer Methods and Programs in Biomedicine, Volume 233. https://doi.org/10.1016/j.cmpb.2023.107482.
• Chevallier M., Whyte M. and Fleuriot J. D. (2022). Constrained Training of Neural Networks via Theorem Proving.  Proceedings of OVERLAY 2022,  as part of the 21st International Conference of the Italian Association for Artificial Intelligence (AIxIA 2022), CEUR, Volume 3311, pp. 7-12. Longer version available as arXiv:2207.03880.
• Romero Moreno G., Restocchi V. and Fleuriot J. D. (2022). Building Co-morbidity Networks via Bayesian Network Reconstruction. Proceedings of the 11th International Conference on Complex Networks and their Applications.
• Schmoetten R., Palmer J. E. and Fleuriot J. D. (2022). Towards Formalising Schutz’ Axioms for Minkowski Spacetime in Isabelle/HOL. To appear in the Journal of Automated Reasoning.
• MacKenzie C., Huch F., Vaughan J. and Fleuriot J. D. (2022)  Re-imagining the Isabelle Archive of Formal Proofs. To appear in the proceedings of CICM 2022.
• Gunatilleke J., Fleuriot J. and Anand. A. (2022). A literature review on the analysis of symptom-based clinical pathways: Time for a different approach?  PLOS Digital Health.
• Restocchi V., Gaete Villegas J. and Fleuriot J. D. (2022). Multimorbidity profiles and stochastic block modeling improve ICU patient clustering. Artificial Intelligence for Health at IEEE/ACM CCGRID 2022, 925-932.
• Schmoetten R., Palmer J.,  and Fleuriot J. D. (2021).Formalising Geometric Axioms for Minkowski Spacetime and Without-Loss-of-Generality Theorems. Proceedings of the 13th International Conference in Automated Deduction in Geometry, Electronic Proceedings in Theoretical Compuster Science (EPTCS) 352, 116-128.
• Burton J, McMinn M., Vaughan J., Fleuriot J., Guthrie B. (2021). Care-home outbreaks of COVID-19 in Scotland March to May 2020: national linked data cohort analysis. Age and Ageing Journal, Volume 50, Issue 5, September 2021, 1482–1492, Oxford University Press.
• Papapanagiotou P. and Fleuriot J. (2020). Object-level Reasoning with Logics Encoded in HOL Light. To appear in EPTCS.
• Fleuriot J. D. (2020). Mechanizing Mathematics: From Dream to Reality. Chapter to appear in 45 Years of Automated Reasoning (Ed. G. Michaelson), Springer.
• Papapanagiotou P., Vaughan J., Smola F, and Fleuriot J. (2020). A Real-world Case Study of Process and Data Driven Predictive Analytics for Manufacturing Workflows. To appear in the proceedings of the 54th Hawaii International Conference on System Sciences (HICSS-54).
• Wingfield L., Ceresa C., Thorogood S., Fleuriot J, Knight S. (2020). Artificial Intelligence and Liver Transplant: Predicting Survival of Individual Grafts, A Systematic Review. Liver Transplantation, Volume 26, Issue7, 922-934 .
• Papapanagiotou P. and Fleuriot J. (2019). A Pragmatic, Scalable Approach to Correct-by-construction Process Composition Using Classical Linear Logic Inference. Lecture Notes in Computer Science, Volume 11408, Springer, 77-83.
• Palmer J. and Fleuriot J. (2018) Mechanising an Independent Axiom System for Minkowski Space-time. Proceedings of the 12th International Conference on Automated Deduction in Geometry, 64-79.
• Morris I. and Fleuriot J. (2018). Towards a Mechanisation in Isabelle of Birkhoff’s Ruler and Protractor Geometry. Proceedings of the 12th International Conference on Automated Deduction in Geometry, 46-63.
• Narboux J., Janicic P. and Fleuriot J. (2018). Computer-assisted Theorem Proving in Synthetic Geometry. Chapter in the Handbook of Geometric Constraint Systems Principles (ISBN 9781498738910), 21-44, Chapman and Hall/CRC, July 2018.
• Jiang Y., Papapanagiotou P. and Fleuriot J. (2018). Machine Learning for Automated Inductive Theorem Proving. Proceedings of the 13th International Artificial Intelligence and Symbolic Computation (AISC) Conference 2018, Lecture Notes in Artificial Intelligence, Volume 11110, 87-103.
• Papapanagiotou P. and Fleuriot J. (2018). Correct-by-construction Process Composition Using Classical Linear Logic Inference. Logic-Based Program Synthesis and Transformation (LOPSTR) Symposium 2018.
• Wingfield L., Kulendran M., Khan O., Fleuriot J. (2017) Bringing Artificial Intelligence to Patient Care in Bariatric Surgery: A Feasibility Study. International Journal of Surgery, Volume 47 , S92.
• Papapanagiotou P. and Fleuriot J. (2017). WorkflowFM: A Logic-based Formal Verification Framework for Process Specification and Composition. Proceedings of the 26th International Conference on Automated Deduction (CADE 26). LNCS Volume 10395, 357-370, Springer
• Dewanti, A., Papapanagiotou, P., Gilhooly, C., Fleuriot, J., Manataki, A. & Moss, L. (2017). Development of workflow-based guidelines for the care of burns in Scotland. Proceedings of the 9th International Conference e-Health 2017,  155-158.
• Alexandru C-A., Clutterbuck D., Papapanagiotou P., Fleuriot J. and Manataki A. (2017). A Step Towards the Standardisation of HIV Care Practices, 10th International Conference on Health Informatics.
• Papapanagiotou P., Dewanti A., Manataki A., Fleuriot J., Gilhooly C., Moss L. (2016). Workflow modelling of burns care protocols. The 26th SICS Annual Scientific Meeting, Scottish Intensive Care Society.
• Obua S., Scott P. and Fleuriot J. (2016). ProofScript: Proof Scripting for the Masses. International Colloquium on Theoretical Aspects of Computing, ICTAC 2016, Springer LNCS, Volume 9965, 333-348.
• Manataki A., Fleuriot J. and Papapanagiotou P. (2016)  A workflow-driven, formal methods approach to the generation of structured checklists for intra-hospital patient transfers. The IEEE Journal of Biomedical and Health Informatics, Issue 99, 1-7.
• Scott P. and Fleuriot J. (2016). Compass-free Navigation of Mazes. EPiC Series in Computing, Volume 39, 143-155.
• Obua S., Fleuriot J., Scott P., and Aspinall D. (2015). Type Inference for ZFH. Proceedings of the International Conference on Intelligent Mathematics (CICM 2015), Springer LNCS, Volume 9150, 87-101.
• Papapanagiotou P. and Fleuriot J. D. (2015). Modelling and implementation of correct by construction healthcare workflows. Proceedings of Process-oriented Information Systems in Healthcare (ProHealth’14), LNBIB 202, 28-39.
• Papapanagiotou P., Fleuriot J., Manataki A., Winter A., Nandwani R., Clutterbuck D. and Wilks D. (2014). Rigorous development of computer based Integrated Care Pathways for HIV patients.  Proceedings of the Health Informatics Scotland Conference 2014.
• Manataki A., Fleuriot J. D., and Papapanagiotou P. (2014). Tracheostomy transfers: A case study in the application of formal methods to intra-hospital patient transfers. Proceedings of the 27th IEEE International Symposium on Computer-Based Medical Systems (CBMS 2014).
• Papapanagiotou P. and Fleuriot J. D. (2014). Formal Verification of Collaboration Patterns in Healthcare. Behaviour and Information Technology, 33 (12): 1278-1293.
• Meikle L. I. and Fleuriot J. D. (2012): Integrating Systems around the User: Combining Isabelle, Maple, and QEPCAD in the Prover’s Palette. Electr. Notes Theor. Comput. Sci. 285: 115-119.
• Scott, P. and Fleuriot, J. D. (2012) . Towards a Synthetic Proof of the Polygonal Jordan Curve Theorem. In Proceedings of the Automated Deduction in Geometry workshop (ADG 2012), 147-156.
• Scott, P. and Fleuriot, J. D. (2012) A Combinator Language for Theorem Discovery. In Proceedings of the Conferences on Intelligent Computer Mathematics (CICM 2012), Lecture Notes in Computer Science,  Volume 7362,  371-385, DOI:10.1007/978-3-642-31374-5_25.
• Papapanagiotou, P., Fleuriot, J. D., and Grando A. (2012) Rigorous process-based modelling of patterns for collaborative work in healthcare teams. In Proceedings of the 25th IEEE International Symposium on Computer-Based Medical Systems (CBMS 2012), DOI:10.1109/CBMS.2012.6266330.
• Papapanagiotou, P., Fleuriot, J. D. , and Wilson, S. (2012). Diagrammatically-driven formal verification of web-services composition. In Proceedings of the Diagrams 2012 conference, Lecture Notes in Computer Science Volume 7352, 241-255, DOI: 10.1007/978-3-642-31223-6_25.
• Fleuriot, J. D. (2011). Exploring the Foundations of Discrete Analytical Geometry in Isabelle/HOL. Lecture Notes in Computer Science, 2011, Volume 6877/2011, 34-50, DOI: 10.1007/978-3-642-25070-5_2.
• Papapanagiotou, P. and Fleuriot, J. D. (2011). Formal verification of Web Services composition using Linear Logic and the pi-calculus.  Proceedings of the 9th IEEE European Conference on Web Services (ECOWS 2011), 1 – 38, DOI: 10.1109/ECOWS.2011.18.
• Scott, P. and Fleuriot J. D. (2011). Composable Discovery Engines for Interactive Theorem Proving. Lecture Notes in Computer Science, 2011, Volume 6898/2011, 370-375, DOI: 10.1007/978-3-642-22863-6_28.
• Scott, P. and Fleuriot J. D. (2011). An Investigation of Hilbert’s Implicit Reasoning through Proof Discovery in Idle-Time. Lecture Notes in Computer Science, 2011, Volume 6877/2011, 182-200, DOI: 10.1007/978-3-642-25070-5_11.
• Papapanagiotou, P. and Fleuriot J. D. (2011). A theorem proving framework for the formal verification of Web Services Composition. Proceedings of the 7th International Workshop on Automated Specification and Verification of Web Systems, EPTCS 61, pages 1-17, DOI: 10.4204/EPTCS.61.
• Wilson, S. and Fleuriot, J. D. and Smaill. A. (2010). Automation for Dependently Typed Functional Programming. Fundamenta Informaticae.
• Papapanagiotou, P. and Fleuriot J. D. (2010). A Isabelle-like Procedural Language for HOL Light. In Proceedings of LPAR 2010, LNCS.
• Meikle, L. and Fleuriot, J. D. (2010). Integrating Systems around the User: Combining Isabelle, Maple, and QEPCAD in the Prover’s Palette. In Proceedings of the User Interfaces for Theorem Provers Workshop, FLOC 2010.
• Meikle, L. and Fleuriot, J. D. (2010). Automation for Geometry in Interactive Theorem Provers. In Proceedings of PAAR, FLOC 2010.
• Scott, P. and Fleuriot, J. D. (2010). Idle Time Proofs in Geometry. Proceedings of Automated Deduction in Geometry (ADG 2010), TU Munich.
• Wilson, S. and Fleuriot, J. D. and Smaill. (2010). Inductive Proof Automation for Coq. Proceedings of the Second Coq Workshop, FLOC 2010.
• Meikle, L. and Fleuriot, J. D. (2008). Combining Isabelle and QEPCAD-B in the Prover’s Palette. In Intelligent Computer Mathematics, volume 5144 of Lecture Notes in Computer Science, pages 314-330.
• Meikle, L. and Fleuriot, J. D. (2008). Prover’s Palette: A user-centric approach to verification with Isabelle and QEPCAD-B. In Computer Aided Verification, CAV, volume 5123 of Lecture Notes in Computer Science, pages 309-313. Springer.
• Meikle, L. I. and Fleuriot, J. D. (2006). Mechanical theorem proving in computational geometry. In Automated Deduction in Geometry, volume 3763 of LNCS, pages 1-18. Springer-Verlag.
• Dixon, L. and Fleuriot, J. D. (2005). A proof-centric approach to mathematical assistants. Journal of Applied Logic: Towards Computer Aided Mathematics Systems, 4(4):505-532.
• Bundy, A., Dixon, L., Gow, J. and Fleuriot, J. D. (2005). Constructing induction rules for deductive synthesis proofs. In Electronic notes in Theoretical Computer Science: Constructive Logic for Automated Software Engineering, pages 3-21.
• Wilson, S. and Fleuriot, J. D. (2005). Combining dynamic geometry, automated geometry theorem proving and diagrammatic proofs. In Proceedings of the User Interfaces for Theorem Provers Workshop.
• Dixon, L. and Fleuriot, J. D. (2004). Higher order rippling in IsaPlanner. In Theorem Proving in Higher Order Logics, TPHOLs 2004, volume 3223 of LNCS, pages 83-98. Springer.
• Brak, R. L., Fleuriot, J. D. and McGinnis, J. (2004). Theorem proving for protocol languages. In Proceedings of the Second European Workshop on Multi-Agent Systems (EUMAS 2004).
• Dixon, L. and Fleuriot, J. D. (2003). IsaPlanner: A prototype proof planner in Isabelle. In Proceedings of the 19th International Conference on Automated Deduction, CADE, volume 2741 of LNCS, pages 279-283.
• Meikle, L. I. and Fleuriot, J. D. (2003). Formalizing Hilbert’s grundlagen in Isabelle/Isar. In Theorem Proving in Higher Order Logics: 16th International Conference, TPHOLs 2003, volume 2758 of Lecture Notes in Computer Science, pages 319-334.
• Maclean, E., Fleuriot, J. and Smaill, A. (2002). Proof-planning non-standard analysis. In Proceedings of the Seventh International Symposium on Artificial Intelligence and Mathematics, Fort Lauderdale, Florida.
• Fleuriot, J. D. (2001). Theorem proving in infinitesimal geometry. Logic Journal of the IGPL, 9(3):471-498.
• Heneveld, A., Maclean, E., Bundy, A., Fleuriot, J. and Smaill, A. (2001). Solving integrals at the method level. In Kerber, M. and Kohlhase, M., (eds.), Symbolic Computation and Automated Reasoning, pages 251-252.
• Fleuriot, J. D. (2001). Nonstandard geometric proofs. In Wang, D. and Richter-Gebert, J., (eds.), Automated Deduction in Geometry, volume 2061, pages 238260. A shorter version appeared in the published in Proceedings of ADG 2000, pages 259-279, Zurich, Switzerland.
• Fleuriot, J. D. and Paulson, L. C. (2000). Mechanizing nonstandard real analysis. LMS Journal of Computation and Mathematics, 3(14):140-190.
• Fleuriot, J. D. (2000). On the mechanization of real analysis in Isabelle/HOL. In Harrison, J. and Aagaard, M., (eds.), Theorem Proving in Higher Order Logics: 13th International Conference,TPHOLs 2000, volume 1869 of Lecture Notes in Computer Science, pages 146-162. Springer-Verlag.
• Fleuriot, J. D. and Paulson, L. C. (1999). Proving Newton’s Propositio Kepleriana using geometry and nonstandard analysis in Isabelle. In Automated Deduction in Geometry 1998, volume 1669 of Lecture Notes in Artificial Intelligence, pages 47-66.
• Fleuriot, J. D. and Paulson, L. C. (1998). A combination of nonstandard analysis and geometry theorem proving, with application to Newton’s Principia. In Proceedings of the Fifteenth International Conference on Automated Deduction, CADE, volume 1421.

In Limbo

• Wilson, S. and Fleuriot, J. D. Geometry Explorer: Combining dynamic geometry, automated geometry theorem proving and diagrammatic proofs. To appear in: Electronic Notes in Theoretical Computer Science (Camera ready version submitted but awaiting to be published as a UITP special issue since 2006!).