[FOM] proof assistants and foundations of mathematics
Frédéric Blanqui
frederic.blanqui at inria.fr
Tue Aug 21 03:58:58 EDT 2018
Hello.
Another such system is Dedukti (https://deducteam.github.io/). It is
based on LF + a user-defined (decidable) congruence on objects and types
given by rewrite rules. The point is to replace axioms by rewrite rules
as much as possible. For instance, Peano arithmetic, HOL, some subset of
ZF, functional pure type systems (PTS) including system F, Fw, CC, CIC,
etc. can be encoded into a Dedukti theory with no axiom but rewrite
rules. See http://www.lsv.fr/~dowek/Publi/expressing.pdf for more details.
But, currently, Dedukti is just a proof/type checker. It has very little
support for interactive proof development. Instead, it comes with
additional tools for translating proofs developed elsewhere to Dedukti,
and from Dedukti to other provers. For instance, Krajono
(http://deducteam.gforge.inria.fr/krajono/index.html) translates Matita
(a clone of Coq) proofs into Dedukti proofs; Holide
(http://deducteam.gforge.inria.fr/holide/index.html) translates
OpenTheory proofs (from HOL, HOL-Light, etc.) into Dedukti proofs.
François Thiré (http://www.lsv.fr/~fthire/) is developing tools for
automatically translating Matita proofs into HOL. And an extension of
Dedukti allowing the interactive development of proofs is under
development (https://github.com/rlepigre/lambdapi).
Frédéric.
Le 14/08/2018 à 10:36, Till Mossakowski a écrit :
> Am 11.08.2018 um 21:39 schrieb Timothy Y. Chow:
>> What I think Jose implicitly desires is a proof assistant that has the
>> feature that it can verify "T is a theorem of S if your logic is L"
>> where S and L are arbitrary and *user-specified*. Moreover, the
>> verification of such statements should assume as little as possible.
>> So if the next Ed Nelson comes along who doesn't even trust PRA, he
>> can still plug in his favorite set of axioms and proof calculus and
>> find out if his theorem is really a theorem by his own standards. He
>> won't have to go off and write his own home-grown, bug-ridden proof
>> assistant.
>>
>>
> actually, one can formally specifcy a logic L and verify "T is a theorem
> of S if your logic is L" with any logical framework, e.g. LF. Also
> Isabelle/Pure is capable of doing this, although in practice, mostly
> L=HOL. A recent system that also covers model theory and soundness and
> completeness proofs is MMT, see https://uniformal.github.io/ MMT is not
> only logic-independent but even "foundation independent" in the sense
> that it works with different logical frameworks, although in practice,
> mostly LF is used.
>
> Till Mossakowski
>
>
>
> _______________________________________________
> FOM mailing list
> FOM at cs.nyu.edu
> https://cs.nyu.edu/mailman/listinfo/fom
More information about the FOM
mailing list