Archive for February, 2012

Negation and proofs by contradiction

Introduction The last blog entry gave an introduction to Modern Eiffel’s proof engine. The basic rules have been explained, the boolean operations “=>”, “and” and “or” have been introduced with their corresponding axioms and some proofs have been given for expressions using these operations. The class BOOLEAN up to now looks like immutable class BOOLEAN […]

Leave a comment

Introduction to the proof engine

In the previous blog entry the outline of Modern Eiffel has been described. In this blog entry I’m going to talk about proofs of assertions involving boolean expressions with the help of Modern Eiffel’s proof engine. The kind of assertions to prove We are going to proof basic properties of boolean expressions like reflexivity_of_implication: all(a:BOOLEAN) […]

Leave a comment