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