Showing cs.AIShow all
3 papers · 1 filter
cs.AI2025
Machine Learning for Quantifier Selection in cvc5
Jan Jakubův, Mikoláš Janota, Jelle Piepenbrock +1
In this work we considerably improve the state-of-the-art SMT solving on first-order quantified problems by efficient machine learning guidance of quantifier selection. Quantifiers…
cs.AI2025
Quantifier Instantiations: To Mimic or To Revolt?
Jan Jakubův, Mikoláš Janota
Quantified formulas pose a significant challenge for Satisfiability Modulo Theories (SMT) solvers due to their inherent undecidability. Existing instantiation techniques, such as e…
cs.AI2024
Solving Hard Mizar Problems with Instantiation and Strategy Invention
Jan Jakubův, Mikoláš Janota, Josef Urban
In this work, we prove over 3000 previously ATP-unproved Mizar/MPTP problems by using several ATP and AI methods, raising the number of ATP-solved Mizar problems from 75\% to above…