MaLARea

swMATH10278MaRDI QIDQ22241FDOQ22241

Author name not available (Why is that?)

Official website: http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.83.5291

Cited In (only showing first 100 items - show all)

• A neurally-guided, parallel theorem prover
• GamePad
• Guiding high-performance SAT solvers with unsat-core predictions
• CVC4SY
• ATP Cross-Verification of the Mizar MPTP Challenge Problems
• The role of entropy in guiding a connection prover
• Machine learning guidance for connection tableaux
• TacticToe: learning to prove with tactics
• Premise selection in the Naproche system
• Automated reasoning in the wild
• HOList
• Learning2Reason
• Make E Smart Again (Short Paper)
• Prolog Technology Reinforcement Learning Prover
• Detecting inconsistencies in large first-order knowledge bases
• Large theory reasoning with SUMO at CASC
• Hammering Mizar by Learning Clause Guidance (Short Paper).
• 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
• 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
• Towards finding longer proofs
• 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
• ILTP
• MizarMode
• MPTP 0.2
• MoMM
• Mizar
• I-SATCHMO
• MML
• ML4PG
• MaLeCoP
• E-MaLeS 1.1
• MaSh
• ileanCoP
• DLog
• leanCoP
• E Theorem Prover
• Flyspeck
• PRocH
• SystemOnTPTP
• HOLyHammer
• SMTtoTPTP
• FOOL
• E-MaLeS
• SInE
• BliStr
• Tactician
• 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
• FALCON
• Automated and human proofs in general mathematics: an initial comparison
• Overview and evaluation of premise selection techniques for large theory mathematics
• BliStrTune
• QuickSpec
• SNARK
• FEMaLeCoP
• LogAnswer
• SEPIA
• SRASS
• Hierarchical invention of theorem proving strategies
• Theoryguru
• Seq2Seq
• DeepMath
• Naproche
• ATPboost
• ENIGMA
• Jinja not Java
• TacticToe
• Holophrasm
• Automated reasoning service for HOL Light
• AGES
• 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
• mizar-items
• 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
• lazyCoP
• 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)
• ATPboost: learning premise selection in binary setting with ATP feedback
• Enhancing ENIGMA given clause guidance
• Hammering towards QED

This page was built for software: MaLARea