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…