Conproof



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:

  • full automation of first order provability
  • proof caching
  • integrated version management

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 type theory of Conproof is the lambda-P fragment of a lambda-typed lambda calculus with local definitions.
  • The logic of Conproof is classical first order predicate logic implemented in "LF style", with partial functions modeled through proof object arguments.
  • The axioms of Conproof are those of ZFC set theory (in Morse-Kelley style.)

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:

  • The lambda terms compiled from a Conproof text can be checked by all main current type theoretical proof assistants.
  • The full Mizar library can without too much effort be translated into a Conproof version.

(last modification 2001-11-09)