Teacher: Aldo Dragoni
Content:
- 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.