The role of entropy in guiding a connection prover
From MaRDI portal
Publication:2142077
DOI10.1007/978-3-030-86059-2_13OpenAlexW3201967611MaRDI QIDQ2142077
Miroslav Olšák, Josef Urban, Zsolt Zombori
Publication date: 25 May 2022
Full work available at URL: https://arxiv.org/abs/2105.14706
reinforcement learningmachine learningautomated theorem provingentropy regularizationgraph neural networksconnection calculus
Uses Software
Cites Work
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- MizAR 40 for Mizar 40
- Theorem proving in higher order logics. 21st international conference, TPHOLs 2008, Montreal, Canada, August 18--21, 2008. Proceedings
- IeanCOP: lean connection-based theorem proving
- A vision for automated deduction rooted in the connection method
- TacticToe: learning to prove with tactics
- Machine learning guidance for connection tableaux
- The Tactician. A seamless, interactive tactic learner and prover for Coq
- ENIGMA-NG: efficient neural and gradient-boosted inference guidance for \(\mathrm{E}\)
- Premise selection for mathematics by corpus analysis and kernel methods
- ENIGMA: efficient learning-based inference guiding machine
- System Description: E 1.8
- MaLeCoP Machine Learning Connection Prover
- FEMaLeCoP: Fairly Efficient Machine Learning Connection Prover
- leanCoP 2.0 and ileanCoP 1.2: High Performance Lean Theorem Proving in Classical and Intuitionistic Logic (System Descriptions)
- MaLARea SG1 - Machine Learner for Automated Reasoning with Semantic Guidance
- A Brief Overview of HOL4
- The Isabelle Framework
- Deep Network Guided Proof Search
- TacticToe: Learning to Reason with HOL4 Tactics
- ENIGMA Anonymous: Symbol-Independent Inference Guiding Machine (System Description)
- Prolog Technology Reinforcement Learning Prover
This page was built for publication: The role of entropy in guiding a connection prover
