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

boolalg.Xor()

Logical XOR (exclusive OR) function. returns True if an odd number of the arguments are True, and the rest are False. returns False if an even number of the arguments are True, and the rest are False.

boolalg.Nand()

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.

boolalg.Nor()

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.

boolalg.Equivalent()

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

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

static inference.satisfiable(expr, algorithm='dpll')

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