Selected Topics in Automated Reasoning

Structure of the lecture
  • Introduction
  • We will start by explaining the importance of logical formalization in various areas (mathematics, verification, knowledge representation).
  • Propositional and first-order logic (reminder)
  • syntax, semantics
  • validity, satisfiability, entailment
  • automated reasoning in propositional logic (DPLL method, resolution)
  • automated reasoning in first-order logic
  • Decidability/Undecidability for fragments of first-order logic
  • general undecidability results
  • decidable fragments of first-order logic
  • tractable fragments of first-order logic
  • Automated reasoning in numerical domains (a crash course)
  • We will mention - probably without proof - decidability and undecidability results (and the main techniques for proving decidability) for various numerical domains (real numbers, integers, Presburger arithmetic, ...)
  • Combinations of decision procedures
  • We will explain how logical theories can be combined, and will present some important techniques for reasoning in combinations of theories.
  • Applications in mathematics, verification, knowledge representation
  • Automated reasoning in verification
  • Automated reasoning and knowledge representation (databases; non-classical logics)
  • Automated reasoning in algebra