Fast Reflexive Arithmetic Tactics the Linear Case and Beyond

DOI10.1007/978-3-540-74464-1_4zbMath1178.03020OpenAlexW1753642991MaRDI QIDQ3612435

Frédéric Besson

Publication date: 10 March 2009

Published in: Lecture Notes in Computer Science (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/978-3-540-74464-1_4

Mathematics Subject Classification ID

Mechanization of proofs and logical operations (03B35)

Related Items (17)

Formalizing the Face Lattice of Polyhedra ⋮ Sharper and Simpler Nonlinear Interpolants for Program Verification ⋮ Distant decimals of \(\pi \): formal proofs of some algorithms computing them and guarantees of exact computation ⋮ Unnamed Item ⋮ A bi-directional extensible interface between Lean and Mathematica ⋮ Pourchet’s theorem in action: decomposing univariate nonnegative polynomials as sums of five squares ⋮ A Short Presentation of Coq ⋮ Coquelicot: a user-friendly library of real analysis for Coq ⋮ A formalization of convex polyhedra based on the simplex method ⋮ Unnamed Item ⋮ Extensible and Efficient Automation Through Reflective Tactics ⋮ On the Generation of Positivstellensatz Witnesses in Degenerate Cases ⋮ A Modular Integration of SAT/SMT Solvers to Coq through Proof Witnesses ⋮ Modular SMT Proofs for Fast Reflexive Checking Inside Coq ⋮ Tactics for Reasoning Modulo AC in Coq ⋮ Ready,Set, Verify! Applyinghs-to-coqto real-world Haskell code ⋮ Formal Proofs for Nonlinear Optimization

Uses Software

• Coq
• CSDP

This page was built for publication: Fast Reflexive Arithmetic Tactics the Linear Case and Beyond