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
