Fast Reflexive Arithmetic Tactics the Linear Case and Beyond

DOI10.1007/978-3-540-74464-1_4MaRDI QIDQ3612435zbMATH OpenOpenAlexFDO

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

Mathematics Subject Classification ID

Mechanization of proofs and logical operations (03B35)

Recommendations

• Extensible and efficient automation through reflective tactics
• Proof synthesis and reflection for linear arithmetic
• Mtac: a monad for typed tactic programming in Coq
• A Coq tactic for equality learning in linear arithmetic
• Modular SMT proofs for fast reflexive checking inside Coq

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
• A Coq tactic for equality learning in linear arithmetic
• Pourchet’s theorem in action: decomposing univariate nonnegative polynomials as sums of five squares
• 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

Describes a project that uses

Uses Software

• CSDP
• Coq

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)