RbJ's Archive of Ancient (& modern) Writings
The most ancient stuff I have here is some of my undergraduate philosophy essays.
- Expert Systems in Decision Support (1982)
- This was a paper I wrote while trying to make a career transition into some area which involved logic.
It did the trick, but it's long winded, speculative and insubstantial.
- Persistent Applicative Heaps and Knowledge Bases (1985)
- This one was written after I had tried a bit of knowledge engineering and then transferred again into relational databases.
I wrote it for a workshop on persistent databases at Appin in Scotland.
As I got close to the workshop I realised that the paper wasn't converging, so this version got stacked and I prepared a much shorter version for the workshop which was published by Glasgow University in the informal procedings.
When they came to making a proper book out of it my paper was dropped.
At the workshop I decided to talk about something completely different, and more controversial.
I caused an uproar.
I still think there are some good ideas here.
I still like the idea of functional knowledge bases (functional in the sense used in functional programming languages).
- Logical foundations and formal verification
- This paper was for me a milestone, a real breakthrough.
At least, so I thought at the time.
- Creative Foundations for Program Verification (1986)
- This is a neat compression of the fundamental defect in the previous paper.
- Logical Necessity and the Foundations of Mathematics (1987)
- This is an aborted sketch of a paper heading for making the case for reflexive mathematical foundations systems.
Around about this time I gave a short presentation at a meeting of the British Logic Colloquim in Cambridge, delivering essentially the same message.
I have no idea to this day whether anyone had a clue what I was on about.
- ProofPower related writings:
- ProofPower is a proof tool supporting the development and checking of formal specifications in higher order logic, the Z specification language, and (with the compliance tool add-on) of SPARK (safety critical Ada subset) programs using the DERA (now QinetiQ) compliance notation.
ProofPower was originally developed by a collaborative R&D project involving ICL, the Universities of Cambridge and Kent, and Program Validation Limited.
I lead the project, Rob Arthan lead the ProofPower development team.
- I wrote the ProofPower Z Tutorial and ProofPower HOL Tutorial Notes.
These are not available from this site, but from the official ProofPower site.
- Methods and Tools for the Verification of Critical Properties (86Kb gzipped postscript)
- This was an invited paper at one of the BCS refinement workshops.
It makes some methodological points and illustrates them using the ProofPower Z support, including some proofs scripts.
One of a small collection of papers relating to ProofPower available from the official site.
- ClawZ related writings:
- ClawZ is the latest bit of ProofPower related work I have been involved in (in this I exclude my own applications of ProofPower).
This was a project to enable the DERA compliance notation and its ProofPower based tool support to be used for the verification of Simulink diagrams (or code generated from them).
The project was undertaken by Lemma1 (Rob Arthan) as prime contractor to DERA and Roger Bishop Jones Limited (me) as subcontractor to Lemma1 between February and May 1999.
A tool was specified and implemented to translate Simulink model files into the ProofPower Z specification ascii format, together with some Z libraries to permit evaluation of the tool by DERA (now QINETIQ ).
Pretty much all of the project documentation (mostly my work, some by Rob Arthan), is online as postscript at the Lemma1 site.
created 1996-6-6 modified 2010-1-28