-->
Home » , , » ACL2 is a software system consisting of a programming language, an extensible theory in a first-order logic.
Thursday
27 February 2014

ACL2 is a software system consisting of a programming language, an extensible theory in a first-order logic.

ACL2 is both a programming language in which you can model computer systems and a tool to help you prove properties of those models.

ACL2 is part of the Boyer-Moore family of provers, for which its authors have received the 2005 ACM Software System Award.

Functions that display or change history

ACL2 keeps track of the commands that you have executed that have extended the logic or the rule database, as by the definition of macros, functions, etc. Using the facilities in this section you can review the sequence of commands executed so far. For example, you can ask to see the most recently executed command, or the command 10 before that, or the command that introduced a given function symbol. You can also undo back through some previous command, restoring the logical world to what it was before the given command.

The annotations printed in the margin in response to some of these commands (such as `P', `L', and `V') are explained in the documentation for :pc.

Several technical terms are used in the documentation of the history commands. You must understand these terms to use the commands. These terms are documented via :doc entries of their own. See command, see events, see command-descriptor, and see logical-name.

ACL2_Logo
    Libraries (Books).
    Libraries of books (files containing definitions and theorems) extend the code that we have written. The installation instructions explain how to fetch the community books, which are contributed and maintained by the members of the ACL2 community. For more information, see the acl2-books project page.

    Documentation.
    There is an extensive user's manual for the ACL2 system, and an even more comprehensive manual that documents not only the ACL2 system but also many community books. See below to learn more.
    License and Copyright.
    ACL2 is freely available under the terms of the LICENSE file distributed with ACL2. License, copyright, and authorship information is available from the ACL2 documentation.
    Extensions.
    The ACL2 distribution includes the following extensions, which were developed by the individuals shown.
        ACL2(r)
        Support for the real numbers by way of non-standard analysis
        Ruben Gamboa
        ACL2(h)
        Support for hash cons, applicative hash tables, and function memoization for reuse of previously computed results
        Bob Boyer, Warren A. Hunt, Jr., Jared Davis, and Sol Swords
        ACL2(p)
        Support for parallel evaluation
        David L. Rager
    Another extension of ACL2 is the Eclipse-based ACL2 Sedan (ACL2s). Unlike the systems above, ACL2s is distributed and maintained by Pete Manolios and his research group. ACL2s comes with a standard executable ACL2 image for Windows, but it also comes with pre-certified community books and an extension of ACL2 with additional features, including extra automation for termination proofs as well as counterexample generation.

To learn about ACL2, read at least the following two links.

    Industrial Applications of ACL2 (10 minutes) to help you understand what sophisticated users can do;
    A Flying Tour (10 minutes) to get an overview of the system and what skills the user must have.

If you want to learn how to use ACL2, we recommend that you read a selection of the materials referenced below, depending on your learning style, and do suggested exercises.

   A Walking Tour (1 hour) provides an overview of the theorem prover.

    The Try ACL2 [External link to http://tryacl2.org] web site provides interactive lessons to get you started using ACL2.
    Introduction to the Theorem Prover (10-40 hours) provides instruction on how to interact with the system. Unlike the three documents above, this document expects you to think! It cites the necessary background pages on programming in ACL2 and on the logic and then instructs you in the-method, which is how expert users use ACL2. It concludes with some challenge problems for the ACL2 beginner (including solutions) and an FAQ. Most users will spend several hours a day for several days working through this material.
    The book Computer-Aided Reasoning: An Approach [External link to http://www.cs.utexas.edu/users/moore/publications/acl2-books/car/index.html] is worth a careful read, as you work exercises and learn the-method.
    Annotated ACL2 Scripts and Demos contains relatively elementary proof scripts that have been annotated to help train the newcomer.
    Many files (``books'') in the ACL2 community books (see community-books) are extensively annotated.
    An Alternative Introduction document, while largely subsumed by the Introduction to the Theorem Prover mentioned above, still might be useful because it covers much of the tutorial material in a different way.

At this point you are probably ready to use ACL2 on your own small projects. A common mistake for beginners is to browse the documentation and then try to do something that is too big! Think of a very small project and then simplify it!

Note that ACL2 has a very supportive user network. See the link to ``Mailing Lists'' on the ACL2 home page [External link to http://www.cs.utexas.edu/users/moore/acl2] .

The topics listed below are a hodge podge, developed over time. Although some of these are not mentioned above, you might find some to be useful as well.

If you liked this article, subscribe to the feed by clicking the image below to keep informed about new contents of the blog:

0 commenti:

Post a Comment

Random Posts

  • Venenux Gnu/Linux is a Debian-based community distribution developed in South America and designed for Spanish-speaking
    22.11.2009 - 0 Comments
    VENENUX GNU/Linux is a Debian-based community distribution developed in South America and designed for Spanish-speaking users.VENENUX GNU / Linux is a distribution of GNU Operating System 100% free targeted primarily to users in Latin America,…
  • Imagineos (formerly GoblinX) is a bootable live CD distribution based on Slackware Linux.
    05.07.2010 - 0 Comments
    Imagineos (formerly GoblinX) is a bootable live CD distribution based on Slackware Linux. The primary goal for Imagineos is to create a more pleasant and functional desktop, standardising all icons and themes to make it easy for novice users to…
  • Cairo-Dock is an animated application launch bar for the desktop compatible with Compiz-Fusion, Beryl, Compiz, Metacity, Kwin, Xcompmgr.
    09.11.2010 - 0 Comments
    Cairo-Dock is an animated application launch bar for the desktop, comparable to the dock in Mac OS X or Rocket Dock (for Windows). Now, you can use Cairo-Dock with OpenGL (to use your graphic card!). Some screenshotsIt is compatible with…
  • These were our 10 most popular post of 2018 from Linuxlandit & The Conqueror Penguin.
    23.01.2019 - 2 Comments
    The year 2018 was a year full of good events for the world of free software. New distributions, consolidations and updates of existing ones. Our readers have inclined in this case for alternative distributions and various software. he most…
  • USBprog - An open source all purpose tool (AVR ISP, ARM7/ARM9, AT89,JTAG, RS232, IO)
    10.09.2011 - 0 Comments
    usbprog is a free programming adapter. You can easily install different firmware versions from an "online pool" over USB. The adapter can be used for programming and debugging AVR and ARM processors, as USB to RS232 converter, as JTAG interface or…
  • Guides and tutorials for Zorin OS: Error While Installing Zorin OS.
    25.01.2023 - 2 Comments
    Zorin OS 12 is the new version of this desktop Linux distribution that was born in 2008 and has always been characterized by being aimed at the most novice users who are less familiar with GNU/Linux. Zorin OS is known for offering an interface very…
  • Zenwalk is odern and user-friendly GNU/Linux operating system
    20.08.2008 - 0 Comments
    Zenwalk Linux Zenwalk Linux (formerly Minislack) is a Slackware-based GNU/Linux operating system with a goal of being slim and fast by using only one application per task and with focus on graphical desktop and multimedia usage. Zenwalk features…
  • Lubuntu is a fast, lightweight and energy-saving variant of Ubuntu using the LXDE (Lightweight X11 Desktop Environment) desktop.
    20.03.2010 - 0 Comments
    Lubuntu is a fast, lightweight and energy-saving variant of Ubuntu using the LXDE (Lightweight X11 Desktop Environment) desktop. It is intended to have low-resource system requirements and is designed primarily for netbooks, mobile devices and…
  • The KaOS team has published a new snapshot of the distribution's rolling desktop operating system.
    21.11.2019 - 0 Comments
    The KaOS team has published a new snapshot of the distribution's rolling desktop operating system. The project is removing Python 2 packages and is publishing cutting edge packages for KDE Plasma 5.17. "Quite a few big changes for this release,…
  • Perl Installation Comments
    27.09.2008 - 0 Comments
    Installing Perl on Unix Perl support for MySQL is provided by means of the DBI/DBD client interface. The Perl DBD/DBI client code requires Perl Version 5.004 or later.The interface will not work if you have an older version of Perl.MySQL Perl…

Recent Posts

Recent Posts Widget

Popular Posts

Labels

Archive

page counter follow us in feedly
 
Copyright © 2014 Linuxlandit & The Conqueror Penguin
-->