Stability | experimental |
---|---|

Maintainer | erkokl@gmail.com |

Safe Haskell | None |

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 `B`

# 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 `B`

.

One of De Morgan's laws, again as an axiom in terms of our uninterpeted logical connectives.