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
• 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
• Guiding high-performance SAT solvers with unsat-core predictions
• 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
• Automated proof compression by invention of new definitions
• 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
• Machine learning for mathematical software
• Premise selection in the Naproche system
• E-MaLeS 1.1
• MizAR 40 for Mizar 40
• A learning-based fact selector for Isabelle/HOL
• Automated reasoning and presentation support for formalizing mathematics in MizAR
• Evaluation of automated theorem proving on the Mizar mathematical library
• Sine qua non for large theory reasoning
• Automated and human proofs in general mathematics: an initial comparison
• Overview and evaluation of premise selection techniques for large theory mathematics
• Hierarchical invention of theorem proving strategies
• Automated reasoning service for HOL Light
• Theorem proving in large formal mathematics as an emerging AI field
• Lemmatization for stronger reasoning in large theories
• ATP and presentation service for Mizar formalizations
• An abstraction-refinement framework for reasoning with large theories
• 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
• Automated reasoning in the wild
• Learning-assisted automated reasoning with \(\mathsf{Flyspeck}\)
• Premise selection for mathematics by corpus analysis and kernel methods
• MaLeCoP. Machine learning connection prover
• Proof-pattern recognition and lemma discovery in ACL2
• Mizar: state-of-the-art and beyond
• 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
• TacticToe: learning to reason with HOL4 tactics
• MaLARea SG1 - Machine Learner for Automated Reasoning with Semantic Guidance
• Large theory reasoning with SUMO at CASC

This page was built for software: MaLARea