We describe a tutorial that demonstrates the use of the ACL2 theorem prover. We have three goals: to enable a motivated reader to start on a path towards effective use of ACL2; to provide ideas for other interactive theorem prover projects; and to elicit feedback on how we might incorporate features of other proof tools into ACL2. © 2008 Springer Berlin Heidelberg.
CITATION STYLE
Kaufmann, M., & Moore, J. S. (2008). An ACL2 tutorial. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 5170 LNCS, pp. 17–21). Springer Verlag. https://doi.org/10.1007/978-3-540-71067-7_4
Mendeley helps you to discover research relevant for your work.