Description of the main methods for automated reasoning
Subject
Summary of first order predicate logic; the resolution method; completeness of resolution (Herbrand Theorem, semantic trees); refinements of resolution; the DPLL method for SAT; sequent calculus; the Theorema system.
