Boolean Formulas¶

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

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)

Python

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

Sage Live

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

We can create a truth table from a formula:

Sage

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

Python

>>> from sage.all import *
>>> 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
>>> f.truthtable(end=Integer(3))
a      b      c      value
False  False  False  True
False  False  True   True
False  True   False  False
>>> f.truthtable(start=Integer(4))
a      b      c      value
True   False  False  True
True   False  True   False
True   True   False  True
True   True   True   True
>>> propcalc.formula("a").truthtable()
a      value
False  False
True   True

Sage Live

f.truthtable()
f.truthtable(end=3)
f.truthtable(start=4)
propcalc.formula("a").truthtable()

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

Sage

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

Python

>>> from sage.all import *
>>> f.evaluate({'a':True, 'b':False, 'c':True})
False
>>> f.evaluate({'a':False, 'b':False, 'c':True})
True

Sage Live

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

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

Sage

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)

Python

>>> from sage.all import *
>>> f.convert_cnf_table()
>>> f
(a|~b|c)&(a|~b|~c)&(~a|b|~c)
>>> f.convert_cnf_recur()
>>> f
(a|~b|c)&(a|~b|~c)&(~a|b|~c)

Sage Live

f.convert_cnf_table()
f
f.convert_cnf_recur()
f

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

Sage

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

Python

>>> from sage.all import *
>>> f = propcalc.formula("a|b")
>>> f.is_satisfiable()
True
>>> f = f & ~f
>>> f.is_satisfiable()
False
>>> f.is_contradiction()
True
>>> f = f | ~f
>>> f.is_tautology()
True

Sage Live

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

The equality operator compares semantic equivalence:

Sage

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

Python

>>> from sage.all import *
>>> f = propcalc.formula("(a|b)&c")
>>> g = propcalc.formula("c&(b|a)")
>>> f == g
True
>>> g = propcalc.formula("a|b&c")
>>> f == g
False

Sage Live

f = propcalc.formula("(a|b)&c")
g = propcalc.formula("c&(b|a)")
f == g
g = propcalc.formula("a|b&c")
f == g

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

Sage

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

Python

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

Sage Live

propcalc.formula("")
propcalc.formula("a&b~(c|(d)")
propcalc.formula("a&&b")
propcalc.formula("a&b a")

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

Sage

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

Python

>>> from sage.all import *
>>> 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

Sage Live

propcalc.formula("~a&9b")

AUTHORS:

Chris Gorecki (2006): initial version
Paul Scurek (2013-08-03): added polish_notation, full_tree, updated docstring formatting
Paul Scurek (2013-08-08): added implies()

class sage.logic.boolformula.BooleanFormula(exp, tree, vo)[source]¶

Bases: object

Boolean formulas.

INPUT:

self – calling object
exp – string; this contains the boolean expression to be manipulated
tree – list; this contains the parse tree of the expression
vo – list; this contains the variables in the expression, in the order that they appear; each variable only occurs once in the list

add_statement(other, op)[source]¶

Combine two formulas with the given operator.

INPUT:

other – instance of BooleanFormula; this is the formula on the right of the operator
op – 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

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)

Python

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

>>> s.add_statement(f, '->')
(a&b)->(c^d)

Sage Live

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

convert_cnf()[source]¶

Convert boolean formula to conjunctive normal form.

OUTPUT: an instance of BooleanFormula in conjunctive normal form

EXAMPLES:

This example illustrates how to convert a formula to cnf:

Sage

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)

Python

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

Sage Live

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

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

Sage

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

Python

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

Sage Live

t = propcalc.formula("a ^ b <-> c")
t.convert_cnf_table(); t
t == s

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()[source]¶

Convert boolean formula to conjunctive normal form.

OUTPUT: an instance of BooleanFormula in conjunctive normal form

EXAMPLES:

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

Sage

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)

Python

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

Sage Live

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

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()[source]¶

Convert boolean formula to conjunctive normal form.

OUTPUT: an instance of BooleanFormula in conjunctive normal form

EXAMPLES:

This example illustrates how to convert a formula to cnf:

Sage

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)

Python

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

Sage Live

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

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

Sage

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

Python

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

Sage Live

t = propcalc.formula("a ^ b <-> c")
t.convert_cnf_table(); t
t == s

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()[source]¶

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

EXAMPLES:

Sage

sage: import sage.logic.propcalc as propcalc
sage: s = propcalc.formula("a^b<->c")
sage: s.convert_expression(); s
a^b<->c

Python

>>> from sage.all import *
>>> import sage.logic.propcalc as propcalc
>>> s = propcalc.formula("a^b<->c")
>>> s.convert_expression(); s
a^b<->c

Sage Live

import sage.logic.propcalc as propcalc
s = propcalc.formula("a^b<->c")
s.convert_expression(); s

convert_opt(tree)[source]¶

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

INPUT:

tree – 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

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

Python

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

Sage Live

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

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.

dist_not(tree)[source]¶

Distribute ‘~’ operators over ‘&’ and ‘|’ operators.

INPUT:

tree a list; this represents a branch of a parse tree

OUTPUT: a new list

EXAMPLES:

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

Sage

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

Python

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

Sage Live

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

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.

dist_ors(tree)[source]¶

Distribute ‘|’ over ‘&’.

INPUT:

tree – list; this represents a branch of a parse tree

OUTPUT: a new list

EXAMPLES:

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

Sage

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

Python

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

Sage Live

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

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.

equivalent(other)[source]¶

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

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

Python

>>> from sage.all import *
>>> import sage.logic.propcalc as propcalc
>>> f = propcalc.formula("(a|b)&c")
>>> g = propcalc.formula("c&(a|b)")
>>> f.equivalent(g)
True

>>> g = propcalc.formula("a|b&c")
>>> f.equivalent(g)
False

Sage Live

import sage.logic.propcalc as propcalc
f = propcalc.formula("(a|b)&c")
g = propcalc.formula("c&(a|b)")
f.equivalent(g)
g = propcalc.formula("a|b&c")
f.equivalent(g)

evaluate(var_values)[source]¶

Evaluate a formula for the given input values.

INPUT:

var_values – 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

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

Python

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

Sage Live

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

full_tree()[source]¶

Return a full syntax parse tree of the calling 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

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

Python

>>> from sage.all import *
>>> import sage.logic.propcalc as propcalc
>>> s = propcalc.formula("a->(b&c)")
>>> s.full_tree()
['->', 'a', ['&', 'b', 'c']]

>>> t = propcalc.formula("a & ((~b | c) ^ a -> c) <-> ~b")
>>> t.full_tree()
['<->', ['&', 'a', ['->', ['^', ['|', ['~', 'b'], 'c'], 'a'], 'c']], ['~', 'b']]

>>> f = propcalc.formula("~~(a&~b)")
>>> f.full_tree()
['~', ['~', ['&', 'a', ['~', 'b']]]]

Sage Live

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

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)[source]¶

Determine if bit c of the number x is 1.

INPUT:

x – integer; this is the number from which to take the bit
c – 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

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

Python

>>> from sage.all import *
>>> import sage.logic.propcalc as propcalc
>>> s = propcalc.formula("a&b")
>>> s.get_bit(Integer(2), Integer(1))
True
>>> s.get_bit(Integer(8), Integer(0))
False

Sage Live

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

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

Sage

sage: s.get_bit(64, 7)
False

Python

>>> from sage.all import *
>>> s.get_bit(Integer(64), Integer(7))
False

Sage Live

s.get_bit(64, 7)

Nor is it an error to use a negative number:

Sage

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

Python

>>> from sage.all import *
>>> s.get_bit(-Integer(1), Integer(3))
False
>>> s.get_bit(Integer(64), -Integer(1))
True
>>> s.get_bit(Integer(64), -Integer(2))
False

Sage Live

s.get_bit(-1, 3)
s.get_bit(64, -1)
s.get_bit(64, -2)

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)[source]¶

Return the next operator in a string.

INPUT:

str – 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

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

Python

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

Sage Live

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

Note

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

iff(other)[source]¶

Combine two formulas with the <-> operator.

INPUT:

other – boolean formula; this is the formula on the right side of the operator

OUTPUT:

A boolean formula of the form self <-> other.

EXAMPLES:

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

Sage

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)

Python

>>> from sage.all import *
>>> import sage.logic.propcalc as propcalc
>>> s = propcalc.formula("a&b")
>>> f = propcalc.formula("c^d")
>>> s.iff(f)
(a&b)<->(c^d)

Sage Live

import sage.logic.propcalc as propcalc
s = propcalc.formula("a&b")
f = propcalc.formula("c^d")
s.iff(f)

ifthen(other)[source]¶

Combine two formulas with the -> operator.

INPUT:

other – boolean formula; this is the formula on the right side of the operator

OUTPUT:

A boolean formula of the form self -> other.

EXAMPLES:

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

Sage

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)

Python

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

Sage Live

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

implies(other)[source]¶

Determine if calling formula implies other formula.

INPUT:

self – calling object
other – instance of BooleanFormula

OUTPUT: a boolean value to be determined as follows:

True – if self implies other
False – if self does not imply ``other

EXAMPLES:

This example illustrates determining if one formula implies another:

Sage

sage: import sage.logic.propcalc as propcalc
sage: f = propcalc.formula("a<->b")
sage: g = propcalc.formula("b->a")
sage: f.implies(g)
True

Python

>>> from sage.all import *
>>> import sage.logic.propcalc as propcalc
>>> f = propcalc.formula("a<->b")
>>> g = propcalc.formula("b->a")
>>> f.implies(g)
True

Sage Live

import sage.logic.propcalc as propcalc
f = propcalc.formula("a<->b")
g = propcalc.formula("b->a")
f.implies(g)

Sage

sage: h = propcalc.formula("a->(a|~b)")
sage: i = propcalc.formula("a")
sage: h.implies(i)
False

Python

>>> from sage.all import *
>>> h = propcalc.formula("a->(a|~b)")
>>> i = propcalc.formula("a")
>>> h.implies(i)
False

Sage Live

h = propcalc.formula("a->(a|~b)")
i = propcalc.formula("a")
h.implies(i)

Python

>>> from sage.all import *
>>> h = propcalc.formula("a->(a|~b)")
>>> i = propcalc.formula("a")
>>> h.implies(i)
False

Sage Live

h = propcalc.formula("a->(a|~b)")
i = propcalc.formula("a")
h.implies(i)

AUTHORS:

Paul Scurek (2013-08-08)

is_consequence(*hypotheses)[source]¶

Determine if self (the desired conclusion) is a logical consequence of the hypotheses. The function call is_consequence(conclusion, *hypotheses) is a synonym for conclusion.is_consequence(*hypotheses).

INPUT:

*hypotheses – instances of BooleanFormula

OUTPUT: a boolean value to be determined as follows:

True – if self (the desired conclusion) is a logical consequence of the set of hypotheses
False – if self (the desired conclusion) is not a logical consequence of the set of hypotheses

EXAMPLES:

Sage

sage: from sage.logic.propcalc import formula
sage: formula("a | b").is_consequence(formula("b"))
True
sage: formula("a & b").is_consequence(formula("b"))
False
sage: formula("b").is_consequence(formula("a"), formula("a -> b"))
True
sage: formula("b -> a").is_consequence(formula("a -> b"))
False
sage: formula("~b -> ~a").is_consequence(formula("a -> b"))
True

Python

>>> from sage.all import *
>>> from sage.logic.propcalc import formula
>>> formula("a | b").is_consequence(formula("b"))
True
>>> formula("a & b").is_consequence(formula("b"))
False
>>> formula("b").is_consequence(formula("a"), formula("a -> b"))
True
>>> formula("b -> a").is_consequence(formula("a -> b"))
False
>>> formula("~b -> ~a").is_consequence(formula("a -> b"))
True

Sage Live

from sage.logic.propcalc import formula
formula("a | b").is_consequence(formula("b"))
formula("a & b").is_consequence(formula("b"))
formula("b").is_consequence(formula("a"), formula("a -> b"))
formula("b -> a").is_consequence(formula("a -> b"))
formula("~b -> ~a").is_consequence(formula("a -> b"))

Sage

sage: f, g, h = propcalc.get_formulas("a & ~b", "c -> b", "c | e")
sage: propcalc.formula("a & e").is_consequence(f, g, h)
True
sage: i = propcalc.formula("a & ~e")
sage: i.is_consequence(f, g, h)
False
sage: from sage.logic.boolformula import is_consequence
sage: is_consequence(i, f, g, h)
False
sage: is_consequence(propcalc.formula("((p <-> q) & r) -> ~c"), f, g, h)
True

Python

>>> from sage.all import *
>>> f, g, h = propcalc.get_formulas("a & ~b", "c -> b", "c | e")
>>> propcalc.formula("a & e").is_consequence(f, g, h)
True
>>> i = propcalc.formula("a & ~e")
>>> i.is_consequence(f, g, h)
False
>>> from sage.logic.boolformula import is_consequence
>>> is_consequence(i, f, g, h)
False
>>> is_consequence(propcalc.formula("((p <-> q) & r) -> ~c"), f, g, h)
True

Sage Live

f, g, h = propcalc.get_formulas("a & ~b", "c -> b", "c | e")
propcalc.formula("a & e").is_consequence(f, g, h)
i = propcalc.formula("a & ~e")
i.is_consequence(f, g, h)
from sage.logic.boolformula import is_consequence
is_consequence(i, f, g, h)
is_consequence(propcalc.formula("((p <-> q) & r) -> ~c"), f, g, h)

Python

>>> from sage.all import *
>>> f, g, h = propcalc.get_formulas("a & ~b", "c -> b", "c | e")
>>> propcalc.formula("a & e").is_consequence(f, g, h)
True
>>> i = propcalc.formula("a & ~e")
>>> i.is_consequence(f, g, h)
False
>>> from sage.logic.boolformula import is_consequence
>>> is_consequence(i, f, g, h)
False
>>> is_consequence(propcalc.formula("((p <-> q) & r) -> ~c"), f, g, h)
True

Sage Live

f, g, h = propcalc.get_formulas("a & ~b", "c -> b", "c | e")
propcalc.formula("a & e").is_consequence(f, g, h)
i = propcalc.formula("a & ~e")
i.is_consequence(f, g, h)
from sage.logic.boolformula import is_consequence
is_consequence(i, f, g, h)
is_consequence(propcalc.formula("((p <-> q) & r) -> ~c"), f, g, h)

Only a tautology is a logical consequence of an empty set of formulas:

Sage

sage: propcalc.formula("a | ~a").is_consequence()
True
sage: propcalc.formula("a | b").is_consequence()
False

Python

>>> from sage.all import *
>>> propcalc.formula("a | ~a").is_consequence()
True
>>> propcalc.formula("a | b").is_consequence()
False

Sage Live

propcalc.formula("a | ~a").is_consequence()
propcalc.formula("a | b").is_consequence()

AUTHORS:

Paul Scurek (2013-08-12)

is_contradiction()[source]¶

Determine if the formula is always False.

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

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

Python

>>> from sage.all import *
>>> import sage.logic.propcalc as propcalc
>>> f = propcalc.formula("a&~a")
>>> f.is_contradiction()
True

>>> f = propcalc.formula("a|~a")
>>> f.is_contradiction()
False

>>> f = propcalc.formula("a|b")
>>> f.is_contradiction()
False

Sage Live

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

is_satisfiable()[source]¶

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

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

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

Python

>>> from sage.all import *
>>> import sage.logic.propcalc as propcalc
>>> f = propcalc.formula("a|b")
>>> f.is_satisfiable()
True

>>> g = f & (~f)
>>> g.is_satisfiable()
False

Sage Live

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

is_tautology()[source]¶

Determine if the formula is always True.

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

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

Python

>>> from sage.all import *
>>> import sage.logic.propcalc as propcalc
>>> f = propcalc.formula("a|~a")
>>> f.is_tautology()
True

>>> f = propcalc.formula("a&~a")
>>> f.is_tautology()
False

>>> f = propcalc.formula("a&b")
>>> f.is_tautology()
False

Sage Live

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

length()[source]¶

Return the length of self.

OUTPUT:

The length of the Boolean formula. This is the number of operators plus the number of variables (counting multiplicity). Parentheses are ignored.

EXAMPLES:

Sage

sage: import sage.logic.propcalc as propcalc
sage: s = propcalc.formula("a")
sage: s.length()
1
sage: s = propcalc.formula("(a)")
sage: s.length()
1
sage: s = propcalc.formula("~a")
sage: s.length()
2
sage: s = propcalc.formula("a -> b")
sage: s.length()
3
sage: s = propcalc.formula("alpha -> beta")
sage: s.length()
3
sage: s = propcalc.formula("a -> a")
sage: s.length()
3
sage: s = propcalc.formula("~(a -> b)")
sage: s.length()
4
sage: s = propcalc.formula("((a&b)|(a&c))->~d")
sage: s.length()
10

Python

>>> from sage.all import *
>>> import sage.logic.propcalc as propcalc
>>> s = propcalc.formula("a")
>>> s.length()
1
>>> s = propcalc.formula("(a)")
>>> s.length()
1
>>> s = propcalc.formula("~a")
>>> s.length()
2
>>> s = propcalc.formula("a -> b")
>>> s.length()
3
>>> s = propcalc.formula("alpha -> beta")
>>> s.length()
3
>>> s = propcalc.formula("a -> a")
>>> s.length()
3
>>> s = propcalc.formula("~(a -> b)")
>>> s.length()
4
>>> s = propcalc.formula("((a&b)|(a&c))->~d")
>>> s.length()
10

Sage Live

import sage.logic.propcalc as propcalc
s = propcalc.formula("a")
s.length()
s = propcalc.formula("(a)")
s.length()
s = propcalc.formula("~a")
s.length()
s = propcalc.formula("a -> b")
s.length()
s = propcalc.formula("alpha -> beta")
s.length()
s = propcalc.formula("a -> a")
s.length()
s = propcalc.formula("~(a -> b)")
s.length()
s = propcalc.formula("((a&b)|(a&c))->~d")
s.length()

polish_notation()[source]¶

Convert the calling boolean formula into polish notation.

OUTPUT: string representation of the formula in polish notation

EXAMPLES:

This example illustrates converting a formula to polish notation:

Sage

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'

Python

>>> from sage.all import *
>>> import sage.logic.propcalc as propcalc
>>> f = propcalc.formula("~~a|(c->b)")
>>> f.polish_notation()
'|~~a->cb'

>>> g = propcalc.formula("(a|~b)->c")
>>> g.polish_notation()
'->|a~bc'

Sage Live

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

AUTHORS:

Paul Scurek (2013-08-03)

reduce_op(tree)[source]¶

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

INPUT:

tree – 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

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

Python

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

Sage Live

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

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.

satformat()[source]¶

Return the satformat representation of a boolean formula.

OUTPUT: the satformat of the formula as a string

EXAMPLES:

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

Sage

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'

Python

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

Sage Live

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

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(), then satformat() will call convert_cnf(). Please see the notes for convert_cnf() and convert_cnf_recur() for performance issues.

to_infix(tree)[source]¶

Convert a parse tree from prefix to infix form.

INPUT:

tree – 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

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

Python

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

Sage Live

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

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.

tree()[source]¶

Return the parse tree of this boolean expression.

OUTPUT: the parse tree as a nested list

EXAMPLES:

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

Sage

sage: import sage.logic.propcalc as propcalc
sage: s = propcalc.formula("man -> monkey & human")
sage: s.tree()
['->', 'man', ['&', 'monkey', 'human']]

Python

>>> from sage.all import *
>>> import sage.logic.propcalc as propcalc
>>> s = propcalc.formula("man -> monkey & human")
>>> s.tree()
['->', 'man', ['&', 'monkey', 'human']]

Sage Live

import sage.logic.propcalc as propcalc
s = propcalc.formula("man -> monkey & human")
s.tree()

Sage

sage: f = propcalc.formula("a & ((~b | c) ^ a -> c) <-> ~b")
sage: f.tree()
['<->',
 ['&', 'a', ['->', ['^', ['|', ['~', 'b', None], 'c'], 'a'], 'c']],
 ['~', 'b', None]]

Python

>>> from sage.all import *
>>> f = propcalc.formula("a & ((~b | c) ^ a -> c) <-> ~b")
>>> f.tree()
['<->',
 ['&', 'a', ['->', ['^', ['|', ['~', 'b', None], 'c'], 'a'], 'c']],
 ['~', 'b', None]]

Sage Live

f = propcalc.formula("a & ((~b | c) ^ a -> c) <-> ~b")
f.tree()

Python

>>> from sage.all import *
>>> f = propcalc.formula("a & ((~b | c) ^ a -> c) <-> ~b")
>>> f.tree()
['<->',
 ['&', 'a', ['->', ['^', ['|', ['~', 'b', None], 'c'], 'a'], 'c']],
 ['~', 'b', None]]

Sage Live

f = propcalc.formula("a & ((~b | c) ^ a -> c) <-> ~b")
f.tree()

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)[source]¶

Return a truth table for the calling formula.

INPUT:

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

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

Python

>>> from sage.all import *
>>> import sage.logic.propcalc as propcalc
>>> s = propcalc.formula("a&b|~(c|a)")
>>> 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

Sage Live

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

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

Sage

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

Python

>>> from sage.all import *
>>> s.truthtable(Integer(1), Integer(5))
a      b      c      value
False  False  True   False
False  True   False  True
False  True   True   False
True   False  False  False

Sage Live

s.truthtable(1, 5)

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.

sage.logic.boolformula.is_consequence(self, *hypotheses)[source]¶

INPUT:

*hypotheses – instances of BooleanFormula

OUTPUT: a boolean value to be determined as follows:

True – if self (the desired conclusion) is a logical consequence of the set of hypotheses
False – if self (the desired conclusion) is not a logical consequence of the set of hypotheses

EXAMPLES:

Sage

sage: from sage.logic.propcalc import formula
sage: formula("a | b").is_consequence(formula("b"))
True
sage: formula("a & b").is_consequence(formula("b"))
False
sage: formula("b").is_consequence(formula("a"), formula("a -> b"))
True
sage: formula("b -> a").is_consequence(formula("a -> b"))
False
sage: formula("~b -> ~a").is_consequence(formula("a -> b"))
True

Python

>>> from sage.all import *
>>> from sage.logic.propcalc import formula
>>> formula("a | b").is_consequence(formula("b"))
True
>>> formula("a & b").is_consequence(formula("b"))
False
>>> formula("b").is_consequence(formula("a"), formula("a -> b"))
True
>>> formula("b -> a").is_consequence(formula("a -> b"))
False
>>> formula("~b -> ~a").is_consequence(formula("a -> b"))
True

Sage Live

from sage.logic.propcalc import formula
formula("a | b").is_consequence(formula("b"))
formula("a & b").is_consequence(formula("b"))
formula("b").is_consequence(formula("a"), formula("a -> b"))
formula("b -> a").is_consequence(formula("a -> b"))
formula("~b -> ~a").is_consequence(formula("a -> b"))

Sage

sage: f, g, h = propcalc.get_formulas("a & ~b", "c -> b", "c | e")
sage: propcalc.formula("a & e").is_consequence(f, g, h)
True
sage: i = propcalc.formula("a & ~e")
sage: i.is_consequence(f, g, h)
False
sage: from sage.logic.boolformula import is_consequence
sage: is_consequence(i, f, g, h)
False
sage: is_consequence(propcalc.formula("((p <-> q) & r) -> ~c"), f, g, h)
True

Python

>>> from sage.all import *
>>> f, g, h = propcalc.get_formulas("a & ~b", "c -> b", "c | e")
>>> propcalc.formula("a & e").is_consequence(f, g, h)
True
>>> i = propcalc.formula("a & ~e")
>>> i.is_consequence(f, g, h)
False
>>> from sage.logic.boolformula import is_consequence
>>> is_consequence(i, f, g, h)
False
>>> is_consequence(propcalc.formula("((p <-> q) & r) -> ~c"), f, g, h)
True

Sage Live

f, g, h = propcalc.get_formulas("a & ~b", "c -> b", "c | e")
propcalc.formula("a & e").is_consequence(f, g, h)
i = propcalc.formula("a & ~e")
i.is_consequence(f, g, h)
from sage.logic.boolformula import is_consequence
is_consequence(i, f, g, h)
is_consequence(propcalc.formula("((p <-> q) & r) -> ~c"), f, g, h)

Python

>>> from sage.all import *
>>> f, g, h = propcalc.get_formulas("a & ~b", "c -> b", "c | e")
>>> propcalc.formula("a & e").is_consequence(f, g, h)
True
>>> i = propcalc.formula("a & ~e")
>>> i.is_consequence(f, g, h)
False
>>> from sage.logic.boolformula import is_consequence
>>> is_consequence(i, f, g, h)
False
>>> is_consequence(propcalc.formula("((p <-> q) & r) -> ~c"), f, g, h)
True

Sage Live

f, g, h = propcalc.get_formulas("a & ~b", "c -> b", "c | e")
propcalc.formula("a & e").is_consequence(f, g, h)
i = propcalc.formula("a & ~e")
i.is_consequence(f, g, h)
from sage.logic.boolformula import is_consequence
is_consequence(i, f, g, h)
is_consequence(propcalc.formula("((p <-> q) & r) -> ~c"), f, g, h)

Only a tautology is a logical consequence of an empty set of formulas:

Sage

sage: propcalc.formula("a | ~a").is_consequence()
True
sage: propcalc.formula("a | b").is_consequence()
False

Python

>>> from sage.all import *
>>> propcalc.formula("a | ~a").is_consequence()
True
>>> propcalc.formula("a | b").is_consequence()
False

Sage Live

propcalc.formula("a | ~a").is_consequence()
propcalc.formula("a | b").is_consequence()

AUTHORS:

Paul Scurek (2013-08-12)