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

machine learningtheorem provingdynamic clusteringheuristic optimisationheuristic selection

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)
• MPTP 0.2: Design, implementation, and initial experiments
• Machine learning for first-order theorem proving
• 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
• iProver – An Instantiation-Based Theorem Prover for First-Order Logic (System Description)

Cited in

(8)

• The CADE-28 Automated Theorem Proving System Competition – CASC-28
• Alien coding
• Using mixture of experts method in combining search-guiding heuristics for theorem proving
• Fully reusing clause deduction algorithm based on standard contradiction separation rule
• Graph sequence learning for premise selection
• Targeted configuration of an SMT solver
• Ground joinability and connectedness in the superposition calculus
• The 11th IJCAR automated theorem proving system competition – CASC-J11

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)