# 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 | ||