Lab for Automated Reasoning and Analysis LARA

Differences

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

Link to this comparison view

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
  
 
sav08/approaches_to_reliable_complex_proofs.txt · Last modified: 2009/03/05 13:25 by vkuncak
 
© EPFL 2018 - Legal notice