Research paper and software
Quadarith
An investigation of formulation search for closed first-order formulas over the reals whose atomic relations are quadratic.
Current state
Jaewook Lee and I are developing a formulation-search calculus in which logical decompositions, exact reformulations, relaxations, witness checks, and complete decision procedures are expressed as verified rules. A search procedure looks for a finite derivation of a formula or its negation. Every accepted step is checked in exact arithmetic or by an independent checker, so the search policy affects which derivation is attempted without affecting the validity of a completed one. If the available search budget establishes neither side, then we report unknown. The current partial prototype includes Python modeling and solving components and a Lean tactic. The Python frontend is currently quantifier-free, and the APIs and certificate formats may change.
Future plans
We are continuing to develop the manuscript and the Python and Lean implementation. The code and paper are currently private. I will add public artifacts here when they are ready.
Details
- Phase
- Private pre-release
- Domain
- Quadratic reasoning · automated theorem proving · exact optimization
- My role
- Developer and coauthor
- With
- Jaewook Lee