摘  要：

Interactive and automatic theorem provers are both very widely used with their own strengths. Interactive provers provide expressive formalism and have been used in the formal verification of hardware, software and protocols.  Isabelle is one of the most successful examples.  In contrast to interactive provers, automatic provers are usually lack of expressiveness but offer powerful automation.  There has been active research in both of these areas and a current trend is the integration of them. In this seminar, I will give an overview of interactive and automatic theorem proving, their applications and the current research direction.

报告人简介：

Dr. Jia Meng is a researcher with National ICT Australia's Logic and Computation Program. She is also an adjunct research fellow of Australian National University.  She obtained her B.A., M.A. and Ph.D. from the University of Cambridge in 2002 and 2005 respectively. She is a main developer of theorem prover Isabelle. Her major research areas include interactive theorem proving, automatic theorem proving and the integration of them. In addition to these, she is also interested in static analysis and machine learning.