Enhancing ENIGMA given clause guidance

DOI10.1007/978-3-319-96812-4_11MaRDI QIDQ1798957zbMATH OpenOpenAlexFDO

Authors Jan Jakubův, Josef Urban

Publication date 18 October 2018

Full work available at URL https://zenodo.org/record/4515348

Mathematics Subject Classification ID

Recommendations

• ENIGMA: efficient learning-based inference guiding machine
• ENIGMAWatch: ProofWatch meets ENIGMA
• Internal guidance for Satallax
• Guiding an automated theorem prover with neural rewriting
• Extending E prover with similarity based clause selection strategies

Cited in

(12)

• Internal guidance for Satallax
• ENIGMA: efficient learning-based inference guiding machine
• Fast and slow enigmas and parental guidance
• Vampire with a brain is a good ITP hammer
• Improving ENIGMA-style clause selection while learning from history
• The CADE-27 automated theorem proving system competition -- CASC-27
• ENIGMAWatch: ProofWatch meets ENIGMA
• Hammering Mizar by Learning Clause Guidance (Short Paper).
• ENIGMA-NG: efficient neural and gradient-boosted inference guidance for \(\mathrm{E}\)
• ENIGMA
• Make E Smart Again (Short Paper)
• ENIGMA Anonymous: Symbol-Independent Inference Guiding Machine (System Description)

Describes a project that uses

Uses Software

• LIBLINEAR
• E Theorem Prover
• MaLARea

This page was built for publication: Enhancing ENIGMA given clause guidance

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q1798957)