Custom Automations in Mizar

1. Bancerek, G., Urban, J.: Integrated semantic browsing of the Mizar mathematical library for authoring Mizar articles. In: Mathematical Knowledge Management, pp. 44–57. Springer (2004)

2. Cairns, P., Gow, J.: Integrating searching and authoring in Mizar. J. Autom. Reason. 39(2), 141–160 (2007)

   Article  MATH  Google Scholar 

3. Caminati, M.: Preliminaries to classical first-order model theory. Form. Math. 19(3), 155–167 (2011)

   Article  Google Scholar 

4. Grabowski, A., Korniłowicz, A., Naumowicz, A.: Mizar in a nutshell. J. Form. Reason. 3(2), 153–245 (2010)

   MATH  Google Scholar 

5. Naumowicz, A.: Evaluating prospective built-in elements of computer algebra in Mizar. Stud. Log. Gramm. Rhetor. 10(23), 191–200 (2007)

   Google Scholar 

6. Naumowicz, A., Byliński, C.: Improving Mizar texts with properties and requirements. In: Mathematical Knowledge Management, pp. 290–301. Springer (2004)

7. Rudnicki, P., Trybulec, A.: On equivalents of well-foundedness. J. Autom. Reason. 23(3), 197–234 (1999)

   Article  MathSciNet  MATH  Google Scholar 

8. Rudnicki, P., Urban, J.: Escape to ATP for Mizar. In: First Workshop on Proof eXchange for Theorem Proving. http://pxtp2011.loria.fr/ (2011). Accessed 23 Oct 2012

9. Urban, J.: MizarMode–an integrated proof assistance tool for the Mizar way of formalizing mathematics. J. Appl. Log. 4(4), 414–427 (2006)

   Article  MathSciNet  MATH  Google Scholar 

10. Urban, J.: MoMM-fast interreduction and retrieval in large libraries of formalized mathematics. Int. J. Artif. Intell. Tools 15(1), 109 (2006)

    Article  Google Scholar 

11. Wiedijk, F.: Mizar’s soft type system. In: Proceedings of the 20th International Conference on Theorem Proving in Higher Order Logics, pp. 383–399. Springer (2007)

Download references