M.S. in Computer Science (2009), Faculty of Mathematics and Physics, Charles University, Prague
B.S. in Computer Science (2006), Faculty of Mathematics and Physics, Charles University, Prague
I am a PhD student at the Department of Theoretical Computer Science and Mathematical Logic, Faculty of Mathematics and Physics, Charles University.
My supervisor is prof. RNDr. Petr Štěpánek, DrSc. and my consultant is Mgr. Josef Urban, Ph.D..
I am a member of Automated Reasoning Group.
I am interested in computational logic, interactive theorem provers and systems for formal mathematics, especially in their type systems.
Proving Valid Quantified Boolean Formulas in HOL Light
O. Kunčar, ITP 2011 (accepted)
Reconstruction of the Mizar Type System in the HOL Light System
[PDF]
O. Kunčar, in WDS'10 Proceedings of Contributed Papers: Part I – Mathematics and Computer Sciences (eds. J. Safrankova and J. Pavlu), Prague, Matfyzpress, pp. 7-12, Jun 2010.
Systems For Formal Mathematics
[PDF (czech only)]
O. Kunčar, master thesis, advisor: Josef Urban, Sep 2009.
Preferred projects are listed here (in Czech).
E-mail: ondrej.kuncar(zavinac=at)mff.cuni.cz
updated: 11. 1. 2011