Hierarchical invention of theorem proving strategies

DOI10.3233/AIC-180761zbMath1462.68213arXiv1611.08733MaRDI QIDQ5145434

Jan Jakubův, Josef Urban

Publication date: 20 January 2021

Published in: AI Communications (Search for Journal in Brave)

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

zbMATH Keywords

automated theorem provingparameter learningclause weight functionsproof search heuristics

Mathematics Subject Classification ID

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 (9)

Fast and slow enigmas and parental guidance ⋮ Make E Smart Again (Short Paper) ⋮ Learning theorem proving components ⋮ Alien coding ⋮ Targeted configuration of an SMT solver ⋮ Relaxed weighted path order in theorem proving ⋮ ENIGMA-NG: efficient neural and gradient-boosted inference guidance for \(\mathrm{E}\) ⋮ BliStrTune ⋮ The 10th IJCAR automated theorem proving system competition – CASC-J10

Uses Software

• MPTP
• OTTER
• E Theorem Prover
• Flyspeck
• MaLARea
• Easychair
• E-MaLeS
• BliStr
• GNU parallel

Cites Work

• MaLeS: a framework for automatic tuning of automated theorem provers
• MizAR 40 for Mizar 40
• A learning-based fact selector for Isabelle/HOL
• MPTP-motivation, implementation, first experiments
• MPTP 0.2: Design, implementation, and initial experiments
• Premise selection for mathematics by corpus analysis and kernel methods
• Bayesian Optimization in a Billion Dimensions via Random Embeddings
• ParamILS: An Automatic Algorithm Configuration Framework
• Hammering towards QED
• Sine Qua Non for Large Theory Reasoning

This page was built for publication: Hierarchical invention of theorem proving strategies