• Students can recognize whether a given problem is amenable to

techniques from automated reasoning (K4).

• Students can formulate and reason about algorithms operating on

formulas and expressions (K4).

• Students can tell why proofs found by computational logic are

formally rigorous (K4).

• Students can analyze a given logical calculus for 'soundness' and

'completeness' (K4).

• Students can apply a given logical calculus to a given problem (K4).
• Students have some understanding of the computational limitations of

computational logic (K4).

• Syntax and semantics of propositional logic, equational logic, and

predicate logic.

• Classical formal reasoning mechanisms for the aforementioned logics

(e.g., resolution, Knuth-Bendix completion).

• Some ideas for managing extremely large search spaces.