34971
2013
2013
eng
46
2
14
article
Association for Computing Machinery
New York
1
--
--
--
A model-theoretic approach to belief change in answer set programming
We address the problem of belief change in (nonmonotonic) logic programming under answer set semantics. Our formal techniques are analogous to those of distance-based belief revision in propositional logic. In particular, we build upon the model theory of logic programs furnished by SE interpretations, where an SE interpretation is a model of a logic program in the same way that a classical interpretation is a model of a propositional formula. Hence we extend techniques from the area of belief revision based on distance between models to belief change in logic programs.
We first consider belief revision: for logic programs P and Q, the goal is to determine a program R that corresponds to the revision of P by Q, denoted P * Q. We investigate several operators, including (logic program) expansion and two revision operators based on the distance between the SE models of logic programs. It proves to be the case that expansion is an interesting operator in its own right, unlike in classical belief revision where it is relatively uninteresting. Expansion and revision are shown to satisfy a suite of interesting properties; in particular, our revision operators satisfy all or nearly all of the AGM postulates for revision.
We next consider approaches for merging a set of logic programs, P-1,...,P-n. Again, our formal techniques are based on notions of relative distance between the SE models of the logic programs. Two approaches are examined. The first informally selects for each program P-i those models of P-i that vary the least from models of the other programs. The second approach informally selects those models of a program P-0 that are closest to the models of programs P-1,...,P-n. In this case, P-0 can be thought of as a set of database integrity constraints. We examine these operators with regards to how they satisfy relevant postulate sets.
Last, we present encodings for computing the revision as well as the merging of logic programs within the same logic programming framework. This gives rise to a direct implementation of our approach in terms of off-the-shelf answer set solvers. These encodings also reflect the fact that our change operators do not increase the complexity of the base formalism.
ACM transactions on computational logic
10.1145/2480759.2480766
1529-3785 (print)
wos:2011-2013
14
WOS:000320619600007
Delgrande, J (reprint author), Simon Fraser Univ, Burnaby, BC V5A 1S6, Canada., jim@cs.sfu.ca; torsten@cs.uni-potsdam.de; tompits@kr.tuwien.ac.at; woltran@dbai.tuwien.ac.at
Canadian NSERC Discovery Grant; German Science Foundation (DFG) [SCHA
550/8-2]; Austrian Science Fund (FWF) [P21698]; Vienna University of
Technology [9006.09/008]
James Delgrande
Torsten Schaub
Hans Tompits
Stefan Woltran
eng
uncontrolled
Theory
eng
uncontrolled
Answer set programming
eng
uncontrolled
belief revision
eng
uncontrolled
belief merging
eng
uncontrolled
program encodings
eng
uncontrolled
strong equivalence
Institut für Informatik und Computational Science
Referiert
Institut für Informatik
34972
2013
2013
eng
40
2
14
article
Association for Computing Machinery
New York
1
--
--
--
Tableau calculi for logic programs under answer set semantics
We introduce formal proof systems based on tableau methods for analyzing computations in Answer Set Programming (ASP). Our approach furnishes fine-grained instruments for characterizing operations as well as strategies of ASP solvers. The granularity is detailed enough to capture a variety of propagation and choice methods of algorithms used for ASP solving, also incorporating SAT-based and conflict-driven learning approaches to some extent. This provides us with a uniform setting for identifying and comparing fundamental properties of ASP solving approaches. In particular, we investigate their proof complexities and show that the run-times of best-case computations can vary exponentially between different existing ASP solvers. Apart from providing a framework for comparing ASP solving approaches, our characterizations also contribute to their understanding by pinning down the constitutive atomic operations. Furthermore, our framework is flexible enough to integrate new inference patterns, and so to study their relation to existing ones. To this end, we generalize our approach and provide an extensible basis aiming at a modular incorporation of additional language constructs. This is exemplified by augmenting our basic tableau methods with cardinality constraints and disjunctions.
ACM transactions on computational logic
10.1145/2480759.2480767
1529-3785 (print)
wos:2011-2013
15
WOS:000320619600008
Gebser, M (reprint author), Univ Potsdam, Inst Informat, August Bebel Str 89, D-14482 Potsdam, Germany., fgebser@cs.uni-potsdam.de; torsteng@cs.uni-potsdam.de
German Science Foundation (DFG) [SCHA 550/8-1/2]
Martin Gebser
Torsten Schaub
eng
uncontrolled
Theory
eng
uncontrolled
Answer Set Programming
eng
uncontrolled
tableau calculi
eng
uncontrolled
proof complexity
Institut für Informatik und Computational Science
Referiert
Institut für Informatik
8294
2015
eng
393
396
7
article
Universitätsverlag Potsdam
Potsdam
0
--
--
--
Empirical and Normative Research on Fundamental Ideas of Embedded System Development
KEYCIT 2014 - Key Competencies in Informatics and ICT
1868-0844 (print)
2191-1940 (online)
urn:nbn:de:kobv:517-opus4-82949
online registration
Steffen Büchner
eng
uncontrolled
Theory
eng
uncontrolled
Embedded Systems
eng
uncontrolled
Fundamental Ideas
Datenverarbeitung; Informatik
Institut für Informatik und Computational Science
Open Access
CID (2015) 07
Posters
Universität Potsdam
https://publishup.uni-potsdam.de/files/8294/cid07_S393-396.pdf