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 ofBooleanFormula
OUTPUT: a boolean value to be determined as follows:
True
– if the formulas are logically consistentFalse
– 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)