Proving Newton's Propositio Kepleriana Using Geometry and Nonstandard Analysis in Isabelle. - Jacques D. Fleuriot; Lawrence C. Paulson (Automated Deduction in Geometry, 1998)

A Combination of Nonstandard Analysis and Geometry Theorem Proving, with Application to Newton's Principia. - Jacques D. Fleuriot; Lawrence C. Paulson (CADE, 1998)

Nonstandard Geometric Proofs. - Jacques D. Fleuriot (Automated Deduction in Geometry, 2000)

On the Mechanization of Real Analysis in Isabelle/HOL. - Jacques D. Fleuriot (TPHOLs, 2000)

Mechanizing Nonstandard Real Analysis. - Jacques D. Fleuriot; Lawrence C. Paulson (LMS J. Comput. Math., 2000)

Theorem Proving in Infinitesimal Geometry. - Jacques D. Fleuriot (Log. J. IGPL, 2001)

Proof planning Non-standard Analysis. - Ewen Maclean; Jacques D. Fleuriot; Alan Smaill (AI&M, 2002)

IsaPlanner: A Prototype Proof Planner in Isabelle. - Lucas Dixon; Jacques D. Fleuriot (CADE, 2003)

Formalizing Hilbert's Grundlagen in Isabelle/Isar. - Laura I. Meikle; Jacques D. Fleuriot (TPHOLs, 2003)

Mechanical Theorem Proving in Computational Geometry. - Laura I. Meikle; Jacques D. Fleuriot (Automated Deduction in Geometry, 2004)

Higher Order Rippling in IsaPlanner. - Lucas Dixon; Jacques D. Fleuriot (TPHOLs, 2004)

Constructing Induction Rules for Deductive Synthesis Proofs. - Alan Bundy; Lucas Dixon; Jeremy Gow; Jacques D. Fleuriot (CLASE, 2005)

A proof-centric approach to mathematical assistants. - Lucas Dixon; Jacques D. Fleuriot (J. Appl. Log., 2006)

Combining Isabelle and QEPCAD-B in the Prover's Palette. - Laura I. Meikle; Jacques D. Fleuriot (AISC/MKM/Calculemus, 2008)

Prover's Palette: A User-Centric Approach to Verification with Isabelle and QEPCAD-B. - Laura I. Meikle; Jacques D. Fleuriot (CAV, 2008)

Exploring the Foundations of Discrete Analytical Geometry in Isabelle/HOL. - Jacques D. Fleuriot (Automated Deduction in Geometry, 2010)

An Investigation of Hilbert's Implicit Reasoning through Proof Discovery in Idle-Time. - Phil Scott; Jacques D. Fleuriot (Automated Deduction in Geometry, 2010)

Automation for Geometry in Isabelle/HOL. - Laura I. Meikle; Jacques D. Fleuriot (PAAR@IJCAR, 2010)

An Isabelle-Like Procedural Mode for HOL Light. - Petros Papapanagiotou; Jacques D. Fleuriot (LPAR (Yogyakarta), 2010)

Integrating Systems around the User: Combining Isabelle, Maple, and QEPCAD in the Prover's Palette. - Laura I. Meikle; Jacques D. Fleuriot (UITP, 2010)

Automation for Dependently Typed Functional Programming. - Sean Wilson; Jacques D. Fleuriot; Alan Smaill (Fundam. Informaticae, 2010)

Formal Verification of Web Services Composition Using Linear Logic and the pi-calculus. - Petros Papapanagiotou; Jacques D. Fleuriot (ECOWS, 2011)

Composable Discovery Engines for Interactive Theorem Proving. - Phil Scott; Jacques D. Fleuriot (ITP, 2011)

A theorem proving framework for the formal verification of Web Services Composition - Petros Papapanagiotou; Jacques D. Fleuriot (WWV, 2011)

A Combinator Language for Theorem Discovery. - Phil Scott; Jacques D. Fleuriot (AISC/MKM/Calculemus, 2012)

Rigorous process-based modelling of patterns for collaborative work in healthcare teams. - Petros Papapanagiotou; Jacques D. Fleuriot; Adela Grando (CBMS, 2012)

Diagrammatically-Driven Formal Verification of Web-Services Composition. - Petros Papapanagiotou; Jacques D. Fleuriot; Sean Wilson (Diagrams, 2012)

Modelling and Implementation of Correct by Construction Healthcare Workflows. - Petros Papapanagiotou; Jacques D. Fleuriot (Business Process Management Workshops, 2014)

Tracheostomy Transfers: A Case Study in the Application of Formal Methods to Intra-hospital Patient Transfers. - Areti Manataki; Jacques D. Fleuriot; Petros Papapanagiotou (CBMS, 2014)

Formal verification of collaboration patterns in healthcare. - Petros Papapanagiotou; Jacques D. Fleuriot (Behav. Inf. Technol., 2014)

ProofPeer: Collaborative Theorem Proving. - Steven Obua; Jacques D. Fleuriot; Phil Scott; David Aspinall 001 (CoRR, 2014)

Type Inference for ZFH. - Steven Obua; Jacques D. Fleuriot; Phil Scott; David Aspinall 001 (CICM, 2015)

ProofScript: Proof Scripting for the Masses. - Steven Obua; Phil Scott; Jacques D. Fleuriot (ICTAC, 2016)

Compass-free Navigation of Mazes. - Phil Scott; Jacques D. Fleuriot (SCSS, 2016)

Preface to the special issue on geometric reasoning. - Jacques D. Fleuriot; Tetsuo Ida (Ann. Math. Artif. Intell., 2016)

Social Network Processes in the Isabelle and Coq Theorem Proving Communities. - Jacques D. Fleuriot; Steven Obua; Phil Scott (CoRR, 2016)

A Step Towards the Standardisation of HIV Care Practices. - Cristina Adriana Alexandru; Daniel Clutterbuck; Petros Papapanagiotou; Jacques D. Fleuriot; Areti Manataki (HEALTHINF, 2017)

WorkflowFM: A Logic-Based Framework for Formal Process Specification and Composition. - Petros Papapanagiotou; Jacques D. Fleuriot (CADE, 2017)

Local Lexing. - Steven Obua; Phil Scott; Jacques D. Fleuriot (CoRR, 2017)

Compiling Purely Functional Structured Programs. - Phil Scott; Steven Obua; Jacques D. Fleuriot (CoRR, 2017)

Bootstrapping LCF Declarative Proofs. - Phil Scott; Steven Obua; Jacques D. Fleuriot (CoRR, 2017)

A Workflow-Driven Formal Methods Approach to the Generation of Structured Checklists for Intrahospital Patient Transfers. - Areti Manataki; Jacques D. Fleuriot; Petros Papapanagiotou (IEEE J. Biomed. Health Informatics, 2017)

Machine Learning for Inductive Theorem Proving. - Yaqing Jiang; Petros Papapanagiotou; Jacques D. Fleuriot (AISC, 2018)

A Pragmatic, Scalable Approach to Correct-by-Construction Process Composition Using Classical Linear Logic Inference. - Petros Papapanagiotou; Jacques D. Fleuriot (LOPSTR, 2018)

The Boyer-Moore Waterfall Model Revisited. - Petros Papapanagiotou; Jacques D. Fleuriot (CoRR, 2018)

Correct-by-construction Process Composition Using Classical Linear Logic Inference. - Petros Papapanagiotou; Jacques D. Fleuriot (CoRR, 2018)

Where are the Natural Numbers in Hilbert's Foundations of Geometry? - Phil Scott; Jacques D. Fleuriot (CoRR, 2019)

Object-Level Reasoning with Logics Encoded in HOL Light. - Petros Papapanagiotou; Jacques D. Fleuriot (LFMTP, 2020)

A Real-world Case Study of Process and Data Driven Predictive Analytics for Manufacturing Workflows. - Petros Papapanagiotou; James Vaughan; Filip Smola; Jacques D. Fleuriot (HICSS, 2021)

Real Exponents as the Limits of Sequences of Rational Exponents. - Jacques D. Fleuriot (Arch. Formal Proofs, 2021)

Schutz' Independent Axioms for Minkowski Spacetime. - Richard Schmoetten; Jake E. Palmer; Jacques D. Fleuriot (Arch. Formal Proofs, 2021)

Hyperdual Numbers and Forward Differentiation. - Filip Smola; Jacques D. Fleuriot (Arch. Formal Proofs, 2021)

An Evaluation of the Archive of Formal Proofs. - Carlin MacKenzie; Jacques D. Fleuriot; James Vaughan (CoRR, 2021)

Interpretable Machine Learning Classifiers for Brain Tumour Survival Prediction. - Colleen E. Charlton; Michael Tin Chung Poon; Paul M. Brennan; Jacques D. Fleuriot (CoRR, 2021)

Formalising the Foundations of Discrete Reinforcement Learning in Isabelle/HOL. - Mark Chevallier; Jacques D. Fleuriot (CoRR, 2021)

Formalising Geometric Axioms for Minkowski Spacetime and Without-Loss-of-Generality Theorems. - Richard Schmoetten; Jake E. Palmer; Jacques D. Fleuriot (ADG, 2021)

Dr.Aid: Supporting Data-governance Rule Compliance for Decentralized Collaboration in an Automated Way. - Rui Zhao 009; Malcolm P. Atkinson 001; Petros Papapanagiotou; Federica Magnoni; Jacques D. Fleuriot (Proc. ACM Hum. Comput. Interact., 2021)

Constrained Training of Neural Networks via Theorem Proving. - Mark Chevallier; Matthew Whyte; Jacques D. Fleuriot (OVERLAY@AI*IA, 2022)

Multimorbidity profiles and stochastic block modeling improve ICU patient clustering. - Valerio Restocchi; Jorge Gaete-Villegas; Jacques D. Fleuriot (CCGRID, 2022)

Re-imagining the Isabelle Archive of Formal Proofs. - Carlin MacKenzie; Fabian Huch; James Vaughan; Jacques D. Fleuriot (CICM, 2022)

Constructing the Reals as Dedekind Cuts of Rationals. - Jacques D. Fleuriot; Lawrence C. Paulson (Arch. Formal Proofs, 2022)

Towards Formalising Schutz' Axioms for Minkowski Spacetime in Isabelle/HOL. - Richard Schmoetten; Jake E. Palmer; Jacques D. Fleuriot (J. Autom. Reason., 2022)

Neurosymbolic AI for Reasoning on Graph Structures: A Survey. - Lauren Nicole Delong; Ramon Fernández Mir; Matthew Whyte; Zonglin Ji; Jacques D. Fleuriot (CoRR, 2023)

Neurosymbolic AI for Reasoning on Biomedical Knowledge Graphs. - Lauren Nicole Delong; Ramon Fernández Mir; Zonglin Ji; Fiona Niamh Coulter Smith; Jacques D. Fleuriot (CoRR, 2023)

Correction: Towards Formalising Schutz' Axioms for Minkowski Spacetime in Isabelle/HOL. - Richard Schmoetten; Jake E. Palmer; Jacques D. Fleuriot (J. Autom. Reason., 2023)

Development of prediction models for one-year brain tumour survival using machine learning: a comparison of accuracy and interpretability. - Colleen E. Charlton; Michael Tin Chung Poon; Paul M. Brennan; Jacques D. Fleuriot (Comput. Methods Programs Biomed., 2023)

Verifying Properties of Activities of Daily Living. - Ricardo Contreras; Filip Smola; Jiawei Zheng; Jane Hillston; Jacques D. Fleuriot (DataMod, 2024)

Alignment-based conformance checking over probabilistic events. - Jiawei Zheng; Petros Papapanagiotou; Jacques D. Fleuriot (HICSS, 2024)

Lie Groups and Algebras. - Richard Schmoetten; Jacques D. Fleuriot (Arch. Formal Proofs, 2024)

Deep Embedding of Intuitionistic Linear Logic. - Filip Smola; Jacques D. Fleuriot (Arch. Formal Proofs, 2024)

Linear Resources and Process Compositions. - Filip Smola; Jacques D. Fleuriot (Arch. Formal Proofs, 2024)

A Construction of the Lie Algebra of a Lie Group in Isabelle/HOL. - Richard Schmoetten; Jacques D. Fleuriot (CoRR, 2024)

MARS: A neurosymbolic approach for interpretable drug discovery. - Lauren Nicole Delong; Yojana Gadiya; Paola Galdi; Jacques D. Fleuriot; Daniel Domingo-Fernández (CoRR, 2024)

Process-aware Human Activity Recognition. - Jiawei Zheng; Petros Papapanagiotou; Jacques D. Fleuriot; Jane Hillston (CoRR, 2024)

Linear Resources in Isabelle/HOL. - Filip Smola; Jacques D. Fleuriot (J. Autom. Reason., 2024)

Evaluating Personalised Beneficial Interventions in the Daily Lives of Older Adults Using a Camera. - Longfei Chen; Chris Lochhead; Robert B. Fisher; Nusa Faric; Jacques D. Fleuriot; Subramanian Ramamoorthy (AIiH (2), 2025)

Formally Verified Neurosymbolic Trajectory Learning via Tensor-based Linear Temporal Logic on Finite Traces. - Mark Chevallier; Filip Smola; Richard Schmoetten; Jacques D. Fleuriot (CoRR, 2025)

Comparing Care Pathways Between COVID-19 Pandemic Waves Using Electronic Health Records: A Process Mining Case Study. - Konstantin Georgiev; Jacques D. Fleuriot; Petros Papapanagiotou; Joanne McPeake; Susan D. Shenkin; Atul Anand (J. Heal. Informatics Res., 2025)

Neurosymbolic AI for Reasoning Over Knowledge Graphs: A Survey. - Lauren Nicole Delong; Ramon Fernández Mir; Jacques D. Fleuriot (IEEE Trans. Neural Networks Learn. Syst., 2025)

A Personalised Formal Verification Framework for Monitoring Activities of Daily Living of Older Adults Living Independently in Their Homes. - Ricardo Contreras; Filip Smola; Nusa Faric; Jiawei Zheng; Jane Hillston; Jacques D. Fleuriot (CoRR, 2025)

Evaluating Personalized Beneficial Interventions in the Daily Lives of Older Adults Using a Camera. - Longfei Chen; Chris Lochhead; Robert B. Fisher; Nusa Faric; Jacques D. Fleuriot; Subramanian Ramamoorthy (CoRR, 2025)

GradSTL: Comprehensive Signal Temporal Logic for Neurosymbolic Reasoning and Learning. - Mark Chevallier; Filip Smola; Richard Schmoetten; Jacques D. Fleuriot (CoRR, 2025)

Constructing the Lie Algebra of Smooth Vector Fields on a Lie Group in Isabelle/HOL. - Richard Schmoetten; Jacques D. Fleuriot (J. Autom. Reason., 2025)