Fast and slow enigmas and parental guidance

DOI10.1007/978-3-030-86205-3_10OpenAlexW3203893060MaRDI QIDQ831937

Miroslav Olšák, Zarathustra A. Goertzel, Josef Urban, Karel Chvalovský, Jan Jakubův

Publication date: 24 March 2022

Full work available at URL: https://arxiv.org/abs/2107.06750

Mathematics Subject Classification ID

Artificial intelligence (68Txx)

Uses Software

• MPTP 0.2
• VAMPIRE
• LIBLINEAR
• MaLeCoP
• E Theorem Prover
• Easychair
• randoCoP
• TensorFlow
• BliStr
• BliStrTune
• Waldmeister
• XGBoost
• Proofwatch
• ENIGMA

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• MizAR 40 for Mizar 40
• Experiments with discrimination-tree indexing and path indexing for term retrieval
• MPTP 0.2: Design, implementation, and initial experiments
• ProofWatch: watchlist guidance for large theories in E
• Enhancing ENIGMA given clause guidance
• The anatomy of vampire. Implementing bottom-up procedures with code trees
• Using hints to increase the effectiveness of an automated reasoning program: Case studies
• ENIGMAWatch: ProofWatch meets ENIGMA
• ENIGMA-NG: efficient neural and gradient-boosted inference guidance for \(\mathrm{E}\)
• Faster, higher, stronger: E 2.3
• ENIGMA: efficient learning-based inference guiding machine
• System Description: E 1.8
• Fingerprint Indexing for Paramodulation and Rewriting
• MaLeCoP Machine Learning Connection Prover
• Efficient Low-Level Connection Tableaux
• The CADE-25 Automated Theorem Proving system competition – CASC-25
• Deep Network Guided Proof Search
• A New Class of Automated Theorem-Proving Algorithms
• Loops with Abelian Inner Mapping Groups: An Application of Automated Deduction
• Citius altius fortius
• ENIGMA Anonymous: Symbol-Independent Inference Guiding Machine (System Description)
• Hierarchical invention of theorem proving strategies

This page was built for publication: Fast and slow enigmas and parental guidance