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

Article type: Other

Authors: Wittocx, Johan

Affiliations: Department of Computer Science, K.U. Leuven, Celestijnenlaan 200A, B-3001 Leuven, Belgium. E-mail: johan.wittocx@cs.kuleuven.be

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(·).

Keywords: First-order logic, constraint propagation, grounding, finite model generation

DOI: 10.3233/AIC-2010-0474

Journal: AI Communications, vol. 24, no. 1, pp. 91-93, 2011