13 citations · 19 across the 5 of their papers we have counts for
Showing cs.LOShow all
3 papers · 1 filter
cs.LO2023
Arithmetic as a theory modulo
Gilles Dowek, Benjamin Werner
We present constructive arithmetic in Deduction modulo with rewrite rules only.
cs.LO2023★ 1 cited
A constructive proof of Skolem theorem for constructive logic
Gilles Dowek, Benjamin Werner
If the sequent (Gamma entails forall x exists y A) is provable in first order constructive natural deduction, then the theory (Gamma, forall x (f (x)/y)A), where f is a new functio…
cs.LO2014★ 13 cited
Formal Proofs for Nonlinear Optimization
Victor Magron, Xavier Allamigeon, Stéphane Gaubert +1
We present a formally verified global optimization framework. Given a semialgebraic or transcendental function and a compact semialgebraic domain , we use the nonlinear maxp…