ACL2 ("A Computational Logic for Applicative Common Lisp") is a

software Software is a set of computer programs and associated documentation and data. This is in contrast to hardware, from which the system is built and which actually performs the work. At the lowest programming level, executable code consists ...

system consisting of a

programming language A programming language is a system of notation for writing computer programs. Most programming languages are text-based formal languages, but they may also be graphical. They are a kind of computer language. The description of a programming ...

, created by Timothy Still it was an extensible theory in a

first-order logic First-order logic—also known as predicate logic, quantificational logic, and first-order predicate calculus—is a collection of formal systems used in mathematics, philosophy, linguistics, and computer science. First-order logic uses quantifie ...

, and an

automated theorem prover Automated theorem proving (also known as ATP or automated deduction) is a subfield of automated reasoning and mathematical logic dealing with proving mathematical theorems by computer programs. Automated reasoning over mathematical proof was a maj ...

. ACL2 is designed to support

automated reasoning In computer science, in particular in knowledge representation and reasoning and metalogic, the area of automated reasoning is dedicated to understanding different aspects of reasoning. The study of automated reasoning helps produce computer progra ...

in inductive logical theories, mostly for the purpose of software and hardware verification. The input language and implementation of ACL2 are written in

Common Lisp Common Lisp (CL) is a dialect of the Lisp programming language, published in ANSI standard document ''ANSI INCITS 226-1994 (S20018)'' (formerly ''X3.226-1994 (R1999)''). The Common Lisp HyperSpec, a hyperlinked HTML version, has been derived fro ...

. ACL2 is

free and open-source software Free and open-source software (FOSS) is a term used to refer to groups of software consisting of both free software and open-source software where anyone is freely licensed to use, copy, study, and change the software in any way, and the source ...

Overview

The ACL2 programming language is an applicative (

side-effect In medicine, a side effect is an effect, whether therapeutic or adverse, that is secondary to the one intended; although the term is predominantly employed to describe adverse effects, it can also apply to beneficial, but unintended, consequence ...

free) variant of Common Lisp. ACL2 is untyped. All ACL2 functions are total — that is, every function maps each object in the ACL2

universe The universe is all of space and time and their contents, including planets, stars, galaxies, and all other forms of matter and energy. The Big Bang theory is the prevailing cosmological description of the development of the universe. Acc ...

to another object in its universe. ACL2's base theory

axiom An axiom, postulate, or assumption is a statement that is taken to be true, to serve as a premise or starting point for further reasoning and arguments. The word comes from the Ancient Greek word (), meaning 'that which is thought worthy or f ...

atizes the

semantics Semantics (from grc, σημαντικός ''sēmantikós'', "significant") is the study of reference, meaning, or truth. The term can be used to refer to subfields of several distinct disciplines, including philosophy Philosophy (f ...

of its programming language and its built-in functions. User definitions in the programming language that satisfy a ''definitional principle'' extend the theory in a way that maintains the theory's

logical consistency In classical deductive logic, a consistent theory is one that does not lead to a logical contradiction. The lack of contradiction can be defined in either semantic or syntactic terms. The semantic definition states that a theory is consistent ...

. The core of ACL2's theorem prover is based on

term rewriting In mathematics, computer science, and logic, rewriting covers a wide range of methods of replacing subterms of a formula with other terms. Such methods may be achieved by rewriting systems (also known as rewrite systems, rewrite engines, or reduc ...

, and this core is extensible in that user-discovered

theorem In mathematics, a theorem is a statement that has been proved, or can be proved. The ''proof'' of a theorem is a logical argument that uses the inference rules of a deductive system to establish that the theorem is a logical consequence of th ...

s can be used as ad hoc proof techniques for subsequent

conjecture In mathematics, a conjecture is a conclusion or a proposition that is proffered on a tentative basis without proof. Some conjectures, such as the Riemann hypothesis (still a conjecture) or Fermat's Last Theorem (a conjecture until proven in 19 ...

s. ACL2 is intended to be an "industrial strength" version of the Boyer–Moore theorem prover,

NQTHM Nqthm is a theorem prover sometimes referred to as the Boyer–Moore theorem prover. It was a precursor to ACL2. History The system was developed by Robert S. Boyer and J Strother Moore, professors of computer science at the University of Texas ...

. Toward this goal, ACL2 has many features to support clean engineering of interesting mathematical and computational theories. ACL2 also derives efficiency from being built on Common Lisp; for example, the same specification that is the basis for inductive verification can be

compiled In computing, a compiler is a computer program that translates computer code written in one programming language (the ''source'' language) into another language (the ''target'' language). The name "compiler" is primarily used for programs that ...

and run natively. In 2005, the authors of the Boyer-Moore family of provers, which includes ACL2, received the

ACM Software System Award The ACM Software System Award is an annual award that honors people or an organization "for developing a software system that has had a lasting influence, reflected in contributions to concepts, in commercial acceptance, or both". It is awarded b ...

"for pioneering and engineering a most effective theorem prover (...) as a formal methods tool for verifying safety-critical hardware and software."

Proofs

ACL2 has had numerous industrial applications. In 1995,

J Strother Moore J Strother Moore (his first name is the alphabetic character "J" – not an abbreviated "J.") is a computer scientist. He is a co-developer of the Boyer–Moore string-search algorithm, Boyer–Moore majority vote algorithm, and the Boyer–Moo ...

Matt Kaufmann Matt Kaufmann is a senior research scientist in the department of computer sciences at the University of Texas at Austin, United States. He was a recipient of the 2005 ACM Software System Award along with Robert S. Boyer and J Strother Moore ...

and Tom Lynch used ACL2 to prove the correctness of the floating point division operation of the

AMD K5 The K5 is AMD's first x86 processor to be developed entirely in-house. Introduced in March 1996, its primary competition was Intel's Pentium microprocessor. The K5 was an ambitious design, closer to a Pentium Pro than a Pentium regarding techni ...

microprocessor in the wake of the

Pentium FDIV bug The Pentium FDIV bug is a hardware bug affecting the floating-point unit (FPU) of the early Intel Pentium processors. Because of the bug, the processor would return incorrect binary floating point results when dividing certain pairs of high-pr ...

. Th
interesting applications
page of the ACL2 documentation has a summary of some uses of the system. Industrial users of ACL2 include AMD, Arm, Centaur Technology, IBM, Intel, Oracle, and Collins Aerospace.

References

External links

ACL2 websiteACL2s - ACL2 Sedan - An Eclipse-based interface developed by Peter Dillinger and Pete Manolios that includes powerful features to provide users with more automation and support for specifying conjectures and proving theorems with ACL2.
{{DEFAULTSORT:Acl2 Lisp (programming language) Common Lisp (programming language) software Proof assistants Free theorem provers Lisp programming language family Software using the BSD license

Overview

Proofs

See also

References

External links