logic.rst

Logic

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 & (~sympy.logic.boolalg.And), | (~sympy.logic.boolalg.Or), ~ (sympy.logic.boolalg.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 ~sympy.core.basic.Basic:

>>> (y & x).subs({x: True, y: True})
True
>>> (x | y).atoms() == {x, y}
True

The logic module also includes the following functions to derive boolean expressions from their truth tables-

sympy.logic.boolalg.SOPform

sympy.logic.boolalg.POSform

Boolean functions

sympy.logic.boolalg.BooleanTrue

sympy.logic.boolalg.BooleanFalse

sympy.logic.boolalg.And

sympy.logic.boolalg.Or

sympy.logic.boolalg.Not

sympy.logic.boolalg.Xor

sympy.logic.boolalg.Nand

sympy.logic.boolalg.Nor

sympy.logic.boolalg.Implies

sympy.logic.boolalg.Equivalent

sympy.logic.boolalg.ITE

The following functions can be used to handle Conjunctive and Disjunctive Normal forms-

sympy.logic.boolalg.to_cnf

sympy.logic.boolalg.to_dnf

sympy.logic.boolalg.is_cnf

sympy.logic.boolalg.is_dnf

Simplification and equivalence-testing

sympy.logic.boolalg.simplify_logic

SymPy's simplify() function can also be used to simplify logic expressions to their simplest forms.

sympy.logic.boolalg.bool_map

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} 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