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

Copyright | (c) Levent Erkok
License | BSD3
Maintainer | erkokl@gmail.com
Stability | experimental
Safe Haskell | None
Language | Haskell2010

Data.SBV.Examples.Uninterpreted.Shannon

Contents

- Boolean functions
- Shannon cofactors
- Shannon expansion theorem
- Derivatives
- Universal quantification
- Existential quantification

Description

Proves (instances of) Shannon's expansion theorem and other relevant facts. See: http://en.wikipedia.org/wiki/Shannon's_expansion

Synopsis

- type Ternary = SBool -> SBool -> SBool -> SBool
- type Binary = SBool -> SBool -> SBool
- pos :: (SBool -> a) -> a
- neg :: (SBool -> a) -> a
- shannon :: IO ThmResult
- shannon2 :: IO ThmResult
- derivative :: Ternary -> Binary
- noWiggle :: IO ThmResult
- universal :: Ternary -> Binary
- univOK :: IO ThmResult
- existential :: Ternary -> Binary
- existsOK :: IO ThmResult

# Boolean functions

type Ternary = SBool -> SBool -> SBool -> SBool Source #

A ternary boolean function

type Binary = SBool -> SBool -> SBool Source #

A binary boolean function

# Shannon cofactors

pos :: (SBool -> a) -> a Source #

Positive Shannon cofactor of a boolean function, with respect to its first argument

neg :: (SBool -> a) -> a Source #

Negative Shannon cofactor of a boolean function, with respect to its first argument

# Shannon expansion theorem

shannon :: IO ThmResult Source #

Shannon's expansion over the first argument of a function. We have:

    >>> shannon
    Q.E.D.

shannon2 :: IO ThmResult Source #

Alternative form of Shannon's expansion over the first argument of a function. We have:

    >>> shannon2
    Q.E.D.

# Derivatives

derivative :: Ternary -> Binary Source #

Computing the derivative of a boolean function (boolean difference). Defined as exclusive-or of Shannon cofactors with respect to that variable.

noWiggle :: IO ThmResult Source #

The no-wiggle theorem: If the derivative of a function with respect to a variable is constant False, then that variable does not "wiggle" the function; i.e., any changes to it won't affect the result of the function. In fact, we have an equivalence: The variable only changes the result of the function iff the derivative with respect to it is not False:

    >>> noWiggle
    Q.E.D.

# Universal quantification

universal :: Ternary -> Binary Source #

Universal quantification of a boolean function with respect to a variable. Simply defined as the conjunction of the Shannon cofactors.

univOK :: IO ThmResult Source #

Show that universal quantification is really meaningful: That is, if the universal quantification with respect to a variable is True, then both cofactors are true for those arguments. Of course, this is a trivial theorem if you think about it for a moment, or you can just let SBV prove it for you:

    >>> univOK
    Q.E.D.

# Existential quantification

existential :: Ternary -> Binary Source #

Existential quantification of a boolean function with respect to a variable. Simply defined as the conjunction of the Shannon cofactors.

existsOK :: IO ThmResult Source #

Show that existential quantification is really meaningful: That is, if the existential quantification with respect to a variable is True, then one of the cofactors must be true for those arguments. Again, this is a trivial theorem if you think about it for a moment, but we will just let SBV prove it:

    >>> existsOK
    Q.E.D.