MizAR 40 for Mizar 40
From MaRDI portal
Publication:286800
DOI10.1007/s10817-015-9330-8zbMath1356.68191arXiv1310.2805OpenAlexW1815556503WikidataQ59428699 ScholiaQ59428699MaRDI QIDQ286800
Publication date: 26 May 2016
Published in: Journal of Automated Reasoning (Search for Journal in Brave)
Full work available at URL: https://arxiv.org/abs/1310.2805
automated reasoningartificial intelligencemachine learningMizarformal mathematicslarge theoriespremise selection
Lua error in Module:PublicationMSCList at line 37: attempt to index local 'msc_result' (a nil value).
Related Items (34)
Deepalgebra -- an outline of a program ⋮ Presentation and manipulation of Mizar properties in an Isabelle object logic ⋮ ENIGMA: efficient learning-based inference guiding machine ⋮ Improving stateful premise selection with transformers ⋮ Automating Boolean set operations in Mizar proof checking with the aid of an external SAT solver ⋮ Fast and slow enigmas and parental guidance ⋮ Vampire with a brain is a good ITP hammer ⋮ Make E Smart Again (Short Paper) ⋮ ENIGMA Anonymous: Symbol-Independent Inference Guiding Machine (System Description) ⋮ Prolog Technology Reinforcement Learning Prover ⋮ From informal to formal proofs in Euclidean geometry ⋮ Mizar: State-of-the-art and Beyond ⋮ Formalizing Physics: Automation, Presentation and Foundation Issues ⋮ The role of entropy in guiding a connection prover ⋮ Learning theorem proving components ⋮ System Description: E.T. 0.1 ⋮ A learning-based fact selector for Isabelle/HOL ⋮ The role of the Mizar mathematical library for interactive proof development in Mizar ⋮ Hammer for Coq: automation for dependent type theory ⋮ Contradiction separation based dynamic multi-clause synergized automated deduction ⋮ Random Forests for Premise Selection ⋮ Lemmatization for Stronger Reasoning in Large Theories ⋮ Learning-assisted theorem proving with millions of lemmas ⋮ Hierarchical invention of theorem proving strategies ⋮ Hammering Mizar by Learning Clause Guidance (Short Paper). ⋮ HOL(y)Hammer: online ATP service for HOL Light ⋮ TacticToe: learning to prove with tactics ⋮ Machine learning guidance for connection tableaux ⋮ The Isabelle/Naproche natural language proof assistant ⋮ Mizar ⋮ Semantics of Mizar as an Isabelle object logic ⋮ Mining State-Based Models from Proof Corpora ⋮ Developing Corpus-Based Translation Methods between Informal and Formal Mathematics: Project Description ⋮ SAT-Enhanced Mizar Proof Checking
Uses Software
Cites Work
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- MPTP-motivation, implementation, first experiments
- MPTP 0.2: Design, implementation, and initial experiments
- ATP and presentation service for Mizar formalizations
- HOL(y)Hammer: online ATP service for HOL Light
- Learning-assisted automated reasoning with \(\mathsf{Flyspeck}\)
- Premise selection for mathematics by corpus analysis and kernel methods
- Automated Reasoning Service for HOL Light
- Automated and Human Proofs in General Mathematics: An Initial Comparison
- Overview and Evaluation of Premise Selection Techniques for Large Theory Mathematics
- Lemmatization for Stronger Reasoning in Large Theories
- MaLARea SG1 - Machine Learner for Automated Reasoning with Semantic Guidance
- Theorem Proving in Large Formal Mathematics as an Emerging AI Field
- PRocH: Proof Reconstruction for HOL Light
- Sine Qua Non for Large Theory Reasoning
- MaSh: Machine Learning for Sledgehammer
This page was built for publication: MizAR 40 for Mizar 40
