21 citations · 22 across the 3 of their papers we have counts for
5 papers · 1 filter
Vibe-Coded and Tuned: A State-of-the-Art SMT Solver for QF-LRA
Mikoláš Janota, Jan Jakubův
This paper presents the SMT solver primo, which is fully vibe-coded and then parameter-tuned, achieving state-of-the-art results on linear real arithmetic (QF-LRA). The performance…
First Experiments with Neural cvc5
Jelle Piepenbrock, Mikoláš Janota, Jan Jakubův
he cvc5 solver is today one of the strongest systems for solving first order problems with theories but also without them. In this work we equip its enumeration-based instantiation…
Automated Strategy Invention for Confluence of Term Rewrite Systems
Liao Zhang, Fabian Mitterwallner, Jan Jakubuv +1
Term rewriting plays a crucial role in software verification and compiler optimization. With dozens of highly parameterizable techniques developed to prove various system propertie…
Learning Theorem Proving Components
Karel Chvalovský, Jan Jakubův, Miroslav Olšák +1
Saturation-style automated theorem provers (ATPs) based on the given clause procedure are today the strongest general reasoners for classical first-order logic. The clause selectio…
Extending E Prover with Similarity Based Clause Selection Strategies
Jan Jakubův, Josef Urban
E prover is a state-of-the-art theorem prover for first-order logic with equality. E prover is built around a saturation loop, where new clauses are derived by inference rules from…