Fast Reflexive Arithmetic Tactics the Linear Case and Beyond
From MaRDI portal
Publication:3612435
DOI10.1007/978-3-540-74464-1_4zbMATH Open1178.03020OpenAlexW1753642991MaRDI QIDQ3612435FDOQ3612435
Authors: 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
Recommendations
Cited In (18)
- Formal Proofs for Nonlinear Optimization
- 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
- Towards a scalable proof engine: a performant Prototype rewriting primitive for Coq
- A formal proof of the irrationality of \(\zeta(3)\)
- Ready, set, verify! Applying hs-to-coq to real-world Haskell code
- Modular SMT proofs for fast reflexive checking inside Coq
- Pourchet’s theorem in action: decomposing univariate nonnegative polynomials as sums of five squares
- A Coq tactic for equality learning in linear arithmetic
- Tactics for Reasoning Modulo AC in Coq
- A bi-directional extensible interface between Lean and Mathematica
- Formalizing the Face Lattice of Polyhedra
- On the Generation of Positivstellensatz Witnesses in Degenerate Cases
- A Modular Integration of SAT/SMT Solvers to Coq through Proof Witnesses
- Extensible and efficient automation through reflective tactics
- Coquelicot: a user-friendly library of real analysis for Coq
- A Short Presentation of Coq
Uses Software
This page was built for publication: Fast Reflexive Arithmetic Tactics the Linear Case and Beyond
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q3612435)
