Lab for Automated Reasoning and Analysis LARA

Differences

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

Link to this comparison view

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