logic.py

               #'(Human(h) & Mother(m, h)) ==> Human(m)'
               '(Mother(m, h) & Human(h)) ==> Human(m)'
               ])
)


def fol_bc_ask(KB, goals, theta={}):
    """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}']
    """

    if goals == []:
        yield theta
        raise StopIteration()
    
    q1 = subst(theta, goals[0])

    for r in KB.clauses:
        sar = standardize_apart(r)
        
        # Split into head and body
        if is_symbol(sar.op):
            head = sar
            body = []
        elif sar.op == '>>': # sar = (Body1 & Body2 & ...) >> Head
            head = sar.args[1]
            body = sar.args[0] # as conjunction
        else:
            raise Exception("Invalid clause in FolKB: %s" % r)

        theta1 = unify(head, q1, {})

        if theta1 is not None:
            if body == []:
                new_goals = goals[1:]
            else:
                new_goals = conjuncts(body) + goals[1:]

            for ans in fol_bc_ask(KB, new_goals, subst_compose(theta1, theta)):
                yield ans

    raise StopIteration()

def subst_compose (s1, s2):
    """Return the substitution which is equivalent to applying s2 to
    the result of applying s1 to an expression.

    >>> s1 = {x: A, y: B}
    >>> s2 = {z: x, x: C}
    >>> p = F(x) & G(y) & expr('H(z)')
    >>> subst(s1, p)
    ((F(A) & G(B)) & H(z))
    >>> subst(s2, p)
    ((F(C) & G(y)) & H(x))
    
    >>> subst(s2, subst(s1, p))
    ((F(A) & G(B)) & H(x))
    >>> subst(subst_compose(s1, s2), p)
    ((F(A) & G(B)) & H(x))

    >>> subst(s1, subst(s2, p))
    ((F(C) & G(B)) & H(A))
    >>> subst(subst_compose(s2, s1), p)
    ((F(C) & G(B)) & H(A))
    >>> ppsubst(subst_compose(s1, s2))
    {x: A, y: B, z: x}
    >>> ppsubst(subst_compose(s2, s1))
    {x: C, y: B, z: A}
    >>> subst(subst_compose(s1, s2), p) == subst(s2, subst(s1, p))
    True
    >>> subst(subst_compose(s2, s1), p) == subst(s1, subst(s2, p))
    True
    """
    sc = {}
    for x, v in s1.items():
        if s2.has_key(v):
            w = s2[v]
            sc[x] = w # x -> v -> w
        else:
            sc[x] = v
    for x, v in s2.items():
        if not (s1.has_key(x)):
            sc[x] = v
        # otherwise s1[x] preemptys s2[x]
    return sc

#______________________________________________________________________________

# 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 = 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 == dict:
        return pretty_dict(x)
    elif t == set:
        return pretty_set(x)

def pretty_dict(d):
    """Print the dictionary d.
    
    Prints a string representation of the dictionary
    with keys in sorted order according to their string
    representation: {a: A, d: D, ...}.
    >>> 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}'
    """

    def format(k, v):
        return "%s: %s" % (repr(k), repr(v))

    ditems = d.items()
    ditems.sort(key=str)
    k, v = ditems[0]
    dpairs = format(k, v)
    for (k, v) in ditems[1:]:
        dpairs += (', ' + format(k, v))
    return '{%s}' % dpairs

def pretty_set(s):
    """Print the set s.

    >>> 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])'
    """

    slist = list(s)
    slist.sort(key=str)
    return 'set(%s)' % slist

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

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