3 papers
cs.LO2026
Nonlinear Arithmetic with SMTLIB Division is Undecidable
Dejan Jovanovic
We show that the nonlinear real arithmetic theory (NRA) as defined in the SMTLIB standard is undecidable. The undecidability arises from the treatment of division by zero as an uni…
cs.CL2025
A Neurosymbolic Approach to Natural Language Formalization and Verification
Chenyang An, Sam Bayless, Stefano Buliani +27
Large Language Models perform well at natural language interpretation and reasoning, but their lack of formal correctness guarantees limits their adoption in regulated industries l…
cs.LO2021
Interpolation and Model Checking for Nonlinear Arithmetic
Dejan Jovanović, Bruno Dutertre
We present a new model-based interpolation procedure for satisfiability modulo theories (SMT). The procedure uses a new mode of interaction with the SMT solver that we call solving…