A Logic of Fixpoint Definitions

Abstract. We introduce the fixpoint definitions, which is a reformula-tion of fixpoint logic constructs. We define the logic FO(FD), an exten-sion of first order logic with fixpoint definitions. We illustrate the relation between fixpoint definitions and non-monotone inductive definitions in FO(ID), which is developed as an integration of ASP and classical logic. We investigate the satisfiability problem, SAT(FD), of the propositional fragment of FO(FD). We also demonstrate how to extend existing SAT solvers to become SAT(FD) solvers.