Title: Automated Reasoning in Higher-order Logic
Subjects: Type theory, Automatic theorem proving