logic.py

#______________________________________________________________________________


class FolKB(KB):

    """A knowledge base consisting of first-order definite clauses.
    >>> kb0 = FolKB([expr('Farmer(Mac)'), expr('Rabbit(Pete)'),
    ...              expr('(Rabbit(r) & Farmer(f)) ==> Hates(f, r)')])
    >>> kb0.tell(expr('Rabbit(Flopsie)'))
    >>> kb0.retract(expr('Rabbit(Pete)'))
    >>> kb0.ask(expr('Hates(Mac, x)'))[x]
    Flopsie
    >>> kb0.ask(expr('Wife(Pete, x)'))
    False
    """

    def __init__(self, initial_clauses=[]):
        self.clauses = []  # inefficient: no indexing
        for clause in initial_clauses:
            self.tell(clause)

    def tell(self, sentence):
        if is_definite_clause(sentence):
            self.clauses.append(sentence)
        else:
            raise Exception("Not a definite clause: %s" % sentence)

    def ask_generator(self, query):
        return fol_bc_ask(self, query)

    def retract(self, sentence):
        self.clauses.remove(sentence)

    def fetch_rules_for_goal(self, goal):
        return self.clauses


def test_ask(query, kb=None):
    q = expr(query)
    vars = variables(q)
    answers = fol_bc_ask(kb or test_kb, q)
    return sorted([pretty(dict((x, v) for x, v in list(a.items()) if x in vars))
                   for a in answers],
                  key=repr)

test_kb = FolKB(
    list(map(expr, ['Farmer(Mac)',
                    'Rabbit(Pete)',
                    'Mother(MrsMac, Mac)',
                    'Mother(MrsRabbit, Pete)',
                    '(Rabbit(r) & Farmer(f)) ==> Hates(f, r)',
                    '(Mother(m, c)) ==> Loves(m, c)',
                    '(Mother(m, r) & Rabbit(r)) ==> Rabbit(m)',
                    '(Farmer(f)) ==> Human(f)',
                    # Note that this order of conjuncts
                    # would result in infinite recursion:
                    #'(Human(h) & Mother(m, h)) ==> Human(m)'
                    '(Mother(m, h) & Human(h)) ==> Human(m)'
                    ]))
)

crime_kb = FolKB(
    list(map(expr,
             ['(American(x) & Weapon(y) & Sells(x, y, z) & Hostile(z)) ==> Criminal(x)',
              'Owns(Nono, M1)',
              'Missile(M1)',
              '(Missile(x) & Owns(Nono, x)) ==> Sells(West, x, Nono)',
              'Missile(x) ==> Weapon(x)',
              'Enemy(x, America) ==> Hostile(x)',
              'American(West)',
              'Enemy(Nono, America)'
              ]))
)


def fol_bc_ask(KB, query):
    """A simple backward-chaining algorithm for first-order logic. [Fig. 9.6]
    KB should be an instance of FolKB, and goals a list of literals.
    >>> test_ask('Farmer(x)')
    ['{x: Mac}']
    >>> test_ask('Human(x)')
    ['{x: Mac}', '{x: MrsMac}']
    >>> test_ask('Hates(x, y)')
    ['{x: Mac, y: MrsRabbit}', '{x: Mac, y: Pete}']
    >>> test_ask('Loves(x, y)')
    ['{x: MrsMac, y: Mac}', '{x: MrsRabbit, y: Pete}']
    >>> test_ask('Rabbit(x)')
    ['{x: MrsRabbit}', '{x: Pete}']
    >>> test_ask('Criminal(x)', crime_kb)
    ['{x: West}']
    """
    return fol_bc_or(KB, query, {})


def fol_bc_or(KB, goal, theta):
    for rule in KB.fetch_rules_for_goal(goal):
        lhs, rhs = parse_definite_clause(standardize_variables(rule))
        for theta1 in fol_bc_and(KB, lhs, unify(rhs, goal, theta)):
            yield theta1


def fol_bc_and(KB, goals, theta):
    if theta is None:
        pass
    elif not goals:
        yield theta
    else:
        first, rest = goals[0], goals[1:]
        for theta1 in fol_bc_or(KB, subst(theta, first), theta):
            for theta2 in fol_bc_and(KB, rest, theta1):
                yield theta2

#______________________________________________________________________________

# Example application (not in the book).
# You can use the Expr class to do symbolic differentiation.  This used to be
# a part of AI; now it is considered a separate field, Symbolic Algebra.


def diff(y, x):
    """Return the symbolic derivative, dy/dx, as an Expr.
    However, you probably want to simplify the results with simp.
    >>> diff(x * x, x)
    ((x * 1) + (x * 1))
    >>> simp(diff(x * x, x))
    (2 * x)
    """
    if y == x:
        return ONE
    elif not y.args:
        return ZERO
    else:
        u, op, v = y.args[0], y.op, y.args[-1]
        if op == '+':
            return diff(u, x) + diff(v, x)
        elif op == '-' and len(args) == 1:
            return -diff(u, x)
        elif op == '-':
            return diff(u, x) - diff(v, x)
        elif op == '*':
            return u * diff(v, x) + v * diff(u, x)
        elif op == '/':
            return (v*diff(u, x) - u*diff(v, x)) / (v * v)
        elif op == '**' and isnumber(x.op):
            return (v * u ** (v - 1) * diff(u, x))
        elif op == '**':
            return (v * u ** (v - 1) * diff(u, x)
                    + u ** v * Expr('log')(u) * diff(v, x))
        elif op == 'log':
            return diff(u, x) / u
        else:
            raise ValueError("Unknown op: %s in diff(%s, %s)" % (op, y, x))


def simp(x):
    if not x.args:
        return x
    args = list(map(simp, x.args))
    u, op, v = args[0], x.op, args[-1]
    if op == '+':
        if v == ZERO:
            return u
        if u == ZERO:
            return v
        if u == v:
            return TWO * u
        if u == -v or v == -u:
            return ZERO
    elif op == '-' and len(args) == 1:
        if u.op == '-' and len(u.args) == 1:
            return u.args[0]  # --y ==> y
    elif op == '-':
        if v == ZERO:
            return u
        if u == ZERO:
            return -v
        if u == v:
            return ZERO
        if u == -v or v == -u:
            return ZERO
    elif op == '*':
        if u == ZERO or v == ZERO:
            return ZERO
        if u == ONE:
            return v
        if v == ONE:
            return u
        if u == v:
            return u ** 2
    elif op == '/':
        if u == ZERO:
            return ZERO
        if v == ZERO:
            return Expr('Undefined')
        if u == v:
            return ONE
        if u == -v or v == -u:
            return ZERO
    elif op == '**':
        if u == ZERO:
            return ZERO
        if v == ZERO:
            return ONE
        if u == ONE:
            return ONE
        if v == ONE:
            return u
    elif op == 'log':
        if u == ONE:
            return ZERO
    else:
        raise ValueError("Unknown op: " + op)
    # If we fall through to here, we can not simplify further
    return Expr(op, *args)


def d(y, x):
    "Differentiate and then simplify."
    return simp(diff(y, x))

#_________________________________________________________________________

# Utilities for doctest cases
# These functions print their arguments in a standard order
# to compensate for the random order in the standard representation


def pretty(x):
    t = type(x)
    if t is dict:
        return pretty_dict(x)
    elif t is set:
        return pretty_set(x)
    else:
        return repr(x)


def pretty_dict(d):
    """Return dictionary d's repr but with the items sorted.
    >>> pretty_dict({'m': 'M', 'a': 'A', 'r': 'R', 'k': 'K'})
    "{'a': 'A', 'k': 'K', 'm': 'M', 'r': 'R'}"
    >>> pretty_dict({z: C, y: B, x: A})
    '{x: A, y: B, z: C}'
    """
    return '{%s}' % ', '.join('%r: %r' % (k, v)
                              for k, v in sorted(list(d.items()), key=repr))


def pretty_set(s):
    """Return set s's repr but with the items sorted.
    >>> pretty_set(set(['A', 'Q', 'F', 'K', 'Y', 'B']))
    "set(['A', 'B', 'F', 'K', 'Q', 'Y'])"
    >>> pretty_set(set([z, y, x]))
    'set([x, y, z])'
    """
    return 'set(%r)' % sorted(s, key=repr)


def pp(x):
    print(pretty(x))


def ppsubst(s):
    """Pretty-print substitution s"""
    ppdict(s)


def ppdict(d):
    print(pretty_dict(d))


def ppset(s):
    print(pretty_set(s))

#________________________________________________________________________


class logicTest:

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

### An earlier version of the code failed on this:
>>> dpll_satisfiable(A & ~B & C & (A | ~D) & (~E | ~D) & (C | ~D) & (~A | ~F) & (E | ~F) & (~D | ~F) & (B | ~C | D) & (A | ~E | F) & (~A | E | D))
{B: False, C: True, A: True, F: False, D: True, E: 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))
"""