Machine learning for quantifier selection in cvc5

DOI10.1016/J.IJAR.2025.109602MaRDI QIDQ6870125zbMATH OpenFDO

Authors Jan Jakubův, Mikoláš Janota, Jelle Piepenbrock, Josef Urban

Publication date 21 January 2026

Published in International Journal of Approximate Reasoning (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1016/J.IJAR.2025.109602

zbMATH Keywords

artificial intelligenceautomated theorem provingmachine learningsatisfiability modulo theories

Mathematics Subject Classification ID

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

Cites work

• \textsf{lazyCoP}: lazy paramodulation meets neurally guided search
• A Brief Overview of HOL4
• A Greedy Heuristic for the Set-Covering Problem
• A neurally-guided, parallel theorem prover
• An abstraction-refinement framework for reasoning with large theories
• Complete Instantiation for Quantified Formulas in Satisfiabiliby Modulo Theories
• Enhancing ENIGMA given clause guidance
• ENIGMA Anonymous: Symbol-Independent Inference Guiding Machine (System Description)
• ENIGMA: efficient learning-based inference guiding machine
• Fast and slow enigmas and parental guidance
• GRUNGE: a grand unified ATP challenge
• Hammering Mizar by Learning Clause Guidance (Short Paper).
• scientific article; zbMATH DE number 3639144 (Why is no real title available?)
• scientific article; zbMATH DE number 621810 (Why is no real title available?)
• scientific article; zbMATH DE number 1951640 (Why is no real title available?)
• scientific article; zbMATH DE number 234014 (Why is no real title available?)
• Learning guided automated reasoning: a brief survey
• Machine learning. A probabilistic perspective
• Mizar 60 for Mizar 50
• Model checking
• MPTP 0.2: Design, implementation, and initial experiments
• MPTP-motivation, implementation, first experiments
• Premise selection for mathematics by corpus analysis and kernel methods
• Quantifier instantiation techniques for finite model finding in SMT
• Regularization in Spider-style strategy discovery and schedule construction
• Revisiting enumerative instantiation
• Simplify: a theorem prover for program checking
• Solving hard Mizar problems with instantiation and strategy invention
• Solving quantified linear arithmetic by counterexample-guided instantiation
• Syntax-guided quantifier instantiation
• Targeted configuration of an SMT solver
• The CADE-22 automated theorem proving system competition -- CASC-22
• The Isabelle ENIGMA
• The role of the Mizar mathematical library for interactive proof development in Mizar
• The TPTP problem library
• Towards learning quantifier instantiation in SMT
• Vampire with a brain is a good ITP hammer

This page was built for publication: Machine learning for quantifier selection in cvc5

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