Formulas consist of the following operators:
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:
EXAMPLES:
We can create boolean formulas in different ways:
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 input:
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
Return an instance of BooleanFormula
INPUT:
OUTPUT:
An instance of BooleanFormula
EXAMPLES:
This example illustrates ways to create a boolean formula.
sage: import sage.logic.propcalc as propcalc
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)
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