Cezary Kaliszyk
Universitat Innsbruck
My Publications
Aligning concepts across proof assistant libraries
Journal of Symbolic Computation
January 2019
Foreword to the Special Issue on Automated Reasoning
AI Communications
May 2018
Hammer for Coq: Automation for Dependent Type Theory
Journal of Automated Reasoning
February 2018
Formal microeconomic foundations and the first welfare theorem
January 2018
Formal microeconomic foundations and the first welfare theorem
January 2018
Progress in the Independent Certiﬁcation of Mizar Mathematical Library in Isabelle
September 2017
Automating Formalization by Statistical and Semantic Parsing of Mathematics
January 2017
Monte Carlo Tableau Proof Search
January 2017
Isabelle Formalization of Set Theoretic Structures and Set Comprehensions
January 2017
Presentation and Manipulation of Mizar Properties in an Isabelle Object Logic
January 2017
Classification of Alignments Between Concepts of Formal Mathematical Systems
January 2017
A FORMAL PROOF OF THE KEPLER CONJECTURE
Forum of Mathematics Pi
January 2017
Goal Translation for a Hammer for Coq (Extended Abstract)
Electronic Proceedings in Theoretical Computer Science
June 2016
Proceedings First International Workshop on Hammers for Type Theories
Electronic Proceedings in Theoretical Computer Science
June 2016
A Learning-Based Fact Selector for Isabelle/HOL
Journal of Automated Reasoning
February 2016
What’s in a Theorem Name?
January 2016
Towards Formal Proof Metrics
January 2016
Towards a mizar environment for isabelle: foundations and language
January 2016
Wikis and Collaborative Systems for Large Formal Mathematics
January 2016
Proceedings Fourth Workshop on Proof eXchange for Theorem Proving
Electronic Proceedings in Theoretical Computer Science
July 2015
MizAR 40 for Mizar 40
Journal of Automated Reasoning
July 2015
Learning-assisted theorem proving with millions of lemmas
Journal of Symbolic Computation
July 2015
Intelligent Computer Mathematics
January 2015
Random Forests for Premise Selection
January 2015
Lemmatization for Stronger Reasoning in Large Theories
January 2015
Efficient Low-Level Connection Tableaux
January 2015
FEMaLeCoP: Fairly Efficient Machine Learning Connection Prover
January 2015
Learning to Parse on Aligned Corpora (Rough Diamond)
January 2015
Formalizing Physics: Automation, Presentation and Foundation Issues
January 2015
System Description: E.T. 0.1
January 2015
Certified Connection Tableaux Proofs for HOL Light and TPTP
January 2015
Premise Selection and External Provers for HOL4
January 2015
Sharing HOL4 and HOL Light Proof Knowledge
January 2015
HOL(y)Hammer: Online ATP Service for HOL Light
Mathematics in Computer Science
June 2014
Initial Experiments with TPTP-style Automated Theorem Provers on ACL2 Problems
Electronic Proceedings in Theoretical Computer Science
June 2014
Learning-Assisted Automated Reasoning with Flyspeck
Journal of Automated Reasoning
June 2014
Towards Knowledge Management for HOL Light
January 2014
Matching Concepts across HOL Libraries
January 2014
Developing Corpus-Based Translation Methods between Informal and Formal Mathematics: Pr...
January 2014
Proceedings 10th International Workshop On User Interfaces for Theorem Provers
Electronic Proceedings in Theoretical Computer Science
July 2013
Scalable LCF-Style Proof Translation
January 2013
Automated Reasoning Service for HOL Light
January 2013
Communicating Formal Proofs: The Case of Flyspeck
January 2013
MaSh: Machine Learning for Sledgehammer
January 2013
PRocH: Proof Reconstruction for HOL Light
January 2013
Formal Mathematics on Display: A Wiki for Flyspeck
January 2013
Lemma Mining over HOL Light
January 2013
Algebraic Analysis of Huzita’s Origami Operations and Their Extensions
January 2013
General Bindings and Alpha-Equivalence in Nominal Isabelle
Logical Methods in Computer Science
June 2012
Quotients revisited for Isabelle/HOL
January 2011
Reasoning about Constants in Nominal Isabelle or How to Formalize the Second Fixed Poin...
January 2011
Proof Assistant Decision Procedures for Formalizing Origami
January 2011
General Bindings and Alpha-Equivalence in Nominal Isabelle
January 2011
CTP-based programming languages?
ACM SIGSAM Bulletin
July 2010
Counting Derangements, Non Bijective Functions and the Birthday Problem
Formalized Mathematics
January 2010
Merging Procedural and Declarative Proof
January 2009
Web Interfaces for Proof Assistants
Electronic Notes in Theoretical Computer Science
May 2007
SIE – Intelligent Web Proxy Framework
January 2004
Automating Side Conditions in Formalized Partial Functions
Metis-based Paramodulation Tactic for HOL Light
Improving Statistical Linguistic Algorithms for Parsing Mathematics
Deep Network Guided Proof Search
TacticToe: Learning to Reason with HOL4 Tactics
Machine Learning of Coq Proof Guidance: First Experiments
Initial Experiments with External Provers and Premise Selection on HOL Light Corpora
Initial Experiments on Deriving a Complete HOL Simplification Set
Stronger Automation for Flyspeck by Feature Weighting and Strategy Evolution
Beagle as a HOL4 external ATP method
Machine Learner for Automated Reasoning 0.4 and 0.5
Cooperative Repositories for Formal Proofs
Certified Computer Algebra on Top of an Interactive Theorem Prover