AFTACK: Approximation Fixpoint Theory as a General Algebraic Theory of Constructive Knowledge

We study extensions of approximation fixpoint theory that make it applicable far beyond the realm of non-monotonic reasoning.

Approximation Fixpoint Theory (AFT) is an algebraic fixpoint theory of nonmonotone operators. It was founded in order to unify semantics of various non-monotonic logics, in particular default logic (DL), autoepistemic logic (AEL), and logic programming (LP). Using AFT, one can obtain a family of semantics for any of these logics by defining (only) a semantic operator: an operator that maps interpretations to interpretations given a logic theory. The high level of abstraction and mathematical elegance of AFT make it a suitable tool for studying the underlying principles present in all such logics. Following its original succes in unifying DL, AEL and LP, AFT has been applied to numerous other domains, prompting several extensions of the original theory. AFT has greatly simplified the characterisation and subsequent study of semantics and constructive processes in the different domains to which it has been applied.

The goal of this project is to lift AFT into a general theory for constructive knowledge. By doing so, we aim to bring the benefits the theory offers (such as the fact that it unifies domains, that stratification results are freely available, … ) to a wide range of application areas within computer science.  Specific areas of interest are recursive function definitions, domain theory, and causality. 

 

Project Info

Start: 01/01/2021

End: 31/12/2024

Funding: FWO

Members: Bart Bogaerts 

In collaboration with: Joost Vennekens, Marc Denecker (KU Leuven)