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.