Hammering Floating-Point Arithmetic (Q6496632): Difference between revisions

@@ Property / cites work @@
+A Modular Integration of SAT/SMT Solvers to Coq through Proof Witnesses
+Normal rank
@@ Property / cites work @@
+Mizar: State-of-the-art and Beyond
@@ Property / cites work: Mizar: State-of-the-art and Beyond / rank @@
+Normal rank
@@ Property / cites work @@
+Extending SMT solvers to higher-order logic
@@ Property / cites work: Extending SMT solvers to higher-order logic / rank @@
+Normal rank
@@ Property / cites work @@
+A formally verified, optimized monitor for metric first-order dynamic logic
+Normal rank
@@ Property / cites work @@
+Superposition for higher-order logic
@@ Property / cites work: Superposition for higher-order logic / rank @@
+Normal rank
@@ Property / cites work @@
+Interactive theorem proving and program development. Coq'Art: the calculus of inductive constructions. Foreword by Gérard Huet and Christine Paulin-Mohring.
+Normal rank
@@ Property / cites work @@
+Extending Sledgehammer with SMT solvers
@@ Property / cites work: Extending Sledgehammer with SMT solvers / rank @@
+Normal rank
@@ Property / cites work @@
+Fast LCF-Style Proof Reconstruction for Z3
@@ Property / cites work: Fast LCF-Style Proof Reconstruction for Z3 / rank @@
+Normal rank
@@ Property / cites work @@
+Automating the verification of floating-point programs
+Normal rank
@@ Property / cites work @@
+Formal Methods for Hardware Verification
@@ Property / cites work: Formal Methods for Hardware Verification / rank @@
+Normal rank
@@ Property / cites work @@
+A Skeptic's approach to combining HOL and Maple
@@ Property / cites work: A Skeptic's approach to combining HOL and Maple / rank @@
+Normal rank
@@ Property / cites work @@
+Lifting and Transfer: A Modular Design for Quotients in Isabelle/HOL
+Normal rank
@@ Property / cites work @@
+HOL(y)Hammer: online ATP service for HOL Light
@@ Property / cites work: HOL(y)Hammer: online ATP service for HOL Light / rank @@
+Normal rank
@@ Property / cites work @@
+Lightweight relevance filtering for machine-generated resolution problems
+Normal rank
@@ Property / cites work @@
+Handbook of Floating-Point Arithmetic
@@ Property / cites work: Handbook of Floating-Point Arithmetic / rank @@
+Normal rank
@@ Property / cites work @@
+Towards satisfiability modulo parametric bit-vectors
+Normal rank
@@ Property / cites work @@
+Proceedings Thirteenth International Workshop on the ACL2 Theorem Prover and Its Applications
+Normal rank
@@ Property / cites work @@
+Q3150300
@@ Property / cites work: Q3150300 / rank @@
+Normal rank
@@ Property / cites work @@
+A Mechanically Checked Proof of IEEE Compliance of the Floating Point Multiplication, Division and Square Root Algorithms of the AMD-K7<sup>™</sup> Processor
+Normal rank
@@ Property / cites work @@
+Faster, higher, stronger: E 2.3
@@ Property / cites work: Faster, higher, stronger: E 2.3 / rank @@
+Normal rank
@@ Property / cites work @@
+A Brief Overview of HOL4
@@ Property / cites work: A Brief Overview of HOL4 / rank @@
+Normal rank
@@ Property / cites work @@
+ATP and presentation service for Mizar formalizations
+Normal rank
@@ Property / cites work @@
+Q2751379
@@ Property / cites work: Q2751379 / rank @@
+Normal rank