Conproof currently is just a dream in my head, but I really would like to implement it.
Conproof is a proof checker (a computer program that checks mathematical proof for its correctness), which is the least common multiple of:
Strictly speaking it's not the least multiple, because Conproof has a few extras:
Conproof really is an enhanced Mizar clone. The idea of Conproof is that it is to Mizar what C is to Pascal (C is sugared assembly, and Conproof is sugared type theory; also Mizar's syntax is influenced by Pascal's syntax, and Conproof's syntax is like Mizar's but more "C like".) The main difference between Conproof and Mizar is that Conproof doesn't use the "Church's iota" approach to treat partial functions outside their domain.
The "foundations" of Conproof are:
The interface of Conproof consists of simple "compiler" programs (implemented in C and Java) that operate on plain text ascii files. The main Conproof program is the checker that checks a Conproof text for correctness and produces an "interface" file (and also renumbers internal labels and adds cached proof information.) A second Conproof program produces a TeX file from a Conproof text to make its contents more accessible. A third program "compiles" a Conproof text to a huge typed lambda term (which can be checked by independent programs.)
Conproof really consists of three separate parts: the main proof checker, the first order inference engine and the computer algebra module. The architecture has been designed to make it possible to easily replace either of the latter two modules with alternative implementations.
Conproof intentionally has been designed such that the following two properties hold:
(last modification 2001-11-09)