B012995 - COMPUTATIONAL AND SYMBOLIC GEOMETRY

Italian.

Interactive theorem proving applied to geometry and algebra.
 Introduction to Higher-Order Logic. Introduction to the HOL interactive proof assistant. Decision procedure 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 about Computer Proof Checking, Symbolic Calculus and decision procedure for Algebra and Geometry. One of the aims is to let the students 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 important in formal mathematics and in mathematical foundations of computer sciences and scientific calculus.

None

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.

Final oral examination: A selection of exercises is proposed. The tests are conceived to assess the ability of the students to apply their skills to problem modelling and solving. In the evaluation, special attention is paid to the correctness of the solution procedure, as well as to the originality and effectiveness of the methods adopted.

A number of questions are posed. The oral examination is designed to evaluate the degree of understanding of the theory presented in the course. In the assessment, special attention is paid to communication skills, critical thinking and appropriate use of mathematical language.

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. The HOL library of developed theories on multivariate analysis, and on the algebra of real and complex numbers and of quaternions.