Mizar: State-of-the-art and beyond G Bancerek, C Byliński, A Grabowski, A Korniłowicz, R Matuszewski, ... Conferences on Intelligent Computer Mathematics, 261-279, 2015 | 154 | 2015 |

The role of the Mizar Mathematical Library for interactive proof development in Mizar G Bancerek, C Byliński, A Grabowski, A Korniłowicz, R Matuszewski, ... Journal of Automated Reasoning 61 (1-4), 9-32, 2018 | 81 | 2018 |

Methods of lemma extraction in natural deduction proofs K P±k Journal of Automated Reasoning 50 (2), 217-228, 2013 | 32 | 2013 |

Towards a Mizar environment for Isabelle: foundations and language C Kaliszyk, K P±k, J Urban Proceedings of the 5th ACM SIGPLAN Conference on Certified Programs and …, 2016 | 20 | 2016 |

Improving legibility of formal proofs based on the close reference principle is NP-hard K P±k Journal of Automated Reasoning 55 (3), 295-306, 2015 | 17 | 2015 |

Basic properties of the rank of matrices over a field K P±k Formalized Mathematics 15 (4), 199-211, 2007 | 16 | 2007 |

Improving legibility of natural deduction proofs is not trivial K P±k arXiv preprint arXiv:1407.1140, 2014 | 14 | 2014 |

Trust in RDF graphs D Tomaszuk, K P±k, H Rybiński Advances in Databases and Information Systems, 273-283, 2013 | 13 | 2013 |

Semantics of Mizar as an Isabelle object logic C Kaliszyk, K P±k Journal of Automated Reasoning 63 (3), 557-595, 2019 | 10 | 2019 |

Laplace expansion K P±k, A Trybulec Formalized Mathematics 15 (3), 143-150, 2007 | 10 | 2007 |

THE ALGORITHMS FOR IMPROVING AND REORGANIZING NATURAL DEDUCTION PROOFS K P±k order, 0 | 10* | |

Stirling numbers of the second kind K Pak Formalized Mathematics 13 (2), 337-345, 2005 | 9 | 2005 |

The Catalan Numbers. Part II K P±k | 9* | |

Affine Indepedence in Vector Spaces K P±k | 9* | |

Progress in the independent certification of Mizar Mathematical Library in Isabelle C Kaliszyk, K P±k 2017 Federated Conference on Computer Science and Information Systems …, 2017 | 8 | 2017 |

Automated improving of proof legibility in the Mizar system K P±k Intelligent Computer Mathematics, 373-387, 2014 | 8 | 2014 |

Presentation and manipulation of Mizar properties in an Isabelle object logic C Kaliszyk, K P±k International Conference on Intelligent Computer Mathematics, 193-207, 2017 | 7 | 2017 |

Topological manifolds K P±k Formalized Mathematics 22 (2), 179-186, 2014 | 7 | 2014 |

Linear transformations of Euclidean topological spaces K P±k Formalized Mathematics 19 (2), 103-108, 2011 | 7 | 2011 |

Basic properties of metrizable topological spaces K P±k Formalized Mathematics 17 (3), 201-205, 2009 | 7 | 2009 |