All Stories

  1. Improved Assistance for Interactive Proof (Keynote)

    Article • January 2023, ACM (Association for Computing Machinery)

    Cezary Kaliszyk

  2. Aligning concepts across proof assistant libraries

    Article • Journal of Symbolic Computation, January 2019, Elsevier

    Cezary Kaliszyk

  3. Foreword to the Special Issue on Automated Reasoning

    Article • AI Communications, May 2018, IOS Press

    Cezary Kaliszyk

  4. Hammer for Coq: Automation for Dependent Type Theory

    Article • Journal of Automated Reasoning, February 2018, Springer Science + Business Media

    Cezary Kaliszyk

  5. Formal microeconomic foundations and the first welfare theorem

    Article • January 2018, ACM (Association for Computing Machinery)

    Cezary Kaliszyk

  6. Formal microeconomic foundations and the first welfare theorem

    Article • January 2018, ACM (Association for Computing Machinery)

    Cezary Kaliszyk

  7. Progress in the Independent Certification of Mizar Mathematical Library in Isabelle

    Article • September 2017, Polish Information Processing Society PTI

    Cezary Kaliszyk

  8. Automating Formalization by Statistical and Semantic Parsing of Mathematics

    Article • January 2017, Springer Science + Business Media

    Cezary Kaliszyk

  9. Monte Carlo Tableau Proof Search

    Article • January 2017, Springer Science + Business Media

    Cezary Kaliszyk

  10. Isabelle Formalization of Set Theoretic Structures and Set Comprehensions

    Article • January 2017, Springer Science + Business Media

    Cezary Kaliszyk

  11. Presentation and Manipulation of Mizar Properties in an Isabelle Object Logic

    Article • January 2017, Springer Science + Business Media

    Cezary Kaliszyk

  12. Classification of Alignments Between Concepts of Formal Mathematical Systems

    Article • January 2017, Springer Science + Business Media

    Cezary Kaliszyk

  13. A FORMAL PROOF OF THE KEPLER CONJECTURE

    Article • Forum of Mathematics Pi, January 2017, Cambridge University Press

    Cezary Kaliszyk

  14. Goal Translation for a Hammer for Coq (Extended Abstract)

    Article • Electronic Proceedings in Theoretical Computer Science, June 2016, Open Publishing Association

    Cezary Kaliszyk

  15. Proceedings First International Workshop on Hammers for Type Theories

    Article • Electronic Proceedings in Theoretical Computer Science, June 2016, Open Publishing Association

    Cezary Kaliszyk

  16. A Learning-Based Fact Selector for Isabelle/HOL

    Article • Journal of Automated Reasoning, February 2016, Springer Science + Business Media

    Cezary Kaliszyk

  17. What’s in a Theorem Name?

    Article • January 2016, Springer Science + Business Media

    Cezary Kaliszyk

  18. Towards Formal Proof Metrics

    Article • January 2016, Springer Science + Business Media

    Cezary Kaliszyk

  19. Towards a mizar environment for isabelle: foundations and language

    Article • January 2016, ACM (Association for Computing Machinery)

    Cezary Kaliszyk

  20. Wikis and Collaborative Systems for Large Formal Mathematics

    Article • January 2016, Springer Science + Business Media

    Cezary Kaliszyk

  21. Proceedings Fourth Workshop on Proof eXchange for Theorem Proving

    Article • Electronic Proceedings in Theoretical Computer Science, July 2015, Open Publishing Association

    Cezary Kaliszyk

  22. MizAR 40 for Mizar 40

    Article • Journal of Automated Reasoning, July 2015, Springer Science + Business Media

    Cezary Kaliszyk

  23. Learning-assisted theorem proving with millions of lemmas

    Article • Journal of Symbolic Computation, July 2015, Elsevier

    Cezary Kaliszyk

  24. Certified Connection Tableaux Proofs for HOL Light and TPTP

    Article • January 2015, ACM (Association for Computing Machinery)

    Cezary Kaliszyk

  25. Premise Selection and External Provers for HOL4

    Article • January 2015, ACM (Association for Computing Machinery)

    Cezary Kaliszyk

  26. Intelligent Computer Mathematics

    Article • January 2015, Springer Science + Business Media

    Cezary Kaliszyk

  27. Random Forests for Premise Selection

    Article • January 2015, Springer Science + Business Media

    Cezary Kaliszyk

  28. Lemmatization for Stronger Reasoning in Large Theories

    Article • January 2015, Springer Science + Business Media

    Cezary Kaliszyk

  29. Efficient Low-Level Connection Tableaux

    Article • January 2015, Springer Science + Business Media

    Cezary Kaliszyk

  30. FEMaLeCoP: Fairly Efficient Machine Learning Connection Prover

    Article • January 2015, Springer Science + Business Media

    Cezary Kaliszyk

  31. Learning to Parse on Aligned Corpora (Rough Diamond)

    Article • January 2015, Springer Science + Business Media

    Cezary Kaliszyk

  32. Formalizing Physics: Automation, Presentation and Foundation Issues

    Article • January 2015, Springer Science + Business Media

    Cezary Kaliszyk

  33. System Description: E.T. 0.1

    Article • January 2015, Springer Science + Business Media

    Cezary Kaliszyk

  34. Sharing HOL4 and HOL Light Proof Knowledge

    Article • January 2015, Springer Science + Business Media

    Cezary Kaliszyk

  35. HOL(y)Hammer: Online ATP Service for HOL Light

    Article • Mathematics in Computer Science, June 2014, Springer Science + Business Media

    Cezary Kaliszyk

  36. Initial Experiments with TPTP-style Automated Theorem Provers on ACL2 Problems

    Article • Electronic Proceedings in Theoretical Computer Science, June 2014, Open Publishing Association

    Cezary Kaliszyk

  37. Learning-Assisted Automated Reasoning with Flyspeck

    Article • Journal of Automated Reasoning, June 2014, Springer Science + Business Media

    Cezary Kaliszyk

  38. Towards Knowledge Management for HOL Light

    Article • January 2014, Springer Science + Business Media

    Cezary Kaliszyk

  39. Matching Concepts across HOL Libraries

    Article • January 2014, Springer Science + Business Media

    Cezary Kaliszyk

  40. Developing Corpus-Based Translation Methods between Informal and Formal Mathematics: Project Description

    Article • January 2014, Springer Science + Business Media

    Cezary Kaliszyk

  41. Proceedings 10th International Workshop On User Interfaces for Theorem Provers

    Article • Electronic Proceedings in Theoretical Computer Science, July 2013, Open Publishing Association

    Cezary Kaliszyk

  42. Scalable LCF-Style Proof Translation

    Article • January 2013, Springer Science + Business Media

    Cezary Kaliszyk

  43. Automated Reasoning Service for HOL Light

    Article • January 2013, Springer Science + Business Media

    Cezary Kaliszyk

  44. Communicating Formal Proofs: The Case of Flyspeck

    Article • January 2013, Springer Science + Business Media

    Cezary Kaliszyk

  45. MaSh: Machine Learning for Sledgehammer

    Article • January 2013, Springer Science + Business Media

    Cezary Kaliszyk

  46. PRocH: Proof Reconstruction for HOL Light

    Article • January 2013, Springer Science + Business Media

    Cezary Kaliszyk

  47. Formal Mathematics on Display: A Wiki for Flyspeck

    Article • January 2013, Springer Science + Business Media

    Cezary Kaliszyk

  48. Lemma Mining over HOL Light

    Article • January 2013, Springer Science + Business Media

    Cezary Kaliszyk

  49. Algebraic Analysis of Huzita’s Origami Operations and Their Extensions

    Article • January 2013, Springer Science + Business Media

    Cezary Kaliszyk

  50. General Bindings and Alpha-Equivalence in Nominal Isabelle

    Article • Logical Methods in Computer Science, June 2012, Logical Methods in Computer Science

    Cezary Kaliszyk

  51. Quotients revisited for Isabelle/HOL

    Article • January 2011, ACM (Association for Computing Machinery)

    Cezary Kaliszyk

  52. Reasoning about Constants in Nominal Isabelle or How to Formalize the Second Fixed Point Theorem

    Article • January 2011, Springer Science + Business Media

    Cezary Kaliszyk

  53. Proof Assistant Decision Procedures for Formalizing Origami

    Article • January 2011, Springer Science + Business Media

    Cezary Kaliszyk

  54. General Bindings and Alpha-Equivalence in Nominal Isabelle

    Article • January 2011, Springer Science + Business Media

    Cezary Kaliszyk

  55. CTP-based programming languages?

    Article • ACM SIGSAM Bulletin, July 2010, ACM (Association for Computing Machinery)

    Cezary Kaliszyk

  56. Counting Derangements, Non Bijective Functions and the Birthday Problem

    Article • Formalized Mathematics, January 2010, De Gruyter

    Cezary Kaliszyk

  57. Merging Procedural and Declarative Proof

    Article • January 2009, Springer Science + Business Media

    Cezary Kaliszyk

  58. Web Interfaces for Proof Assistants

    Article • Electronic Notes in Theoretical Computer Science, May 2007, Elsevier

    Cezary Kaliszyk

  59. SIE – Intelligent Web Proxy Framework

    Article • January 2004, Springer Science + Business Media

    Cezary Kaliszyk

  60. Automating Side Conditions in Formalized Partial Functions

    Article • Springer Science + Business Media

    Cezary Kaliszyk

  61. Metis-based Paramodulation Tactic for HOL Light

    Article • EasyChair

    Cezary Kaliszyk

  62. Improving Statistical Linguistic Algorithms for Parsing Mathematics

    Article • EasyChair

    Cezary Kaliszyk

  63. Deep Network Guided Proof Search

    Article • EasyChair

    Cezary Kaliszyk

  64. TacticToe: Learning to Reason with HOL4 Tactics

    Article • EasyChair

    Cezary Kaliszyk

  65. Machine Learning of Coq Proof Guidance: First Experiments

    Article • EasyChair

    Cezary Kaliszyk

  66. Initial Experiments with External Provers and Premise Selection on HOL Light Corpora

    Article • EasyChair

    Cezary Kaliszyk

  67. Initial Experiments on Deriving a Complete HOL Simplification Set

    Article • EasyChair

    Cezary Kaliszyk

  68. Stronger Automation for Flyspeck by Feature Weighting and Strategy Evolution

    Article • EasyChair

    Cezary Kaliszyk

  69. Beagle as a HOL4 external ATP method

    Article • EasyChair

    Cezary Kaliszyk

  70. Machine Learner for Automated Reasoning 0.4 and 0.5

    Article • EasyChair

    Cezary Kaliszyk

  71. Cooperative Repositories for Formal Proofs

    Article • Springer Science + Business Media

    Cezary Kaliszyk

  72. Certified Computer Algebra on Top of an Interactive Theorem Prover

    Article • Springer Science + Business Media

    Cezary Kaliszyk