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:
Clicking on the 'output' tab at the bottom and clicking on the appropriate value line gives the results.