Heterogeneous heuristic optimisation and scheduling for first-order theorem proving

DOI10.1007/978-3-030-81097-9_8MaRDI QIDQ2128804zbMATH OpenOpenAlexFDO

Authors Edvard K. Holden, Konstantin Korovin

Publication date 22 April 2022

Full work available at URL https://doi.org/10.1007/978-3-030-81097-9_8

zbMATH Keywords

dynamic clusteringheuristic optimisationheuristic selectionmachine learningtheorem proving

Mathematics Subject Classification ID

Learning and adaptive systems in artificial intelligence (68T05) Problem solving in the context of artificial intelligence (heuristics, search strategies, etc.) (68T20) Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15)

Recommendations

• Bayesian ranking for strategy scheduling in automated theorem provers
• Using mixture of experts method in combining search-guiding heuristics for theorem proving
• Machine learning for first-order theorem proving
• Guiding an automated theorem prover with neural rewriting
• E-MaLeS 1.1

Cites work

• E-MaLeS 1.1
• Implementing Superposition in iProver (System Description)
• iProver – An Instantiation-Based Theorem Prover for First-Order Logic (System Description)
• Machine learning for first-order theorem proving
• MPTP 0.2: Design, implementation, and initial experiments
• SATzilla: portfolio-based algorithm selection for SAT
• System description: E 1.8
• The TPTP problem library and associated infrastructure. From CNF to TH0, TPTP v6.4.0

Cited in

(12)

• Ground joinability and connectedness in the superposition calculus
• Using mixture of experts method in combining search-guiding heuristics for theorem proving
• The CADE-28 Automated Theorem Proving System Competition – CASC-28
• Alien coding
• The 11th IJCAR automated theorem proving system competition – CASC-J11
• Targeted configuration of an SMT solver
• Fully reusing clause deduction algorithm based on standard contradiction separation rule
• Graph sequence learning for premise selection
• Learning guided automated reasoning: a brief survey
• Lemma discovery and strategies for automated induction
• Regularization in Spider-style strategy discovery and schedule construction
• A higher-order Vampire (short paper)

Describes a project that uses

Uses Software

• MPTP 0.2
• VAMPIRE
• SPASS
• TPTP
• SATzilla
• Sledgehammer
• iProver
• E Theorem Prover
• Easychair
• E-MaLeS
• BliStr
• BliStrTune
• XGBoost

This page was built for publication: Heterogeneous heuristic optimisation and scheduling for first-order theorem proving

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