Copyright | (c) Levent Erkok |
---|---|

License | BSD3 |

Maintainer | erkokl@gmail.com |

Stability | experimental |

Safe Haskell | None |

Language | Haskell2010 |

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.
To prevent SBV from translating it to an enumerated type, we simply attach an unused field

B () |

# 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.