An ACL2 Tutorial

DOI10.1007/978-3-540-71067-7_4MaRDI QIDQ3543644zbMATH OpenOpenAlexFDO

Authors 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

Mathematics Subject Classification ID

Recommendations

• The ACL2 Sedan theorem proving system
• ACL2s: ``the ACL2 sedan
• Milestones from the Pure Lisp Theorem Prover to ACL2
• Towards a mechanically checked theory of computation. The ACL2 project
• scientific article; zbMATH DE number 2101985

Cites work

• scientific article; zbMATH DE number 3702108 (Why is no real title available?)
• scientific article; zbMATH DE number 46981 (Why is no real title available?)
• scientific article; zbMATH DE number 88983 (Why is no real title available?)
• scientific article; zbMATH DE number 193479 (Why is no real title available?)
• ACL2s: ``the ACL2 sedan
• Efficient execution in an automated reasoning environment
• Integrating external deduction tools with ACL2
• Meta Reasoning in ACL2
• Nonstandard analysis in ACL2
• Partial functions in ACL2
• Proving Theorems about LISP Functions
• Structured theory development for a mechanized logic

Cited in

(14)

• The right tools for the job: correctness of cone of influence reduction proved using ACL2 and HOL4
• Towards a mechanically checked theory of computation. The ACL2 project
• Executing in Common Lisp, Proving in ACL2
• How can I do that with ACL2? Recent enhancements to ACL2
• Enhancements to ACL2 in versions 5.0, 6.0, and 6.1
• ACL2(ml): machine-learning for ACL2
• Fix your types
• Proceedings of the seventeenth international workshop on the ACL2 theorem prover and its applications, Austin, Texas, USA, May 26--27, 2022
• Integrating external deduction tools with ACL2
• ACL2s: ``the ACL2 sedan
• Linear and nonlinear arithmetic in ACL2
• First order Büchi automata and their application to verification of LTL specifications
• The ACL2 Sedan theorem proving system
• Verifying a scheduling protocol of safety-critical systems

Describes a project that uses

Uses Software

• ACL2s
• NQTHM
• LISP
• Ott
• ACL2

This page was built for publication: An ACL2 Tutorial

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q3543644)