Mathematical reasoning with higher-order anti-unifcation

We show how heuristic-driven theory projection (HDTP, a method based on higher-order anti-unification) can be used to model analogical reasoning in mathematics. More precisely, HDTP provides the framework for a model of the inductive analogy-making process involved in establishing the fundamental concepts of arithmetic. This process is a crucial component for being able to generalise from the concrete experiences that humans have due to their embodied and embedded nature. Such generalisations are a cornerstone of the ability to create an abstract domain like arithmetic. In addition to generalisations, HDTP can also transfer concepts from one domain into another, which is, for example, needed to introduce the concept Z E RO into arithmetic. The approach presented here is closely related to the theories of Information Flow and Institutions. The latter in particular provides a compelling way to integrate concept blending into the HDTP approach.