The following pages link to ACL2 (Q12833):
Displaying 50 items.
- (Q4790655) (← links)
- (Q4790667) (← links)
- (Q4790668) (← links)
- (Q4808727) (← links)
- (Q4809071) (← links)
- (Q4817211) (← links)
- (Q4818805) (← links)
- Improving Real Analysis in Coq: A User-Friendly Approach to Integrals and Derivatives (Q4916067) (← links)
- Computation in Real Closed Infinitesimal and Transcendental Extensions of the Rationals (Q4928437) (← links)
- Verifying Refutations with Extended Resolution (Q4928451) (← links)
- An elementary linear-algebraic proof without computer-aided arguments for the group law on elliptic curves (Q5042554) (← links)
- The Imandra Automated Reasoning System (System Description) (Q5049029) (← links)
- Computer-Aided Verification for Iterative Matrix Inversion Problems in Systems and Control (Q5054245) (← links)
- A Nonstandard Functional Programming Language (Q5056008) (← links)
- Proceedings Seventeenth International Workshop on the ACL2 Theorem Prover and its Applications (Q5083764) (← links)
- Proceedings of the Sixteenth International Workshop on the ACL2 Theorem Prover and its Applications (Q5086891) (← links)
- (Q5088165) (← links)
- (Q5088166) (← links)
- (Q5088167) (← links)
- Proceedings Thirteenth International Workshop on the ACL2 Theorem Prover and Its Applications (Q5088168) (← links)
- (Q5088169) (← links)
- (Q5088170) (← links)
- Pollack-inconsistency (Q5170237) (← links)
- Verifying the bridge between simplicial topology and algebra: the Eilenberg-Zilber algorithm (Q5172125) (← links)
- Transforming Programs into Recursive Functions (Q5179363) (← links)
- On Trojan Horses of Thompson-Goerigk-Type, Their Generation, Intrusion, Detection and Prevention (Q5187821) (← links)
- Scalable Techniques for Formal Verification (Q5187984) (← links)
- Hammering towards QED (Q5195271) (← links)
- Proof Assistant Decision Procedures for Formalizing Origami (Q5200107) (← links)
- A System for Computing and Reasoning in Algebraic Topology (Q5200131) (← links)
- (Q5219924) (← links)
- (Q5219926) (← links)
- Verifying distributed systems (Q5261538) (← links)
- Certified Rule Labeling (Q5277884) (← links)
- Computer Aided Verification (Q5312915) (← links)
- Algebraic Methodology and Software Technology (Q5312973) (← links)
- Ordinals in HOL: Transfinite Arithmetic up to (and Beyond) ω 1 (Q5327341) (← links)
- Mechanical Verification of SAT Refutations with Extended Resolution (Q5327347) (← links)
- A Parallelized Theorem Prover for a Logic with Parallel Execution (Q5327362) (← links)
- Reasoning About Incompletely Defined Programs (Q5387856) (← links)
- Verification Condition Generation Via Theorem Proving (Q5387904) (← links)
- Executing in Common Lisp, Proving in ACL2 (Q5428255) (← links)
- Efficient execution in an automated reasoning environment (Q5437032) (← links)
- A Sound Semantics for OCaml light (Q5458382) (← links)
- Theorem Proving in Higher Order Logics (Q5464646) (← links)
- Theorem Proving in Higher Order Logics (Q5464665) (← links)
- Artificial Intelligence and Symbolic Computation (Q5464700) (← links)
- Meta Reasoning in ACL2 (Q5477654) (← links)
- Theorem Proving in Higher Order Logics (Q5477665) (← links)
- Theorem Proving in Higher Order Logics (Q5477667) (← links)
