2 papers
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.LO2024
Symbolic Computation for All the Fun
Chad E. Brown, Mikoláš Janota, Mirek Olšák
Motivated by the recent 10 million dollar AIMO challenge, this paper targets the problem of finding all functions conforming to a given specification. This is a popular problem at…