- 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.
|
