Differences
This shows you the differences between two versions of the page.
| Both sides previous revision Previous revision | |||
|
sav08:approaches_to_reliable_complex_proofs [2009/03/05 13:25] vkuncak |
sav08:approaches_to_reliable_complex_proofs [2009/03/05 13:25] (current) vkuncak |
||
|---|---|---|---|
| Line 15: | Line 15: | ||
| * need specific provers for specific proofs: if we allow users to write provers, they will cheat and likely make errors | * need specific provers for specific proofs: if we allow users to write provers, they will cheat and likely make errors | ||
| - | Approaches to obtaine flexibility, automation, high assurance ('small trusted proof base'): | + | 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) | - 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 | - 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 | - 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 | ||