Demonstrates uninterpreted sorts and how they can be used for deduction. This example is inspired by the discussion at http://stackoverflow.com/questions/10635783/using-axioms-for-deductions-in-z3, essentially showing how to show the required deduction using SBV.
Representing uninterpreted booleans
The uninterpreted sort
B, corresponding to the carrier.
Uninterpreted connectives over
Axioms of the logical system
Distributivity of OR over AND, as an axiom in terms of
the uninterpreted functions we have introduced. Note how
variables range over the uninterpreted sort
One of De Morgan's laws, again as an axiom in terms of our uninterpeted logical connectives.