Cover Image

SMT and Functional Equation Solving over the Reals: Challenges from the IMO

Fuente: arXiv

Saved in:

Bibliographic Details
Main Authors:	Brown, Chad E., Chvalovský, Karel, Janota, Mikoláš, Olšák, Mirek, Ratschan, Stefan
Format:	Preprint
Published:	2025
Subjects:	Logic in Computer Science
Online Access:	Acceder al recurso
Tags:	Add Tag No Tags, Be the first to tag this record!

Similar Items

LLM2SMT: Building an SMT Solver with Zero Human-Written Code
by: Janota, Mikoláš, et al.
Published: (2026)

Towards Learning Infinite SMT Models (Work in Progress)
by: Janota, Mikoláš, et al.
Published: (2025)

Symbolic Computation for All the Fun
by: Brown, Chad E., et al.
Published: (2024)

Inductive Satisfiability Certification for Universal Quantifiers and Uninterpreted Function Symbols
by: Ratschan, Stefan, et al.
Published: (2026)

Experimental Results for Vampire on the Equational Theories Project
by: Janota, Mikoláš
Published: (2025)

Applications of Quantified Constraint Solving over the Reals -- Bibliography
by: Ratschan, Stefan
Published: (2012)

Reintroducing the Second Player in EPR
by: Chew, Leroy, et al.
Published: (2026)

Deciding Predicate Logical Theories of Real-Valued Functions
by: Ratschan, Stefan
Published: (2023)

Case Study: Saturations as Explicit Models in Equational Theories
by: Janota, Mikoláš, et al.
Published: (2026)

Breaking Symmetries from a Set-Covering Perspective
by: Codish, Michael, et al.
Published: (2025)

Breaking Symmetries with Involutions
by: Codish, Michael, et al.
Published: (2025)

Efficient Solving of Quantified Inequality Constraints over the Real Numbers
by: Ratschan, Stefan
Published: (2002)

Quantifier Instantiations: To Mimic or To Revolt?
by: Jakubův, Jan, et al.
Published: (2025)

Solving Hard Mizar Problems with Instantiation and Strategy Invention
by: Jakubův, Jan, et al.
Published: (2024)

Breaking Symmetries in Quantified Graph Search: A Comparative Study
by: Janota, Mikoláš, et al.
Published: (2025)

From MBQI to Enumerative Instantiation and Back
by: Dančo, Marek, et al.
Published: (2025)

First Experiments with Neural cvc5
by: Piepenbrock, Jelle, et al.
Published: (2025)

Cube-based Isomorph-free Finite Model Finding
by: Chow, Choiwah, et al.
Published: (2025)

Regularization in Spider-Style Strategy Discovery and Schedule Construction
by: Bártek, Filip, et al.
Published: (2024)

Complete Symmetry Breaking for Finite Models
by: Dančo, Marek, et al.
Published: (2025)

Satisfiability of Non-Linear Transcendental Arithmetic as a Certificate Search Problem
by: Lipparini, Enrico, et al.
Published: (2023)

CFaults: Model-Based Diagnosis for Fault Localization in C Programs with Multiple Test Cases
by: Orvalho, Pedro, et al.
Published: (2024)

SAT-Based Techniques for Lexicographically Smallest Finite Models
by: Janota, Mikoláš, et al.
Published: (2025)

Towards Solving More Challenging IMO Problems via Decoupled Reasoning and Proving
by: Liang, Zhenwen, et al.
Published: (2025)

Machine Learning for Quantifier Selection in cvc5
by: Jakubův, Jan, et al.
Published: (2024)

Input-based Three-valued Abstraction Refinement
by: Onderka, Jan, et al.
Published: (2024)

Model-Based Diagnosis with Multiple Observations: A Unified Approach for C Software and Boolean Circuits
by: Orvalho, Pedro, et al.
Published: (2025)

SMT with Uninterpreted Functions and Monotonicity Constraints in Systems Biology
by: Huvar, Ondřej, et al.
Published: (2026)

Lean-SMT: An SMT tactic for discharging proof goals in Lean
by: Mohamed, Abdalrhman, et al.
Published: (2025)

SMT-Layout: A MaxSMT-based Approach Supporting Real-time Interaction of Real-world GUI Layout
by: Li, Bohan, et al.
Published: (2024)

Towards Automatic Linearization via SMT Solving
by: Cao, Jian, et al.
Published: (2024)

Efficient Volume Computation for SMT Formulas
by: Shaw, Arijit, et al.
Published: (2025)

An SMT Theory for n-Indexed Sequences
by: Hara, Hichem Rami Ait El, et al.
Published: (2024)

An SMT-LIB Theory of Finite Fields
by: Hader, Thomas, et al.
Published: (2024)

Hint-Based SMT Proof Reconstruction
by: Clune, Joshua, et al.
Published: (2026)

On SMT Theory Design: The Case of Sequences
by: Hara, Hichem Rami Ait El, et al.
Published: (2024)

A Formal Proof of R(4,5)=25
by: Gauthier, Thibault, et al.
Published: (2024)

Number theory combination: natural density and SMT
by: Toledo, Guilherme V., et al.
Published: (2025)

Integer Reasoning Modulo Different Constants in SMT
by: Pertseva, Elizaveta, et al.
Published: (2025)

Invariant Checking for SMT-based Systems with Quantifiers
by: Redondi, Gianluca, et al.
Published: (2024)