8 citations · 8 across the 5 of their papers we have counts for
Showing 2025 · cs.LOShow all
2 papers · 2 filters
cs.LO2025
SMT and Functional Equation Solving over the Reals: Challenges from the IMO
Chad E. Brown, Karel Chvalovský, Mikoláš Janota +2
We use SMT technology to address a class of problems involving uninterpreted functions and nonlinear real arithmetic. In particular, we focus on problems commonly found in mathemat…
cs.LO2025
Towards Learning Infinite SMT Models (Work in Progress)
Mikoláš Janota, Bartosz Piotrowski, Karel Chvalovský
This short paper proposes to learn models of satisfiability modulo theories (SMT) formulas during solving. Specifically, we focus on infinite models for problems in the logic of li…