Introduction to Higher-Order Logic. Introduction to the HOL interactive proof assistant. Selected examples of formalizations with the HOL Theorem Prover. Development of an individual formalization project.
John Harrison, “Handbook of Practical Logic and Automated Reasoning” Cambridge University Press, 2009
John Harrison, HOL Light TutorialJohn Harrison, The HOL Light Manual
Learning Objectives
Knowledge acquired: Basic skills in Computer Aided Symbolic Computation and Automatic Proof Checking in Algebra and Geometry.
Competence acquired Knowing the operation of an interactive proof assistant.
Skills acquired (at the end of the course): Proof-checking of basic theorems in Algebra and Geometry with the aid ofan interactive proof assitant (e.g. Coq, HOL, Isabelle).
Prerequisites
Courses recommmended: All the courses of disciplinar areas MAT/01 Mathematical Logic, MAT/02 Algebra, MAT/03 Geometry, INF/01Computer Science.
Teaching Methods
Total hours of the course (including the time spent in attending lectures, seminars, private study, examinations, etc...): 225
Hours reserved to private study and other indivual formative activities: 162
Contact hours for: Lectures (hours): 63
Further information
Office hours:
Tuesday, 14.30-16.30
Type of Assessment
Oral exam.
Course program
Introduction to Higher-Order Logic. Lambda Calculus and Type Theory. Lambda Calculus as foundation of Functional Programming. Terms and types in Higher-Order Logic. Inference rules, axioms, theorems. Introduction to the HOL interactive proof assistant. Elements of ML programming. Conversions and symbolic calculus. Interactive theorem proving and elementary tactics. Automatic theorem proving, decision procedures for arithmetic, real and complex analysis, euclidean vector spaces, symbolic manipulations of polynomial and rational expressions. Selected examples of formalizations with the HOL Theorem Prover. Basic examples of theorems and theories formalized in HOL. The HOL library of developed theories. Development of an individual project of formalization.