Isabelle

Isabelle is a generic proof assistant

Implementation of Formal Logic on a Computer

The degree to which proofs can be automated depends on the type of logic.

Logic Type Theoretical Automation
Propositional logic Fully Automated
First-order logic Automatic but not necessarily terminating
Higer-order logic Some automation but mainly interactive

Installation

Goto the Isabelle website and click on the download button. I downloaded into a directory called 'isabelle' then from the command line I typed: isabelle
martin@linux-gye4:~> cd isabelle
martin@linux-gye4:~/isabelle> tar -xzf Isabelle2013_linux.tar.gz
martin@linux-gye4:~/isabelle> Isabelle2013/Isabelle
When running for the first time a builder program is run to build the theories. isabelle
When ready the jEdit program starts up. isabelle

Running

I ran Isabelle and typed in the following program from the manual:

isabelle run

Clicking on the 'output' tab at the bottom and clicking on the appropriate value line gives the results.

isabelle


metadata block
see also:

 

Correspondence about this page

Book Shop - Further reading.

Where I can, I have put links to Amazon for books that are relevant to the subject, click on the appropriate country flag to get more details of the book or to buy it from them.

 

Commercial Software Shop

Where I can, I have put links to Amazon for commercial software, not directly related to this site, but related to the subject being discussed, click on the appropriate country flag to get more details of the software or to buy it from them.

 

This site may have errors. Don't use for critical systems.

Copyright (c) 1998-2017 Martin John Baker - All rights reserved - privacy policy.