Menu
▾
▴
#1 Boolean Operators AND, OR, NOT
This theory defines boolean operators AND, OR, NOT that take expression arguments and have an expression value.
AND and OR are defined infix, associative and commutative.
NOT is defined prefix (hence parenthesized).
Automatic and interactive rewrite rules are also provided for every operator, for all combinations of TRUE and FALSE arguments.
All POs are discharged, some of them using external prover Atelier-B ML.
Boolean operators theory and proof files, at archive root.