Finite domain and symbolic inference methods for extensions of first-order logic

Abstract

In this dissertation, we investigate various sorts of reasoning on finite structures and theories in the logic FO(·), a rich extension of classical logic with, amongst others, inductive definitions and aggregates. In particular, we study the tasks of constraint propagation, grounding, model revision, and debugging for FO(·).