The course may include the following: deductive theorem proving (resolution, sequent-style calculi, natural deduction), inductive theorem proving, equational reasoning (rewrite systems), non-classical logics (modal logics, intuitionistic logic).