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

A SAT based approach for solving formulas over boolean and linear mathematical propositions G Audemard, P Bertoli, A Cimatti, A Korniłowicz, R Sebastiani International Conference on Automated Deduction, 195-210, 2002 | 229 | 2002 |

Mizar in a nutshell A Grabowski, A Kornilowicz, A Naumowicz Journal of Formalized Reasoning 3 (2), 153-245, 2010 | 219 | 2010 |

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, 9-32, 2018 | 199 | 2018 |

Bounded model checking for timed systems G Audemard, A Cimatti, A Kornilowicz, R Sebastiani International Conference on Formal Techniques for Networked and Distributed …, 2002 | 169 | 2002 |

Four Decades of Mizar: Foreword A Grabowski, A Korniłowicz, A Naumowicz Journal of Automated Reasoning 55, 191-198, 2015 | 129 | 2015 |

A Brief Overview of Mizar A Naumowicz, A Korniłowicz International Conference on Theorem Proving in Higher Order Logics, 67-72, 2009 | 109 | 2009 |

On algebraic hierarchies in mathematical repository of Mizar A Grabowski, A Korniłowicz, C Schwarzweller 2016 Federated Conference on Computer Science and Information Systems …, 2016 | 37 | 2016 |

On rewriting rules in Mizar A Korniłowicz Journal of Automated Reasoning 50, 203-210, 2013 | 36 | 2013 |

The definition of the Riemann definite integral and some related lemmas N Endou, A Korniłowicz Formalized Mathematics 8 (1), 93-102, 1999 | 34 | 1999 |

On the topological properties of meet-continuous lattices A Korniłowicz Journal of Formalized Mathematics 8, 1996 | 30 | 1996 |

Cartesian products of relations and relational structures A Korniłowicz Formalized Mathematics 6 (1), 145-152, 1997 | 29 | 1997 |

Flexary connectives in Mizar A Korniłowicz Computer Languages, Systems & Structures 44, 238-250, 2015 | 28 | 2015 |

Kuratowski pairs. Tuples and projections. G Bancerek, A Korniłowicz, A Trybulec Def 6 (x1), 1, 0 | 24 | |

Equality in computer proof-assistants A Grabowski, A Korniłowicz, C Schwarzweller 2015 Federated Conference on Computer Science and Information Systems …, 2015 | 23 | 2015 |

Definitional Expansions in Mizar: In memoriam of Andrzej Trybulec, a pioneer of computerized formalization A Korniłowicz Journal of Automated Reasoning 55, 257-268, 2015 | 22 | 2015 |

Formal Mathematics for Mathematicians: Foreward to the Special Issue A Trybulec, A Kornilowicz, A Naumowicz, K Kuperberg Journal of Automated Reasoning 50, 119-121, 2013 | 22 | 2013 |

On the real valued functions A Korniłowicz Formalized Mathematics 13 (1), 181-187, 2005 | 22 | 2005 |

Integrating boolean and mathematical solving: Foundations, basic algorithms, and requirements G Audemard, P Bertoli, A Cimatti, A Korniłowicz, R Sebastiani International Conference on Artificial Intelligence and Symbolic Computation …, 2002 | 22 | 2002 |

Fundamental Theorem of Arithmetic A Korniłowicz, P Rudnicki Formalized Mathematics 12 (2), 179-186, 2004 | 21 | 2004 |