Seminars
RUS  ENG    JOURNALS   PEOPLE   ORGANISATIONS   CONFERENCES   SEMINARS   VIDEO LIBRARY   PACKAGE AMSBIB  
Calendar
Search
Add a seminar

RSS
Forthcoming seminars




Seminars "Proof Theory" and "Logic Online Seminar"
February 15, 2021 18:30, Moscow, Steklov Mathematical Institute (8 Gubkina), room 313 + Zoom
 


Automated Mathematical Theorem Proving

Wei Chen
Video records:
MP4 274.7 Mb

Number of views:
This page:252
Video files:48
Youtube:

Wei Chen



Abstract: Mathematical discovery and reasoning is considered as the most creative activity of human wisdom. Mathematicians have been investigating the nature of human reasoning and problem solving. In particular, Polya published several books on this topic in 1960s, which are still very inspiring for current research. From 1970s, logicians and computer scientists have been investigating and developing so-called theorem provers to produce proofs automatically and to check human proofs using machines. Invented by de Bruijn, Automath is the first machine checkable language for expressing mathematics, and most modern interactive theorem provers are variants of Edinburgh LCF developed by Gordon and Milner. But there is still a gap between human and mechanical reasoning: precious human intelligence is spent on proving tedious and trivial theorems which are indispensable for machines to check the correctness and integrity of a proof.


We propose to shrink the gap by developing automated theorem provers for human reasoning. Except the automation of logic inference strategies and skills, the main planned innovations are: proving on abstract domains and generalising from cases. We will investigate and implement the mechanism to discover and exploit morphisms between algebraic systems, e.g., duality, quotient sets, Galois connection and insertion, etc., so as to simplify proofs by making use of collapsed structures. We want to equip the theorem prover with the generalisation capability such that they can explore known facts and develop conjectures from cases then prove or refute them automatically. We will adapt the equational proof style as the interface and the LCF style as the internal representation. By doing this, we are able to produce human readable and machine checkable proofs.


These innovations will potentially benefit the development of other research areas, including: search engines, design automation, neural computation, etc. Due to the mechanism of relying and learning from humans in case that the system is stuck, we are able to answer more complex queries, to avoid unnecessary searching, and to accelerate by exploit specific structures. We expect optimistically these benefits brought by techniques developed in this proposed research.

Language: English
 
  Contact us:
 Terms of Use  Registration to the website  Logotypes © Steklov Mathematical Institute RAS, 2024