archives

Negation and proofs by contradiction with the proof engine

A new blog entry has beed created with continues the description of Modern Eiffel's proof engine.

This blog entry focuses on the introduction of negation and it's axioms into the class BOOLEAN and presents a rich set of proofs.

This entry completes the use of the proof engine for propositional calculus. The next entries will focus more on real calculations using inductive data types.

By hbrandl at 2012-02-27 18:26 | LtU Forum | login or register to post comments | other blogs | 3983 reads