bor0 / gidti

Book: Introduction to Dependent Types with Idris
https://leanpub.com/gidti
Other
76 stars 4 forks source link

Chapter 2: table vs column proofs #26

Closed nbloomf closed 6 years ago

nbloomf commented 6 years ago

(Putting on my novice hat)

Table proofs look a lot easier than column proofs. You just plug in truth values and simplify, where column proofs require planning ahead. Why would we bother with column proofs?

(Taking off novice hat)

Table proofs only work for propositional (zeroth order) theorems - the table method is essentially the decidability algorithm for zeroth order logic. That's why they are easy (if verbose) and always work, and why column proofs become necessary once we're using quantifiers.

It's probably worth pointing this out - there are two methods of proof, but they are not equivalent in power.