pedrominicz / mm Goto Github PK

For the Metamath specification, see chapter 4 and appendix C of the Metamath book. A discussion on the theory behind Metamath can be found on section 1.4 of the book. The paper Models for Metamath is also of interest.

The verifiers found in this repository are based on mmverify.py by Raph Levien. Other verifiers can be found in the Metamath website.

TODO:

• read: A machine-oriented logic based on the resolution principle
• read: An automatic theorem prover for substitution and detachment systems
• read: In memoriam Carew Arthur Meredith
• read: A finitely axiomatized formalization of predicate calculus with equality
• read: Condensed detachment as a rule of inference
• read: Principal type-schemes and condensed detachment
• read: ZFC without distinct variable conditions