resolution steps are applied to CNFcomplete for FOL
Initial State: Knowledge base (KB) of axioms and negated theorem in CNF
Operators: Resolution rule picks 2 clauses and adds new clause
Goal Test: Does KB contain the empty clause?
Study of the design of intelligent agents,with intelligent behavior in artifacts.