See TUMonline

An applied introduction to automated and interactive reasoning, climbing through progressively more expressive logics and the proof-search methods each demands. The emphasis is on how modern reasoning systems work and how to use them; foundational results are stated precisely, with proofs sketched at the level of ideas. Four units of five lectures and one exercise session each.

**Unit 1: SAT.** Satisfiability, CNF, NP-completeness. DPLL and conflict-driven clause learning. Solver engineering. Proof certificates: DRAT, LRAT, and checking by a small trusted checker. Encodings and applications.

**Unit 2: SMT.** SMT-LIB and the common theories. Eager reduction and where it fails. DPLL(T). Theory solvers: incremental simplex with Farkas certificates, congruence closure, arrays. Nelson-Oppen combination. Z3 and cvc5.

**Unit 3: First-order theorem proving.** Semi-decidability and decidable fragments. Unification and resolution. Reduction orderings, LPO and KBO, and the problem of equality. Superposition, redundancy, saturation. Prover architecture; TPTP; E and Vampire.

**Unit 4: Interactive theorem proving in Lean.** Dependent type theory, Curry-Howard, the trusted kernel and the de Bruijn criterion. Proof terms and tactics. Automation over Mathlib, related back to the machinery of the earlier units. Formalization at scale; hammers, premise selection, autoformalization.

Basic mathematical logic or discrete mathematics: propositional and first-order logic, proofs by induction. Confident programming in a general-purpose language for the practical exercises, in which students extend a provided solver skeleton and script against solver APIs.

No prior exposure to proof assistants or automated reasoning tools is assumed. The module Logic (IN2049) is a useful precursor but is not required.

**Lectures** present the algorithms, results, and engineering, with short tool demonstrations where a system is under discussion.

**Exercise sessions**, one per unit, are devoted to guided problem solving and the discussion of submitted solutions.

**Practical assignments**, one per unit, are the principal self-study component and run across the whole unit. Each pairs light theoretical tasks with heavier practical ones requiring hands-on work with a state-of-the-art system.