A SAT based approach for solving formulas over boolean and linear mathematical propositions G Audemard, P Bertoli, A Cimatti, A Korniłowicz, R Sebastiani Automated Deduction—CADE-18: 18th International Conference on Automated …, 2002 | 226 | 2002 |
Mizar: State-of-the-art and beyond G Bancerek, C Byliński, A Grabowski, A Korniłowicz, R Matuszewski, ... Intelligent Computer Mathematics: International Conference, CICM 2015 …, 2015 | 223 | 2015 |
Mizar in a nutshell A Grabowski, A Kornilowicz, A Naumowicz Journal of Formalized Reasoning 3 (2), 153-245, 2010 | 196 | 2010 |
Bounded model checking for timed systems G Audemard, A Cimatti, A Kornilowicz, R Sebastiani Formal Techniques for Networked and Distributed Sytems—FORTE 2002: 22nd …, 2002 | 171 | 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, 9-32, 2018 | 159 | 2018 |
Four Decades of Mizar: Foreword A Grabowski, A Korniłowicz, A Naumowicz Journal of Automated Reasoning 55, 191-198, 2015 | 117 | 2015 |
A Brief Overview of Mizar A Naumowicz, A Korniłowicz Theorem Proving in Higher Order Logics: 22nd International Conference …, 2009 | 102 | 2009 |
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 | 31 | 1996 |
Cartesian products of relations and relational structures A Korniłowicz Formalized Mathematics 6 (1), 145-152, 1997 | 29 | 1997 |
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 | 26 | 2016 |
Kuratowski pairs. Tuples and projections. G Bancerek, A Korniłowicz, A Trybulec Def 6 (x1), 1, 0 | 24 | |
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 …, 2002 | 23 | 2002 |
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 |
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: In memoriam of Andrzej Trybulec, a pioneer of computerized formalization A Korniłowicz Journal of Automated Reasoning 55, 257-268, 2015 | 20 | 2015 |