- MoMM - rule induction (machine learning) algorithm targeted for the Mizar-logic
- generalization over local objects (constants, assumptions)
- subsumption/inference taking into account the dependent type hierarchy
- MizAR - now uses SInE+Vampire by default
- video of MizAR used inside Emacs: http://mws.cs.ru.nl/~urban/ams11/out4.ogv
Josef Urban
2011-01-14
