MaLARea

swMATH10278MaRDI QIDQ22241FDOQ22241

Author name not available (Why is that?)

Cited In (55)

• Learning2Reason
• Hammering Mizar by Learning Clause Guidance (Short Paper).
• A neurally-guided, parallel theorem prover
• Automated Reasoning in the Wild
• Machine learning for first-order theorem proving
• The TPTP problem library and associated infrastructure and associated infrastructure. The FOF and CNF parts, v3.5.0
• ATP-based cross-verification of Mizar proofs: method, systems, and first experiments
• Proof-Pattern Recognition and Lemma Discovery in ACL2
• MaLeCoP Machine Learning Connection Prover
• Guiding high-performance SAT solvers with unsat-core predictions
• Theorem Proving in Large Formal Mathematics as an Emerging AI Field
• Lemma Mining over HOL Light
• Comparing machine learning models to choose the variable ordering for cylindrical algebraic decomposition
• The TPTP problem library and associated infrastructure. From CNF to TH0, TPTP v6.4.0
• Mizar: State-of-the-art and Beyond
• Sine Qua Non for Large Theory Reasoning
• Premise Selection in the Naproche System
• Evaluation of Automated Theorem Proving on the Mizar Mathematical Library
• ATP Cross-Verification of the Mizar MPTP Challenge Problems
• The role of entropy in guiding a connection prover
• Towards finding longer proofs
• Machine learning guidance for connection tableaux
• TacticToe: learning to prove with tactics
• ENIGMA-NG: efficient neural and gradient-boosted inference guidance for \(\mathrm{E}\)
• ENIGMA: efficient learning-based inference guiding machine
• Automated reasoning. 4th international joint conference, IJCAR 2008, Sydney, Australia, August 12--15, 2008 Proceedings
• Automated verification of refinement laws
• TacticToe: Learning to Reason with HOL4 Tactics
• Machine learning for mathematical software
• E-MaLeS 1.1
• MizAR 40 for Mizar 40
• A learning-based fact selector for Isabelle/HOL
• Hierarchical invention of theorem proving strategies
• ATP and presentation service for Mizar formalizations
• An abstraction-refinement framework for reasoning with large theories
• Automated Proof Compression by Invention of New Definitions
• HOL(y)Hammer: online ATP service for HOL Light
• Learning-assisted theorem proving with millions of lemmas
• Improved Cross-Validation for Classifiers that Make Algorithmic Choices to Minimise Runtime Without Compromising Output Correctness
• 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
• ENIGMA Anonymous: Symbol-Independent Inference Guiding Machine (System Description)
• Make E Smart Again (Short Paper)
• Prolog Technology Reinforcement Learning Prover
• ATPboost: learning premise selection in binary setting with ATP feedback
• Enhancing ENIGMA given clause guidance
• Hammering towards QED
• Detecting inconsistencies in large first-order knowledge bases
• MaLARea SG1 - Machine Learner for Automated Reasoning with Semantic Guidance
• Automated Reasoning and Presentation Support for Formalizing Mathematics in Mizar
• Large theory reasoning with SUMO at CASC

This page was built for software: MaLARea