An ACL2 Tutorial
From MaRDI portal
Publication:3543644
DOI10.1007/978-3-540-71067-7_4zbMath1165.68461OpenAlexW1595255563MaRDI QIDQ3543644
Matt Kaufmann, J. Strother Moore
Publication date: 4 December 2008
Published in: Lecture Notes in Computer Science (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.1007/978-3-540-71067-7_4
Related Items
Verifying a scheduling protocol of safety-critical systems, The ACL2 Sedan Theorem Proving System, The right tools for the job: correctness of cone of influence reduction proved using ACL2 and HOL4, ACL2s: “The ACL2 Sedan”
Uses Software
Cites Work
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Integrating external deduction tools with ACL2
- Partial functions in ACL2
- Structured theory development for a mechanized logic
- ACL2s: “The ACL2 Sedan”
- Proving Theorems about LISP Functions
- Efficient execution in an automated reasoning environment
- Meta Reasoning in ACL2
- Nonstandard analysis in ACL2