5 ms·
I can't wrap myself around how theorem provers work. Is there something like a beginner tutorial with examples from simple uses? And which theorem prover would
by antman 6y ago
I can't wrap myself around how theorem provers work. Is there something like a beginner tutorial with examples from simple uses? And which theorem prover would be intuitive for an introduction to this space?
- sumtechguy 6y agoStart with the idea x=a+c. x can now be short hand for a+c. That may help? If you think of a theorem in the light that it is a giant function you can break it down that way too. Like sprintf is shorthand for the monster of bit of code that is sprintf.
- strgcmc 6y agoThis probably isn't a simple nor use-friendly intro, but it's pretty comprehensive at least: https://flint.cs.yale.edu/cs430/coq/pdf/Tutorial.pdf https://flint.cs.yale.edu/cs430/coq/pdf/Tutorial.pdf (section 1.2 has the first minimal proof, although familiarity with formal logic is kind of a pre-req to properly parsing this style of writing) I remember learning and using Coq in a similar 300-level CS course at my university, 10+ years ago.
- fiddlerwoaroof 6y agoThe Little Prover might be a good choice: it’s about ACL2, which was used to prove various floating point implementations were correct. It’s a fairly accessible guide to proving theorems in this system.
- currymj 6y agoYes, this exists. it is called the "Natural Number Game" and interactively teaches you to use the Lean theorem prover to prove simple theorems about addition, multiplication, and so on. It runs in the browser. https://wwwf.imperial.ac.uk/~buzzard/xena/natural_number_game/ https://wwwf.imperial.ac.uk/~buzzard/xena/natural_number_gam...
- umenthum 6y agoI highly recommend Software Foundations Volume 1: Logical Foundations as an introduction to theorem proving in Coq. Try working through the first few chapters and see what you think: https://softwarefoundations.cis.upenn.edu/lf-current/toc.html https://softwarefoundations.cis.upenn.edu/lf-current/toc.htm...