1 -*- outline -*-

     2 

     3 * proofgeneral.

     4 

     5   $ sudo apt-get install proofgeneral

     6   $ sudo apt-get install proofgeneral-coq

     7   $ sudo apt-get install proofgeneral-misc

     8   $ sudo apt-get install proofgeneral-doc

     9   $ sudo apt-get install proofgeneral-minlog

    10 

    11 or build from source:

    12 

    13   $ make clean

    14   $ make compile EMACS=xemacs

    15   $ cat ~/.emacs

    16 ...

    17 (load-file "dir/generic/proof-site.el")

    18 ...

    19 

    20 See

    21 

    22   http://proofgeneral.inf.ed.ac.uk/

    23 

    24 * Isabelle.

    25 

    26 Isabelle is a generic proof assistant.

    27 

    28 It allows mathematical formulas to be expressed in a formal language and

    29 provides tools for proving those formulas in a logical calculus. The main

    30 application is the formalization of mathematical proofs and in particular

    31 formal verification, which includes proving the correctness of computer

    32 hardware or software and proving properties of computer languages and

    33 protocols.

    34 

    35 See

    36 

    37   http://isabelle.in.tum.de/overview.html

    38   http://en.wikipedia.org/wiki/Isabelle_(theorem_prover)

    39 

    40 * IsarMathLib.

    41 

    42 This site is an experimental HTML rendering of fragments of the IsarMathLib

    43 project. IsarMathLib is a library of mathematical proofs formally verified by

    44 the Isabelle theorem proving environment. The formalization is based on the

    45 Zermelo-Fraenkel set theory.

    46 

    47 See

    48 

    49   http://isarmathlib.org/