SAT-Enhanced Mizar Proof Checking

1. Alama, J., Kohlhase, M., Mamane, L., Naumowicz, A., Rudnicki, P., Urban, J.: Licensing the Mizar Mathematical Library. In: Davenport, J.H., Farmer, W.M., Urban, J., Rabe, F. (eds.) MKM 2011 and Calculemus 2011. LNCS, vol. 6824, pp. 149–163. Springer, Heidelberg (2011)

   Chapter  Google Scholar 

2. Armand, M., Faure, G., Grégoire, B., Keller, C., Théry, L., Werner, B.: A modular integration of SAT/SMT solvers to Coq through proof witnesses. In: Jouannaud, J.-P., Shao, Z. (eds.) CPP 2011. LNCS, vol. 7086, pp. 135–150. Springer, Heidelberg (2011)

   Chapter  Google Scholar 

3. Caminati, M.B., Rosolini, G.: Custom automations in Mizar. Journal of Automated Reasoning 50(2), 147–160 (2013)

   Article  MathSciNet  MATH  Google Scholar 

4. Grabowski, A., Korniłowicz, A., Naumowicz, A.: Mizar in a nutshell. Journal of Formalized Reasoning 3(2), 153–245 (2010)

   MathSciNet  MATH  Google Scholar 

5. Grabowski, A., Schwarzweller, C.: Revisions as an essential tool to maintain mathematical repositories. In: Kauers, M., Kerber, M., Miner, R., Windsteiger, W. (eds.) MKM/CALCULEMUS 2007. LNCS (LNAI), vol. 4573, pp. 235–249. Springer, Heidelberg (2007)

   Chapter  Google Scholar 

6. Grabowski, A., Schwarzweller, C.: Towards automatically categorizing mathematical knowledge. In: Proceedings of Federated Conference on Computer Science and Information Systems – FedCSIS 2012, Wroclaw, Poland, September 9–12, pp. 63–68 (2012)

   Google Scholar 

7. Kaliszyk, C., Urban, J.: Mizar 40 for Mizar 40. CoRR, abs/1310.2805 (2013)

   Google Scholar 

8. Korniłowicz, A.: Tentative experiments with ellipsis in Mizar. In: Jeuring, J., Campbell, J.A., Carette, J., Dos Reis, G., Sojka, P., Wenzel, M., Sorge, V. (eds.) CICM 2012. LNCS (LNAI), vol. 7362, pp. 453–457. Springer, Heidelberg (2012)

   Chapter  Google Scholar 

9. Korniłowicz, A.: On rewriting rules in Mizar. Journal of Automated Reasoning 50(2), 203–210 (2013)

   Article  MathSciNet  MATH  Google Scholar 

10. Naumowicz, A.: An example of formalizing recent mathematical results in Mizar. Journal of Applied Logic 4(4), 396–413 (2006)

    Article  MathSciNet  MATH  Google Scholar 

11. Naumowicz, A.: Evaluating prospective built-in elements of computer algebra in Mizar. Studies in Logic, Grammar and Rhetoric 10(23), 191–200 (2007)

    Google Scholar 

12. Naumowicz, A.: Interfacing external CA systems for Gröbner bases computation in Mizar proof checking. International Journal of Computer Mathematics 87(1), 1–11 (2010)

    Article  MATH  Google Scholar 

13. Naumowicz, A., Byliński, C.: Improving Mizar texts with properties and requirements. In: Asperti, A., Bancerek, G., Trybulec, A. (eds.) MKM 2004. LNCS, vol. 3119, pp. 290–301. Springer, Heidelberg (2004)

    Chapter  Google Scholar 

14. Naumowicz, A., Korniłowicz, A.: A brief overview of Mizar. In: Berghofer, S., Nipkow, T., Urban, C., Wenzel, M. (eds.) TPHOLs 2009. LNCS, vol. 5674, pp. 67–72. Springer, Heidelberg (2009)

    Chapter  Google Scholar 

15. Pąk, K.: Methods of lemma extraction in natural deduction proofs. Journal of Automated Reasoning 50(2), 217–228 (2013)

    Article  MathSciNet  MATH  Google Scholar 

16. Trybulec, A., Korniłowicz, A., Naumowicz, A., Kuperberg, K.: Formal mathematics for mathematicians. Journal of Automated Reasoning 50(2), 119–121 (2013)

    Article  MathSciNet  Google Scholar 

17. Urban, J., Rudnicki, P., Sutcliffe, G.: ATP and presentation service for Mizar formalizations. J. Autom. Reasoning 50(2), 229–241 (2013)

    Article  MathSciNet  MATH  Google Scholar 

18. Weber, T.: Integrating a SAT solver with an LCF-style theorem prover. In: Proceedings of the Third International Workshop on Pragmatical Aspects of Decision Procedures in Automated Reasoning, PDPAR (2005)

    Google Scholar 

Download references