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

Goto the Isabelle website and click on the download button. I downloaded into a directory called 'isabelle' then from the command line I typed:

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.

When ready the jEdit program starts up.

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 the software project, 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.