Logic Module =============== .. module:: 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 & (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 ----------------------- .. automethod:: sympy.logic.boolalg.Xor .. automethod:: sympy.logic.boolalg.Nand .. automethod:: sympy.logic.boolalg.Nor .. automethod:: sympy.logic.boolalg.Equivalent Inference --------- .. module: sympy.logic.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 .. automethod:: sympy.logic.inference.satisfiable .. TODO: write about CNF file format