Cezary Kaliszyk
Cezary Kaliszyk
Geverifieerd e-mailadres voor uibk.ac.at - Homepage
Titel
Geciteerd door
Geciteerd door
Jaar
A formal proof of the Kepler conjecture
T Hales, M Adams, G Bauer, TD Dang, J Harrison, H Le Truong, ...
Forum of Mathematics, Pi 5, 2017
1852017
Learning-assisted automated reasoning with Flyspeck
C Kaliszyk, J Urban
Journal of Automated Reasoning 53 (2), 173-213, 2014
1392014
Hammering towards QED
JC Blanchette, C Kaliszyk, LC Paulson, J Urban
Journal of Formalized Reasoning 9 (1), 101-148, 2016
1082016
Mizar 40 for mizar 40
C Kaliszyk, J Urban
Journal of Automated Reasoning 55 (3), 245-256, 2015
942015
Deep network guided proof search
S Loos, G Irving, C Szegedy, C Kaliszyk
arXiv preprint arXiv:1701.06972, 2017
832017
MaSh: machine learning for sledgehammer
D Kühlwein, JC Blanchette, C Kaliszyk, J Urban
International Conference on Interactive Theorem Proving, 35-50, 2013
822013
HOL (y) Hammer: Online ATP service for HOL Light
C Kaliszyk, J Urban
Mathematics in Computer Science 9 (1), 5-22, 2015
712015
General bindings and alpha-equivalence in Nominal Isabelle
C Urban, C Kaliszyk
European Symposium on Programming, 480-500, 2011
712011
General bindings and alpha-equivalence in Nominal Isabelle
C Urban, C Kaliszyk
European Symposium on Programming, 480-500, 2011
712011
FEMaLeCoP: Fairly efficient machine learning connection prover
C Kaliszyk, J Urban
Logic for Programming, Artificial Intelligence, and Reasoning, 88-96, 2015
492015
A learning-based fact selector for Isabelle/HOL
JC Blanchette, D Greenaway, C Kaliszyk, D Kühlwein, J Urban
Journal of Automated Reasoning 57 (3), 219-244, 2016
472016
Reinforcement learning of theorem proving
C Kaliszyk, J Urban, H Michalewski, M Olšák
Advances in Neural Information Processing Systems, 8822-8833, 2018
462018
Scalable LCF-style proof translation
C Kaliszyk, A Krauss
International Conference on Interactive Theorem Proving, 51-66, 2013
462013
Hammer for Coq: Automation for dependent type theory
Ł Czajka, C Kaliszyk
Journal of automated reasoning 61 (1-4), 423-453, 2018
452018
Learning-assisted theorem proving with millions of lemmas
C Kaliszyk, J Urban
Journal of symbolic computation 69, 109-128, 2015
442015
Efficient semantic features for automated reasoning over large theories
C Kaliszyk, J Urban, J Vyskocil
Twenty-Fourth International Joint Conference on Artificial Intelligence, 2015
432015
Web interfaces for proof assistants
C Kaliszyk
Electronic Notes in Theoretical Computer Science 174 (2), 49-61, 2007
432007
Holstep: A machine learning dataset for higher-order logic theorem proving
C Kaliszyk, F Chollet, C Szegedy
arXiv preprint arXiv:1703.00426, 2017
422017
PRocH: proof reconstruction for HOL light
C Kaliszyk, J Urban
International Conference on Automated Deduction, 267-274, 2013
372013
Stronger automation for Flyspeck by feature weighting and strategy evolution
C Kaliszyk, J Urban
[Sl]: EasyChair, 2013
372013
Het systeem kan de bewerking nu niet uitvoeren. Probeer het later opnieuw.
Artikelen 1–20