Automating Boolean Set Operations in Mizar Proof Checking with the Aid of an External SAT Solver

1. Alama, J., Kohlhase, M., Mamane, L., Naumowicz, A., Rudnicki, P., Urban, J.: Licensing the Mizar mathematical library. In: Lecture Notes in Computer Science of MKM’11, vol. 6824, pp. 149–163. Springer, Berlin (2011)

   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: Lecture Notes in Computer Science, vol. 7086, pp. 135–150. Springer, Berlin (2011)

   Google Scholar 

3. Caminati, M.B., Rosolini, G.: Custom automations in Mizar. J. Autom. Reason. 50(2), 147–160 (2013)

   Article  MATH  MathSciNet  Google Scholar 

4. Adam Grabowski: Automated discovery of properties of rough sets. Fundamenta Informaticae 128(1–2), 65–79 (2013)

   MATH  MathSciNet  Google Scholar 

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

   MATH  Google Scholar 

6. Grabowski, A., Schwarzweller, C.: Translating mathematical vernacular into knowledge repositories. In: Proceedings of the 4th International Conference on Mathematical Knowledge Management MKM’05, pp. 49–64. Springer, Berlin (2006)

   Google Scholar 

7. Grabowski, A., Schwarzweller, C.: Revisions as an essential tool to maintain mathematical repositories. In: Calculemus ’07 /MKM ’07, pp. 235–249. Springer, Berlin (2007)

   Google Scholar 

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

9. Kaliszyk, C., Urban, J.: Mizar 40 for Mizar 40. CoRR (2013). arXiv:1310.2805

10. Kornilowicz, A.: Tentative experiments with ellipsis in Mizar, vol. 7362, pp. 453–457. Springer (2012)

11. Kornilowicz, A.: On rewriting rules in Mizar. J. Autom. Reason. 50(2), 203–210 (2013)

    Article  MATH  MathSciNet  Google Scholar 

12. Naumowicz, A.: An example of formalizing recent mathematical results in Mizar. J. Appl. Log. 4(4), 396–413 (2006)

    Article  MATH  MathSciNet  Google Scholar 

13. 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 

14. Naumowicz, A.: Interfacing external CA systems for Gröbner bases computation in Mizar proof checking. Int. J. Comput. Math. 87(1), 1–11 (2010)

    Article  MATH  Google Scholar 

15. Naumowicz, A.: SAT-enhanced Mizar proof checking. In: Watt, S.M., Davenport, J.H., Sexton, A.P., Sojka, P., Urban, J. (eds.) CICM of Lecture Notes in Computer Science, vol. 8543, pp. 449–452. Springer (2014)

16. Naumowicz, A., Bylinski, C.: Improving Mizar texts with properties and requirements. In: Lecture Notes in Computer Science of MKM’04, vol. 3119, pp. 290–301 (2004)

17. Naumowicz, A., Korniłowicz, A.: A brief overview of Mizar. In: Lecture Notes in Computer Science of TPHOLs’09, vol. 5674, pp. 67–72. Springer, Berlin (2009)

    Google Scholar 

18. Pak, K.: Improving legibility of natural deduction proofs is not trivial. Logical Methods in Computer Science 10(3), 1–30 (2014)

    Article  Google Scholar 

19. Pak, K.: Methods of lemma extraction in natural deduction proofs. J. Autom. Reason. 50(2), 217–228 (2013)

    Article  MATH  Google Scholar 

20. Trybulec, A., Kornilowicz, A., Naumowicz, A., Kuperberg, K.: Formal mathematics for mathematicians. J. Autom. Reason. 50(2), 119–121 (2013)

    Article  MathSciNet  Google Scholar 

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

    Article  MATH  MathSciNet  Google Scholar 

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

Download references