I am working as a researcher at the
Czech Technical Unversity in Prague with
I am interested in interactive theorem proving and machine learning.
Most of my projects are integrated in HOL4.
Here is a
of the tactical prover TacticToe.
Czech Institute of Informatics, Robotics, and Cybernetics
Czech Technical University in Prague
166 36 Prague 6