Title: Separating Knowledge from Computation: An FO(.) Knowledge Base System and its Model Expansion Inference (Kennis scheiden van berekening: een FO(.) kennisbanksysteem en zijn modelexpansie inferentie)
Other Titles: Separating Knowledge from Computation: An FO(.) Knowledge Base System and its Model Expansion Inference
Authors: De Cat, Broes
Issue Date: 16-May-2014
Abstract: The field of Knowledge Representation is devoted to the study of how knowledge can be represented and how it can be used for automated reasoning. A recently proposed approach is the Knowledge Base System paradigm, based on the idea that knowledge is not inherently linked to a specific reasoning task. Instead, the paradigm proposes to express knowledge in a truly declarative language and to accomplish different computational tasks by applying the proper inference to the represented knowledge.In my dissertation, we developed the knowledge base system IDP, intended as a laboratory for the study of software engineering in the context of the KBS paradigm. The aim is to provide a language in which a user can naturally model his applications and to provide robust inference engines that free the user from performance considerations. IDP combines a rich declarative language (an extension of classical logic) with a range of inference engines (for deduction, model expansion, propagation, querying, etc.) and an integration with a procedural language.In the second part of the work, we studied the core inference task of (optimal) model expansion, the task of finding (optimal) models of a logical theory expanding a given structure. Specifically, we developed techniques to address the long-standing instantiation problem: Traditionally, the input theory is transformed into an equivalent propositional theory in an initial grounding phase, after which a search algorithm is applied; however, the grounding phase causes a blowup of the size of the theory, which makes the approach infeasible for many practical applications. We developed several techniques to address the instantiation problem: (i) add support for function symbols in the search algorithm, (ii) detect and exploit implicit functional dependencies and (iii) tightly interleave grounding and search, by maintaining justifications of non-ground parts of the theory. The result is a state-of-the-art model expansion and optimization inference engine, which is among the best MiniZinc and ASP systems.
Publication status: published
KU Leuven publication type: TH
Appears in Collections:Informatics Section

Files in This Item:
File Status SizeFormat
Dissertation Broes De Cat.pdf Published 1954KbAdobe PDFView/Open


All items in Lirias are protected by copyright, with all rights reserved.