ITA | ENG
B012995 - COMPUTATIONAL AND SYMBOLIC GEOMETRY
Main information
Teaching Language
Course Content
Suggested readings
Learning Objectives
Prerequisites
Teaching Methods
Further information
Type of Assessment
Course program
Academic Year 2015-16
Coorte 2015 - Second Cycle Degree in MATHEMATICS
Course year
First year - First Semester
Belonging Department
Mathematics and Computer Science "Ulisse Dini" (DIMAI)
Course Type
Single education field course
Scientific Area
MAT/03 - GEOMETRY
Credits
9
Teaching Hours
72
Teaching Term
21/09/2015 ⇒ 23/12/2015
Attendance required
No
Type of Evaluation
Final Grade
Course Content
show
Course program
show
Lectureship
Mutuality
Course teached as:
B012995 - GEOMETRIA COMPUTAZIONALE SIMBOLICA
Second Cycle Degree in MATHEMATICS
Curriculum APPLICATIVO
B012995 - GEOMETRIA COMPUTAZIONALE SIMBOLICA
Second Cycle Degree in MATHEMATICS
Curriculum APPLICATIVO
Teaching Language
Italian.
Course Content
Interactive theorem proving applied to geometry and algebra.
Introduction to Higher-Order Logic. Introduction to the HOL interactive proof assistant. Selected examples of formalizations with the HOL Theorem Prover in algebra and geometry. Development of an individual formalization project.
Introduction to Higher-Order Logic. Introduction to the HOL interactive proof assistant. Selected examples of formalizations with the HOL Theorem Prover in algebra and geometry. Development of an individual formalization project.
Suggested readings (Search our library's catalogue)
John Harrison, "Handbook of Practical Logic and Automated Reasoning" Cambridge University Press, 2009
John Harrison, HOL Light Tutorial
John Harrison, The HOL Light Manual
John Harrison, HOL Light Tutorial
John 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).
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
Hours reserved to private study and other indivual formative activities: 162
Contact hours for: Lectures (hours): 63
Further information
Marco Maggesi: Tuesday, 14.30-16.30
Giorgio Ottaviani: Monday, 16.00 - 17.30
Giorgio Ottaviani: Monday, 16.00 - 17.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.