Jia Meng

Researcher Logic and Computation Program National ICT Australia Research School of Information Sciences and Engineering The Australian National University Canberra ACT 0200 Australia Email: jia.meng at anu.edu.au A Brief Curriculum Vitae

About Me

I am a researcher with NICTA's Logic and Computation Program and am also an adjunct research fellow of RSISE.

Before I joined NICTA in August 2005, I was a Ph.D. student at the University of Cambridge under the supervision of Prof. Lawrence Paulson and I was a member of Automated Reasoning Group. During my three years as a Ph.D. student, I worked on the integration of interactive and automatic theorem proving.

I graduated with a First Class B.A. Honours Degree in Computer Science from New Hall College, University of Cambridge in June 2002. Between 2002 and 2005, I was a Ph.D. student of Churchill College, University of Cambridge.

My Research Work

Interactive and automatic provers (such as resolution based provers) have both been used widely. Interactive provers offer users expressive formalisms and flexibility and are suitable for proving theorems of any user defined logics. However, they provide limited automation. In comparison, resolution provers provide automation, but only allow first order logic with equality. I am currently working on the L4.verified project, where I investigate how to effectively combine interactive and automatic theorem proving.

Professional Activities

• Program Committee Member, Empirically Successful Automated Reasoning in Large Theories, 2007
• Program Committee Member, The 20th International FLAIRS Conference
• Reviewer, Third International Joint Conference on Automated Reasoning (IJCAR), 2006
• Program Committee Member, ESAR-06 and Reviewer, JAR issue: Empirically Successful Automated Reasoning

Publications

1. Jia Meng.
   Integration of Interactive and Automatic Provers. In Manuel Carro and Jesus Correas (editors), Second CologNet Workshop on Implementation Technology for Computational Logic Systems, FME2003, September 2003.
2. Jia Meng and Lawrence C. Paulson.
   Experiments On Supporting Interactive Proof Using Resolution.In: David Basin and Micha. Rusinowitch (editors), IJCAR 2004: Second International Joint Conference on Automated Reasoning (Springer LNCS, 2004), 372-384.
3. Jia Meng, Claire Quigley and Lawrence C. Paulson.
   Automation for Interactive Proof: First Prototype. Information and Computation 204 10 (2006), 1575-1596.
4. Hans de Nivelle and Jia Meng.
   Geometric Resolution: A Proof Procedure Based on Finite Model Search. In U. Furbach and N. Shankar (editors), IJCAR 2006: Third International Joint Conference on Automated Reasoning (Springer LNAI, Vol 4130, 2006), 303-317.
5. Jia Meng and Lawrence C. Paulson.
   Lightweight Relevance Filtering for Machine-Generated Resolution Problems. In: Geoff Sutcliffe, Renate Schmidt and Stephan Schulz (editors), ESCoR: Empirically Successful Computerized Reasoning (CEUR Workshop Proceedings, Vol. 192, 2006), 53-69.
6. Jia Meng and Lawrence C. Paulson.
   Translating Higher-Order Problems to First-Order Clauses. In: Geoff Sutcliffe, Renate Schmidt and Stephan Schulz (editors), ESCoR: Empirically Successful Computerized Reasoning (CEUR Workshop Proceedings, Vol. 192, 2006), 70-80.
7. Jia Meng and Lawrence C. Paulson.
   Lightweight Relevance Filtering for Machine-Generated Resolution Problems. Journal of Applied Logic, in press.
8. Jia Meng, Lawrence C. Paulson and Gerwin Klein.
   A Termination Checker for Isabelle Hoare Logic. In: Bernhard Beckert (editor), 4th International Verification Workshop, VERIFY'07 (CEUR Workshop Proceedings, Vol. 259, 2007), 104-118.
9. Jia Meng and Lawrence C. Paulson.
   Translating higher-order problems to first-order clauses. Journal of Automated Reasoning, in press.