Logic Module
===============

.. module:: sympy.logic

Introduction
------------

The logic module for SymPy allows to form and manipulate logic expressions using
symbolic and boolean values

Forming logical expressions
---------------------------

You can build boolean expressions with the standard python operators & (And),
|(Or), ~ (Not):

    >>> from sympy import *
    >>> x, y = symbols('x y')
    >>> y | (x & y)
    Or(And(x, y), y)
    >>> x | y
    Or(x, y)
    >>> ~x
    Not(x)

You can also form implications with >>, <<, and class Equivalent:

    >>> x >> y
    Implies(x, y)
    >>> x << y
    Implies(y, x)

Like most types in SymPy, Boolean expressions inherit from sympy.core.Basic:

    >>> (y & x).subs({x: True, y: True})
    True
    >>> (x | y).atoms()
    set([x, y])

Other boolean functions
-----------------------

.. automethod:: sympy.logic.boolalg.Xor

.. automethod:: sympy.logic.boolalg.Nand

.. automethod:: sympy.logic.boolalg.Nor

.. automethod:: sympy.logic.boolalg.Equivalent

Inference
---------

.. module: sympy.logic.inference

This module implements some inference routines in propositional logic.

The function satisfiable will test that a given boolean expression is satisfiable,
that is, you can assign values to the variables to make the sentence True.

For example, the expression x & ~x is not satisfiable, since there are no values
for x that make this sentence True. On the other hand, x | ~x is satisfiable, and
any value of x would do.

    >>> from sympy.logic.inference import satisfiable
    >>> from sympy import Symbol
    >>> x = Symbol('x')
    >>> satisfiable(x & ~x)
    False
    >>> satisfiable(x | ~x)
    {x: True}

As you see, when a sentence is satisfiable, it returns a model that makes that
sentence True. If it is not satisfiable it will return False

.. automethod:: sympy.logic.inference.satisfiable

.. TODO: write about CNF file format