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.