Matches in DBpedia 2016-04 for { <http://dbpedia.org/resource/ACL2> ?p ?o }
- ACL2 abstract "ACL2 (A Computational Logic for Applicative Common Lisp) is a software system consisting of a programming language, an extensible theory in a first-order logic, and a mechanical theorem prover. ACL2 is designed to support automated reasoning in inductive logical theories, mostly for the purpose of software and hardware verification. The input language and implementation of ACL2 are built on Common Lisp. ACL2 is free, open source (BSD license) software.The ACL2 programming language is an applicative (side-effect free) variant of Common Lisp. ACL2 is untyped. All ACL2 functions are total — that is, every function maps each object in the ACL2 universe to another object in its universe.ACL2's base theory axiomatizes the semantics 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.The core of ACL2's theorem prover is based on term rewriting, and this core is extensible in that user-discovered theorems can be used as ad-hoc proof techniques for subsequent conjectures.ACL2 is intended to be an \"industrial strength\" version of the Boyer–Moore theorem prover, NQTHM. 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 and run natively.In 2005, the authors of the Boyer-Moore family of provers, which includes ACL2, received the ACM Software System Award \"for pioneering and engineering a most effective theorem prover (...) as a formal methods tool for verifying safety-critical hardware and software.\"".
- ACL2 designer J_Strother_Moore.
- ACL2 designer Matt_Kaufmann.
- ACL2 designer Robert_S._Boyer.
- ACL2 developer J_Strother_Moore.
- ACL2 developer Matt_Kaufmann.
- ACL2 influencedBy Common_Lisp.
- ACL2 influencedBy Nqthm.
- ACL2 latestReleaseVersion "7.1".
- ACL2 license BSD_licenses.
- ACL2 wikiPageExternalLink acl2s.ccs.neu.edu.
- ACL2 wikiPageExternalLink acl2.
- ACL2 wikiPageExternalLink index.html?topic=ACL2____INTERESTING-APPLICATIONS.
- ACL2 wikiPageID "162049".
- ACL2 wikiPageLength "5133".
- ACL2 wikiPageOutDegree "47".
- ACL2 wikiPageRevisionID "673778777".
- ACL2 wikiPageWikiLink ACM_Software_System_Award.
- ACL2 wikiPageWikiLink AMD_K5.
- ACL2 wikiPageWikiLink Applicative_programming_language.
- ACL2 wikiPageWikiLink Automated_reasoning.
- ACL2 wikiPageWikiLink Automated_theorem_proving.
- ACL2 wikiPageWikiLink Axiom.
- ACL2 wikiPageWikiLink BSD_licenses.
- ACL2 wikiPageWikiLink Category:Common_Lisp_software.
- ACL2 wikiPageWikiLink Category:Free_theorem_provers.
- ACL2 wikiPageWikiLink Category:Lisp_(programming_language).
- ACL2 wikiPageWikiLink Category:Lisp_programming_language_family.
- ACL2 wikiPageWikiLink Common_Lisp.
- ACL2 wikiPageWikiLink Compiler.
- ACL2 wikiPageWikiLink Computer_hardware.
- ACL2 wikiPageWikiLink Conjecture.
- ACL2 wikiPageWikiLink Consistency.
- ACL2 wikiPageWikiLink Cross-platform.
- ACL2 wikiPageWikiLink File:ACL2_Logo_2014_transparent.png.
- ACL2 wikiPageWikiLink First-order_logic.
- ACL2 wikiPageWikiLink Free_software.
- ACL2 wikiPageWikiLink Functional_programming.
- ACL2 wikiPageWikiLink J_Strother_Moore.
- ACL2 wikiPageWikiLink Machine_code.
- ACL2 wikiPageWikiLink Mathematical_proof.
- ACL2 wikiPageWikiLink Matt_Kaufmann.
- ACL2 wikiPageWikiLink Metaprogramming.
- ACL2 wikiPageWikiLink Nqthm.
- ACL2 wikiPageWikiLink Open_source.
- ACL2 wikiPageWikiLink Partial_function.
- ACL2 wikiPageWikiLink Pentium_FDIV_bug.
- ACL2 wikiPageWikiLink Programming_language.
- ACL2 wikiPageWikiLink Rewriting.
- ACL2 wikiPageWikiLink Robert_S._Boyer.
- ACL2 wikiPageWikiLink Semantics.
- ACL2 wikiPageWikiLink Side_effect_(computer_science).
- ACL2 wikiPageWikiLink Software.
- ACL2 wikiPageWikiLink Subroutine.
- ACL2 wikiPageWikiLink Theorem.
- ACL2 wikiPageWikiLink Type_system.
- ACL2 wikiPageWikiLink Universe_(mathematics).
- ACL2 wikiPageWikiLinkText "A Computational Logic for Applicative Common Lisp".
- ACL2 wikiPageWikiLinkText "ACL2".
- ACL2 bodystyle "width:320px".
- ACL2 designer "Robert S. Boyer, J Strother Moore and Matt Kaufmann".
- ACL2 developer "Matt Kaufmann and J Strother Moore".
- ACL2 influencedBy Common_Lisp.
- ACL2 influencedBy Nqthm.
- ACL2 latestReleaseVersion "7.1".
- ACL2 license BSD_licenses.
- ACL2 logo "150".
- ACL2 name "ACL2".
- ACL2 operatingSystem Cross-platform.
- ACL2 paradigm Functional_programming.
- ACL2 paradigm Metaprogramming.
- ACL2 typing Type_system.
- ACL2 wikiPageUsesTemplate Template:Infobox_programming_language.
- ACL2 wikiPageUsesTemplate Template:Reflist.
- ACL2 wikiPageUsesTemplate Template:Release_date.
- ACL2 wikiPageUsesTemplate Template:Url.
- ACL2 year "19901996".
- ACL2 subject Category:Common_Lisp_software.
- ACL2 subject Category:Free_theorem_provers.
- ACL2 subject Category:Lisp_(programming_language).
- ACL2 subject Category:Lisp_programming_language_family.
- ACL2 hypernym System.
- ACL2 type Language.
- ACL2 type ProgrammingLanguage.
- ACL2 type Language.
- ACL2 type Tool.
- ACL2 type Language.
- ACL2 type Thing.
- ACL2 type Q315.
- ACL2 type Q34770.
- ACL2 type Q9143.
- ACL2 comment "ACL2 (A Computational Logic for Applicative Common Lisp) is a software system consisting of a programming language, an extensible theory in a first-order logic, and a mechanical theorem prover. ACL2 is designed to support automated reasoning in inductive logical theories, mostly for the purpose of software and hardware verification. The input language and implementation of ACL2 are built on Common Lisp.".
- ACL2 label "ACL2".
- ACL2 sameAs Q4650692.
- ACL2 sameAs ACL2.
- ACL2 sameAs m.015hl_.
- ACL2 sameAs Q4650692.
- ACL2 sameAs ACL2.
- ACL2 wasDerivedFrom ACL2?oldid=673778777.
- ACL2 isPrimaryTopicOf ACL2.