ACL2: Implementation of a Computational Logic - UT Computer Science
Jun 10, 2015 - ACL2 is a logic and programming language in which you .... and software systems, augmenting traditional testing by using ... regularity at several companies: ..... Fun example in ACL2(r), a variant of ACL2 that supports the.
ACL2: Implementation of a Computational Logic Matt Kaufmann The University of Texas at Austin Dept. of Computer Science
June 10, 2015
Overview
ACL2 Introduction
Logical Foundations
Conclusion
HELLO!
2/34
Overview
ACL2 Introduction
Logical Foundations
Conclusion
HELLO! I’m so happy to be visiting here! I plan to be in Gothenburg until August 15.
2/34
Overview
ACL2 Introduction
Logical Foundations
Conclusion
HELLO! I’m so happy to be visiting here! I plan to be in Gothenburg until August 15. Thanks, Ali!
2/34
Overview
ACL2 Introduction
Logical Foundations
Conclusion
HELLO! I’m so happy to be visiting here! I plan to be in Gothenburg until August 15. Thanks, Ali! Today I’ll discuss a logic and software tool, ACL2, which has been my focus off and on since the early 1990s.
2/34
Overview
ACL2 Introduction
Logical Foundations
Conclusion
HELLO! I’m so happy to be visiting here! I plan to be in Gothenburg until August 15. Thanks, Ali! Today I’ll discuss a logic and software tool, ACL2, which has been my focus off and on since the early 1990s. (But my intention in Gothenburg is to return to my roots in model theory, especially models of set theory and arithmetic.)
O VERVIEW Quoting the ACL2 home page: ACL2 is a logic and programming language in which you can model computer systems, together with a tool to help you prove properties of those models. “ACL2” denotes "A Computational Logic for Applicative Common Lisp".
5/34
Overview
ACL2 Introduction
Logical Foundations
Conclusion
O VERVIEW Quoting the ACL2 home page: ACL2 is a logic and programming language in which you can model computer systems, together with a tool to help you prove properties of those models. “ACL2” denotes "A Computational Logic for Applicative Common Lisp". Goal for this talk: Say something about ACL2 of interest to logicians.
5/34
Overview
ACL2 Introduction
Logical Foundations
Conclusion
O VERVIEW Quoting the ACL2 home page: ACL2 is a logic and programming language in which you can model computer systems, together with a tool to help you prove properties of those models. “ACL2” denotes "A Computational Logic for Applicative Common Lisp". Goal for this talk: Say something about ACL2 of interest to logicians. I
The focus will be on mechanizing logic for a practical proof assistant.
5/34
Overview
ACL2 Introduction
Logical Foundations
Conclusion
O VERVIEW Quoting the ACL2 home page: ACL2 is a logic and programming language in which you can model computer systems, together with a tool to help you prove properties of those models. “ACL2” denotes "A Computational Logic for Applicative Common Lisp". Goal for this talk: Say something about ACL2 of interest to logicians. I
LESSP informs us that. (COUNT J) decreases according to the well-founded relation. LESSP in each recursive call. Note that: (NUMBERP (DIFFERENCE I J)).
Apr 23, 2015 - Context. Prover Automation and Control ... theorem proving system, including: 4/39 ... In essence, they prove systems correct rather than run massive tests that are ...... Mailing lists available from the ACL2 home page include.
Sep 29, 2006 - port Apple Events and the Open Scripting Architecture. Yet AppleScript is now widely used and is an essential differentiator of the Mac OS. Ap-.
Oct 1, 2013 - Inderjit S. Dhillon Dept of Computer Science UT Austin. Machine Learning: Think Big and ... Python scientific library (scipy). Active development.
as text, web-log and market-basket data analysis. ... We define co-clustering as a pair of maps from rows to row-clusters and from columns to column-clusters.
