Josef Urban

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

Prolog Technology Reinforcement Learning Prover - (System Description).

[BibT_eX]

[DOI]

Zsolt Zombori

Chad E. Brown

Proceedings of the Automated Reasoning - 10th International Joint Conference, 2020

ENIGMA Anonymous: Symbol-Independent Inference Guiding Machine (System Description).

[BibT_eX]

[DOI]

Proceedings of the Automated Reasoning - 10th International Joint Conference, 2020

2019

Can Neural Networks Learn Symbolic Rewriting?

[BibT_eX]

[DOI]

CoRR, 2019

Guiding Theorem Proving by Recurrent Neural Networks.

[BibT_eX]

[DOI]

Bartosz Piotrowski

CoRR, 2019

Hammering Mizar by Learning Clause Guidance.

[BibT_eX]

[DOI]

Zarathustra Amadeus Goertzel

CoRR, 2019

ENIGMAWatch: ProofWatch Meets ENIGMA.

[BibT_eX]

[DOI]

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

Hammering Mizar by Learning Clause Guidance (Short Paper).

[BibT_eX]

[DOI]

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

ENIGMA-NG: Efficient Neural and Gradient-Boosted Inference Guidance for E.

[BibT_eX]

[DOI]

Proceedings of the Automated Deduction - CADE 27, 2019

GRUNGE: A Grand Unified ATP Challenge.

[BibT_eX]

[DOI]

Proceedings of the Automated Deduction - CADE 27, 2019

2018

Machine Learning Guidance and Proof Certification for Connection Tableaux.

[BibT_eX]

[DOI]

Michael Färber

CoRR, 2018

Learning to Prove with Tactics.

[BibT_eX]

[DOI]

CoRR, 2018

Learning to Reason with HOL4 tactics.

[BibT_eX]

[DOI]

Thibault Gauthier

CoRR, 2018

Hierarchical invention of theorem proving strategies.

[BibT_eX]

[DOI]

AI Commun., 2018

Foreword to the Special Issue on Automated Reasoning.

[BibT_eX]

[DOI]

AI Commun., 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

Enhancing ENIGMA Given Clause Guidance.

[BibT_eX]

[DOI]

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

System Description: XSL-Based Translator of Mizar to LaTeX.

[BibT_eX]

[DOI]

Grzegorz Bancerek

Adam Naumowicz

Zarathustra Amadeus Goertzel

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

ProofWatch Meets ENIGMA: First Experiments.

[BibT_eX]

[DOI]

Zarathustra Amadeus Goertzel

Proceedings of the LPAR-22 Workshop and Short Paper Proceedings, 2018

ProofWatch: Watchlist Guidance for Large Theories in E.

[BibT_eX]

[DOI]

Stephan Schulz

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

ATPboost: Learning Premise Selection in Binary Setting with ATP Feedback.

[BibT_eX]

[DOI]

Bartosz Piotrowski

Proceedings of the Automated Reasoning - 9th International Joint Conference, 2018

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

ENIGMA: Efficient Learning-Based Inference Guiding Machine.

[BibT_eX]

[DOI]

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

TacticToe: Learning to Reason with HOL4 Tactics.

[BibT_eX]

[DOI]

Thibault Gauthier

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

Automated Invention of Strategies and Term Orderings for Vampire.

[BibT_eX]

[DOI]

Martin Suda

Proceedings of the GCAI 2017, 2017

BliStrTune: hierarchical invention of theorem proving strategies.

[BibT_eX]

[DOI]

Proceedings of the 6th ACM SIGPLAN Conference on Certified Programs and Proofs, 2017

AI at CADE/IJCAR.

[BibT_eX]

[DOI]

Proceedings of the ARCADE 2017, 2017

Monte Carlo Tableau Proof Search.

[BibT_eX]

[DOI]

Michael Färber

Proceedings of the Automated Deduction - CADE 26, 2017

Detecting Inconsistencies in Large First-Order Knowledge Bases.

[BibT_eX]

[DOI]

Proceedings of the Automated Deduction - CADE 26, 2017

2016

Preface: Twenty Years of the QED Manifesto.

[BibT_eX]

[DOI]

John Harrison

Jasmin Christian Blanchette

Freek Wiedijk

J. Formaliz. Reason., 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]

Michael Färber

CoRR, 2016

DeepMath - Deep Sequence Models for Premise Selection.

[BibT_eX]

[DOI]

CoRR, 2016

The CADE-25 Automated Theorem Proving system competition - CASC-25.

[BibT_eX]

[DOI]

AI Commun., 2016

DeepMath - Deep Sequence Models for Premise Selection.

[BibT_eX]

[DOI]

Proceedings of the Advances in Neural Information Processing Systems 29: Annual Conference on Neural Information Processing Systems 2016, 2016

Extending E Prover with Similarity Based Clause Selection Strategies.

[BibT_eX]

[DOI]

Proceedings of the Intelligent Computer Mathematics - 9th International Conference, 2016

Extracting Higher-Order Goals from the Mizar Mathematical Library.

[BibT_eX]

[DOI]

Chad E. Brown

Proceedings of the Intelligent Computer Mathematics - 9th International Conference, 2016

Learning Intelligent Theorem Proving from Large Formal Corpora.

[BibT_eX]

[DOI]

Proceedings of the International Symposium on Artificial Intelligence and Mathematics, 2016

Towards a mizar environment for isabelle: foundations and language.

[BibT_eX]

[DOI]

Karol Pak

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

Initial Experiments with Statistical Conjecturing over Large Formal Corpora.

[BibT_eX]

[DOI]

Thibault Gauthier

Proceedings of the Joint Proceedings of the FM4M, 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

MaLeS: A Framework for Automatic Tuning of Automated Theorem Provers.

[BibT_eX]

[DOI]

J. Autom. Reason., 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

Formalizing Physics: Automation, Presentation and Foundation Issues.

[BibT_eX]

[DOI]

Proceedings of the Intelligent Computer Mathematics - International Conference, 2015

Auto-hyperlinking the Stacks Project.

[BibT_eX]

[DOI]

Johan Commelin

Proceedings of the CICM 2015, 2015

Mizar: State-of-the-art and Beyond.

[BibT_eX]

[DOI]

Proceedings of the Intelligent Computer Mathematics - International Conference, 2015

Experiments with State-of-the-art Automated Provers on Problems in Tarskian Geometry.

[BibT_eX]

[DOI]

Robert Veroff

Proceedings of the IWIL@LPAR 2015, 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

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

BliStr: The Blind Strategymaker.

[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

Certified Connection Tableaux Proofs for HOL Light and TPTP.

[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

History of Interactive Theorem Proving.

[BibT_eX]

[DOI]

John Harrison

Freek Wiedijk

Proceedings of the Computational Logic, 2014

Learning-Assisted Automated Reasoning with Flyspeck.

[BibT_eX]

[DOI]

J. Autom. Reason., 2014

Premise Selection for Mathematics by Corpus Analysis and Kernel Methods.

[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

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

2013

ATP and Presentation Service for Mizar Formalizations.

[BibT_eX]

[DOI]

Piotr Rudnicki

J. Autom. Reason., 2013

The Mizar Mathematical Library in OMDoc: Translation and Applications.

[BibT_eX]

[DOI]

J. Autom. Reason., 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]

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]

Jasmin Christian Blanchette

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

E-MaLeS 1.1.

[BibT_eX]

[DOI]

Stephan Schulz

Proceedings of the Automated Deduction - CADE-24, 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

Theorem Proving in Large Formal Mathematics as an Emerging AI Field.

[BibT_eX]

[DOI]

Proceedings of the Automated Reasoning and Mathematics, 2013

2012

Parallelizing Mizar

[BibT_eX]

[DOI]

CoRR, 2012

Automated and Human Proofs in General Mathematics: An Initial Comparison.

[BibT_eX]

[DOI]

Jesse Alama

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

Learning from Multiple Proofs: First Experiments.

[BibT_eX]

[DOI]

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

Overview and Evaluation of Premise Selection Techniques for Large Theory Mathematics.

[BibT_eX]

[DOI]

Proceedings of the Automated Reasoning - 6th International Joint Conference, 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

Point-and-Write - Documenting Formal Mathematics by Reference.

[BibT_eX]

[DOI]

Carst Tankink

Christoph Lange

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

Dependencies in Formal Mathematics: Applications and Extraction for Coq and Mizar.

[BibT_eX]

[DOI]

Jesse Alama

Lionel Mamane

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

2011

Dependencies in Formal Mathematics

[BibT_eX]

[DOI]

Jesse Alama

Lionel Mamane

CoRR, 2011

MaLeCoP Machine Learning Connection Prover.

[BibT_eX]

[DOI]

Petr Stepánek

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

Semantic Graph Kernels for Automated Reasoning.

[BibT_eX]

[DOI]

Proceedings of the Eleventh SIAM International Conference on Data Mining, 2011

Escape to ATP for Mizar.

[BibT_eX]

[DOI]

Piotr Rudnicki

Proceedings of the PxTP 2011: First International Workshop on Proof eXchange for Theorem Proving, 2011

Learning2Reason.

[BibT_eX]

[DOI]

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

Licensing the Mizar Mathematical Library.

[BibT_eX]

[DOI]

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

Large Formal Wikis: Issues and Solutions.

[BibT_eX]

[DOI]

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

Content-based encoding of mathematical and code libraries.

[BibT_eX]

[DOI]

Proceedings of the ITP 2011 Workshop on Mathematical Wikis, 2011

Multi-output Ranking for Automated Reasoning.

[BibT_eX]

Proceedings of the KDIR 2011, 2011

An Overview of Methods for Large-Theory Automated Theorem Proving.

[BibT_eX]

[DOI]

Proceedings of the First Workshop on Automated Theory Engineering, 2011

2010

Automated Proof Compression by Invention of New Definitions.

[BibT_eX]

[DOI]

David Stanovský

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

Evaluation of Automated Theorem Proving on the Mizar Mathematical Library.

[BibT_eX]

[DOI]

Krystof Hoder

Andrei Voronkov

Proceedings of the Mathematical Software, 2010

Automated Reasoning and Presentation Support for Formalizing Mathematics in Mizar.

[BibT_eX]

[DOI]

Proceedings of the Intelligent Computer Mathematics, 10th International Conference, 2010

A Wiki for Mizar: Motivation, Considerations, and Initial Prototype.

[BibT_eX]

[DOI]

Proceedings of the Intelligent Computer Mathematics, 10th International Conference, 2010

2008

ATP-based Cross-Verification of Mizar Proofs: Method, Systems, and First Experiments.

[BibT_eX]

[DOI]

Math. Comput. Sci., 2008

Automated Reasoning for Mizar: Artificial Intelligence through Knowledge Exchange.

[BibT_eX]

[DOI]

Proceedings of the LPAR 2008 Workshops, 2008

MaLARea SG1- Machine Learner for Automated Reasoning with Semantic Guidance.

[BibT_eX]

[DOI]

Proceedings of the Automated Reasoning, 4th International Joint Conference, 2008

2007

ATP Cross-Verification of the Mizar MPTP Challenge Problems.

[BibT_eX]

[DOI]

Proceedings of the Logic for Programming, 2007

MaLARea: a Metasystem for Automated Reasoning in Large Theories.

[BibT_eX]

[DOI]

Proceedings of the CADE-21 Workshop on Empirically Successful Automated Reasoning in Large Theories, 2007

2006

MPTP 0.2: Design, Implementation, and Initial Experiments.

[BibT_eX]

[DOI]

J. Autom. Reason., 2006

MizarMode - an integrated proof assistance tool for the Mizar way of formalizing mathematics.

[BibT_eX]

[DOI]

J. Appl. Log., 2006

Momm - Fast Interreduction and Retrieval in Large Libraries of Formalized Mathematics.

[BibT_eX]

[DOI]

Int. J. Artif. Intell. Tools, 2006

Presenting and Explaining Mizar.

[BibT_eX]

[DOI]

Grzegorz Bancerek

Proceedings of the 7th Workshop on User Interfaces for Theorem Provers, 2006

2005

XML-izing Mizar: Making Semantic Processing and Presentation of MML Easy.

[BibT_eX]

[DOI]

Proceedings of the Mathematical Knowledge Management, 4th International Conference, 2005

2004

MPTP - Motivation, Implementation, First Experiments.

[BibT_eX]

[DOI]

J. Autom. Reason., 2004

Integrated Semantic Browsing of the Mizar Mathematical Library for Authoring Mizar Articles.

[BibT_eX]

[DOI]

Grzegorz Bancerek

Proceedings of the Mathematical Knowledge Management, Third International Conference, 2004

2003

MPTP 0.1: System Description.

[BibT_eX]

[DOI]

Proceedings of the 4th International Workshop on First-Order Theorem Proving, 2003

Translating Mizar for First Order Theorem Provers.

[BibT_eX]

[DOI]

Proceedings of the Mathematical Knowledge Management, Second International Conference, 2003

2001

BRAIN - an architecture for a broadband radio access network of the next generation.

[BibT_eX]

[DOI]

Tomás Robles Valladares

Wirel. Commun. Mob. Comput., 2001

2000

Broadband Radio Access for IP-based networks (BRAIN)-a key enabler for mobile Internet access.

[BibT_eX]

[DOI]

Dave Wisely

Werner Mohr