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

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


B () 

type SB = SBV B Source

Handy shortcut for the type of symbolic values over B

Uninterpreted connectives over B

and :: SB -> SB -> SB Source

Uninterpreted logical connective and

or :: SB -> SB -> SB Source

Uninterpreted logical connective or

not :: SB -> SB Source

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 ThmResult Source

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