Cezary Kaliszyk

Proceedings of the Workshop on Practical Aspects of Automated Reasoning Co-located with the 11th International Joint Conference on Automated Reasoning (FLoC/IJCAR 2022), Haifa, Israel, August, 11, 2022

Formalizing a Diophantine Representation of the Set of Prime Numbers.

[BibT_eX]

[DOI]

Zarathustra Amadeus Goertzel

Proceedings of the 13th International Conference on Interactive Theorem Proving, 2022

The Isabelle ENIGMA.

[BibT_eX]

[DOI]

Proceedings of the 13th International Conference on Interactive Theorem Proving, 2022

Learning Higher-Order Logic Programs From Failures.

[BibT_eX]

[DOI]

David M. Cerna

Proceedings of the Thirty-First International Joint Conference on Artificial Intelligence, 2022

Adversarial Learning to Reason in an Arbitrary Logic.

[BibT_eX]

[DOI]

Proceedings of the Thirty-Fifth International Florida Artificial Intelligence Research Society Conference, 2022

Proofgold: Blockchain for Formal Methods.

[BibT_eX]

[DOI]

Proceedings of the 4th International Workshop on Formal Methods for Blockchains, 2022

Lash 1.0 (System Description).

[BibT_eX]

[DOI]

Chad E. Brown

Proceedings of the Automated Reasoning - 11th International Joint Conference, 2022

2021

A study of continuous vector representations for theorem proving.

[BibT_eX]

[DOI]

J. Log. Comput., 2021

TacticToe: Learning to Prove with Tactics.

[BibT_eX]

[DOI]

J. Autom. Reason., 2021

Machine Learning Guidance for Connection Tableaux.

[BibT_eX]

[DOI]

J. Autom. Reason., 2021

Learning Higher-Order Programs without Meta-Interpretive Learning.

[BibT_eX]

[DOI]

David M. Cerna

CoRR, 2021

A Study of Continuous Vector Representationsfor Theorem Proving.

[BibT_eX]

[DOI]

CoRR, 2021

Towards Finding Longer Proofs.

[BibT_eX]

[DOI]

Proceedings of the Automated Reasoning with Analytic Tableaux and Related Methods, 2021

Online Machine Learning Techniques for Coq: A Comparison.

[BibT_eX]

[DOI]

Proceedings of the Intelligent Computer Mathematics - 14th International Conference, 2021

Disambiguating Symbolic Expressions in Informal Documents.

[BibT_eX]

[DOI]

Dennis Müller

Proceedings of the 9th International Conference on Learning Representations, 2021

JEFL: Joint Embedding of Formal Proof Libraries.

[BibT_eX]

[DOI]

Qingxiang Wang

Proceedings of the Frontiers of Combining Systems - 13th International Symposium, 2021

2020

Relaxed Weighted Path Order in Theorem Proving.

[BibT_eX]

[DOI]

Jan Jakubuv

Math. Comput. Sci., 2020

Mac Lane's Comparison Theorem for the Kleisli Construction Formalized in Coq.

[BibT_eX]

[DOI]

Burak Ekici

Math. Comput. Sci., 2020

A Survey of Languages for Formalizing Mathematics.

[BibT_eX]

[DOI]

Florian Rabe

Proceedings of the Intelligent Computer Mathematics - 13th International Conference, 2020

Property Preserving Embedding of First-order Logic.

[BibT_eX]

[DOI]

Stephanie Autherith

Proceedings of the 6th Global Conference on Artificial Intelligence, 2020

Property Invariant Embedding for Automated Reasoning.

[BibT_eX]

[DOI]

Miroslav Olsák

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.

[BibT_eX]

[DOI]

Proceedings of the 9th ACM SIGPLAN International Conference on Certified Programs and Proofs, 2020

2019

Aligning concepts across proof assistant libraries.

[BibT_eX]

[DOI]

J. Symb. Comput., 2019

Semantics of Mizar as an Isabelle Object Logic.

[BibT_eX]

[DOI]

J. Autom. Reason., 2019

Can Neural Networks Learn Symbolic Rewriting?

[BibT_eX]

[DOI]

CoRR, 2019

Linear Programming.

[BibT_eX]

[DOI]

Arch. Formal Proofs, 2019

Certification of Nonclausal Connection Tableaux Proofs.

[BibT_eX]

[DOI]

Proceedings of the Automated Reasoning with Analytic Tableaux and Related Methods, 2019

Declarative Proof Translation (Short Paper).

[BibT_eX]

[DOI]

Proceedings of the 10th International Conference on Interactive Theorem Proving, 2019

Higher-Order Tarski Grothendieck as a Foundation for Formal Proof.

[BibT_eX]

[DOI]

Chad E. Brown

Proceedings of the 10th International Conference on Interactive Theorem Proving, 2019

GRUNGE: A Grand Unified ATP Challenge.

[BibT_eX]

[DOI]

Proceedings of the Automated Deduction - CADE 27, 2019

2018

Hammer for Coq: Automation for Dependent Type Theory.

[BibT_eX]

[DOI]

Lukasz Czajka

J. Autom. Reason., 2018

Machine Learning Guidance and Proof Certification for Connection Tableaux.

[BibT_eX]

[DOI]

CoRR, 2018

Learning to Prove with Tactics.

[BibT_eX]

[DOI]

CoRR, 2018

Learning to Reason with HOL4 tactics.

[BibT_eX]

[DOI]

CoRR, 2018

Foreword to the Special Issue on Automated Reasoning.

[BibT_eX]

[DOI]

AI Commun., 2018

Von-Neumann-Morgenstern Utility Theorem.

[BibT_eX]

[DOI]

Arch. Formal Proofs, 2018

Reinforcement Learning of Theorem Proving.

[BibT_eX]

[DOI]

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.

[BibT_eX]

[DOI]

Qingxiang Wang

Proceedings of the Intelligent Computer Mathematics - 11th International Conference, 2018

Isabelle Import Infrastructure for the Mizar Mathematical Library.

[BibT_eX]

[DOI]

Proceedings of the Intelligent Computer Mathematics - 11th International Conference, 2018

Concrete Semantics with Coq and CoqHammer.

[BibT_eX]

[DOI]

Lukasz Czajka

Burak Ekici

Proceedings of the Intelligent Computer Mathematics - 11th International Conference, 2018

Towards Formal Foundations for Game Theory.

[BibT_eX]

[DOI]

Proceedings of the Interactive Theorem Proving - 9th International Conference, 2018

Towards a Unified Ordering for Superposition-Based Automated Reasoning.

[BibT_eX]

[DOI]

Jan Jakubuv

Proceedings of the Mathematical Software - ICMS 2018, 2018

Formal microeconomic foundations and the first welfare theorem.

[BibT_eX]

[DOI]

Proceedings of the 7th ACM SIGPLAN International Conference on Certified Programs and Proofs, 2018

2017

Microeconomics and the First Welfare Theorem.

[BibT_eX]

[DOI]

Arch. Formal Proofs, 2017

System Description: Statistical Parsing of Informalized Mizar Formulas.

[BibT_eX]

[DOI]

Proceedings of the 19th International Symposium on Symbolic and Numeric Algorithms for Scientific Computing, 2017

Classification of Alignments Between Concepts of Formal Mathematical Systems.

[BibT_eX]

[DOI]

Proceedings of the Intelligent Computer Mathematics - 10th International Conference, 2017

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

[BibT_eX]

[DOI]

Proceedings of the Intelligent Computer Mathematics - 10th International Conference, 2017

Isabelle Formalization of Set Theoretic Structures and Set Comprehensions.

[BibT_eX]

[DOI]

Proceedings of the Mathematical Aspects of Computer and Information Sciences, 2017

Deep Network Guided Proof Search.

[BibT_eX]

[DOI]

Proceedings of the LPAR-21, 2017

TacticToe: Learning to Reason with HOL4 Tactics.

[BibT_eX]

[DOI]

Proceedings of the LPAR-21, 2017

Automating Formalization by Statistical and Semantic Parsing of Mathematics.

[BibT_eX]

[DOI]

Proceedings of the Interactive Theorem Proving - 8th International Conference, 2017

HolStep: A Machine Learning Dataset for Higher-order Logic Theorem Proving.

[BibT_eX]

[DOI]

François Chollet

Christian Szegedy

Proceedings of the 5th International Conference on Learning Representations, 2017

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

[BibT_eX]

[DOI]

Proceedings of the 2017 Federated Conference on Computer Science and Information Systems, 2017

Monte Carlo Tableau Proof Search.

[BibT_eX]

[DOI]

Jasmin Christian Blanchette

Proceedings of the Automated Deduction - CADE 26, 2017

2016

Hammering towards QED.

[BibT_eX]

[DOI]

Lawrence C. Paulson

Jasmin Christian Blanchette

J. Formaliz. Reason., 2016

A Learning-Based Fact Selector for Isabelle/HOL.

[BibT_eX]

[DOI]

J. Autom. Reason., 2016

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

[BibT_eX]

[DOI]

CoRR, 2016

Monte Carlo Connection Prover.

[BibT_eX]

[DOI]

CoRR, 2016

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

[BibT_eX]

[DOI]

Lukasz Czajka

Proceedings of the Proceedings First International Workshop on Hammers for Type Theories, 2016

What's in a Theorem Name?

[BibT_eX]

[DOI]

David Aspinall

Proceedings of the Interactive Theorem Proving - 7th International Conference, 2016

Towards Formal Proof Metrics.

[BibT_eX]

[DOI]

David Aspinall

Proceedings of the Fundamental Approaches to Software Engineering, 2016

Towards a mizar environment for isabelle: foundations and language.

[BibT_eX]

[DOI]

Proceedings of the 5th ACM SIGPLAN Conference on Certified Programs and Proofs, 2016

A Standard for Aligning Mathematical Concepts.

[BibT_eX]

[DOI]

Proceedings of the Joint Proceedings of the FM4M, 2016

Initial Experiments with Statistical Conjecturing over Large Formal Corpora.

[BibT_eX]

[DOI]

Proceedings of the Joint Proceedings of the FM4M, 2016

TH1: The TPTP Typed Higher-Order Form with Rank-1 Polymorphism.

[BibT_eX]

[DOI]

Geoff Sutcliffe

Florian Rabe

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.

[BibT_eX]

[DOI]

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.

[BibT_eX]

[DOI]

Math. Comput. Sci., 2015

Learning-assisted theorem proving with millions of lemmas.

[BibT_eX]

[DOI]

J. Symb. Comput., 2015

MizAR 40 for Mizar 40.

[BibT_eX]

[DOI]

J. Autom. Reason., 2015

Erratum to : Learning-Assisted Automated Reasoning with Flyspeck.

[BibT_eX]

[DOI]

J. Autom. Reason., 2015

A formal proof of the Kepler conjecture.

[BibT_eX]

[DOI]

CoRR, 2015

Efficient Low-Level Connection Tableaux.

[BibT_eX]

[DOI]

Proceedings of the Automated Reasoning with Analytic Tableaux and Related Methods, 2015

Formalizing Physics: Automation, Presentation and Foundation Issues.

[BibT_eX]

[DOI]

Proceedings of the Intelligent Computer Mathematics - International Conference, 2015

Improving Statistical Linguistic Algorithms for Parsing Mathematics.

[BibT_eX]

[DOI]

Proceedings of the IWIL@LPAR 2015, 2015

FEMaLeCoP: Fairly Efficient Machine Learning Connection Prover.

[BibT_eX]

[DOI]

Proceedings of the Logic for Programming, Artificial Intelligence, and Reasoning, 2015

Sharing HOL4 and HOL Light Proof Knowledge.

[BibT_eX]

[DOI]

Proceedings of the Logic for Programming, Artificial Intelligence, and Reasoning, 2015

Learning to Parse on Aligned Corpora (Rough Diamond).

[BibT_eX]

[DOI]

Proceedings of the Interactive Theorem Proving - 6th International Conference, 2015

Efficient Semantic Features for Automated Reasoning over Large Theories.

[BibT_eX]

[DOI]

Proceedings of the Twenty-Fourth International Joint Conference on Artificial Intelligence, 2015

Metis-based Paramodulation Tactic for HOL Light.

[BibT_eX]

[DOI]

Proceedings of the Global Conference on Artificial Intelligence, 2015

Lemmatization for Stronger Reasoning in Large Theories.

[BibT_eX]

[DOI]

Proceedings of the Frontiers of Combining Systems - 10th International Symposium, 2015

Random Forests for Premise Selection.

[BibT_eX]

[DOI]

Proceedings of the Frontiers of Combining Systems - 10th International Symposium, 2015

Certified Connection Tableaux Proofs for HOL Light and TPTP.

[BibT_eX]

[DOI]

Proceedings of the 2015 Conference on Certified Programs and Proofs, 2015

Premise Selection and External Provers for HOL4.

[BibT_eX]

[DOI]

Proceedings of the 2015 Conference on Certified Programs and Proofs, 2015

System Description: E.T. 0.1.

[BibT_eX]

[DOI]

Proceedings of the Automated Deduction - CADE-25, 2015

2014

Learning-Assisted Automated Reasoning with Flyspeck.

[BibT_eX]

[DOI]

J. Autom. Reason., 2014

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

[BibT_eX]

[DOI]

Sebastiaan J. C. Joosten

Proceedings of the Proceedings Twelfth International Workshop on the ACL2 Theorem Prover and its Applications, 2014

Machine Learning of Coq Proof Guidance: First Experiments.

[BibT_eX]

[DOI]

Lionel Mamane

Proceedings of the 6th International Symposium on Symbolic Computation in Software Science, 2014

Wikis and Collaborative Systems for Large Formal Mathematics.

[BibT_eX]

[DOI]

Proceedings of the Semantic Web Collaborative Spaces, 2014

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

[BibT_eX]

[DOI]

Proceedings of the Intelligent Computer Mathematics - International Conference, 2014

Towards Knowledge Management for HOL Light.

[BibT_eX]

[DOI]

Florian Rabe

Proceedings of the Intelligent Computer Mathematics - International Conference, 2014

Matching Concepts across HOL Libraries.

[BibT_eX]

[DOI]

Proceedings of the Intelligent Computer Mathematics - International Conference, 2014

Machine Learner for Automated Reasoning 0.4 and 0.5.

[BibT_eX]

[DOI]

Proceedings of the 4th Workshop on Practical Aspects of Automated Reasoning, 2014

Beagle as a HOL4 external ATP method.

[BibT_eX]

[DOI]

Proceedings of the 4th Workshop on Practical Aspects of Automated Reasoning, 2014

2013

Formal Mathematics on Display: A Wiki for Flyspeck.

[BibT_eX]

[DOI]

Proceedings of the Intelligent Computer Mathematics, 2013

Automated Reasoning Service for HOL Light.

[BibT_eX]

[DOI]

Proceedings of the Intelligent Computer Mathematics, 2013

Lemma Mining over HOL Light.

[BibT_eX]

[DOI]

Jasmin Christian Blanchette

Proceedings of the Logic for Programming, Artificial Intelligence, and Reasoning, 2013

Communicating Formal Proofs: The Case of Flyspeck.

[BibT_eX]

[DOI]

Proceedings of the Interactive Theorem Proving - 4th International Conference, 2013

MaSh: Machine Learning for Sledgehammer.

[BibT_eX]

[DOI]

Daniel Kühlwein

Proceedings of the Interactive Theorem Proving - 4th International Conference, 2013

Scalable LCF-Style Proof Translation.

[BibT_eX]

[DOI]

Alexander Krauss

Proceedings of the Interactive Theorem Proving - 4th International Conference, 2013

Stronger Automation for Flyspeck by Feature Weighting and Strategy Evolution.

[BibT_eX]

[DOI]

Proceedings of the Third International Workshop on Proof Exchange for Theorem Proving, 2013

PRocH: Proof Reconstruction for HOL Light.

[BibT_eX]

[DOI]

Proceedings of the Automated Deduction - CADE-24, 2013

Initial Experiments on Deriving a Complete HOL Simplification Set.

[BibT_eX]

[DOI]

Thomas Sternagel

Proceedings of the Third International Workshop on Proof Exchange for Theorem Proving, 2013

2012

General Bindings and Alpha-Equivalence in Nominal Isabelle

[BibT_eX]

[DOI]

Christian Urban

Log. Methods Comput. Sci., 2012

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

[BibT_eX]

[DOI]

Proceedings of the Third Workshop on Practical Aspects of Automated Reasoning, 2012

Algebraic Analysis of Huzita's Origami Operations and Their Extensions.

[BibT_eX]

[DOI]

Fadoua Ghourabi

Asem Kasem

Proceedings of the Automated Deduction in Geometry - 9th International Workshop, 2012

2011

Quotients revisited for Isabelle/HOL.

[BibT_eX]

[DOI]

Christian Urban

Proceedings of the 2011 ACM Symposium on Applied Computing (SAC), TaiChung, Taiwan, March 21, 2011

Proof Assistant Decision Procedures for Formalizing Origami.

[BibT_eX]

[DOI]

Tetsuo Ida

Proceedings of the Intelligent Computer Mathematics - 18th Symposium, 2011

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

[BibT_eX]

[DOI]

Henk Barendregt

Proceedings of the Certified Programs and Proofs - First International Conference, 2011

2010

Counting Derangements, Non Bijective Functions and the Birthday Problem.

[BibT_eX]

[DOI]

Formaliz. Math., 2010

CTP-based programming languages?: considerations about an experimental design.

[BibT_eX]

[DOI]

Florian Haftmann

Walther Neuper

ACM Commun. Comput. Algebra, 2010

2009

Computing with Classical Real Numbers.

[BibT_eX]

[DOI]

Russell O'Connor

J. Formaliz. Reason., 2009

2008

Merging Procedural and Declarative Proof.

[BibT_eX]

[DOI]

Freek Wiedijk

Proceedings of the Types for Proofs and Programs, International Conference, 2008

A Real Semantic Web for Mathematics Deserves a Real Semantics.

[BibT_eX]

[DOI]

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.

[BibT_eX]

[DOI]

Proceedings of the Intelligent Computer Mathematics, 9th International Conference, 2008

2007

Certified Computer Algebra on Top of an Interactive Theorem Prover.

[BibT_eX]

[DOI]

Freek Wiedijk

Proceedings of the Towards Mechanized Mathematical Assistants, 14th Symposium, 2007

Cooperative Repositories for Formal Proofs.

[BibT_eX]

[DOI]

Pierre Corbineau

Proceedings of the Towards Mechanized Mathematical Assistants, 14th Symposium, 2007

2006

Web Interfaces for Proof Assistants.

[BibT_eX]

[DOI]