You cannot select more than 25 topics
Topics must start with a letter or number, can include dashes ('-') and can be up to 35 characters long.
79 lines
1.5 KiB
Plaintext
79 lines
1.5 KiB
Plaintext
### PropKB
|
|
>>> kb = PropKB()
|
|
>>> kb.tell(A & B)
|
|
>>> kb.tell(B >> C)
|
|
>>> kb.ask(C) ## The result {} means true, with no substitutions
|
|
{}
|
|
>>> kb.ask(P)
|
|
False
|
|
>>> kb.retract(B)
|
|
>>> kb.ask(C)
|
|
False
|
|
|
|
>>> pl_true(P, {})
|
|
>>> pl_true(P | Q, {P: True})
|
|
True
|
|
|
|
# Notice that the function pl_true cannot reason by cases:
|
|
>>> pl_true(P | ~P)
|
|
|
|
# However, tt_true can:
|
|
>>> tt_true(P | ~P)
|
|
True
|
|
|
|
# The following are tautologies from [Fig. 7.11]:
|
|
>>> tt_true("(A & B) <=> (B & A)")
|
|
True
|
|
>>> tt_true("(A | B) <=> (B | A)")
|
|
True
|
|
>>> tt_true("((A & B) & C) <=> (A & (B & C))")
|
|
True
|
|
>>> tt_true("((A | B) | C) <=> (A | (B | C))")
|
|
True
|
|
>>> tt_true("~~A <=> A")
|
|
True
|
|
>>> tt_true("(A >> B) <=> (~B >> ~A)")
|
|
True
|
|
>>> tt_true("(A >> B) <=> (~A | B)")
|
|
True
|
|
>>> tt_true("(A <=> B) <=> ((A >> B) & (B >> A))")
|
|
True
|
|
>>> tt_true("~(A & B) <=> (~A | ~B)")
|
|
True
|
|
>>> tt_true("~(A | B) <=> (~A & ~B)")
|
|
True
|
|
>>> tt_true("(A & (B | C)) <=> ((A & B) | (A & C))")
|
|
True
|
|
>>> tt_true("(A | (B & C)) <=> ((A | B) & (A | C))")
|
|
True
|
|
|
|
# The following are not tautologies:
|
|
>>> tt_true(A & ~A)
|
|
False
|
|
>>> tt_true(A & B)
|
|
False
|
|
|
|
### [Fig. 7.13]
|
|
>>> alpha = expr("~P12")
|
|
>>> to_cnf(Fig[7,13] & ~alpha)
|
|
((~P12 | B11) & (~P21 | B11) & (P12 | P21 | ~B11) & ~B11 & P12)
|
|
>>> tt_entails(Fig[7,13], alpha)
|
|
True
|
|
>>> pl_resolution(PropKB(Fig[7,13]), alpha)
|
|
True
|
|
|
|
### [Fig. 7.15]
|
|
>>> pl_fc_entails(Fig[7,15], expr('SomethingSilly'))
|
|
False
|
|
|
|
### Unification:
|
|
>>> unify(x, x, {})
|
|
{}
|
|
>>> unify(x, 3, {})
|
|
{x: 3}
|
|
|
|
|
|
>>> to_cnf((P&Q) | (~P & ~Q))
|
|
((~P | P) & (~Q | P) & (~P | Q) & (~Q | Q))
|
|
|