sbv-2.8: SMT Based Verification: Symbolic Haskell theorem prover using SMT solving.

Safe HaskellNone




Demonstrates uninterpreted sorts and how they can be used for deduction. This example is inspired by the discussion at, essentially showing how to show the required deduction using SBV.


Representing uninterpreted booleans

data B Source

The uninterpreted sort B, corresponding to the carrier.




type SB = SBV BSource

Handy shortcut for the type of symbolic values over B

Uninterpreted connectives over B

and :: SB -> SB -> SBSource

Uninterpreted logical connective and

or :: SB -> SB -> SBSource

Uninterpreted logical connective or

not :: SB -> SBSource

Uninterpreted logical connective not

Axioms of the logical system

ax1 :: [String]Source

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.

ax2 :: [String]Source

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

ax3 :: [String]Source

Double negation axiom, similar to the above.

Demonstrated deduction

test :: IO ThmResultSource

Proves the equivalence NOT (p OR (q AND r)) == (NOT p AND NOT q) OR (NOT p AND NOT r), following from the axioms we have specified above. We have:

>>> test