An Interface Between Clam and HOL

This paper describes an interface between the Clam proof planner and the HOL interactive theorem prover. The interface sends a HOL goal to Clam for planning, and translates the resulting plan back into a HOL tactic that should solve the goal.

This paper has been accepted to TPHOLs98. It supersedes the paper entitled "A Prototype Interface Between Clam and HOL" and features many improvements over that work.

paper