Differences
This shows you the differences between two versions of the page.
Last revision Both sides next revision | |||
sav08:approaches_to_reliable_complex_proofs [2008/05/28 04:18] vkuncak created |
sav08:approaches_to_reliable_complex_proofs [2009/03/05 13:25] 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 | ||
- | Obtaining flexibility, automation, high assurance ('small trusted proof base'): | + | 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 |