2 papers
cs.LO2026
Inductive Satisfiability Certification for Universal Quantifiers and Uninterpreted Function Symbols
Stefan Ratschan, Anggha Nugraha, Mikoláš Janota +1
The combination of uninterpreted function symbols and universal quantification occurs in many applications of automated reasoning, for example, due to their ability to reason about…
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…