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, simplify=False)[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.

Notes

The operator operator & will perform bitwise operations on integers and for convenience will construct an Add when the arguments are symbolic, but the And function does not perform bitwise operations and when any argument is True it is simply removed from the arguments:

>>> And(x, y).subs(x, 1)
y

Examples

>>> from sympy.core import symbols
>>> from sympy.abc import x, y
>>> from sympy.logic.boolalg import And
>>> 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.

Notes

The operator operator | will perform bitwise operations on integers and for convenience will construct an Or when the arguments are symbolic, but the Or function does not perform bitwise operations and when any argument is False it is simply removed from the arguments:

>>> Or(x, y).subs(x, 0)
y

Examples

>>> from sympy.core import symbols
>>> from sympy.abc import x, y
>>> from sympy.logic.boolalg import Or
>>> x | y
Or(x, y)

Attributes

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

Logical Not function (negation)

Notes

De Morgan rules are 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 iff 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

Table Of Contents

Previous topic

Computing Integrals using Meijer G-Functions

Next topic

Matrices

This Page