Title: A resolution style proof procedure for higher-order logic
Subjects: First-order logic, Automatic theorem proving