The logic module for SymPy allows to form and manipulate logic expressions using symbolic and boolean values.
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])
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)))
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 |
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 |
Logical Not function (negation)
Note: De Morgan rules applied automatically
Attributes
nargs |
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 |
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 |
Logical implication.
A implies B is equivalent to !A v B
Attributes
nargs |
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
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