FORMAL PROVE SYSTEM 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 are.
|status.txt||0 kB||12-10-2004 11:26|