auto-proof.rst
author Oleksandr Gavenko <gavenkoa@gmail.com>
Sun, 12 Apr 2009 22:28:55 +0300
changeset 71 38902bb40d47
parent 70 7994c7089afb
child 82 716febef6188
permissions -rw-r--r--
Explain bluetooth description.
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
56
24f1a6ce1a72 auto proog system.
Oleksandr Gavenko <gavenkoa@gmail.com>
parents:
diff changeset
     1
-*- outline -*-
24f1a6ce1a72 auto proog system.
Oleksandr Gavenko <gavenkoa@gmail.com>
parents:
diff changeset
     2
24f1a6ce1a72 auto proog system.
Oleksandr Gavenko <gavenkoa@gmail.com>
parents:
diff changeset
     3
* proofgeneral.
24f1a6ce1a72 auto proog system.
Oleksandr Gavenko <gavenkoa@gmail.com>
parents:
diff changeset
     4
24f1a6ce1a72 auto proog system.
Oleksandr Gavenko <gavenkoa@gmail.com>
parents:
diff changeset
     5
  $ sudo apt-get install proofgeneral
24f1a6ce1a72 auto proog system.
Oleksandr Gavenko <gavenkoa@gmail.com>
parents:
diff changeset
     6
  $ sudo apt-get install proofgeneral-coq
24f1a6ce1a72 auto proog system.
Oleksandr Gavenko <gavenkoa@gmail.com>
parents:
diff changeset
     7
  $ sudo apt-get install proofgeneral-misc
24f1a6ce1a72 auto proog system.
Oleksandr Gavenko <gavenkoa@gmail.com>
parents:
diff changeset
     8
  $ sudo apt-get install proofgeneral-doc
24f1a6ce1a72 auto proog system.
Oleksandr Gavenko <gavenkoa@gmail.com>
parents:
diff changeset
     9
  $ sudo apt-get install proofgeneral-minlog
24f1a6ce1a72 auto proog system.
Oleksandr Gavenko <gavenkoa@gmail.com>
parents:
diff changeset
    10
24f1a6ce1a72 auto proog system.
Oleksandr Gavenko <gavenkoa@gmail.com>
parents:
diff changeset
    11
or build from source:
24f1a6ce1a72 auto proog system.
Oleksandr Gavenko <gavenkoa@gmail.com>
parents:
diff changeset
    12
24f1a6ce1a72 auto proog system.
Oleksandr Gavenko <gavenkoa@gmail.com>
parents:
diff changeset
    13
  $ make clean
24f1a6ce1a72 auto proog system.
Oleksandr Gavenko <gavenkoa@gmail.com>
parents:
diff changeset
    14
  $ make compile EMACS=xemacs
24f1a6ce1a72 auto proog system.
Oleksandr Gavenko <gavenkoa@gmail.com>
parents:
diff changeset
    15
  $ cat ~/.emacs
24f1a6ce1a72 auto proog system.
Oleksandr Gavenko <gavenkoa@gmail.com>
parents:
diff changeset
    16
...
24f1a6ce1a72 auto proog system.
Oleksandr Gavenko <gavenkoa@gmail.com>
parents:
diff changeset
    17
(load-file "dir/generic/proof-site.el")
24f1a6ce1a72 auto proog system.
Oleksandr Gavenko <gavenkoa@gmail.com>
parents:
diff changeset
    18
...
24f1a6ce1a72 auto proog system.
Oleksandr Gavenko <gavenkoa@gmail.com>
parents:
diff changeset
    19
24f1a6ce1a72 auto proog system.
Oleksandr Gavenko <gavenkoa@gmail.com>
parents:
diff changeset
    20
See
24f1a6ce1a72 auto proog system.
Oleksandr Gavenko <gavenkoa@gmail.com>
parents:
diff changeset
    21
24f1a6ce1a72 auto proog system.
Oleksandr Gavenko <gavenkoa@gmail.com>
parents:
diff changeset
    22
  http://proofgeneral.inf.ed.ac.uk/
24f1a6ce1a72 auto proog system.
Oleksandr Gavenko <gavenkoa@gmail.com>
parents:
diff changeset
    23
24f1a6ce1a72 auto proog system.
Oleksandr Gavenko <gavenkoa@gmail.com>
parents:
diff changeset
    24
* Isabelle.
24f1a6ce1a72 auto proog system.
Oleksandr Gavenko <gavenkoa@gmail.com>
parents:
diff changeset
    25
24f1a6ce1a72 auto proog system.
Oleksandr Gavenko <gavenkoa@gmail.com>
parents:
diff changeset
    26
Isabelle is a generic proof assistant.
24f1a6ce1a72 auto proog system.
Oleksandr Gavenko <gavenkoa@gmail.com>
parents:
diff changeset
    27
24f1a6ce1a72 auto proog system.
Oleksandr Gavenko <gavenkoa@gmail.com>
parents:
diff changeset
    28
It allows mathematical formulas to be expressed in a formal language and
24f1a6ce1a72 auto proog system.
Oleksandr Gavenko <gavenkoa@gmail.com>
parents:
diff changeset
    29
provides tools for proving those formulas in a logical calculus. The main
24f1a6ce1a72 auto proog system.
Oleksandr Gavenko <gavenkoa@gmail.com>
parents:
diff changeset
    30
application is the formalization of mathematical proofs and in particular
24f1a6ce1a72 auto proog system.
Oleksandr Gavenko <gavenkoa@gmail.com>
parents:
diff changeset
    31
formal verification, which includes proving the correctness of computer
24f1a6ce1a72 auto proog system.
Oleksandr Gavenko <gavenkoa@gmail.com>
parents:
diff changeset
    32
hardware or software and proving properties of computer languages and
24f1a6ce1a72 auto proog system.
Oleksandr Gavenko <gavenkoa@gmail.com>
parents:
diff changeset
    33
protocols.
24f1a6ce1a72 auto proog system.
Oleksandr Gavenko <gavenkoa@gmail.com>
parents:
diff changeset
    34
24f1a6ce1a72 auto proog system.
Oleksandr Gavenko <gavenkoa@gmail.com>
parents:
diff changeset
    35
See
24f1a6ce1a72 auto proog system.
Oleksandr Gavenko <gavenkoa@gmail.com>
parents:
diff changeset
    36
24f1a6ce1a72 auto proog system.
Oleksandr Gavenko <gavenkoa@gmail.com>
parents:
diff changeset
    37
  http://isabelle.in.tum.de/overview.html
24f1a6ce1a72 auto proog system.
Oleksandr Gavenko <gavenkoa@gmail.com>
parents:
diff changeset
    38
  http://en.wikipedia.org/wiki/Isabelle_(theorem_prover)
24f1a6ce1a72 auto proog system.
Oleksandr Gavenko <gavenkoa@gmail.com>
parents:
diff changeset
    39
24f1a6ce1a72 auto proog system.
Oleksandr Gavenko <gavenkoa@gmail.com>
parents:
diff changeset
    40
* IsarMathLib.
24f1a6ce1a72 auto proog system.
Oleksandr Gavenko <gavenkoa@gmail.com>
parents:
diff changeset
    41
70
7994c7089afb Explain proof assistant.
Oleksandr Gavenko <gavenkoa@gmail.com>
parents: 56
diff changeset
    42
The goal of the project is to create a library of formalized mathematics,
7994c7089afb Explain proof assistant.
Oleksandr Gavenko <gavenkoa@gmail.com>
parents: 56
diff changeset
    43
similar to the Mizar Mathematical Library, but written for the Isabelle/Isar
7994c7089afb Explain proof assistant.
Oleksandr Gavenko <gavenkoa@gmail.com>
parents: 56
diff changeset
    44
theorem prover (ZF logic).
7994c7089afb Explain proof assistant.
Oleksandr Gavenko <gavenkoa@gmail.com>
parents: 56
diff changeset
    45
7994c7089afb Explain proof assistant.
Oleksandr Gavenko <gavenkoa@gmail.com>
parents: 56
diff changeset
    46
See
7994c7089afb Explain proof assistant.
Oleksandr Gavenko <gavenkoa@gmail.com>
parents: 56
diff changeset
    47
7994c7089afb Explain proof assistant.
Oleksandr Gavenko <gavenkoa@gmail.com>
parents: 56
diff changeset
    48
  http://savannah.nongnu.org/projects/isarmathlib
7994c7089afb Explain proof assistant.
Oleksandr Gavenko <gavenkoa@gmail.com>
parents: 56
diff changeset
    49
  http://lists.nongnu.org/mailman/listinfo/isarmathlib-devel
7994c7089afb Explain proof assistant.
Oleksandr Gavenko <gavenkoa@gmail.com>
parents: 56
diff changeset
    50
7994c7089afb Explain proof assistant.
Oleksandr Gavenko <gavenkoa@gmail.com>
parents: 56
diff changeset
    51
** http://isarmathlib.org/
7994c7089afb Explain proof assistant.
Oleksandr Gavenko <gavenkoa@gmail.com>
parents: 56
diff changeset
    52
56
24f1a6ce1a72 auto proog system.
Oleksandr Gavenko <gavenkoa@gmail.com>
parents:
diff changeset
    53
This site is an experimental HTML rendering of fragments of the IsarMathLib
24f1a6ce1a72 auto proog system.
Oleksandr Gavenko <gavenkoa@gmail.com>
parents:
diff changeset
    54
project. IsarMathLib is a library of mathematical proofs formally verified by
24f1a6ce1a72 auto proog system.
Oleksandr Gavenko <gavenkoa@gmail.com>
parents:
diff changeset
    55
the Isabelle theorem proving environment. The formalization is based on the
24f1a6ce1a72 auto proog system.
Oleksandr Gavenko <gavenkoa@gmail.com>
parents:
diff changeset
    56
Zermelo-Fraenkel set theory.
24f1a6ce1a72 auto proog system.
Oleksandr Gavenko <gavenkoa@gmail.com>
parents:
diff changeset
    57
70
7994c7089afb Explain proof assistant.
Oleksandr Gavenko <gavenkoa@gmail.com>
parents: 56
diff changeset
    58
** Tiddly Formal Math.
7994c7089afb Explain proof assistant.
Oleksandr Gavenko <gavenkoa@gmail.com>
parents: 56
diff changeset
    59
7994c7089afb Explain proof assistant.
Oleksandr Gavenko <gavenkoa@gmail.com>
parents: 56
diff changeset
    60
This site is an experimental TiddlyWiki rendering of fragments of the
7994c7089afb Explain proof assistant.
Oleksandr Gavenko <gavenkoa@gmail.com>
parents: 56
diff changeset
    61
IsarMathLib project. IsarMathLib is a library of mathematical proofs formally
7994c7089afb Explain proof assistant.
Oleksandr Gavenko <gavenkoa@gmail.com>
parents: 56
diff changeset
    62
verified by the Isabelle theorem proving environment. The formalization is
7994c7089afb Explain proof assistant.
Oleksandr Gavenko <gavenkoa@gmail.com>
parents: 56
diff changeset
    63
based on the Zermelo-Fraenkel set theory.
7994c7089afb Explain proof assistant.
Oleksandr Gavenko <gavenkoa@gmail.com>
parents: 56
diff changeset
    64
56
24f1a6ce1a72 auto proog system.
Oleksandr Gavenko <gavenkoa@gmail.com>
parents:
diff changeset
    65
See
24f1a6ce1a72 auto proog system.
Oleksandr Gavenko <gavenkoa@gmail.com>
parents:
diff changeset
    66
70
7994c7089afb Explain proof assistant.
Oleksandr Gavenko <gavenkoa@gmail.com>
parents: 56
diff changeset
    67
  http://formalmath.tiddlyspot.com/