报告一题目：Deductive Database & Abduction：Journey from Past to Future

报告时间：12月15日 14：00

报告地点：数学馆201

腾讯会议号：650-854-178

主持人：陈仪香 教授

报告摘要：

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.

报告人简介：

AIII人工智能国际研究院（Artificial Intelligence International Institute）创始人与院长

威麟信息Origami创始人与CEO

新加坡SUTD科技与设计大学特聘教授

中国工信部国家人工智能标准总体组专家成员

WAIC世界人工智能大会国际战略顾问与专家

新加坡SWITCH x SFF科技生态专家与倡导者

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.

报告二题目：Human-Oriented Theorem Proving in Practice

报告时间：12月15日 15：15

报告地点：数学馆201

腾讯会议号：650-854-178

主持人：陈仪香 教授

报告摘要：

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.