On the Representation of Mathematical Concepts and their Translation into First-Order Logic

Abstract

To prove difficult theorems in a mathematical field requires substantial knowledge of that field. In this thesis a frame-based knowledge representation formalism including higher-order sorted logic is presented, which supports a conceptual representation and to a large extent guarantees the consistency of the built-up knowledge bases. In order to operationalize this knowledge, for instance, in an automated theorem proving system, a class of sound morphisms from higher-order into first-order logic is given, in addition a sound and complete translation is presented. The translations are bijective and hence compatible with a later proof presentation. In order to prove certain theorems the comprehension axioms are necessary, (but difficult to handle in an automated system); such theorems are called truly higher-order. Many apparently higher-order theorems (i.e. theorems that are stated in higher-order syntax) however are essentially first-order in the sense that they can be proved without the comprehension axioms: for proving these theorems the translation technique as presented in this thesis is well-suited.