Integrating external deduction tools with ACL2 (Q1006728): Difference between revisions

@@ Property / DOI @@
-.1016/j.jal.2007.07.002
@@ Property / DOI: 10.1016/j.jal.2007.07.002 / rank @@
-Normal rank
@@ Property / author @@
-J. Strother Moore
@@ Property / author: J. Strother Moore / rank @@
-Normal rank
@@ Property / author @@
+J. Strother Moore
@@ Property / author: J. Strother Moore / rank @@
+Normal rank
@@ Property / describes a project that uses @@
+SMT-LIB
@@ Property / describes a project that uses: SMT-LIB / rank @@
+Normal rank
@@ Property / describes a project that uses @@
+LISP
@@ Property / describes a project that uses: LISP / rank @@
+Normal rank
@@ Property / describes a project that uses @@
+Ivy
@@ Property / describes a project that uses: Ivy / rank @@
+Normal rank
@@ Property / describes a project that uses @@
+HOL90
@@ Property / describes a project that uses: HOL90 / rank @@
+Normal rank
@@ Property / describes a project that uses @@
+ACL2
@@ Property / describes a project that uses: ACL2 / rank @@
+Normal rank
@@ Property / describes a project that uses @@
+Chaff
@@ Property / describes a project that uses: Chaff / rank @@
+Normal rank
@@ Property / describes a project that uses @@
+PROSPER
@@ Property / describes a project that uses: PROSPER / rank @@
+Normal rank
@@ Property / MaRDI profile type @@
+Publication
@@ Property / MaRDI profile type: Publication / rank @@
+Normal rank
@@ Property / full work available at URL @@
+https://doi.org/10.1016/j.jal.2007.07.002
+Normal rank
@@ Property / OpenAlex ID @@
+W2024791001
@@ Property / OpenAlex ID: W2024791001 / rank @@
+Normal rank
@@ Property / cites work @@
+Integrating external deduction tools with ACL2
@@ Property / cites work: Integrating external deduction tools with ACL2 / rank @@
+Normal rank
@@ Property / cites work @@
+Interpolants and Symbolic Model Checking
@@ Property / cites work: Interpolants and Symbolic Model Checking / rank @@
+Normal rank
@@ Property / cites work @@
+A mechanically checked proof of the AMD5/sub K/86/sup TM/ floating-point division program
+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 @@
+Structured theory development for a mechanized logic
+Normal rank
@@ Property / cites work @@
+Q3932277
@@ Property / cites work: Q3932277 / rank @@
+Normal rank
@@ Property / cites work @@
+Q5573961
@@ Property / cites work: Q5573961 / rank @@
+Normal rank
@@ Property / cites work @@
+Automated Deduction – CADE-19
@@ Property / cites work: Automated Deduction – CADE-19 / rank @@
+Normal rank
@@ Property / cites work @@
+Q4016540
@@ Property / cites work: Q4016540 / rank @@
+Normal rank
@@ Property / cites work @@
+Formal Methods in Computer-Aided Design
@@ Property / cites work: Formal Methods in Computer-Aided Design / rank @@
+Normal rank
@@ Property / cites work @@
+Verification Condition Generation Via Theorem Proving
+Normal rank
@@ Property / cites work @@
+Q5287513
@@ Property / cites work: Q5287513 / rank @@
+Normal rank
@@ Property / cites work @@
+Isabelle/HOL. A proof assistant for higher-order logic
+Normal rank
@@ Property / cites work @@
+Q3997095
@@ Property / cites work: Q3997095 / rank @@
+Normal rank
@@ Property / cites work @@
+Meta Reasoning in ACL2
@@ Property / cites work: Meta Reasoning in ACL2 / rank @@
+Normal rank
@@ Property / cites work @@
+A SAT-Based Decision Procedure for the Subclass of Unrollable List Formulas in ACL2 (SULFA)
+Normal rank
@@ Property / cites work @@
+Correct Hardware Design and Verification Methods
@@ Property / cites work: Correct Hardware Design and Verification Methods / rank @@
+Normal rank
@@ Property / cites work @@
+Q4790648
@@ Property / cites work: Q4790648 / rank @@
+Normal rank
@@ Property / cites work @@
+Q2782479
@@ Property / cites work: Q2782479 / rank @@
+Normal rank
@@ Property / cites work @@
+Q2729073
@@ Property / cites work: Q2729073 / rank @@
+Normal rank
@@ Property / cites work @@
+Programming Combinations of Deduction and BDD-based Symbolic Calculation
+Normal rank
@@ Property / cites work @@
+Automated Reasoning
@@ Property / cites work: Automated Reasoning / rank @@
+Normal rank
@@ Property / cites work @@
+Q4809048
@@ Property / cites work: Q4809048 / rank @@
+Normal rank
@@ Property / DOI @@
+.1016/J.JAL.2007.07.002
@@ Property / DOI: 10.1016/J.JAL.2007.07.002 / rank @@
+Normal rank
@@ links / mardi / name / links / mardi / name @@
+Publication:1006728