The following pages link to J Strother Moore (Q928667):
Displaying 48 items.
- Rewriting with equivalence relations in ACL2 (Q928668) (← links)
- (Q1006726) (redirect page) (← links)
- Integrating external deduction tools with ACL2 (Q1006728) (← links)
- The addition of bounded quantification and partial functions to a computational logic and its theorem prover (Q1107510) (← links)
- A mechanical proof of the termination of Takeuchi's function (Q1259437) (← links)
- A formal model of asynchronous communication and its use in mechanically verifying a biphase mark protocol (Q1318283) (← links)
- Introduction to the OBDD algorithm for the ATP community (Q1332638) (← links)
- Partial functions in ACL2 (Q1425160) (← links)
- Structured theory development for a mechanized logic (Q1595929) (← links)
- On the desirability of mechanizing calculational proofs (Q1607098) (← links)
- Milestones from the Pure Lisp Theorem Prover to ACL2 (Q2280212) (← links)
- Limited second-order functionality in a first-order setting (Q2303245) (← links)
- Executable JVM model for analytical reasoning: A study (Q2566223) (← links)
- Towards a mechanically checked theory of computation. The ACL2 project (Q2734953) (← links)
- ACL2s: ``the ACL2 sedan'' (Q2867932) (← links)
- Proof Pearl: Proving a Simple Von Neumann Machine Turing Complete (Q2879266) (← links)
- Rough Diamond: An Extension of Equivalence-Based Rewriting (Q2879275) (← links)
- (Q3021914) (← links)
- A fast string searching algorithm (Q3090391) (← links)
- Proof Checking the RSA Public Key Encryption Algorithm (Q3340195) (← links)
- (Q3345811) (← links)
- Machines Reasoning About Machines: 2015 (Q3460540) (← links)
- (Q3490989) (← links)
- An ACL2 Tutorial (Q3543644) (← links)
- (Q3709921) (← links)
- A Mechanical Proof of the Unsolvability of the Halting Problem (Q3766888) (← links)
- (Q3835049) (← links)
- (Q3894958) (← links)
- (Q4016540) (← links)
- (Q4040283) (← links)
- Proving Theorems about LISP Functions (Q4105761) (← links)
- (Q4503919) (← links)
- (Q4551175) (← links)
- A mechanically checked proof of the AMD5/sub K/86/sup TM/ floating-point division program (Q4571480) (← links)
- (Q4790668) (← links)
- (Q4817211) (← links)
- Efficient execution in an automated reasoning environment (Q5437032) (← links)
- Theorem Proving in Higher Order Logics (Q5464646) (← links)
- Meta Reasoning in ACL2 (Q5477654) (← links)
- Theorem Proving in Higher Order Logics (Q5477668) (← links)
- Formal Methods in Computer-Aided Design (Q5492967) (← links)
- (Q5663380) (← links)
- Correct Hardware Design and Verification Methods (Q5897074) (← links)
- Correct Hardware Design and Verification Methods (Q5897076) (← links)
- A theorem prover for a computational logic (Q6488518) (← links)
- How can I do that with ACL2? Recent enhancements to ACL2 (Q6586531) (← links)
- Enhancements to ACL2 in versions 5.0, 6.0, and 6.1 (Q6587250) (← links)
- Iteration in ACL2 (Q6591494) (← links)
