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 | 272 | 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 | 232 | 2002 |
Mizar in a nutshell A Grabowski, A Kornilowicz, A Naumowicz Journal of Formalized Reasoning 3 (2), 153-245, 2010 | 221 | 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 | 206 | 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 | 170 | 2002 |
Four Decades of Mizar: Foreword A Grabowski, A Korni³owicz, A Naumowicz Journal of Automated Reasoning 55, 191-198, 2015 | 132 | 2015 |
A Brief Overview of Mizar A Naumowicz, A Korni³owicz International Conference on Theorem Proving in Higher Order Logics, 67-72, 2009 | 110 | 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 |
Fundamental Theorem of Arithmetic A Korni³owicz, P Rudnicki Formalized Mathematics 12 (2), 179-186, 2004 | 23 | 2004 |
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 |