Author:Cezary Kaliszyk

Publications
Prover9 Unleashed: Automated Configuration for Enhanced Proof Discovery Kristina Aleksandrova, Jan Jakubuv and Cezary Kaliszyk In:Proceedings of 25th Conference on Logic for Programming, Artificial Intelligence and Reasoning
Experiments with Choice in Dependently-Typed Higher-Order Logic Daniel Ranalter, Chad Brown and Cezary Kaliszyk In:Proceedings of 25th Conference on Logic for Programming, Artificial Intelligence and Reasoning
Experiments on Infinite Model Finding in SMT Solving Julian Parsert, Chad Brown, Mikolas Janota and Cezary Kaliszyk In:Proceedings of 24th International Conference on Logic for Programming, Artificial Intelligence and Reasoning
Property Preserving Embedding of First-order Logic Julian Parsert, Stephanie Autherith and Cezary Kaliszyk In:GCAI 2020. 6th Global Conference on Artificial Intelligence (GCAI 2020)
TacticToe: Learning to Reason with HOL4 Tactics Thibault Gauthier, Cezary Kaliszyk and Josef Urban In:LPAR-21. 21st International Conference on Logic for Programming, Artificial Intelligence and Reasoning
Deep Network Guided Proof Search Sarah Loos, Geoffrey Irving, Christian Szegedy and Cezary Kaliszyk In:LPAR-21. 21st International Conference on Logic for Programming, Artificial Intelligence and Reasoning
Improving Statistical Linguistic Algorithms for Parsing Mathematics Cezary Kaliszyk, Josef Urban and Jiri Vyskocil In:IWIL-2015. 11th International Workshop on the Implementation of Logics
Metis-based Paramodulation Tactic for HOL Light Michael Färber and Cezary Kaliszyk In:GCAI 2015. Global Conference on Artificial Intelligence
Beagle as a HOL4 external ATP method Thibault Gauthier, Cezary Kaliszyk, Chantal Keller and Michael Norrish In:PAAR-2014. 4th Workshop on Practical Aspects of Automated Reasoning
Machine Learner for Automated Reasoning 0.4 and 0.5 Cezary Kaliszyk, Josef Urban and Jiri Vyskocil In:PAAR-2014. 4th Workshop on Practical Aspects of Automated Reasoning
Machine Learning of Coq Proof Guidance: First Experiments Cezary Kaliszyk, Lionel Mamane and Josef Urban In:SCSS 2014. 6th International Symposium on Symbolic Computation in Software Science
Initial Experiments with External Provers and Premise Selection on HOL Light Corpora Cezary Kaliszyk and Josef Urban In:PAAR-2012. Third Workshop on Practical Aspects of Automated Reasoning
Stronger Automation for Flyspeck by Feature Weighting and Strategy Evolution Cezary Kaliszyk and Josef Urban In:PxTP 2013. Third International Workshop on Proof Exchange for Theorem Proving
Initial Experiments on Deriving a Complete HOL Simplification Set Cezary Kaliszyk and Thomas Sternagel In:PxTP 2013. Third International Workshop on Proof Exchange for Theorem Proving

Keyphrases

A* proof search, ATP Competitions, automated reasoning⁴, automated theorem proving², automatic theorem provers, Beagle, choice, completion, computational linguistics, Coq, deep learning, dependent HOL, feature weighting, first-order logic², Flyspeck², formal mathematics², higher-order logic³, HOL, HOL Light⁴, HOL4, infinite model, interactive theorem proving², large theories², logical properties, machine learning⁴, MESON, METIS, Mizar, Neural Embedding, paramodulation, Parsing Mathematics, premise selection, proof advice, proof assistants, proof automation, Proof tactics, proof translation, rewriting, simple type theory, SMT, Strategy evolution, strategy invention, Strategy Scheduling, SyGuS, tableaux, theorem proving, type checking, type theory.