FO(.) extended with constructive definitions using Approximation Fixpoint Theory

Classical first-order logic FO is a commonly used knowledge representation language with one clear drawback: its expressivity. Therefore a great body of research has tried to improve this expressivity by extending it with additional constructs such as aggregates, arithmetics, intensional objects, etc. In mathematics, different kinds of constructive definitions are used to define formal concepts. In general constructive definitions define possibly infinite concepts by a finite set of rules resulting in a construction process that starts from a default value and gradually builds the actual value using the definition rules. E.g., the set of natural numbers is inductively defined by two simple rules: "0 is a natural number." and "if x is a natural number, then x+1 is a natural number too.".  By default, nothing is a natural number, in the first step we derive that 0 is a natural number, then we derive 1 as a natural number, next 2 and so on. Previous research has succesfully extended FO with inductive definitions using Approximation Fipxoint Theory (AFT), but a more general theory regarding arbitrary constructive definitions, remains a largely unsolved problem. The aim of this PhD is to investigate (1) the different classes of constructive definitions in human knowledge, (2) the significant differences and relations between these classes and (3) the possibility to extend FO with a general theory for arbitrary constructive definitions using AFT.