| Publication | Date of Publication | Type |
|---|
Mizar 60 for Mizar 50
| 2024-11-26 | Paper |
Initial experiments with TPTP-style automated theorem provers on ACL2 problems
| 2024-08-19 | Paper |
The Isabelle ENIGMA
| 2024-07-15 | Paper |
Formalizing a Diophantine representation of the set of prime numbers
| 2024-07-15 | Paper |
Learning Proof Transformations and Its Applications in Interactive Theorem Proving
| 2024-05-03 | Paper |
VizAR: visualization of automated reasoning proofs (system description)
Lecture Notes in Computer Science | 2024-02-28 | Paper |
Combining higher-order logic with set theory formalizations
Journal of Automated Reasoning | 2023-06-27 | Paper |
Declarative Proof Translation (Short Paper)
| 2023-02-03 | Paper |
Higher-Order Tarski Grothendieck as a Foundation for Formal Proof.
| 2023-02-03 | Paper |
Lash 1.0 (system description)
| 2022-12-07 | Paper |
Towards finding longer proofs
| 2022-05-25 | Paper |
Formalizing a Diophantine Representation of the Set of Prime Numbers
| 2022-04-26 | Paper |
Online machine learning techniques for Coq: a comparison
| 2022-04-22 | Paper |
JEFL: joint embedding of formal proof libraries
| 2022-03-24 | Paper |
A study of continuous vector representations for theorem proving
Journal Of Logic And Computation | 2022-01-03 | Paper |
Property invariant embedding for automated reasoning
| 2021-07-06 | Paper |
TacticToe: learning to prove with tactics
Journal of Automated Reasoning | 2021-06-09 | Paper |
Machine learning guidance for connection tableaux
Journal of Automated Reasoning | 2021-06-09 | Paper |
A survey of languages for formalizing mathematics
| 2021-01-20 | Paper |
Mac Lane's comparison theorem for the Kleisli construction formalized in Coq
Mathematics in Computer Science | 2020-10-30 | Paper |
Relaxed weighted path order in theorem proving
Mathematics in Computer Science | 2020-10-30 | Paper |
Certification of nonclausal connection tableaux proofs
| 2020-05-14 | Paper |
GRUNGE: a grand unified ATP challenge
| 2020-03-10 | Paper |
Hammering towards QED
| 2019-09-18 | Paper |
Semantics of Mizar as an Isabelle object logic
Journal of Automated Reasoning | 2019-09-02 | Paper |
Isabelle formalization of set theoretic structures and set comprehensions
Mathematical Aspects of Computer and Information Sciences | 2019-03-14 | Paper |
TacticToe: learning to reason with HOL4 tactics
EPiC Series in Computing | 2019-01-10 | Paper |
Deep network guided proof search
EPiC Series in Computing | 2019-01-10 | Paper |
Concrete semantics with Coq and CoqHammer
| 2018-10-18 | Paper |
Isabelle import infrastructure for the Mizar Mathematical Library
| 2018-10-18 | Paper |
First experiments with neural translation of informal to formal mathematics
| 2018-10-18 | Paper |
Towards formal foundations for game theory
| 2018-10-04 | Paper |
Hammer for Coq: automation for dependent type theory
Journal of Automated Reasoning | 2018-08-21 | Paper |
Towards a unified ordering for superposition-based automated reasoning
| 2018-08-17 | Paper |
Aligning concepts across proof assistant libraries
Journal of Symbolic Computation | 2018-06-14 | Paper |
Automating formalization by statistical and semantic parsing of mathematics
| 2018-01-04 | Paper |
Monte Carlo tableau proof search
| 2017-09-22 | Paper |
Classification of alignments between concepts of formal mathematical systems
| 2017-07-21 | Paper |
Presentation and manipulation of Mizar properties in an Isabelle object logic
| 2017-07-21 | Paper |
Lemmatization for stronger reasoning in large theories
Frontiers of Combining Systems | 2017-02-27 | Paper |
Random forests for premise selection
Frontiers of Combining Systems | 2017-02-27 | Paper |
A learning-based fact selector for Isabelle/HOL
Journal of Automated Reasoning | 2016-10-27 | Paper |
What's in a theorem name?
Interactive Theorem Proving | 2016-10-27 | Paper |
MizAR 40 for Mizar 40
Journal of Automated Reasoning | 2016-05-26 | Paper |
FEMaLeCoP: Fairly Efficient Machine Learning Connection Prover
Logic for Programming, Artificial Intelligence, and Reasoning | 2016-01-12 | Paper |
Sharing HOL4 and HOL Light proof knowledge
Logic for Programming, Artificial Intelligence, and Reasoning | 2016-01-12 | Paper |
Efficient Low-Level Connection Tableaux
Lecture Notes in Computer Science | 2015-12-11 | Paper |
System description: E.T. 0.1
Automated Deduction - CADE-25 | 2015-12-02 | Paper |
Formalizing physics: automation, presentation and foundation issues
Lecture Notes in Computer Science | 2015-11-20 | Paper |
Learning to parse on aligned corpora (rough diamond)
Interactive Theorem Proving | 2015-09-14 | Paper |
Erratum to: ``Learning-assisted automated reasoning with \(\mathsf{Flyspeck}\)
Journal of Automated Reasoning | 2015-07-02 | Paper |
Learning-assisted automated reasoning with \(\mathsf{Flyspeck}\)
Journal of Automated Reasoning | 2015-06-23 | Paper |
HOL(y)Hammer: online ATP service for HOL Light
Mathematics in Computer Science | 2015-03-25 | Paper |
Learning-assisted theorem proving with millions of lemmas
Journal of Symbolic Computation | 2015-01-14 | Paper |
Towards Knowledge Management for HOL Light
Lecture Notes in Computer Science | 2014-08-07 | Paper |
Matching concepts across HOL libraries
Lecture Notes in Computer Science | 2014-08-07 | Paper |
Developing corpus-based translation methods between informal and formal mathematics: project description
Lecture Notes in Computer Science | 2014-08-07 | Paper |
Lemma Mining over HOL Light
Logic for Programming, Artificial Intelligence, and Reasoning | 2014-01-17 | Paper |
Web interfaces for proof assistants
Electronic Notes in Theoretical Computer Science | 2013-12-20 | Paper |
Algebraic analysis of Huzita's origami operations and their extensions
Automated Deduction in Geometry | 2013-09-20 | Paper |
Automated reasoning service for HOL Light
Lecture Notes in Computer Science | 2013-08-09 | Paper |
Formal mathematics on display: a wiki for Flyspeck
Lecture Notes in Computer Science | 2013-08-09 | Paper |
Communicating formal proofs: the case of Flyspeck
Interactive Theorem Proving | 2013-08-07 | Paper |
MaSh: machine learning for Sledgehammer
Interactive Theorem Proving | 2013-08-07 | Paper |
Scalable LCF-style proof translation
Interactive Theorem Proving | 2013-08-07 | Paper |
PRocH: proof reconstruction for HOL Light
Automated Deduction – CADE-24 | 2013-06-14 | Paper |
General bindings and alpha-equivalence in Nominal Isabelle
Logical Methods in Computer Science | 2012-07-03 | Paper |
Reasoning about constants in Nominal Isabelle or how to formalize the second fixed point theorem
Certified Programs and Proofs | 2011-11-22 | Paper |
Proof assistant decision procedures for formalizing origami
Lecture Notes in Computer Science | 2011-07-29 | Paper |
General bindings and alpha-equivalence in Nominal Isabelle
Programming Languages and Systems | 2011-05-19 | Paper |
Computing with classical real numbers
| 2009-10-22 | Paper |
Merging Procedural and Declarative Proof
Lecture Notes in Computer Science | 2009-07-02 | Paper |
Automating Side Conditions in Formalized Partial Functions
Lecture Notes in Computer Science | 2009-01-27 | Paper |
Certified Computer Algebra on Top of an Interactive Theorem Prover
Towards Mechanized Mathematical Assistants | 2007-11-28 | Paper |
Cooperative Repositories for Formal Proofs
Towards Mechanized Mathematical Assistants | 2007-11-28 | Paper |
