Milestones from the Pure Lisp Theorem Prover to ACL2 (Q2280212): Difference between revisions

@@ 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/s00165-019-00490-3
+Normal rank
@@ Property / OpenAlex ID @@
+W2964806919
@@ Property / OpenAlex ID: W2964806919 / rank @@
+Normal rank
@@ Property / cites work @@
+A man-machine theorem-proving system
@@ Property / cites work: A man-machine theorem-proving system / rank @@
+Normal rank
@@ Property / cites work @@
+Q4016540
@@ Property / cites work: Q4016540 / rank @@
+Normal rank
@@ Property / cites work @@
+Splitting and reduction heuristics in automatic theorem proving
+Normal rank
@@ Property / cites work @@
+Q5663380
@@ Property / cites work: Q5663380 / rank @@
+Normal rank
@@ Property / cites work @@
+Proving Theorems about LISP Functions
@@ Property / cites work: Proving Theorems about LISP Functions / rank @@
+Normal rank
@@ Property / cites work @@
+A fast string searching algorithm
@@ Property / cites work: A fast string searching algorithm / rank @@
+Normal rank
@@ Property / cites work @@
+Q3894958
@@ Property / cites work: Q3894958 / rank @@
+Normal rank
@@ Property / cites work @@
+Q3932277
@@ Property / cites work: Q3932277 / rank @@
+Normal rank
@@ Property / cites work @@
+The addition of bounded quantification and partial functions to a computational logic and its theorem prover
+Normal rank
@@ Property / cites work @@
+Q4040283
@@ Property / cites work: Q4040283 / rank @@
+Normal rank
@@ Property / cites work @@
+Q3835049
@@ Property / cites work: Q3835049 / rank @@
+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 @@
+Efficient certified RAT verification
@@ Property / cites work: Efficient certified RAT verification / rank @@
+Normal rank
@@ Property / cites work @@
+The reflective Milawa theorem prover is sound (down to the machine code that runs it)
+Normal rank
@@ Property / cites work @@
+Q5610986
@@ Property / cites work: Q5610986 / rank @@
+Normal rank
@@ Property / cites work @@
+Q5287513
@@ Property / cites work: Q5287513 / rank @@
+Normal rank
@@ Property / cites work @@
+Q2754047
@@ Property / cites work: Q2754047 / rank @@
+Normal rank
@@ Property / cites work @@
+Efficient, verified checking of propositional proofs
+Normal rank
@@ Property / cites work @@
+An extension of the Boyer-Moore theorem prover to support first-order quantification
+Normal rank
@@ Property / cites work @@
+Q5670164
@@ Property / cites work: Q5670164 / rank @@
+Normal rank
@@ Property / cites work @@
+Linear resolution with selection function
@@ Property / cites work: Linear resolution with selection function / rank @@
+Normal rank
@@ Property / cites work @@
+Limited second-order functionality in a first-order setting
+Normal rank
@@ Property / cites work @@
+Q3154457
@@ Property / cites work: Q3154457 / rank @@
+Normal rank
@@ Property / cites work @@
+Q5601829
@@ Property / cites work: Q5601829 / rank @@
+Normal rank
@@ Property / cites work @@
+Q3857731
@@ Property / cites work: Q3857731 / rank @@
+Normal rank
@@ Property / cites work @@
+Automated Deduction – CADE-19
@@ Property / cites work: Automated Deduction – CADE-19 / rank @@
+Normal rank
@@ Property / cites work @@
+Simplification by Cooperating Decision Procedures
@@ Property / cites work: Simplification by Cooperating Decision Procedures / rank @@
+Normal rank
@@ Property / cites work @@
+Isabelle/HOL. A proof assistant for higher-order logic
+Normal rank
@@ Property / cites work @@
+A Machine-Oriented Logic Based on the Resolution Principle
+Normal rank
@@ Property / cites work @@
+A Practical Decision Procedure for Arithmetic with Function Symbols
+Normal rank
@@ Property / cites work @@
+Toward Mechanical Mathematics
@@ Property / cites work: Toward Mechanical Mathematics / rank @@
+Normal rank
@@ Property / cites work @@
+Prolegomena to a theory of mechanized formal reasoning
+Normal rank