Approximation Fixpoint Theory in Coq

Approximation Fixpoint Theory (AFT) is an abstract framework based on lattice theory that unifies semantics of different non-monotonic logic. AFT has revealed itself to be applicable in a variety of new domains within knowledge representation. In this work, we present a formalisation of the key constructions and results of AFT in the Coq theorem prover, together with a case study illustrating its application to propositional logic programming.