Abstract
Formal mathematical logic is ideally suited to describing computational processes. We discuss the use of one particular mechanized mathematical logic, namely ACL2 (A Computational Logic for Applicative Common Lisp) to model computational problems and to prove theorems about such models. After a few elementary examples, we explain how computational artifacts are formalized in ACL2 and we summarize the main industrial applications of ACL2 as of 1999.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
References
Boyer, R., Goldschlag, D., Kaufmann, M., and Moore, J. S. (1991). Functional instantiation in first-order logic. In Lifschitz, V., editor, Artificial Intelligence and Mathematical Theory of Computation: Papers in Honor of John McCarthy, pages 7–26. Academic Press.
Boyer, R. S. and Moore, J. S. (1975). Proving theorems about pure lisp functions. JACM, 22(1):129–144.
Boyer, R. S. and Moore, J. S. (1979). A Computational Logic. Academic Press, New York.
Boyer, R. S. and Moore, J. S. (1996). Mechanized formal reasoning about programs and computing machines. In Veroff, R., editor, Automated Reasoning and Its Applications: Essays in Honor of Larry Wos, pages 147–176. MIT Press.
Boyer, R. S. and Moore, J. S. (1997). A Computational Logic Handbook, Second Edition. Academic Press, New York.
Boyer, R. S. and Moore, J. S. (1999). Single-threaded objects in ACL2. (submitted for publication).
Brock, B., Kaufmann, M., and Moore, J. S. (1996). ACL2 theorems about commercial microprocessors. In Srivas, M. and Camilleri, A., editors, Formal Methods in Computer-Aided Design (FMCAD′96), pages 275–293. Springer-Verlag, LNCS 1166.
Brock, B. and Moore, J. S. (1999). A mechanically checked proof of a comparator sort algorithm, (submitted for publication).
Bryant, R. (1992). Symbolic boolean manipulation with ordered binary decision diagrams. Technical Report CMU-CS-92-160, School of Computer Science, Carnegie Mellon University.
Cohen, R. M. (1997). The defensive Java Virtual Machine specification, version 0.53. Technical report, Electronic Data Systems Corp, Austin Technical Services Center, 98 San Jacinto Blvd, Suite 500, Austin, TX 78701.
Goodstein, R. L. (1964). Recursive Number Theory. North-Holland Publishing Company, Amsterdam.
Gordon, M. and Melham, T. (1993). Introduction to HOL: A Theorem Proving Environment for Higher Order Logic. Cambridge University Press.
Greve, D. A. (1998). Symbolic simulation of the JEM1 microprocessor. Technical Report (submitted), Advanced Technology Center, Rockwell Collins, Inc., Cedar Rapids, IA 52498.
Greve, D. A. and Wilding, M. M. (Jan. 12, 1998). Stack-based Java a back-to-future step. Electronic Engineering Times, page 92.
Kaufmann, M. (1998). ACL2 support for verification projects. In Kirchner, C. and Kirchner, H., editors, Proceedings 15th International Conference on Automated Deduction, pages 220–238. LNAI 1421, Springer-Verlag.
Kaufmann, M., Manolios, P., and Moore, J. S. (2000). ACL2: A Tutorial Introduction. Kluwer.
Kaufmann, M. and Moore, J. S. (1997). An industrial strength theorem prover for a logic based on Common Lisp. IEEE Transactions on Software Engineering, 23(4):203–213.
Kaufmann, M. and Moore, J. S. (1999a). The ACL2 User’s Manual http://www.cs.utexas.edu/users/moore/acl2/acl2-doc.html.
Kaufmann, M. and Moore, J. S. (1999b). Structured theory development for a mechanized logic, (submitted for publication).
Lindholm, T. and Yellin, F. (1996). The Java Virtual Machine Specification. Addison-Wesley.
Manolios, P., Namjoshi, K., and Sumners, R. (1999). Linking theorem proving and model-checking with well-founded bisimulation. In Computed Aided Verification, CAV ′99, pages 369–379. Springer-Verlag LNCS 1633.
McCarthy, J. (1959). Programs with common sense. In Proceedings of the Teddington Conference on the Mechanization of Thought Processes, pages 75–91. H.M.Stationery Office.
McCarthy, J. (1962). Towards a mathematical science of computation. In Proceedings of IFIP Congress, pages 21–28. North-Holland.
McCarthy, J. (1963). A basis for a mathematical theory of computation. In Computer Programming and Formal Systems, pages 33–70. North-Holland Publishing Company, Amsterdam, The Netherlands.
McCune, W. (1994). Otter 3.0 Reference Manual and Guide. Tech. Report ANL-94/6, Argonne National Laboratory, Argonne, IL. See also URL http://www.mcs.anl.gov/AR/otter/.
Moore, J. S. (1994). Introduction to the OBDD algorithm for the ATP community. Journal of Automated Reasoning, 12(1):33–45.
Moore, J. S. (1999a). A mechanically checked proof of a multiprocessor result via a uniprocessor view. Formal Methods in System Design, 14(2):213–228.
Moore, J. S. (1999b). Proving theorems about Java-like byte code. In Olderog, E.-R. and Steffen, B., editors, Correct System Design — Recent Insights and Advances, pages 139–162. LNCS 1710.
Moore, J. S., Lynch, T., and Kaufmann, M. (1998). A mechanically checked proof of the correctness of the kernel of the AMD5K86 floating point division algorithm. IEEE Transactions on Computers, 47(9):913–926.
Owre, S., Rushby, J., and Shankar, N. (1992). PVS: A prototype verification system. In Kapur, D., editor, 11th International Conference on Automated Deduction (CADE), pages 748–752. Lecture Notes in Artificial Intelligence, Vol 607, Springer-Verlag.
Russinoff, D. M. (1998). A mechanically checked proof of IEEE compliance of the floating point multiplication, division, and square root algorithms of the AMD-K7 processor, http://www.onr.com/user/russ/david/k7-div-sqrt.html.
Sawada, J. and Hunt, W. (1998). Processor verification with precise exceptions and speculative execution. In Computed Aided Verification, CAV ′98, pages 135–146. Springer-Verlag LNCS 1427.
Shoenfield, J. R. (1967). Mathematical Logic. Addison-Wesley, Reading, Ma.
Smith, S. W. and Austel, V. (1998). Trusting trusted hardware: Towards a formal model for programmable secure coprocessors. In Proceedings of the Third USENIX Workshop on Electronic Commerce, pages 83–98.
Standards Committee of the IEEE Computer Society (1985). IEEE standard for binary floating-point arithmetic. Technical Report IEEE Std. 754–1985, IEEE, 345 East 47th Street, New York, NY 10017.
Steele, Jr., G. L. (1990). Common Lisp The Language, Second Edition. Digital Press, 30 North Avenue, Burlington, MA 01803.
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2000 Springer Science+Business Media New York
About this chapter
Cite this chapter
Moore, J.S. (2000). Towards a Mechanically Checked Theory of Computation. In: Minker, J. (eds) Logic-Based Artificial Intelligence. The Springer International Series in Engineering and Computer Science, vol 597. Springer, Boston, MA. https://doi.org/10.1007/978-1-4615-1567-8_23
Download citation
DOI: https://doi.org/10.1007/978-1-4615-1567-8_23
Publisher Name: Springer, Boston, MA
Print ISBN: 978-1-4613-5618-9
Online ISBN: 978-1-4615-1567-8
eBook Packages: Springer Book Archive