User loginNavigation 
Predicate calculus in program verificationPredicate calculus is an indispensable tool for program verification. Therefore any program verifier has to be able to reason with quantified expressions, i.e. universally and existentially quantified expressions. The proof engine of Modern Eiffel is able to perform such reasoning. The following article The previous articles Introduction to the proof engine and Proofs by contradiction illustrate the basics of the proof engine. By hbrandl at 20120402 15:43  LtU Forum  previous forum topic  next forum topic  other blogs  3356 reads

Browse archivesActive forum topics 
Recent comments
5 days 3 hours ago
1 week 7 hours ago
1 week 7 hours ago
1 week 7 hours ago
1 week 8 hours ago
1 week 9 hours ago
1 week 10 hours ago
1 week 14 hours ago
1 week 16 hours ago
1 week 20 hours ago