Heterogeneous heuristic optimisation and scheduling for first-order theorem proving

DOI10.1007/978-3-030-81097-9_8zbMATH Open1485.68282OpenAlexW3185228372MaRDI QIDQ2128804FDOQ2128804

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

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

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)

Cites Work

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

Cited In (7)

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

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)