Title: Extensional Paramodulation for Higher-Order Logic and its Effective Implementation Leo-III (Dissertations in Artificial Intelligence)