Experiments on Supporting Interactive Proof Using Resolution. - Jia Meng 002; Lawrence C. Paulson (IJCAR, 2004)

The integration of higher order interactive proof with first order automatic theorem proving. - Jia Meng 002 (2005)

Geometric Resolution: A Proof Procedure Based on Finite Model Search. - Hans de Nivelle; Jia Meng 002 (IJCAR, 2006)

Automation for interactive proof: First prototype. - Jia Meng 002; Claire Quigley; Lawrence C. Paulson (Inf. Comput., 2006)

Erratum to "Automation for interactive proof: First prototype" [Inform. and Comput. 204(2006) 1575-1596]. - Jia Meng 002; Claire Quigley; Lawrence C. Paulson (Inf. Comput., 2006)

A Termination Checker for Isabelle Hoare Logic. - Jia Meng 002; Lawrence C. Paulson; Gerwin Klein (VERIFY, 2007)

Translating Higher-Order Clauses to First-Order Clauses. - Jia Meng 002; Lawrence C. Paulson (J. Autom. Reason., 2008)

Lightweight relevance filtering for machine-generated resolution problems. - Jia Meng 002; Lawrence C. Paulson (J. Appl. Log., 2009)