Let's implement a SAT-solver (AIMA ch. 7).

The boolean satisfiability problem (SAT) was recognized as one of the
first NP-complete problems[1]; Norvig implemented it in AIMA-Lisp by
expanding the truth table for a proposition and figuring out whether
any of the rows were satisfied.[2]

The truth-table method is somewhat inefficient, however; and a few
algorithms have been developed (such as DPLL[3] and WalkSAT[4]) which
are more efficient.

Gomes, et al. wrote a good survey of the relevant algorithms[5]; we
can't avoid implementing something like this if we're ever going to
have logical agents, unfortunately.

Footnotes:
[1] http://en.wikipedia.org/wiki/Boolean_satisfiability_problem

[2] http://www.cs.berkeley.edu/~russell/code/logic/algorithms/prop.lisp

[3] http://en.wikipedia.org/wiki/DPLL_algorithm

[4] http://en.wikipedia.org/wiki/WalkSAT

[5] http://www.cs.cornell.edu/gomes/papers/SATSolvers-KR-Handbook.pdf