LARA

Differences

This shows you the differences between two versions of the page.

Link to this comparison view

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