Isabelle and its use at X-Logic.org
Overview
This provides information about ProofPower and the various formal theories developed at X-Logic.org using ProofPower.
Isabelle is a specification and proof development and checking tool developed by Larry Paulson and others initially at the University of Cambridge. It is an intellectual descendent of Edinburgh LCF. It is a generic proof tool, supporting multiple object logics, and provides strong interactive proof support and an extensive library of well developed object languages and applications.
Theory of Knowledge in Isabelle.
Isabelle and its logics
Isabelle is a specification and proof development and checking tool developed by Larry Paulson and others initially at the University of Cambridge. It is an intellectual descendent of Edinburgh LCF. It is a generic proof tool, supporting multiple object logics, and provides strong interactive proof support and an extensive library of well developed object languages and applications.
Why Isabelle?

I am using Isabelle for the following reasons:

  1. It is probably the most advanced tool of its genre both in terms of automatic support for interactive proof and in terms of the already available theory base available to build on.
  2. For applications I naturally care about how long things take to do!
  3. Apart from the possibility that it is the most productive tool to use for my applications, there is much to be learned from isabelle which wont come from a scan of the documentation.

Neither X-Logic nor OpenMind are tied to this particular proof tool, the idea is to be able to mix and match.

Isabelle Documentation
To understand the specifications and proofs I am developing using Isabelle you will probably have to look at the Isabelle documentation sometime. One way to get it is just to download the whole isabelle system and look in the docs directory!
Theory of Knowledge in Isabelle
Theory of Knowledge in Isabelle.
A model in isabelle contributing to X-Logic architecture and the design of XL-Glue. This version includes the use of signatures.

up quick index © RBJ

$Id: index.xml,v 1.1.1.1 2000/12/04 17:23:22 rbjones Exp $