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 | 223 | 2002 |

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 | 184 | 2015 |

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

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

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

Four decades of Mizar A Grabowski, A Korniłowicz, A Naumowicz Journal of Automated Reasoning 55 (3), 191-198, 2015 | 106 | 2015 |

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

On rewriting rules in Mizar A Korniłowicz Journal of Automated Reasoning 50 (2), 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 | 33 | 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 Journal of Formalized Mathematics 8, 1996 | 28 | 1996 |

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 | 25 | 2016 |

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

Formal mathematics for mathematicians A Trybulec, A Kornilowicz, A Naumowicz, K Kuperberg Journal of Automated Reasoning 50 (2), 119-121, 2013 | 22 | 2013 |

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

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

Intersections of intervals and balls in En T A Korniłowicz, Y Shidama Formalized Mathematics 12 (3), 301-306, 2004 | 21 | 2004 |

Standard ordering of instruction locations A Trybulec, P Rudnicki, A Korniłowicz Formalized Mathematics 9 (2), 291-301, 2001 | 21 | 2001 |

Definitional expansions in Mizar A Korniłowicz Journal of Automated Reasoning 55 (3), 257-268, 2015 | 20 | 2015 |

Integrating boolean and mathematical solving: Foundations, basic algorithms, and requirements G Audemard, P Bertoli, A Cimatti, A Korniłowicz, R Sebastiani Artificial Intelligence, Automated Reasoning, and Symbolic Computation, 231-245, 2002 | 20 | 2002 |