LARA

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.

Justification:

  • 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

Approaches:

  • 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'):

  1. prove correctness of proof procedures (can be harder than prove the problem on which it is used)
  2. each proof procedure generates a proof object (checked by simple proof checker) - errors detected late, generating proofs hard, slows down
  3. 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