Approaches to Reliable Complex Proofs
Interactive theorem proving: combine user interaction and automated proof to prove complex properties for which high degree of confidence is relevant.
- even careful paper and pencil proofs can be vague and contain errors
- proofs of complex theorems require creativity that is beyond the reach of automated methods
- proof checking: spell out the entire proof using inference system of HOL - tedious, used in Automath, and in early stages of other systems)
- solution: incorporate all automation available (decision procedures, theorem provers, simplifiers, heuristics) into proof checking
Issue with automation:
- automated provers are complex, what if their implementation contains an error?
- need specific provers for specific proofs: if we allow users to write provers, they will cheat and likely make errors
Three approaches to obtaine flexibility, automation, high assurance ('small trusted proof base'):
- prove correctness of proof procedures (can be harder than prove the problem on which it is used)
- each proof procedure generates a proof object (checked by simple proof checker) - errors detected late, generating proofs hard, slows down
- LCF approach: proof procedures create theorems by invoking only basic inference rules - can be slow, but very flexible, can be combined with other two techniques