A mathematical benchmark for inductive theorem provers

DOI10.29007/JR72MaRDI QIDQ7025217zbMATH OpenFDO

Authors T. Gauthier, Chad E. Brown, Mikoláš Janota, Josef Urban

Publication date 19 February 2025

Full work available at URL https://doi.org/10.29007/JR72

zbMATH Keywords

arithmeticautomated theorem proversbenchmarkinductioninductive theorem proversoeis

Mathematics Subject Classification ID

Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15)

Cites work

• A tale of two set theories
• Alien coding
• Automating Inductive Proofs Using Theory Exploration
• Cooperating techniques for solving nonlinear real arithmetic in the \texttt{cvc5} SMT solver (system description)
• Deep reinforcement learning for synthesizing functions in higher-order logic
• Dynamic rippling, middle-out reasoning and lemma discovery
• First neural conjecturing datasets and experiments
• Induction for SMT solvers
• Inductive benchmarks for automated reasoning
• Integer induction in saturation
• The On-Line Encyclopedia of Integer Sequences
• TIP: tons of inductive problems
• Tree neural networks in HOL4

Cited in

(2)

• Artificial intelligence and inherent mathematical difficulty
• Learning conjecturing from scratch

This page was built for publication: A mathematical benchmark for inductive theorem provers

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