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
Related Items
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
