Title of Report 1: Deductive Database&Absorption: Journey from Past to Future

Report time: 14:00, December 15th

报告摘要：

In this talk, we will cover the following 3 areas.

The first is to share the some of the Fifth Generation Computer research work done in 1980-1990s on Deductive Database and Abduction.

The second will cover industry use cases integrating deductive database system and constraint configurator system with big data system.

Lastly, we will explore and discuss what are future potential research and innovative applications using deduction, induction, constraint solving and abduction.

报告人简介：

Dr. James Ong is an entrepreneur and community builder who has incubated, invested and mentored various technology start-ups and he is actively involved in the AI and tech ecosystem in China and ASEAN. He is the founder and CEO of Origami that provides strategy, technology and investment advisory services for venturing towards Autonomous Enterprise where he has more than 35 years of experience on digital transformation in Asia, US and Europe across multiple industry verticals. James founded Artificial Intelligence International Institute (AIII), a think tank advocating Sustainable AI for Humanity. He is also adjunct professor at SUTD and serves as mentor at NUS, SUTD and NTU. He started his career as an AI scientist at leading US MCC research lab on advanced AI Fifth Generation Computer research and received his PhD in Management Information System specializing on AI for Business Process Automation and MA & BA in Computer Science from the University of Texas at Austin.

Report 2 Title: Human Oriented Theory Proving in Practice

Report time: December 15th 15:15

报告摘要：

Mechanical theorem proving has been broadly applied in the formal verification of software and hardware designs. Modern theorem proving is either built on the development of type theory, where the proofs are heavily dependent on human efforts, or built on first order logic, where the proofs are usually unreadable. We are developing a meta-calculation environment which can produce customised theorem provers according to the rules specified by the users. The central innovation is the concept proof strategy that allows flexible control of proof search process. More general, we try to understand the nature of human reasoning, which should be independent of the underlying inference frameworks. In this talk, we investigate the potential applications of this framework in engineering practice by presenting examples from hardware designs, software development, to mathematical problem solving. We conclude three features of next-generation human-oriented automatic theorem proving: a. automatic human readable reasoning; b. automatic abstraction and derivation; c. automatic discovery.

报告人简介：

Dr Wei Chen : BSc, Nanjing University of Science and Technology, 2001. Huawei Technologies Ltd, 2001 - 2003. MSc in Formal Verification, Tsinghua University, 2007. PhD in Theoretical Computer Science, University of Nottingham, 2012. Research Scientist on Type Theory, Ludwig-Maximilian University Munich, 2012 - 2013. Research Fellow on FM and ML for Mobile Security, University of Edinburgh, 2013 - 2019.

Research Interests: computational theory, mathematical logic, theorem proving, formal verification, and mathematical discovery and reasoning.