HOL4-Beagle: an implementation of an higher order to first order translation

Thibault Gauthier

CECS SEMINAR SERIES

DATE: 2013-09-04
TIME: 16:00:00 - 17:00:00
LOCATION: RSISE Seminar Room, ground floor, building 115, cnr. North and Daley Roads, ANU
CONTACT: JavaScript must be enabled to display this email address.

ABSTRACT:
The interactive theorem prover HOL4 is enhanced with an external automated theorem prover Beagle. Performance of this architecture is evaluated against problems solved by the internal first-order prover METIS$\_$TAC during HOL4 build. It is shown that Beagle proves 82% of 300 translated theorems in 15 seconds of real time on one single CPU. The necessary work involves an implementation of a sound translation of the HOL4 logic to Beagle formalism: typed first-order arithmetic. Ideas on how to complete the project are briefly exposed, such as a generic Beagle proof output and a HOL4 proof replayer.