Module that creates boolean formulas as instances of the BooleanFormula class.

Formulas consist of the operators &, |, ~, ^, ->, <->, corresponding to and, or, not, xor, if...then, if and only if. Operators can be applied to variables that consist of a leading letter and trailing underscores and alphanumerics. Parentheses may be used to explicitly show order of operation.

EXAMPLES:

Create boolean formulas and combine them with ifthen() method:

sage: import sage.logic.propcalc as propcalc
sage: f = propcalc.formula("a&((b|c)^a->c)<->b")
sage: g = propcalc.formula("boolean<->algebra")
sage: (f&~g).ifthen(f)
((a&((b|c)^a->c)<->b)&(~(boolean<->algebra)))->(a&((b|c)^a->c)<->b)

We can create a truth table from a formula:

sage: f.truthtable()
a      b      c      value
False  False  False  True
False  False  True   True
False  True   False  False
False  True   True   False
True   False  False  True
True   False  True   False
True   True   False  True
True   True   True   True
sage: f.truthtable(end=3)
a      b      c      value
False  False  False  True
False  False  True   True
False  True   False  False
sage: f.truthtable(start=4)
a      b      c      value
True   False  False  True
True   False  True   False
True   True   False  True
True   True   True   True
sage: propcalc.formula("a").truthtable()
a      value
False  False
True   True

Now we can evaluate the formula for a given set of inputs:

sage: f.evaluate({'a':True, 'b':False, 'c':True})
False
sage: f.evaluate({'a':False, 'b':False, 'c':True})
True

And we can convert a boolean formula to conjunctive normal form:

sage: f.convert_cnf_table()
sage: f
(a|~b|c)&(a|~b|~c)&(~a|b|~c)
sage: f.convert_cnf_recur()
sage: f
(a|~b|c)&(a|~b|~c)&(~a|b|~c)

Or determine if an expression is satisfiable, a contradiction, or a tautology:

sage: f = propcalc.formula("a|b")
sage: f.is_satisfiable()
True
sage: f = f & ~f
sage: f.is_satisfiable()
False
sage: f.is_contradiction()
True
sage: f = f | ~f
sage: f.is_tautology()
True

The equality operator compares semantic equivalence:

sage: f = propcalc.formula("(a|b)&c")
sage: g = propcalc.formula("c&(b|a)")
sage: f == g
True
sage: g = propcalc.formula("a|b&c")
sage: f == g
False

It is an error to create a formula with bad syntax:

sage: propcalc.formula("")
Traceback (most recent call last):
...
SyntaxError: malformed statement
sage: propcalc.formula("a&b~(c|(d)")
Traceback (most recent call last):
...
SyntaxError: malformed statement
sage: propcalc.formula("a&&b")
Traceback (most recent call last):
...
SyntaxError: malformed statement
sage: propcalc.formula("a&b a")
Traceback (most recent call last):
...
SyntaxError: malformed statement

It is also an error to not abide by the naming conventions:

sage: propcalc.formula("~a&9b")
Traceback (most recent call last):
...
NameError: invalid variable name 9b: identifiers must begin with a letter and contain only alphanumerics and underscores

AUTHORS:

  • Chris Gorecki (2006): initial version
  • Paul Scurek (2013-08-03): added polish_notation, full_tree, updated docstring formatting
class sage.logic.boolformula.BooleanFormula(exp, tree, vo)

Initialize the data fields

INPUT:

  • self – calling object
  • exp – a string. This contains the boolean expression to be manipulated
  • tree – a list. This contains the parse tree of the expression.
  • vo – a list. This contains the variables in the expression, in the order that they appear. Each variable only occurs once in the list.

OUTPUT:

None

EXAMPLES:

This example illustrates the creation of a statement.

sage: import sage.logic.propcalc as propcalc
sage: s = propcalc.formula("a&b|~(c|a)")
sage: s
a&b|~(c|a)
add_statement(other, op)

Combine two formulas with the given operator.

INPUT:

  • self – calling object. This is the formula on the left side of the operator.
  • other – instance of BooleanFormula class. This is the formula on the right of the operator.
  • op – a string. This is the operator used to combine the two formulas.

OUTPUT:

The result as an instance of BooleanFormula

EXAMPLES:

This example shows how to create a new formula from two others.

sage: import sage.logic.propcalc as propcalc
sage: s = propcalc.formula("a&b")
sage: f = propcalc.formula("c^d")
sage: s.add_statement(f, '|')
(a&b)|(c^d)
sage: s.add_statement(f, '->')
(a&b)->(c^d)
convert_cnf()

Convert boolean formula to conjunctive normal form.

INPUT:

  • self – calling object

OUTPUT:

An instance of BooleanFormula in conjunctive normal form

EXAMPLES:

This example illustrates how to convert a formula to cnf.

sage: import sage.logic.propcalc as propcalc
sage: s = propcalc.formula("a ^ b <-> c")
sage: s.convert_cnf()
sage: s
(a|b|~c)&(a|~b|c)&(~a|b|c)&(~a|~b|~c)

We now show that convert_cnf() and convert_cnf_table() are aliases.

sage: t = propcalc.formula("a ^ b <-> c")
sage: t.convert_cnf_table(); t
(a|b|~c)&(a|~b|c)&(~a|b|c)&(~a|~b|~c)
sage: t == s
True

Note

This method creates the cnf parse tree by examining the logic table of the formula. Creating the table requires \(O(2^n)\) time where \(n\) is the number of variables in the formula.

convert_cnf_recur()

Convert boolean formula to conjunctive normal form.

INPUT:

  • self – calling object

OUTPUT:

An instance of BooleanFormula in conjunctive normal form

EXAMPLES:

This example hows how to convert a formula to conjunctive normal form.

sage: import sage.logic.propcalc as propcalc
sage: s = propcalc.formula("a^b<->c")
sage: s.convert_cnf_recur()
sage: s
(~a|a|c)&(~b|a|c)&(~a|b|c)&(~b|b|c)&(~c|a|b)&(~c|~a|~b)

Note

This function works by applying a set of rules that are guaranteed to convert the formula. Worst case the converted expression has an O(2^n) increase in size (and time as well), but if the formula is already in CNF (or close to) it is only O(n).

This function can require an exponential blow up in space from the original expression. This in turn can require large amounts of time. Unless a formula is already in (or close to) being in cnf convert_cnf() is typically preferred, but results can vary.

convert_cnf_table()

Convert boolean formula to conjunctive normal form.

INPUT:

  • self – calling object

OUTPUT:

An instance of BooleanFormula in conjunctive normal form

EXAMPLES:

This example illustrates how to convert a formula to cnf.

sage: import sage.logic.propcalc as propcalc
sage: s = propcalc.formula("a ^ b <-> c")
sage: s.convert_cnf()
sage: s
(a|b|~c)&(a|~b|c)&(~a|b|c)&(~a|~b|~c)

We now show that convert_cnf() and convert_cnf_table() are aliases.

sage: t = propcalc.formula("a ^ b <-> c")
sage: t.convert_cnf_table(); t
(a|b|~c)&(a|~b|c)&(~a|b|c)&(~a|~b|~c)
sage: t == s
True

Note

This method creates the cnf parse tree by examining the logic table of the formula. Creating the table requires \(O(2^n)\) time where \(n\) is the number of variables in the formula.

convert_expression()

Convert the string representation of a formula to conjunctive normal form.

INPUT:

  • self – calling object

OUTPUT:

None

EXAMPLES:

We show how the converted formula is printed in conjunctive normal form.

sage: import sage.logic.propcalc as propcalc
sage: s = propcalc.formula("a^b<->c")
sage: s.convert_cnf_recur(); s  #long time
(~a|a|c)&(~b|a|c)&(~a|b|c)&(~b|b|c)&(~c|a|b)&(~c|~a|~b)
convert_opt(tree)

Convert a parse tree to the tuple form used by bool_opt.

INPUT:

  • self – calling object
  • tree – a list. This is a branch of a parse tree and can only contain the ‘&’, ‘|’ and ‘~’ operators along with variables.

OUTPUT:

A 3-tuple

EXAMPLES:

This example illustrates the conversion of a formula into its corresponding tuple.

sage: import sage.logic.propcalc as propcalc, sage.logic.logicparser as logicparser
sage: s = propcalc.formula("a&(b|~c)")
sage: tree = ['&', 'a', ['|', 'b', ['~', 'c', None]]]
sage: logicparser.apply_func(tree, s.convert_opt)
('and', ('prop', 'a'), ('or', ('prop', 'b'), ('not', ('prop', 'c'))))

Note

This function only works on one branch of the parse tree. To apply the function to every branch of a parse tree, pass the function as an argument in apply_func() in logicparser.py.

dist_not(tree)

Distribute ~ operators over & and | operators.

INPUT:

  • self calling object
  • tree a list. This represents a branch of a parse tree.

OUTPUT:

A new list

EXAMPLES:

This example illustrates the distribution of ‘~’ over ‘&’.

sage: import sage.logic.propcalc as propcalc, sage.logic.logicparser as logicparser
sage: s = propcalc.formula("~(a&b)")
sage: tree = ['~', ['&', 'a', 'b'], None]
sage: logicparser.apply_func(tree, s.dist_not) #long time
['|', ['~', 'a', None], ['~', 'b', None]]

Note

This function only operates on a single branch of a parse tree. To apply the function to an entire parse tree, pass the function as an argument to apply_func() in logicparser.py.

dist_ors(tree)

Distribute | over &.

INPUT:

  • self – calling object
  • tree – a list. This represents a branch of a parse tree.

OUTPUT:

A new list

EXAMPLES:

This example illustrates the distribution of ‘|’ over ‘&’.

sage: import sage.logic.propcalc as propcalc, sage.logic.logicparser as logicparser
sage: s = propcalc.formula("(a&b)|(a&c)")
sage: tree = ['|', ['&', 'a', 'b'], ['&', 'a', 'c']]
sage: logicparser.apply_func(tree, s.dist_ors) #long time
['&', ['&', ['|', 'a', 'a'], ['|', 'b', 'a']], ['&', ['|', 'a', 'c'], ['|', 'b', 'c']]]

Note

This function only operates on a single branch of a parse tree. To apply the function to an entire parse tree, pass the function as an argument to apply_func() in logicparser.py.

equivalent(other)

Determine if two formulas are semantically equivalent.

INPUT:

  • self – calling object
  • other – instance of BooleanFormula class.

OUTPUT:

A boolean value to be determined as follows:

True - if the two formulas are logically equivalent

False - if the two formulas are not logically equivalent

EXAMPLES:

This example shows how to check for logical equivalence.

sage: import sage.logic.propcalc as propcalc
sage: f = propcalc.formula("(a|b)&c")
sage: g = propcalc.formula("c&(a|b)")
sage: f.equivalent(g)
True
sage: g = propcalc.formula("a|b&c")
sage: f.equivalent(g)
False
evaluate(var_values)

Evaluate a formula for the given input values.

INPUT:

  • self – calling object
  • var_values – a dictionary. This contains the pairs of variables and their boolean values.

OUTPUT:

The result of the evaluation as a boolean.

EXAMPLES:

This example illustrates the evaluation of a boolean formula.

sage: import sage.logic.propcalc as propcalc
sage: f = propcalc.formula("a&b|c")
sage: f.evaluate({'a':False, 'b':False, 'c':True})
True
sage: f.evaluate({'a':True, 'b':False, 'c':False})
False
full_tree()

Return a full syntax parse tree of the calling formula.

INPUT:

  • self – calling object. This is a boolean formula.

OUTPUT:

The full syntax parse tree as a nested list

EXAMPLES:

This example shows how to find the full syntax parse tree of a formula.

sage: import sage.logic.propcalc as propcalc
sage: s = propcalc.formula("a->(b&c)")
sage: s.full_tree()
['->', 'a', ['&', 'b', 'c']]
sage: t = propcalc.formula("a & ((~b | c) ^ a -> c) <-> ~b")
sage: t.full_tree()
['<->', ['&', 'a', ['->', ['^', ['|', ['~', 'b'], 'c'], 'a'], 'c']], ['~', 'b']]
sage: f = propcalc.formula("~~(a&~b)")
sage: f.full_tree()
['~', ['~', ['&', 'a', ['~', 'b']]]]

Note

This function is used by other functions in the logic module that perform syntactic operations on a boolean formula.

AUTHORS:

  • Paul Scurek (2013-08-03)
get_bit(x, c)

Determine if bit c of the number x is 1.

INPUT:

  • self – calling object
  • x – an integer. This is the number from which to take the bit.
  • c – an integer. This is the but number to be taken, where 0 is the low order bit.

OUTPUT:

A boolean to be determined as follows:

True - if bit c of x is 1

False - if bit c of x is not 1

EXAMPLES:

This example illustrates the use of get_bit().

sage: import sage.logic.propcalc as propcalc
sage: s = propcalc.formula("a&b")
sage: s.get_bit(2, 1)
True
sage: s.get_bit(8, 0)
False

It is not an error to have a bit out of range.

sage: s.get_bit(64, 7)
False

Nor is it an error to use a negative number.

sage: s.get_bit(-1, 3)
False
sage: s.get_bit(64, -1)
True
sage: s.get_bit(64, -2)
False

Note

The 0 bit is the low order bit. Errors should be handled gracefully by a return of false, and negative numbers x always return false while a negative c will index from the high order bit.

get_next_op(str)

Return the next operator in a string.

INPUT:

  • self – calling object
  • str – a string. This contains a logical expression.

OUTPUT:

The next operator as a string

EXAMPLES:

This example illustrates how to find the next operator in a formula.

sage: import sage.logic.propcalc as propcalc
sage: s = propcalc.formula("f&p")
sage: s.get_next_op("abra|cadabra")
'|'

Note

The parameter str is not necessarily the string representation of the calling object.

iff(other)

Combine two formulas with the <-> operator.

INPUT:

  • self – calling object. This is the formula on the left side of the operator.
  • other – a boolean formula. This is the formula on the right side of the operator.

OUTPUT:

A boolean formula of the following form:

self <-> other

EXAMPLES:

This example illustrates how to combine two formulas with ‘<->’.

sage: import sage.logic.propcalc as propcalc
sage: s = propcalc.formula("a&b")
sage: f = propcalc.formula("c^d")
sage: s.iff(f)
(a&b)<->(c^d)
ifthen(other)

Combine two formulas with the -> operator.

INPUT:

  • self – calling object. This is the formula on the left side of the operator.
  • other – a boolean formula. This is the formula on the right side of the operator.

OUTPUT:

A boolean formula of the following form:

self -> other

EXAMPLES:

This example illustrates how to combine two formulas with ‘->’.

sage: import sage.logic.propcalc as propcalc
sage: s = propcalc.formula("a&b")
sage: f = propcalc.formula("c^d")
sage: s.ifthen(f)
(a&b)->(c^d)
is_contradiction()

Determine if the formula is always False.

INPUT:

  • self – calling object

OUTPUT:

A boolean value to be determined as follows:

True - if the formula is a contradiction

False - if the formula is not a contradiction

EXAMPLES:

This example illustrates how to check if a formula is a contradiction.

sage: import sage.logic.propcalc as propcalc
sage: f = propcalc.formula("a&~a")
sage: f.is_contradiction()
True
sage: f = propcalc.formula("a|~a")
sage: f.is_contradiction()
False
sage: f = propcalc.formula("a|b")
sage: f.is_contradiction()
False
is_satisfiable()

Determine if the formula is True for some assignment of values.

INPUT:

  • self – calling object

OUTPUT:

A boolean value to be determined as follows:

True - if there is an assignment of values that makes the formula True

False - if the formula cannot be made True by any assignment of values

EXAMPLES:

This example illustrates how to check a formula for satisfiability.

sage: import sage.logic.propcalc as propcalc
sage: f = propcalc.formula("a|b")
sage: f.is_satisfiable()
True
sage: g = f & (~f)
sage: g.is_satisfiable()
False
is_tautology()

Determine if the formula is always True.

INPUT:

  • self – calling object

OUTPUT:

A boolean value to be determined as follows:

True - if the formula is a tautology

False - if the formula is not a tautology

EXAMPLES:

This example illustrates how to check if a formula is a tautology.

sage: import sage.logic.propcalc as propcalc
sage: f = propcalc.formula("a|~a")
sage: f.is_tautology()
True
sage: f = propcalc.formula("a&~a")
sage: f.is_tautology()
False
sage: f = propcalc.formula("a&b")
sage: f.is_tautology()
False
polish_notation()

Convert the calling boolean formula into polish notation

INPUT:

  • self – calling object

OUTPUT:

A string representation of the formula in polish notation.

EXAMPLES:

This example illustrates converting a formula to polish notation.

sage: import sage.logic.propcalc as propcalc
sage: f = propcalc.formula("~~a|(c->b)")
sage: f.polish_notation()
'|~~a->cb'
sage: g = propcalc.formula("(a|~b)->c")
sage: g.polish_notation()
'->|a~bc'

AUTHORS:

  • Paul Scurek (2013-08-03)
reduce_op(tree)

Convert if-and-only-if, if-then, and xor operations to operations only involving and/or operations.

INPUT:

  • self – calling object
  • tree – a list. This represents a branch of a parse tree.

OUTPUT:

A new list with no ^, ->, or <-> as first element of list.

EXAMPLES:

This example illustrates the use of reduce_op() with apply_func().

sage: import sage.logic.propcalc as propcalc, sage.logic.logicparser as logicparser
sage: s = propcalc.formula("a->b^c")
sage: tree = ['->', 'a', ['^', 'b', 'c']]
sage: logicparser.apply_func(tree, s.reduce_op)
['|', ['~', 'a', None], ['&', ['|', 'b', 'c'], ['~', ['&', 'b', 'c'], None]]]

Note

This function only operates on a single branch of a parse tree. To apply the function to an entire parse tree, pass the function as an argument to apply_func() in logicparser.py.

satformat()

Return the satformat representation of a boolean formula.

INPUT:

  • self – calling object

OUTPUT:

The satformat of the formula as a string

EXAMPLES:

This example illustrates how to find the satformat of a formula.

sage: import sage.logic.propcalc as propcalc
sage: f = propcalc.formula("a&((b|c)^a->c)<->b")
sage: f.convert_cnf()
sage: f
(a|~b|c)&(a|~b|~c)&(~a|b|~c)
sage: f.satformat()
'p cnf 3 0\n1 -2 3 0 1 -2 -3 \n0 -1 2 -3'

Note

See www.cs.ubc.ca/~hoos/SATLIB/Benchmarks/SAT/satformat.ps for a description of satformat.

If the instance of boolean formula has not been converted to CNF form by a call to convert_cnf() or convert_cnf_recur() satformat() will call convert_cnf(). Please see the notes for convert_cnf() and convert_cnf_recur() for performance issues.

to_infix(tree)

Convert a parse tree from prefix to infix form.

INPUT:

  • self – calling object
  • tree – a list. This represents a branch of a parse tree.

OUTPUT:

A new list

EXAMPLES:

This example shows how to convert a parse tree from prefix to infix form.

sage: import sage.logic.propcalc as propcalc, sage.logic.logicparser as logicparser
sage: s = propcalc.formula("(a&b)|(a&c)")
sage: tree = ['|', ['&', 'a', 'b'], ['&', 'a', 'c']]
sage: logicparser.apply_func(tree, s.to_infix)
[['a', '&', 'b'], '|', ['a', '&', 'c']]

Note

This function only operates on a single branch of a parse tree. To apply the function to an entire parse tree, pass the function as an argument to apply_func() in logicparser.py.

tree()

Return the parse tree of this boolean expression.

INPUT:

  • self – calling object

OUTPUT:

The parse tree as a nested list

EXAMPLES:

This example illustrates how to find the parse tree of a boolean formula.

sage: import sage.logic.propcalc as propcalc
sage: s = propcalc.formula("man -> monkey & human")
sage: s.tree()
['->', 'man', ['&', 'monkey', 'human']]
sage: f = propcalc.formula("a & ((~b | c) ^ a -> c) <-> ~b")
sage: f.tree()
['<->',
 ['&', 'a', ['->', ['^', ['|', ['~', 'b', None], 'c'], 'a'], 'c']],
 ['~', 'b', None]]

Note

This function is used by other functions in the logic module that perform semantic operations on a boolean formula.

truthtable(start=0, end=-1)

Return a truth table for the calling formula.

INPUT:

  • self – calling object
  • start – (default: 0) an integer. This is the first row of the truth table to be created.
  • end – (default: -1) an integer. This is the laste row of the truth table to be created.

OUTPUT:

The truth table as a 2-D array

EXAMPLES:

This example illustrates the creation of a truth table.

sage: import sage.logic.propcalc as propcalc
sage: s = propcalc.formula("a&b|~(c|a)")
sage: s.truthtable()
a      b      c      value
False  False  False  True
False  False  True   False
False  True   False  True
False  True   True   False
True   False  False  False
True   False  True   False
True   True   False  True
True   True   True   True

We can now create a truthtable of rows 1 to 4, inclusive.

sage: s.truthtable(1, 5)
a      b      c      value
False  False  True   False
False  True   False  True
False  True   True   False
True   False  False  False

Note

Each row of the table corresponds to a binary number, with each variable associated to a column of the number, and taking on a true value if that column has a value of 1. Please see the logictable module for details. The function returns a table that start inclusive and end exclusive so truthtable(0, 2) will include row 0, but not row 2.

When sent with no start or end parameters, this is an exponential time function requiring O(2**n) time, where n is the number of variables in the expression.

Previous topic

Module that creates formulas of propositional calculus

Next topic

Module used to evaluate boolean formulas

This Page