Automating Induction with an SMT Solver (Q2891425): Difference between revisions

@@ Property / describes a project that uses @@
+Boogie
@@ Property / describes a project that uses: Boogie / rank @@
+Normal rank
@@ Property / describes a project that uses @@
+ACL2s
@@ Property / describes a project that uses: ACL2s / rank @@
+Normal rank
@@ Property / describes a project that uses @@
+Zeno
@@ Property / describes a project that uses: Zeno / rank @@
+Normal rank
@@ Property / describes a project that uses @@
+KRAKATOA
@@ Property / describes a project that uses: KRAKATOA / rank @@
+Normal rank
@@ Property / describes a project that uses @@
+Caduceus
@@ Property / describes a project that uses: Caduceus / rank @@
+Normal rank
@@ Property / describes a project that uses @@
+z3
@@ Property / describes a project that uses: z3 / rank @@
+Normal rank
@@ Property / describes a project that uses @@
+Sledgehammer
@@ Property / describes a project that uses: Sledgehammer / rank @@
+Normal rank
@@ Property / describes a project that uses @@
+VeriFun
@@ Property / describes a project that uses: VeriFun / rank @@
+Normal rank
@@ Property / describes a project that uses @@
+ACL2
@@ Property / describes a project that uses: ACL2 / rank @@
+Normal rank
@@ Property / MaRDI profile type @@
+MaRDI publication profile
@@ Property / MaRDI profile type: MaRDI publication profile / rank @@
+Normal rank
@@ Property / full work available at URL @@
+https://doi.org/10.1007/978-3-642-27940-9_21
+Normal rank
@@ Property / OpenAlex ID @@
+W1831545713
@@ Property / OpenAlex ID: W1831545713 / rank @@
+Normal rank
@@ Property / cites work @@
+Refinement Calculus
@@ Property / cites work: Refinement Calculus / 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 @@
+Sledgehammer: Judgement Day
@@ Property / cites work: Sledgehammer: Judgement Day / rank @@
+Normal rank
@@ Property / cites work @@
+Rippling: Meta-Level Guidance for Mathematical Reasoning
+Normal rank
@@ Property / cites work @@
+The ACL2 Sedan Theorem Proving System
@@ Property / cites work: The ACL2 Sedan Theorem Proving System / rank @@
+Normal rank
@@ Property / cites work @@
+Simplify: a theorem prover for program checking
@@ Property / cites work: Simplify: a theorem prover for program checking / rank @@
+Normal rank
@@ Property / cites work @@
+Case-Analysis for Rippling and Inductive Proof
@@ Property / cites work: Case-Analysis for Rippling and Inductive Proof / rank @@
+Normal rank
@@ Property / cites work @@
+Q5585021
@@ Property / cites work: Q5585021 / rank @@
+Normal rank
@@ Property / cites work @@
+Dafny: An Automatic Program Verifier for Functional Correctness
+Normal rank
@@ Property / cites work @@
+A Polymorphic Intermediate Verification Language: Design and Logical Encoding
+Normal rank
@@ Property / cites work @@
+Solving SAT and SAT Modulo Theories
@@ Property / cites work: Solving SAT and SAT Modulo Theories / rank @@
+Normal rank
@@ Property / cites work @@
+Zeno: An Automated Prover for Properties of Recursive Data Structures
+Normal rank