Syllabus - CS421

MA410 Artificial Intelligence


MA426 Fourier Analysis

CS424 Object Oriented Programming


CS428 Advanced Operating Systems & Automated Reasoning

There will be a practical assessment in computing, carrying up to 30% of the total marks
Propositional calculus: truth functions and propositional connectives, logical validity, an axiomatization and completeness meta-theorem.
First order theories: axioms, theorems, interpretations, logical validity.
Rules of inference: binary resolution, hyper-resolution, demodulation, subsumption, proof by contradiction.
The set of Support Strategy (and weighting). Introduction to UNIX on Dangan workstations.
Using the OTTER computer package: puzzles, logic circuit design/validation, theorem proving.
A first order for Peano arithmetic.
Godel's Incompleteness Theorem: statement, indication of proof (Godel numbers, recursive functions, represntable functions), relevance to automated theorem proving.
Back to 4th Year Syllabus