5 ms·

How does this relate to the Archive of Formal Proofs [1] and Mizar's Mathematical Library [2]? [1] https://www.isa-afp.org/ https://www.isa-afp.org/ [2] http:

How does this relate to the Archive of Formal Proofs [1] and Mizar's Mathematical Library [2]? [1] https://www.isa-afp.org/ https://www.isa-afp.org/ [2] http://mizar.org/library/ http://mizar.org/library/

yaseer 8y ago
You can also add Coq's to the mix: [3] https://coq.inria.fr/library/ https://coq.inria.fr/library/ Each 1-3 is language specific (Isabelle/HOL, Mizar and Coq respectively). Logipedia too, is using the language Dedukti, although it is designed to translate into other proof languages, and list these on Logipedia.
0815test 8y ago
The systems you mention use a declarative proof approach that's more similar to the way humans might write a math proof, or to the way computer code is written. In contrast, Coq and Lean use "proof scripts" that are more like writing your stuff in a custom macro-assembler that will break as soon as one changes anything in the "script", or even just upgrades to a newer version of the underlying software. Even the resulting proof is basically not readable on its own without re-processing it with the software itself. (Coq used to have a declarative "mathematical proof language", but it was unmantained and they removed it.) Other systems, e.g. Agda use "proof terms" that are more like a proof that can be read "declaratively", but one where every single step has to be recorded; there's no provision for the system to "fill in" some gaps, unlike with declarative proofs. This can definitely impact readability/surveyability of a development, but the inherent maintainance problems of "proof scripts" do not arise. I'm not sure what Dedukti is going for from this basic POV. They mention that they're trying to build a general framework that can support multiple logical/proof systems, but the details are not that clear. It's probably going to be a bit clunkier than the systems you mention, particularly at this early stage of development.
- fspeech 8y ago
  I thought Dedukti has a small kernel. Although “small” may be a relative thing (relative to other dependently typed systems.

yaseer 8y ago

You can also add Coq's to the mix: [3] https://coq.inria.fr/library/ https://coq.inria.fr/library/ Each 1-3 is language specific (Isabelle/HOL, Mizar and Coq respectively). Logipedia too, is using the language Dedukti, although it is designed to translate into other proof languages, and list these on Logipedia.

0815test 8y ago

The systems you mention use a declarative proof approach that's more similar to the way humans might write a math proof, or to the way computer code is written. In contrast, Coq and Lean use "proof scripts" that are more like writing your stuff in a custom macro-assembler that will break as soon as one changes anything in the "script", or even just upgrades to a newer version of the underlying software. Even the resulting proof is basically not readable on its own without re-processing it with the software itself. (Coq used to have a declarative "mathematical proof language", but it was unmantained and they removed it.) Other systems, e.g. Agda use "proof terms" that are more like a proof that can be read "declaratively", but one where every single step has to be recorded; there's no provision for the system to "fill in" some gaps, unlike with declarative proofs. This can definitely impact readability/surveyability of a development, but the inherent maintainance problems of "proof scripts" do not arise. I'm not sure what Dedukti is going for from this basic POV. They mention that they're trying to build a general framework that can support multiple logical/proof systems, but the details are not that clear. It's probably going to be a bit clunkier than the systems you mention, particularly at this early stage of development.

fspeech 8y ago
I thought Dedukti has a small kernel. Although “small” may be a relative thing (relative to other dependently typed systems.