Next:
Structure of the talk
Automated Reasoning for Mizar
Josef Urban
Radboud University Nijmegen
Structure of the talk
Motivation: Erdös will not fit in your head
The Data driven approach
My personal puzzle
Overview of Automated Reasoning and AI over Mizar
Demo of MizAR and MoMM
Some performance data
Proving New Theorems
MaLARea
Example Run of MaLARea on Mizar data
Future
Thanks for your attention!
About this document ...
Josef Urban 2011-01-14
