Menù principale
B027816 - APPLIED LOGIC
Main information
Teaching Language
Course Content
Suggested readings
Learning Objectives
Prerequisites
Teaching Methods
Type of Assessment
Course program
Academic Year 2020-21
Course year
First year - Second Semester
Belonging Department
Humanities (DILEF)
Course Type
Single education field course
Scientific Area
MAT/01 - MATHEMATICAL LOGIC
Credits
6
Teaching Hours
36
Teaching Term
22/02/2021 ⇒ 28/05/2021
Attendance required
Yes
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. Decision procedures in Geometry and Algebra. Selected examples of formalizations with the HOL Theorem Prover in algebra and geometry.
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 (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)
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)
Learning Objectives
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.
Prerequisites
None
Teaching Methods
Lectures (live or recorded): Presentation of the theory described in the course program, with teacher-student direct interaction (when live) or in subsequent meeting (when recorded), 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.
The training sessions will consist of practicing with symbolic computation software and computer theorem checkers.
Virtual class: 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.
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.
The training sessions will consist of practicing with symbolic computation software and computer theorem checkers.
Virtual class: 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.
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.
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. Study of part of the HOL library: multivariate analysis, Euclidean geometry, real and complex numbers, quaternions.