FPS is a system which allows to write and check mathematical proofs in a
formal way. The kernel of the system will be implemented as a module in
OCAML, and the proofs will be writen also in OCAML. The kernel will provide
the theorem type. Values of this type are true (proved) theorems. You can
create them only using some basic rules which are provided by the kernel ---
these rules always leads to true theorems. It means that when you make a
mistake in your proof you can not get incorrect theorem, at most you will
not get anything. 

You can also create more powerful and easier to use rules in your modules,
using the basic rules provided by the kernel, and then you can use them in
your proofs.

The proofs you make are equivalent to proofs in first order Hilbert's logic
(over any signature). But you can use also formulas from higher-order logic.
You can start from any set of axioms as assumptions (e.g. ZFC or Peano
natural numbers), and from them prove your theorems.

There is possible to make definitions. You can define some symbols and then
use them in your proofs. We don't already know what the definition realy

status.txt 0 kB 12-10-2004 11:26

Licznik: 1408

Valid HTML 4.0!