5 citations · 8 across the 9 of their papers we have counts for
6 papers · 1 filter
Formalising Geometric Axioms for Minkowski Spacetime and Without-Loss-of-Generality Theorems
Richard Schmoetten, Jake Palmer, Jacques Fleuriot
This contribution reports on the continued formalisation of an axiomatic system for Minkowski spacetime (as used in the study of Special Relativity) which is closer in spirit to Hi…
Towards Formalising Schutz' Axioms for Minkowski Spacetime in Isabelle/HOL
Richard Schmoetten, Jake E. Palmer, Jacques D. Fleuriot
Special Relativity is a cornerstone of modern physical theory. While a standard coordinate model is well-known and widely taught today, several alternative systems of axioms exist.…
Object-Level Reasoning with Logics Encoded in HOL Light
Petros Papapanagiotou, Jacques Fleuriot
We present a generic framework that facilitates object level reasoning with logics that are encoded within the Higher Order Logic theorem proving environment of HOL Light. This inv…
The Boyer-Moore Waterfall Model Revisited
Petros Papapanagiotou, Jacques Fleuriot
In this paper, we investigate the potential of the Boyer-Moore waterfall model for the automation of inductive proofs within a modern proof assistant. We analyze the basic concepts…
Correct by Construction Resource-based Process Composition
Petros Papapanagiotou, Jacques Fleuriot
The need for rigorous process composition is encountered in many situations pertaining to the development and analysis of complex systems. We discuss the use of Classical Linear Lo…
Bootstrapping LCF Declarative Proofs
Phil Scott, Steven Obua, Jacques Fleuriot
Suppose we have been sold on the idea that formalised proofs in an LCF system should resemble their written counterparts, and so consist of formulas that only provide signposts for…