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