# Ondřej Kunčar

## Education

*
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
*

## Current

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.

## Research Interests

I am interested in computational logic, interactive theorem provers and systems for formal mathematics, especially in their type systems.

## Publications

### Refereed publications

**Proving Valid Quantiﬁed 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.

### Master thesis

**Systems For Formal Mathematics**
** [PDF (czech only)]**

O. Kunčar, master thesis, advisor: Josef Urban, Sep 2009.

## Individual Software Project

Preferred projects are listed here (in Czech).

**E-mail**: ondrej.kuncar(zavinac=at)mff.cuni.cz

updated: 11. 1. 2011