MaLARea
From MaRDI portal
Cited in
(only showing first 100 items - show all)- Automated verification of refinement laws
- ILTP
- mizar-items
- lazyCoP
- MizarMode
- MPTP
- MPTP 0.2
- VAMPIRE
- Metis
- Machine learning for mathematical software
- MoMM
- Mizar
- The TPTP problem library and associated infrastructure. From CNF to TH0, TPTP v6.4.0
- Enhancing ENIGMA given clause guidance
- ATPboost: learning premise selection in binary setting with ATP feedback
- An abstraction-refinement framework for reasoning with large theories
- I-SATCHMO
- MML
- ML4PG
- MaLeCoP
- ATP and presentation service for Mizar formalizations
- HOL(y)Hammer: online ATP service for HOL Light
- MaSh
- TacticToe: learning to prove with tactics
- Machine learning guidance for connection tableaux
- Towards finding longer proofs
- The role of entropy in guiding a connection prover
- leanCoP
- ileanCoP
- A neurally-guided, parallel theorem prover
- DLog
- Guiding high-performance SAT solvers with unsat-core predictions
- E Theorem Prover
- PRocH
- Flyspeck
- SystemOnTPTP
- Comparing machine learning models to choose the variable ordering for cylindrical algebraic decomposition
- ENIGMA-NG: efficient neural and gradient-boosted inference guidance for \(\mathrm{E}\)
- HOLyHammer
- Machine learning for first-order theorem proving
- Learning-assisted automated reasoning with \(\mathsf{Flyspeck}\)
- Premise selection for mathematics by corpus analysis and kernel methods
- ENIGMA: efficient learning-based inference guiding machine
- Detecting inconsistencies in large first-order knowledge bases
- SMTtoTPTP
- FOOL
- The TPTP problem library and associated infrastructure and associated infrastructure. The FOF and CNF parts, v3.5.0
- E-MaLeS
- SInE
- Automated reasoning service for HOL Light
- MizAR 40 for Mizar 40
- BliStr
- Proof-pattern recognition and lemma discovery in ACL2
- Lemma Mining over HOL Light
- Automated and human proofs in general mathematics: an initial comparison
- Overview and evaluation of premise selection techniques for large theory mathematics
- Tactician
- Lemmatization for stronger reasoning in large theories
- MaLeCoP. Machine learning connection prover
- BliStrTune
- Automated proof compression by invention of new definitions
- QuickSpec
- SNARK
- FEMaLeCoP
- FALCON
- A learning-based fact selector for Isabelle/HOL
- LogAnswer
- SRASS
- SEPIA
- Mizar: state-of-the-art and beyond
- Automated reasoning in the wild
- ATP Cross-Verification of the Mizar MPTP Challenge Problems
- MaLARea SG1 - Machine Learner for Automated Reasoning with Semantic Guidance
- Large theory reasoning with SUMO at CASC
- Automated reasoning and presentation support for formalizing mathematics in MizAR
- Theoryguru
- Seq2Seq
- DeepMath
- Naproche
- ATPboost
- TacticToe
- ENIGMA
- Jinja not Java
- Holophrasm
- AGES
- TacticToe: learning to reason with HOL4 tactics
- Learning-assisted theorem proving with millions of lemmas
- Theorem proving in large formal mathematics as an emerging AI field
- E-MaLeS 1.1
- Improved Cross-Validation for Classifiers that Make Algorithmic Choices to Minimise Runtime Without Compromising Output Correctness
- Make E Smart Again (Short Paper)
- ENIGMA Anonymous: Symbol-Independent Inference Guiding Machine (System Description)
- Prolog Technology Reinforcement Learning Prover
- Hierarchical invention of theorem proving strategies
- Hammering towards QED
- Sine qua non for large theory reasoning
- Learning2Reason
- Premise selection in the Naproche system
- Evaluation of automated theorem proving on the Mizar mathematical library
- Hammering Mizar by Learning Clause Guidance (Short Paper).
This page was built for software: MaLARea
