Heterogeneous heuristic optimisation and scheduling for first-order theorem proving

DOI10.1007/978-3-030-81097-9_8zbMath1485.68282OpenAlexW3185228372MaRDI QIDQ2128804

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

theorem provingmachine learningdynamic 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)

Related Items (5)

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 ⋮ Ground joinability and connectedness in the superposition calculus

Uses Software

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

Cites Work

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

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