Title: An approximative inference method for solving ∃∀SO satisfiability problems
Authors: Vlaeminck, Hanne ×
Wittocx, Johan
Vennekens, Joost
Denecker, Marc
Bruynooghe, Maurice #
Issue Date: Sep-2010
Publisher: Springer
Host Document: Lecture Notes in Computer Science vol:6341 pages:326-338
Conference: European Conference on Logics in Artificial Intelligence (JELIA) edition:2010 location:Helsinki date:13-16 September 2010
Abstract: The fragment ∃ ∀ SO(ID) of second order logic extended with inductive definitions is expressive, and many interesting problems, such as conformant planning, can be naturally expressed as finite domain satisfiability problems of this logic. Such satisfiability problems are computationally hard ($\Sigma^P_2$). In this paper, we develop an approximate, sound but incomplete method for solving such problems that transforms a ∃ ∀ SO(ID) to a ∃ SO(ID) problem. The finite domain satisfiability problem for the latter language is in NP and can be handled by several existing solvers. We show that this provides an effective method for solving practically useful problems, such as common examples of conformant planning. We also propose a more complete translation to ∃ SO(FP), existential SO extended with nested inductive and coinductive definitions.
Description: Acceptance rate: 33%
ISSN: 0302-9743
Publication status: published
KU Leuven publication type: IC
Appears in Collections:Informatics Section
Technologiecluster Computerwetenschappen
Computer Science Technology TC, Technology Campus De Nayer Sint-Katelijne-Waver
× corresponding author
# (joint) last author

Files in This Item:
File Description Status SizeFormat
outline.pdfMain article Published 194KbAdobe PDFView/Open


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

© Web of science