Insegnamento mutuato da: B012995 - GEOMETRIA COMPUTAZIONALE SIMBOLICA Corso di Laurea Magistrale in MATEMATICA Curricula APPLICATIVO
Interactive theorem proving applied to geometry and algebra.? Introduction to Higher-Order Logic. Introduction to the HOL interactive proof assistant. Decision procedures in Geometry and Algebra. Selected examples of formalizations with the HOL Theorem Prover in algebra and geometry.
John Harrison, "Handbook of Practical Logic and Automated Reasoning" Cambridge University Press, 2009
??John Harrison, HOL Light Tutorial?? (freely available online)
John Harrison, The HOL Light Manual (freely available online)
Robert M. Solovay, R. D. Arthan, John Harrison, "Some new results on decidability for elementary algebra and geometry" (arXiv 2009)
The course aims to provide the students with fundamental knowledge and understanding of Computer Proof Checking, Symbolic Calculus, and decision procedure for Algebra and Geometry. The course also intends to develop basic technical skills and critical thinking needed when modeling and solving mathematical problems in different settings. Special attention will be paid to help the students to develop communication skills necessary for teamwork. The course covers topics and provides learning skills that are important in Formal Mathematics, in Mathematical Foundations of Computer Sciences, and Scientific Calculus.
Lectures: Presentation of the theory described in the course program, with teacher-student direct interaction, to ensure a full understanding of the subject.
Training sessions: training of the students to modelling and solving a wide selection of problems in Computer Proof Checking, Symbolic Calculus, Formalization of Mathematics, and decision procedure in Algebra and in Geometry. The training sessions are conducted so to:
-- help the students develop communication skills and apply the theoretical knowledge;
-- encourage independent judgement in the students.
Sessions in the computer lab: Practicing with symbolic computation software and computer theorem checkers.
Moodle learning platform: online teacher-student interaction, posting of additional notes, supplementary exercise sheets, examples of final examinations.
Remark: The suggested reading includes supplementary material that may be useful for further personal studies on the subject.
Type of Assessment
The exam consists of two steps:
1. Preparation of an individual project (typically a computer formalization in the HOL Light theorem prover) accompanied with a brief written report.
2. Oral discussion of the project.
The candidate must send to the instructor the report and the code before the oral exam.
The project is conceived to assess the ability of the student to apply the techniques illustrated in the course. Special attention is paid to correctness, originality, and effectiveness of the proposed solution.
The oral examination will evaluate the degree of understanding of the theory presented in the course. The assessment will also consider the communication skills (including the appropriate use of the terminology and the mathematical language), and the critical thinking attitude of the candidate.
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. Study of part of the HOL library: multivariate analysis, Euclidean geometry, real and complex numbers, quaternions.