Cezary Kaliszyk

According to our database1, Cezary Kaliszyk authored at least 103 papers between 2004 and 2020.

Collaborative distances:

Timeline

Legend:

Book 
In proceedings 
Article 
PhD thesis 
Other 

Links

Online presence:

On csauthors.net:

Bibliography

2020
Relaxed Weighted Path Order in Theorem Proving.
Math. Comput. Sci., 2020

Mac Lane's Comparison Theorem for the Kleisli Construction Formalized in Coq.
Math. Comput. Sci., 2020

A Survey of Languages for Formalizing Mathematics.
Proceedings of the Intelligent Computer Mathematics - 13th International Conference, 2020

Property Preserving Embedding of First-order Logic.
Proceedings of the 6th Global Conference on Artificial Intelligence, 2020

Property Invariant Embedding for Automated Reasoning.
Proceedings of the ECAI 2020 - 24th European Conference on Artificial Intelligence, 29 August-8 September 2020, Santiago de Compostela, Spain, August 29 - September 8, 2020, 2020

Exploration of neural machine translation in autoformalization of mathematics in Mizar.
Proceedings of the 9th ACM SIGPLAN International Conference on Certified Programs and Proofs, 2020

2019
Aligning concepts across proof assistant libraries.
J. Symb. Comput., 2019

Semantics of Mizar as an Isabelle Object Logic.
J. Autom. Reason., 2019

Can Neural Networks Learn Symbolic Rewriting?
CoRR, 2019

Towards Finding Longer Proofs.
CoRR, 2019

Linear Programming.
Arch. Formal Proofs, 2019

Certification of Nonclausal Connection Tableaux Proofs.
Proceedings of the Automated Reasoning with Analytic Tableaux and Related Methods, 2019

Declarative Proof Translation (Short Paper).
Proceedings of the 10th International Conference on Interactive Theorem Proving, 2019

Higher-Order Tarski Grothendieck as a Foundation for Formal Proof.
Proceedings of the 10th International Conference on Interactive Theorem Proving, 2019

GRUNGE: A Grand Unified ATP Challenge.
Proceedings of the Automated Deduction - CADE 27, 2019

2018
Hammer for Coq: Automation for Dependent Type Theory.
J. Autom. Reason., 2018

Machine Learning Guidance and Proof Certification for Connection Tableaux.
CoRR, 2018

Learning to Prove with Tactics.
CoRR, 2018

Learning to Reason with HOL4 tactics.
CoRR, 2018

Foreword to the Special Issue on Automated Reasoning.
AI Commun., 2018

Von-Neumann-Morgenstern Utility Theorem.
Arch. Formal Proofs, 2018

Reinforcement Learning of Theorem Proving.
Proceedings of the Advances in Neural Information Processing Systems 31: Annual Conference on Neural Information Processing Systems 2018, 2018

First Experiments with Neural Translation of Informal to Formal Mathematics.
Proceedings of the Intelligent Computer Mathematics - 11th International Conference, 2018

Isabelle Import Infrastructure for the Mizar Mathematical Library.
Proceedings of the Intelligent Computer Mathematics - 11th International Conference, 2018

Concrete Semantics with Coq and CoqHammer.
Proceedings of the Intelligent Computer Mathematics - 11th International Conference, 2018

Towards Formal Foundations for Game Theory.
Proceedings of the Interactive Theorem Proving - 9th International Conference, 2018

Towards a Unified Ordering for Superposition-Based Automated Reasoning.
Proceedings of the Mathematical Software - ICMS 2018, 2018

Formal microeconomic foundations and the first welfare theorem.
Proceedings of the 7th ACM SIGPLAN International Conference on Certified Programs and Proofs, 2018

2017
Microeconomics and the First Welfare Theorem.
Arch. Formal Proofs, 2017

System Description: Statistical Parsing of Informalized Mizar Formulas.
Proceedings of the 19th International Symposium on Symbolic and Numeric Algorithms for Scientific Computing, 2017

Classification of Alignments Between Concepts of Formal Mathematical Systems.
Proceedings of the Intelligent Computer Mathematics - 10th International Conference, 2017

Presentation and Manipulation of Mizar Properties in an Isabelle Object Logic.
Proceedings of the Intelligent Computer Mathematics - 10th International Conference, 2017

Isabelle Formalization of Set Theoretic Structures and Set Comprehensions.
Proceedings of the Mathematical Aspects of Computer and Information Sciences, 2017

Deep Network Guided Proof Search.
Proceedings of the LPAR-21, 2017

TacticToe: Learning to Reason with HOL4 Tactics.
Proceedings of the LPAR-21, 2017

Automating Formalization by Statistical and Semantic Parsing of Mathematics.
Proceedings of the Interactive Theorem Proving - 8th International Conference, 2017

HolStep: A Machine Learning Dataset for Higher-order Logic Theorem Proving.
Proceedings of the 5th International Conference on Learning Representations, 2017

Progress in the Independent Certification of Mizar Mathematical Library in Isabelle.
Proceedings of the 2017 Federated Conference on Computer Science and Information Systems, 2017

Monte Carlo Tableau Proof Search.
Proceedings of the Automated Deduction - CADE 26, 2017

2016
Hammering towards QED.
J. Formaliz. Reason., 2016

A Learning-Based Fact Selector for Isabelle/HOL.
J. Autom. Reason., 2016

Semantic Parsing of Mathematics by Context-based Learning from Aligned Corpora and Theorem Proving.
CoRR, 2016

Monte Carlo Connection Prover.
CoRR, 2016

Goal Translation for a Hammer for Coq (Extended Abstract).
Proceedings of the Proceedings First International Workshop on Hammers for Type Theories, 2016

What's in a Theorem Name?
Proceedings of the Interactive Theorem Proving - 7th International Conference, 2016

Towards Formal Proof Metrics.
Proceedings of the Fundamental Approaches to Software Engineering, 2016

Towards a mizar environment for isabelle: foundations and language.
Proceedings of the 5th ACM SIGPLAN Conference on Certified Programs and Proofs, 2016

A Standard for Aligning Mathematical Concepts.
Proceedings of the Joint Proceedings of the FM4M, 2016

Initial Experiments with Statistical Conjecturing over Large Formal Corpora.
Proceedings of the Joint Proceedings of the FM4M, 2016

TH1: The TPTP Typed Higher-Order Form with Rank-1 Polymorphism.
Proceedings of the 5th Workshop on Practical Aspects of Automated Reasoning co-located with International Joint Conference on Automated Reasoning (IJCAR 2016), 2016

No Choice: Reconstruction of First-order ATP Proofs without Skolem Functions.
Proceedings of the 5th Workshop on Practical Aspects of Automated Reasoning co-located with International Joint Conference on Automated Reasoning (IJCAR 2016), 2016

2015
HOL(y)Hammer: Online ATP Service for HOL Light.
Math. Comput. Sci., 2015

Learning-assisted theorem proving with millions of lemmas.
J. Symb. Comput., 2015

MizAR 40 for Mizar 40.
J. Autom. Reason., 2015

Erratum to : Learning-Assisted Automated Reasoning with Flyspeck.
J. Autom. Reason., 2015

A formal proof of the Kepler conjecture.
CoRR, 2015

Efficient Low-Level Connection Tableaux.
Proceedings of the Automated Reasoning with Analytic Tableaux and Related Methods, 2015

Formalizing Physics: Automation, Presentation and Foundation Issues.
Proceedings of the Intelligent Computer Mathematics - International Conference, 2015

Improving Statistical Linguistic Algorithms for Parsing Mathematics.
Proceedings of the IWIL@LPAR 2015, 2015

FEMaLeCoP: Fairly Efficient Machine Learning Connection Prover.
Proceedings of the Logic for Programming, Artificial Intelligence, and Reasoning, 2015

Sharing HOL4 and HOL Light Proof Knowledge.
Proceedings of the Logic for Programming, Artificial Intelligence, and Reasoning, 2015

Learning to Parse on Aligned Corpora (Rough Diamond).
Proceedings of the Interactive Theorem Proving - 6th International Conference, 2015

Efficient Semantic Features for Automated Reasoning over Large Theories.
Proceedings of the Twenty-Fourth International Joint Conference on Artificial Intelligence, 2015

Metis-based Paramodulation Tactic for HOL Light.
Proceedings of the Global Conference on Artificial Intelligence, 2015

Lemmatization for Stronger Reasoning in Large Theories.
Proceedings of the Frontiers of Combining Systems - 10th International Symposium, 2015

Random Forests for Premise Selection.
Proceedings of the Frontiers of Combining Systems - 10th International Symposium, 2015

Certified Connection Tableaux Proofs for HOL Light and TPTP.
Proceedings of the 2015 Conference on Certified Programs and Proofs, 2015

Premise Selection and External Provers for HOL4.
Proceedings of the 2015 Conference on Certified Programs and Proofs, 2015

System Description: E.T. 0.1.
Proceedings of the Automated Deduction - CADE-25, 2015

2014
Learning-Assisted Automated Reasoning with Flyspeck.
J. Autom. Reason., 2014

Initial Experiments with TPTP-style Automated Theorem Provers on ACL2 Problems.
Proceedings of the Proceedings Twelfth International Workshop on the ACL2 Theorem Prover and its Applications, 2014

Machine Learning of Coq Proof Guidance: First Experiments.
Proceedings of the 6th International Symposium on Symbolic Computation in Software Science, 2014

Wikis and Collaborative Systems for Large Formal Mathematics.
Proceedings of the Semantic Web Collaborative Spaces, 2014

Developing Corpus-Based Translation Methods between Informal and Formal Mathematics: Project Description.
Proceedings of the Intelligent Computer Mathematics - International Conference, 2014

Towards Knowledge Management for HOL Light.
Proceedings of the Intelligent Computer Mathematics - International Conference, 2014

Matching Concepts across HOL Libraries.
Proceedings of the Intelligent Computer Mathematics - International Conference, 2014

Machine Learner for Automated Reasoning 0.4 and 0.5.
Proceedings of the 4th Workshop on Practical Aspects of Automated Reasoning, 2014

Beagle as a HOL4 external ATP method.
Proceedings of the 4th Workshop on Practical Aspects of Automated Reasoning, 2014

2013
Formal Mathematics on Display: A Wiki for Flyspeck.
Proceedings of the Intelligent Computer Mathematics, 2013

Automated Reasoning Service for HOL Light.
Proceedings of the Intelligent Computer Mathematics, 2013

Lemma Mining over HOL Light.
Proceedings of the Logic for Programming, Artificial Intelligence, and Reasoning, 2013

Communicating Formal Proofs: The Case of Flyspeck.
Proceedings of the Interactive Theorem Proving - 4th International Conference, 2013

MaSh: Machine Learning for Sledgehammer.
Proceedings of the Interactive Theorem Proving - 4th International Conference, 2013

Scalable LCF-Style Proof Translation.
Proceedings of the Interactive Theorem Proving - 4th International Conference, 2013

Stronger Automation for Flyspeck by Feature Weighting and Strategy Evolution.
Proceedings of the Third International Workshop on Proof Exchange for Theorem Proving, 2013

PRocH: Proof Reconstruction for HOL Light.
Proceedings of the Automated Deduction - CADE-24, 2013

Initial Experiments on Deriving a Complete HOL Simplification Set.
Proceedings of the Third International Workshop on Proof Exchange for Theorem Proving, 2013

2012
General Bindings and Alpha-Equivalence in Nominal Isabelle
Log. Methods Comput. Sci., 2012

Initial Experiments with External Provers and Premise Selection on HOL Light Corpora.
Proceedings of the Third Workshop on Practical Aspects of Automated Reasoning, 2012

Algebraic Analysis of Huzita's Origami Operations and Their Extensions.
Proceedings of the Automated Deduction in Geometry - 9th International Workshop, 2012

2011
Quotients revisited for Isabelle/HOL.
Proceedings of the 2011 ACM Symposium on Applied Computing (SAC), TaiChung, Taiwan, March 21, 2011

Proof Assistant Decision Procedures for Formalizing Origami.
Proceedings of the Intelligent Computer Mathematics - 18th Symposium, 2011

Reasoning about Constants in Nominal Isabelle or How to Formalize the Second Fixed Point Theorem.
Proceedings of the Certified Programs and Proofs - First International Conference, 2011

2010
Counting Derangements, Non Bijective Functions and the Birthday Problem.
Formaliz. Math., 2010

CTP-based programming languages?: considerations about an experimental design.
ACM Commun. Comput. Algebra, 2010

2009
Computing with Classical Real Numbers.
J. Formaliz. Reason., 2009

2008
Merging Procedural and Declarative Proof.
Proceedings of the Types for Proofs and Programs, International Conference, 2008

A Real Semantic Web for Mathematics Deserves a Real Semantics.
Proceedings of the 3rd Semantic Wiki Workshop (SemWiki 2008) at the 5th European Semantic Web Conference (ESWC 2008), 2008

Automating Side Conditions in Formalized Partial Functions.
Proceedings of the Intelligent Computer Mathematics, 9th International Conference, 2008

2007
Web Interfaces for Proof Assistants.
Electron. Notes Theor. Comput. Sci., 2007

Certified Computer Algebra on Top of an Interactive Theorem Prover.
Proceedings of the Towards Mechanized Mathematical Assistants, 14th Symposium, 2007

Cooperative Repositories for Formal Proofs.
Proceedings of the Towards Mechanized Mathematical Assistants, 14th Symposium, 2007

2004
SIE - Intelligent Web Proxy Framework.
Proceedings of the Web Engineering - 4th International Conference, 2004


  Loading...