Completed
Introduction to Holly
Class Central Classrooms beta
YouTube videos curated by Class Central.
Classroom Contents
Verifying Symbolic Computation in the HolPy Theorem Prover - IPAM at UCLA
Automatically move to the next video in the Classroom when playback concludes
- 1 Intro
- 2 Outline
- 3 Introduction to Holly
- 4 Python API for proof automation
- 5 Python API example
- 6 Verification of definite integrals: motivation
- 7 Basic idea
- 8 Example: integration by parts
- 9 Example: trigonometric identity
- 10 Proof reconstruction
- 11 Summary: overall architecture
- 12 Example #1
- 13 Example #2
- 14 Limitations
- 15 Extensions
- 16 New rules
- 17 Examples
- 18 Example #4
- 19 Summary: division of labor
- 20 Summary: comparison with CAS
- 21 Future work
