Logic

Introduction

The logic module for Diofant 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):

>>> y | (x & y)
y | (x & y)
>>> x | y
x | y
>>> ~x
~x

You can also form implications with >> and <<:

>>> x >> y
Implies(x, y)
>>> x << y
Implies(y, x)

Like most types in Diofant, Boolean expressions inherit from Basic:

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

Boolean functions

class diofant.logic.boolalg.BooleanTrue(*args, **kwargs)

Diofant version of True, a singleton that can be accessed via true.

This is the Diofant version of True, for use in the logic module. The primary advantage of using true instead of True is that shorthand boolean operations like ~ and >> will work as expected on this class, whereas with True they act bitwise on 1. Functions in the logic module will return this class when they evaluate to true.

Notes

There is liable to be some confusion as to when True should be used and when true should be used in various contexts throughout Diofant. An important thing to remember is that sympify(True) returns true. This means that for the most part, you can just use True and it will automatically be converted to true when necessary, similar to how you can generally use 1 instead of Integer(1).

The rule of thumb is:

“If the boolean in question can be replaced by an arbitrary symbolic Boolean, like Or(x, y) or x > 1, use true. Otherwise, use True”.

In other words, use true only on those contexts where the boolean is being used as a symbolic representation of truth. For example, if the object ends up in the .args of any expression, then it must necessarily be true instead of True, as elements of .args must be Basic. On the other hand, == is not a symbolic operation in Diofant, since it always returns True or False, and does so in terms of structural equality rather than mathematical, so it should return True. The assumptions system should use True and False. Aside from not satisfying the above rule of thumb, the assumptions system uses a three-valued logic (True, False, None), whereas true and false represent a two-valued logic. When in doubt, use True.

“true == True is True.”

While “true is True” is False, “true == True” is True, so if there is any doubt over whether a function or expression will return true or True, just use == instead of is to do the comparison, and it will work in either case. Finally, for boolean flags, it’s better to just use if x instead of if x is True. To quote PEP 8:

Don’t compare boolean values to True or False using ==.

• Yes: if greeting:

• No: if greeting == True:

• Worse: if greeting is True:

Examples

>>> sympify(True)
true
>>> ~true
false
>>> not True
False
>>> Or(True, False)
true

See also

BooleanFalse

class diofant.logic.boolalg.BooleanFalse(*args, **kwargs)

Diofant version of False, a singleton that can be accessed via false.

This is the Diofant version of False, for use in the logic module. The primary advantage of using false instead of False is that shorthand boolean operations like ~ and >> will work as expected on this class, whereas with False they act bitwise on 0. Functions in the logic module will return this class when they evaluate to false.

Notes

See note in BooleanTrue.

Examples

>>> sympify(False)
false
>>> false >> false
true
>>> False >> False
0
>>> Or(True, False)
true

See also

BooleanTrue

class diofant.logic.boolalg.And(*args)

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

>>> x & y
x & y

Notes

The & operator is provided as a convenience, but note that its use here is different from its normal use in Python, which is bitwise and. Hence, And(a, b) and a & b will return different things if a and b are integers.

>>> (x & y).subs({x: 1})
y

class diofant.logic.boolalg.Or(*args)

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.

Examples

>>> x | y
x | y

Notes

The | operator is provided as a convenience, but note that its use here is different from its normal use in Python, which is bitwise or. Hence, Or(a, b) and a | b will return different things if a and b are integers.

>>> (x | y).subs({x: 0})
y

class diofant.logic.boolalg.Not(arg)

Logical Not function (negation).

Returns True if the statement is False. Returns False if the statement is True.

Examples

>>> Not(True)
false
>>> Not(False)
true
>>> ~And(True, False)
true
>>> ~Or(True, False)
false
>>> ~(And(True, x) & Or(x, False))
~x
>>> ~x
~x
>>> ~((x | y) & (~x | ~y))
~((x | y) & (~x | ~y))

>>> not True
False
>>> ~true
false

class diofant.logic.boolalg.Xor(*args)

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.

Examples

>>> Xor(True, False)
true
>>> Xor(True, True)
false
>>> Xor(True, False, True, True, False)
true
>>> Xor(True, False, True, False)
false
>>> x ^ y
Xor(x, y)

Notes

The ^ operator is provided as a convenience, but note that its use here is different from its normal use in Python, which is bitwise xor. In particular, a ^ b and Xor(a, b) will be different if a and b are integers.

>>> (x ^ y).subs({y: 0})
x

class diofant.logic.boolalg.Nand(*args)

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.

Returns True if any of the arguments are False. Returns False if all arguments are True.

Examples

>>> Nand(False, True)
true
>>> Nand(True, True)
false
>>> Nand(x, y)
~(x & y)

class diofant.logic.boolalg.Nor(*args)

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.

Returns False if any argument is True. Returns True if all arguments are False.

Examples

>>> Nor(True, False)
false
>>> Nor(True, True)
false
>>> Nor(False, True)
false
>>> Nor(False, False)
true
>>> Nor(x, y)
~(x | y)

class diofant.logic.boolalg.Implies(*args)

Logical implication.

A implies B is equivalent to !A v B

Accepts two Boolean arguments; A and B. Returns False if A is True and B is False. Returns True otherwise.

Examples

>>> Implies(True, False)
false
>>> Implies(False, False)
true
>>> Implies(True, True)
true
>>> Implies(False, True)
true
>>> x >> y
Implies(x, y)
>>> y << x
Implies(x, y)

Notes

The >> and << operators are provided as a convenience, but note that their use here is different from their normal use in Python, which is bit shifts. Hence, Implies(a, b) and a >> b will return different things if a and b are integers. In particular, since Python considers True and False to be integers, True >> True will be the same as 1 >> 1, i.e., 0, which has a truth value of False. To avoid this issue, use the Diofant objects true and false.

>>> True >> False
1
>>> true >> false
false

class diofant.logic.boolalg.Equivalent(*args)

Equivalence relation.

Equivalent(A, B) is True iff A and B are both True or both False.

Returns True if all of the arguments are logically equivalent. Returns False otherwise.

Examples

>>> Equivalent(False, False, False)
true
>>> Equivalent(True, False, False)
false
>>> Equivalent(x, And(x, True))
true

class diofant.logic.boolalg.ITE(*args)

If then else clause.

ITE(A, B, C) evaluates and returns the result of B if A is true else it returns the result of C.

Examples

>>> ITE(True, False, True)
false
>>> ITE(Or(True, False), And(True, True), Xor(True, True))
true
>>> ITE(x, y, z)
ITE(x, y, z)
>>> ITE(True, x, y)
x
>>> ITE(False, x, y)
y
>>> ITE(x, y, y)
y

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

diofant.logic.boolalg.to_cnf(expr, simplify=False)

Convert expr to Conjunctive Normal Form (CNF).

If simplify is True, the expr is evaluated to its simplest CNF form.

Examples

>>> to_cnf(~(a | b) | c)
(c | ~a) & (c | ~b)
>>> to_cnf((a | b) & (a | ~a), True)
a | b

See also

is_cnf

diofant.logic.boolalg.to_dnf(expr, simplify=False)

Convert expr to Disjunctive Normal Form (DNF).

If simplify is True, the expr is evaluated to its simplest DNF form.

Examples

>>> to_dnf(b & (a | c))
(a & b) | (b & c)
>>> to_dnf((a & b) | (a & ~b) | (b & c) | (~b & c), True)
a | c

See also

is_dnf

diofant.logic.boolalg.is_cnf(expr)

Checks if expr is in Conjunctive Normal Form (CNF).

A logical expression is in CNF if it is a conjunction of one or more clauses, where a clause is a disjunction of literals.

Examples

>>> is_cnf(a | b | c)
True
>>> is_cnf(a & b & c)
True
>>> is_cnf((a & b) | c)
False

See also

to_cnf, is_dnf, is_nnf

diofant.logic.boolalg.is_dnf(expr)

Checks if expr is in Disjunctive Normal Form (DNF).

A logical expression is in DNF if it is a disjunction of one or more clauses, where a clause is a conjunction of literals.

Examples

>>> is_dnf(a | b | c)
True
>>> is_dnf(a & b & c)
True
>>> is_dnf((a & b) | c)
True
>>> is_dnf(a & (b | c))
False

See also

to_dnf, is_cnf, is_nnf

The following functions can be used to handle Negation Normal Forms

diofant.logic.boolalg.to_nnf(expr, simplify=True)

Converts expr to Negation Normal Form (NNF).

If simplify is True, the result contains no redundant clauses.

Examples

>>> to_nnf(~((~a & ~b) | (c & d)))
(a | b) & (~c | ~d)
>>> to_nnf(Equivalent(a >> b, b >> a))
(a | ~b | (a & ~b)) & (b | ~a | (b & ~a))

See also

is_nnf

diofant.logic.boolalg.is_nnf(expr, simplified=True)

Checks if expr is in Negation Normal Form (NNF).

A logical expression is in NNF if the negation operator is only applied to literals and the only other allowed boolean functions are conjunction and disjunction.

If simplified is True, checks if result contains no redundant clauses.

Examples

>>> is_nnf(a & b | ~c)
True
>>> is_nnf((a | ~a) & (b | c))
False
>>> is_nnf((a | ~a) & (b | c), False)
True
>>> is_nnf(~(a & b) | c)
False
>>> is_nnf((a >> b) & (b >> a))
False

See also

to_nnf, is_cnf, is_dnf

Simplification and equivalence-testing

diofant.logic.boolalg.simplify_logic(expr, form='cnf', deep=True)

This function simplifies a boolean function to its simplified version in SOP or POS form. The return type is an Or or And object in Diofant.

Parameters:

• expr (string or boolean expression)

• form (string (‘cnf’ or ‘dnf’), default to ‘cnf’.) – Selects the normal form in which the result is returned.

• deep (boolean (default True)) – indicates whether to recursively simplify any non-boolean functions contained within the input.

Examples

>>> b = (~x & ~y & ~z) | (~x & ~y & z)
>>> simplify_logic(b)
~x & ~y

>>> sympify(b)
(z & ~x & ~y) | (~x & ~y & ~z)
>>> simplify_logic(_)
~x & ~y

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

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.

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

diofant.logic.inference.satisfiable(expr, algorithm='dpll2', all_models=False)

Check satisfiability of a propositional sentence. Returns a model when it succeeds. Returns {true: true} for trivially true expressions.

On setting all_models to True, if given expr is satisfiable then returns a generator of models. However, if expr is unsatisfiable then returns a generator containing the single element False.

Examples

>>> satisfiable(a & ~b)
{a: True, b: False}
>>> satisfiable(a & ~a)
False
>>> satisfiable(True)
{true: True}
>>> next(satisfiable(a & ~a, all_models=True))
False
>>> models = satisfiable((a >> b) & b, all_models=True)
>>> next(models)
{a: False, b: True}
>>> next(models)
{a: True, b: True}
>>> def use_models(models):
...     for model in models:
...         if model:
...             # Do something with the model.
...             return model
...         else:
...             # Given expr is unsatisfiable.
...             print('UNSAT')
>>> use_models(satisfiable(a >> ~a, all_models=True))
{a: False}
>>> use_models(satisfiable(a ^ a, all_models=True))
UNSAT