Artificial Intelligence & Logic Programming I

Teacher: Aldo Dragoni


  • Artificial Intelligence: history and difference between the logical-symbolic approach and the neural approach.
  • First-order logic: Syntax, Semantics, Formal system.
  • Resolution method: Herbrand’s theorem. Conversion to clausal form of a closed formula. The Resolution Principle for ground clauses. Unification.
    The Resolution Principle. Linear Resolution.
  • Definite programs: Semantics. Correctness of SLD Resolution. The Occur-Check problem. Completeness of SLD Resolution. Independence
    from the Computation Rule. SLD Refutation Procedure. Computational adequacy of Definite Programs.
  • Logic programming: PROLOG. Declarative programming.