Mini - course

AUTOMATED THEOREM PROVING

Place: Lecture room 5, Building A14, Institute of Mathematics, 18 Hoang Quoc                        Viet road, Cau Giay District, Hanoi

Time: 14:00 - 16:00, Friday December 7, 14, 21, 28 , 2007

Lecturer: Professor Thomas Hales of University of Pittsburgh

The subjects of the course are related to lecturer's works on formal proofs and Kepler conjecture. The course consist of (at least) 4 lectures and will be based on three books (all available electronically). The primary text is "Introduction to Logic and Automated Theorem Proving" by John Harrison (Intel Corp.) (637 pages) 2007.  The book is still awaiting publication. Secondary texts are "HOL Light Tutorial" by John Harrison (230 pages) 2006 and "Introduction to the Objective Caml Programming Language" by Jason Hickey (157 pages) 2006.   The course is reserved for young researchers, master students and students of Mathematics as well as of Computer Sciences. It does not require any prerequisites from the students. The first lecture will take place on Friday, December 7, 2007.

Note.  During the first lecture,  Professor  Thomas Hales  will discuss with students to work out the convenient time and program for another mini-course on Discrete Mathematics and Combinatorics

Loạt bài giảng

AUTOMATED THEOREM PROVING

Địa điểm: Phòng 5, Nhà A14, Viện Toán học, 18 đường Hoàng Quốc Việt, Hà Nội

Thời gian: 14:00 - 16:00, các ngày thứ Sáu 7, 14, 21, 28 tháng 12 năm 2007

Giảng viên: G.S. Thomas Hales Đại học Pittsburgh

Chủ đề của loạt bài giảng này liên quan tới các công trình của Giáo sư Thomas Hales về các chứng minh hình thức (formal proofs) và giả thuyết Kepler (Kepler conjecture). Loạt bài giảng này sẽ gồm (ít nhất) 4 buổi và sẽ dựa trên ba cuốn sách (cả ba cuốn đều có bản điện tử). Cuốn sách tham khảo chính sẽ là cuốn "Introduction to Logic and Automated Theorem Proving" của tác giả John Harrison (Intel Corp.) (dài 637 trang) sẽ xuất bản trong năm 2007. Hai cuốn còn lại là "HOL Light Tutorial" của John Harrison (230 trang) xuất bản năm 2006 và "Introduction to the Objective Caml Programming Language" của Jason Hickey (157 trang) xuất bản năm 2006.   Loạt bài giảng này nhằm dành cho các cán bộ nghiên cứu và giảng dạy trẻ, các sinh viên cao hoc và sinh viên năm cuối ngành Toán và Công nghệ thông tin của các trưòng đại học và các viện nghiên cứu và không đòi hỏi người nghe phải có kiến thức chuẩn bị nào. Bài giảng đầu tiên sẽ diễn ra vào thứ Sáu, ngày 7/12/2007.

Chú ý. Trong buổi học đầu tiên, G.S. Thomas Hales  sẽ thảo luận với các sinh viên để tìm thời gian thích hợp và lịch học cho một giáo trình khác nữa về Toán rời rạc và Tổ hợp.