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
Determine if the formulas are logically consistent.
INPUT:
OUTPUT:
A boolean value to be determined as follows:
EXAMPLES:
This example illustrates determining if formulas are logically consistent.
sage: import sage.logic.propcalc
sage: f, g, h, i = propcalc.get_formulas("a<->b", "~b->~c", "d|g", "c&a")
sage: 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
AUTHORS:
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
Convert statements and parse trees into instances of BooleanFormula.
INPUT:
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)]
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)
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)
AUTHORS:
Determine if consequence is a valid consequence of the set of formulas in *formulas.
INPUT:
OUTPUT:
A boolean value to be determined as follows:
EXAMPLES:
This example illustrates determining if a formula is a valid consequence of a set of other formulas:
sage: import sage.logic.propcalc as propcalc
sage: f, g, h, i = propcalc.get_formulas("a&~b", "c->b", "c|e", "e&a")
sage: propcalc.valid_consequence(i, f, g, h)
True
sage: j = propcalc.formula("a&~e")
sage: propcalc.valid_consequence(j, f, g, h)
False
sage: k = propcalc.formula("((p<->q)&r)->~c")
sage: propcalc.valid_consequence(k, f, g, h)
True
AUTHORS: