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.
