Logic

Arguments, validity versus truth, soundness, and the syntax/semantics distinction that organises the whole module.

Atoms, connectives, well-formed formulas and truth tables, with precedence rules and full truth-table construction.

Assumes: What Logic Is

De Morgan, distribution, contraposition and absorption; simplifying formulas and proving equivalence.

Assumes: Propositional Logic

Literals and clauses, conversion algorithms, the Tseitin transformation, and why CNF is the universal input format.

Assumes: Logical Equivalence and Laws

Tautology, contradiction and contingency; semantic entailment, and the deduction and refutation theorems.

Assumes: Normal Forms: NNF, CNF and DNF

Introduction and elimination rules, assumption discharge, and building proofs line by line.

Assumes: Validity, Satisfiability and Entailment

Hilbert-style systems, Gentzen's sequent calculus, structural rules and cut elimination.

Assumes: Natural Deduction

The resolution rule, unit propagation, refutation completeness, and resolving a clause set by hand.

Assumes: Normal Forms: NNF, CNF and DNF

The SAT problem and its NP-completeness, DPLL and CDCL with clause learning, and SMT theories.

Assumes: Resolution and Refutation

Terms, constants, functions, predicates, quantifiers, free and bound variables, and scope.

Assumes: Validity, Satisfiability and Entailment

Structures, domains, interpretations and variable assignments; the satisfaction relation defined precisely.

Assumes: First-Order Logic: Syntax

Quantifier scope ambiguity, restricted quantification, and the standard translation patterns and traps.

Assumes: First-Order Logic: Syntax

Moving quantifiers out, eliminating existentials, and the Herbrand universe, base and theorem.

Assumes: First-Order Logic: Semantics

Substitutions, composition, the most general unifier, the occurs check, and the unification algorithm traced.

Assumes: Prenex Form, Skolemisation and Herbrand Universes

Lifting resolution to FOL, factoring, and refutation proofs over quantified clause sets.

Assumes: Unification

Generalised modus ponens, data- versus goal-driven inference, and Horn clause efficiency.

Assumes: Unification

What the metatheorems guarantee, Gödel's completeness theorem, compactness and the Löwenheim–Skolem theorem.

Assumes: First-Order Resolution

Decidable versus semi-decidable, the halting problem, Church–Turing undecidability of FOL, and Gödel's incompleteness theorems.

Assumes: Soundness, Completeness and Compactness

Quantifying over predicates and relations, the gain in expressive power, characterising the naturals, and the loss of a complete calculus.

Assumes: Decidability and the Limits of Logic

Simple type theory, lambda abstraction, Church's formulation, and HOL in interactive theorem provers.

Assumes: Second-Order Logic

Necessity and possibility, Kripke frames and accessibility relations, and the K, T, S4 and S5 systems.

Assumes: First-Order Logic: Semantics

LTL and CTL operators, expressing safety and liveness, and model checking as verification.

Assumes: Modal Logic

Reasoning about knowledge and belief, common knowledge, and multi-agent puzzles.

Assumes: Modal Logic

Concepts, roles and individuals; the ALC family, TBox and ABox, and the reasoning tasks behind OWL ontologies.

Assumes: First-Order Logic: Semantics

Definite clauses, SLD resolution, Prolog execution order, negation as failure, and Datalog for queries.

Assumes: Forward and Backward Chaining

Why classical entailment cannot retract conclusions; default logic, the closed-world assumption, circumscription and answer set programming.

Assumes: Horn Clauses and Logic Programming

Three-valued and Łukasiewicz systems, fuzzy sets and membership functions, t-norms, and fuzzy inference worked end to end.

Assumes: Propositional Logic

Rejecting excluded middle, the BHK interpretation, and the Curry–Howard correspondence between proofs and programs.

Assumes: Natural Deduction

Attaching probabilities to formulas, Markov logic networks, probabilistic soft logic, and the link to graphical models.

Assumes: First-Order Resolution · Bayes' Theorem

Neuro-symbolic architectures, differentiable logic and fuzzy relaxations, inductive logic programming, and using solvers to verify model behaviour.

Assumes: Probabilistic Logic · SAT and SMT Solvers