Fast Reflexive Arithmetic Tactics the Linear Case and Beyond
From MaRDI portal
Publication:3612435
DOI10.1007/978-3-540-74464-1_4zbMath1178.03020OpenAlexW1753642991MaRDI QIDQ3612435
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
Related Items
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
