System that enables a working mathematician to put theorems and proofs (in the formal language of predicate calculus) into it. GPL

Bezpłatne programy, darmowe, za darmo, gratis - wyszukiwanie i nowości.: "
Hilbert II 0.02.01 (Default branch)
The Goal of Hilbert II, which is in the tradition of Hilbert's program, is the creation of a system that enables a working mathematician to put theorems and proofs (in the formal language of predicate calculus) into it. These proofs are automatically verified by a proof checker. Because this system is not centrally administered and enables references to any location on the Internet, a world wide mathematical knowledge base could be built. Any proof of a theorem in this "mathematical web" could be drilled down to the very elementary rules and axioms. To make it more than a huge number of logical correct formulas, it also contains information in "common mathematical language". Think of an incredible number of mathematical textbooks with hyperlinks, and each of its proofs could be verified by *Hilbert II*. For each theorem, the dependency of other propositions, definitions, and axioms could be easily derived."