Propositional Calculus

Formulas consist of the following operators:

  • & – 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.

AUTHORS:

  • Chris Gorecki (2006): initial version, propcalc, boolformula, logictable, logicparser, booleval

  • Michael Greenberg – boolopt

  • Paul Scurek (2013-08-05): updated docstring formatting

  • Paul Scurek (2013-08-12): added get_formulas(), consistent(), valid_consequence()

EXAMPLES:

We can create boolean formulas in different ways:

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

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

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

sage: f.evaluate({'a':True, 'b':False, 'c':True})
False
sage: f.evaluate({'a':False, 'b':False, 'c':True})
True
>>> from sage.all import *
>>> f.evaluate({'a':True, 'b':False, 'c':True})
False
>>> 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)
>>> 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)

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

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

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

It is also an error to not abide by the naming conventions.
>>> 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.logic.propcalc.consistent(*formulas)[source]

Determine if the formulas are logically consistent.

INPUT:

  • *formulas – instances of BooleanFormula

OUTPUT: a boolean value to be determined as follows:

  • True – if the formulas are logically consistent

  • False – if the formulas are not logically consistent

EXAMPLES:

This example illustrates determining if formulas are logically consistent.

sage: f, g, h, i = propcalc.get_formulas("a<->b", "~b->~c", "d|g", "c&a")
sage: propcalc.consistent(f, g, h, i)
True
>>> from sage.all import *
>>> f, g, h, i = propcalc.get_formulas("a<->b", "~b->~c", "d|g", "c&a")
>>> propcalc.consistent(f, g, h, i)
True

sage: j, k, l, m = propcalc.get_formulas("a<->b", "~b->~c", "d|g", "c&~a")
sage: propcalc.consistent(j, k ,l, m)
False
>>> from sage.all import *
>>> j, k, l, m = propcalc.get_formulas("a<->b", "~b->~c", "d|g", "c&~a")
>>> propcalc.consistent(j, k ,l, m)
False

AUTHORS:

  • Paul Scurek (2013-08-12)

sage.logic.propcalc.formula(s)[source]

Return an instance of BooleanFormula.

INPUT:

  • s – string that contains a logical expression

OUTPUT: an instance of BooleanFormula

EXAMPLES:

This example illustrates ways to create a boolean formula:

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

We now demonstrate some possible errors:

sage: propcalc.formula("((a&b)")
Traceback (most recent call last):
...
SyntaxError: malformed statement
sage: propcalc.formula("_a&b")
Traceback (most recent call last):
...
NameError: invalid variable name _a: identifiers must begin with a letter and contain only alphanumerics and underscores
>>> from sage.all import *
>>> propcalc.formula("((a&b)")
Traceback (most recent call last):
...
SyntaxError: malformed statement
>>> propcalc.formula("_a&b")
Traceback (most recent call last):
...
NameError: invalid variable name _a: identifiers must begin with a letter and contain only alphanumerics and underscores
sage.logic.propcalc.get_formulas(*statements)[source]

Convert statements and parse trees into instances of BooleanFormula.

INPUT:

  • *statements – strings or lists; a list must be a full syntax parse tree of a formula, and a string must be a string representation of a formula

OUTPUT: the converted formulas in a list

EXAMPLES:

This example illustrates converting strings into boolean formulas.

sage: f = "a&(~c<->d)"
sage: g = "d|~~b"
sage: h = "~(a->c)<->(d|~c)"
sage: propcalc.get_formulas(f, g, h)
[a&(~c<->d), d|~~b, ~(a->c)<->(d|~c)]
>>> from sage.all import *
>>> f = "a&(~c<->d)"
>>> g = "d|~~b"
>>> h = "~(a->c)<->(d|~c)"
>>> propcalc.get_formulas(f, g, h)
[a&(~c<->d), d|~~b, ~(a->c)<->(d|~c)]

sage: A, B, C = propcalc.get_formulas("(a&b)->~c", "c", "~(a&b)")
sage: A
(a&b)->~c
sage: B
c
sage: C
~(a&b)
>>> from sage.all import *
>>> A, B, C = propcalc.get_formulas("(a&b)->~c", "c", "~(a&b)")
>>> A
(a&b)->~c
>>> B
c
>>> C
~(a&b)

We can also convert parse trees into formulas.

sage: t = ['a']
sage: u = ['~', ['|', ['&', 'a', 'b'], ['~', 'c']]]
sage: v = "b->(~c<->d)"
sage: formulas= propcalc.get_formulas(t, u, v)
sage: formulas[0]
a
sage: formulas[1]
~((a&b)|~c)
sage: formulas[2]
b->(~c<->d)
>>> from sage.all import *
>>> t = ['a']
>>> u = ['~', ['|', ['&', 'a', 'b'], ['~', 'c']]]
>>> v = "b->(~c<->d)"
>>> formulas= propcalc.get_formulas(t, u, v)
>>> formulas[Integer(0)]
a
>>> formulas[Integer(1)]
~((a&b)|~c)
>>> formulas[Integer(2)]
b->(~c<->d)

AUTHORS:

  • Paul Scurek (2013-08-12)