# Logic Module¶

## 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 <<:

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


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

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


## Boolean functions¶

sympy.logic.boolalg.to_cnf(expr)[source]

Convert a propositional logical sentence s to conjunctive normal form. That is, of the form ((A | ~B | ...) & (B | C | ...) & ...)

Examples

>>> from sympy.logic.boolalg import to_cnf
>>> from sympy.abc import A, B, D
>>> to_cnf(~(A | B) | D)
And(Or(D, Not(A)), Or(D, Not(B)))

class sympy.logic.boolalg.And[source]

Logical AND function.

It evaluates its arguments in order, giving False immediately if any of them are False, and True if they are all True.

Examples

>>> from sympy.core import symbols
>>> from sympy.abc import x, y
>>> x & y
And(x, y)


Attributes

 nargs
class sympy.logic.boolalg.Or[source]

Logical OR function

It evaluates its arguments in order, giving True immediately if any of them are True, and False if they are all False.

Attributes

 nargs
class sympy.logic.boolalg.Not[source]

Logical Not function (negation)

Note: De Morgan rules applied automatically

Attributes

 nargs
class sympy.logic.boolalg.Xor[source]

Logical XOR (exclusive OR) function.

Attributes

 nargs
class sympy.logic.boolalg.Nand[source]

Logical NAND function.

It evaluates its arguments in order, giving True immediately if any of them are False, and False if they are all True.

Attributes

 nargs
class sympy.logic.boolalg.Nor[source]

Logical NOR function.

It evaluates its arguments in order, giving False immediately if any of them are True, and True if they are all False.

Attributes

 nargs
class sympy.logic.boolalg.Implies[source]

Logical implication.

A implies B is equivalent to !A v B

Attributes

 nargs
class sympy.logic.boolalg.Equivalent[source]

Equivalence relation.

Equivalent(A, B) is True if and only if A and B are both True or both False

Attributes

 nargs
class sympy.logic.boolalg.ITE[source]

If then else clause.

Attributes

 nargs

## 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 | y) & (x | ~y) & (~x | y) is satisfiable with both x and y being True.

>>> from sympy.logic.inference import satisfiable
>>> from sympy import Symbol
>>> x = Symbol('x')
>>> y = Symbol('y')
>>> satisfiable(x & ~x)
False
>>> satisfiable((x | y) & (x | ~y) & (~x | y))
{x: True, y: 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

sympy.logic.inference.satisfiable(expr, algorithm='dpll2')[source]

Check satisfiability of a propositional sentence. Returns a model when it succeeds

Examples:

>>> from sympy.abc import A, B
>>> from sympy.logic.inference import satisfiable
>>> satisfiable(A & ~B)
{A: True, B: False}
>>> satisfiable(A & ~A)
False