User loginNavigation |
Proof formatsDuring the development of a language which allows formal verification I have experimented a lot with proof formats. First I have started with a proof language with tactics similar to Isabelle/HOL and Coq. But then I realized that such proofs are fairly difficult to read. In order to understand a proof one often writes down the state of the proof engine at intermediate positions of the tactics. Then I have introduced proof procedures stimulated by some examples in the dafny language. Up to now I think that tactics are not appropriate to write down and document proofs. In the posts Boolean lattices, Predicates as sets and Complete lattices and closure systems I have used a proof format which I think is good to write down and document proofs. Any opinions, remarks etc. are welcome. By hbrandl at 2012-09-25 17:43 | LtU Forum | previous forum topic | next forum topic | other blogs | 4168 reads
|
Browse archives
Active forum topics |
Recent comments
6 weeks 14 hours ago
6 weeks 14 hours ago
6 weeks 14 hours ago
12 weeks 1 day ago
1 year 1 day ago
1 year 1 day ago
1 year 1 day ago
1 year 22 weeks ago
1 year 26 weeks ago
1 year 28 weeks ago