Metamatix

[Thierry Arnoux]

Hi all,

FYI, I recently found out about Metamatix, a verified implementation of a metamath proof checker, written in Coq.

I'm not sure how far the project goes, but it's probably of interest for people in this group.

BR,
_
Thierry

[David A. Wheeler]

We have a list of Metamath tools on the website pages. Will you add it? If not, let me know and I will add it, I just don't want to duplicate effort.

[Thierry Arnoux]

Hi David,

Feel free to add it!

--
You received this message because you are subscribed to the Google Groups "Metamath" group.
To unsubscribe from this group and stop receiving emails from it, send an email to metamath+u...@googlegroups.com.
To view this discussion on the web visit https://groups.google.com/d/msgid/metamath/5DBFBC50-D236-4A71-9F55-82392C457A1A%40dwheeler.com.

[Denis Carnier]

Hi all, 

How delightful to see our tiny project find its way onto your mailing list! I am one of the developers for Metamathix (Arthur Correnson <arthur.c...@cispa.de> being the other). The project is at its infancy, but we already have a minimal implementation of a proof checker (without parsing/output) that we hope to prove correct with respect to a declarative specification or formal semantics for Metamath's underlying logic. To this end, if there already exists a reasonable model for Metamath then we'd love to hear about it. At present, we have proposed a reference logic and semantics, but we are rather unsure if they make sense.

Looking forward to hearing your thoughts,
Denis

[Mario Carneiro]

The paper "models for metamath" (https://arxiv.org/abs/1601.07699) works out the requirements for models of metamath databases. They tend to be rather abstract as metamath is fairly logic-agnostic; you can get more useful models if you add some axioms to make it more like FOL specifically. If you are looking for just the formal definition of metamath provability, the canonical reference is Appendix C of the metamath book (on which that paper builds).

To view this discussion on the web visit https://groups.google.com/d/msgid/metamath/eaea1b13-6b52-4a1f-87a1-1f2d007d08dfn%40googlegroups.com.