FIT4050 · Monash University
Knowledge representation, computational logic, and automated reasoning
- Credit points
- 6
- Level
- 4
- Workload
- —
- Faculty
- Information Technology
What it covers
This unit introduces the formal representation of knowledge and the computational methods used to reason about it in intelligent and verified systems. It covers propositional and first-order logic, satisfiability modulo theories for reasoning within decidable fragments of first-order logic, and representations used in efficient automated reasoning, ranging from CNF and NNF encodings to decision diagrams and other tractable compiled forms. You will study the core decision procedures and symbolic techniques that underpin modern reasoning engines, theorem provers and model-checking tools, and learn how these are used for proof, search, and state-space exploration. Through theoretical and practical work, you will encode and solve concrete problems drawn from artificial intelligence and formal verification, such as planning, scheduling, diagnosis, consistency checking, reachability, and the verification of safety and liveness properties in software and hardware systems. The unit develops the ability to model problems precisely, select appropriate reasoning formalisms and tools, and critically assess the strengths and limitations of contemporary automated reasoning methods.
Assessment
Assessment not published yet.
When and where
Not offered in 2027, or offerings not published yet.