TY - JOUR A1 - Delgrande, James A1 - Schaub, Torsten H. A1 - Tompits, Hans A1 - Woltran, Stefan T1 - A model-theoretic approach to belief change in answer set programming JF - ACM transactions on computational logic N2 - 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. KW - Theory KW - Answer set programming KW - belief revision KW - belief merging KW - program encodings KW - strong equivalence Y1 - 2013 U6 - https://doi.org/10.1145/2480759.2480766 SN - 1529-3785 VL - 14 IS - 2 PB - Association for Computing Machinery CY - New York ER - TY - JOUR A1 - Gebser, Martin A1 - Schaub, Torsten H. T1 - Tableau calculi for logic programs under answer set semantics JF - ACM transactions on computational logic N2 - 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. KW - Theory KW - Answer Set Programming KW - tableau calculi KW - proof complexity Y1 - 2013 U6 - https://doi.org/10.1145/2480759.2480767 SN - 1529-3785 VL - 14 IS - 2 PB - Association for Computing Machinery CY - New York ER - TY - JOUR A1 - Kaminski, Roland A1 - Schaub, Torsten H. A1 - Siegel, Anne A1 - Videla, Santiago T1 - Minimal intervention strategies in logical signaling networks with ASP JF - Theory and practice of logic programming N2 - Proposing relevant perturbations to biological signaling networks is central to many problems in biology and medicine because it allows for enabling or disabling certain biological outcomes. In contrast to quantitative methods that permit fine-grained (kinetic) analysis, qualitative approaches allow for addressing large-scale networks. This is accomplished by more abstract representations such as logical networks. We elaborate upon such a qualitative approach aiming at the computation of minimal interventions in logical signaling networks relying on Kleene's three-valued logic and fixpoint semantics. We address this problem within answer set programming and show that it greatly outperforms previous work using dedicated algorithms. Y1 - 2013 U6 - https://doi.org/10.1017/S1471068413000422 SN - 1471-0684 VL - 13 SP - 675 EP - 690 PB - Cambridge Univ. Press CY - New York ER - TY - GEN A1 - Kaminski, Roland A1 - Schaub, Torsten H. A1 - Siegel, Anne A1 - Videla, Santiago T1 - Minimal intervention strategies in logical signaling networks with ASP T2 - Postprints der Universität Potsdam : Mathematisch Naturwissenschaftliche Reihe N2 - Proposing relevant perturbations to biological signaling networks is central to many problems in biology and medicine because it allows for enabling or disabling certain biological outcomes. In contrast to quantitative methods that permit fine-grained (kinetic) analysis, qualitative approaches allow for addressing large-scale networks. This is accomplished by more abstract representations such as logical networks. We elaborate upon such a qualitative approach aiming at the computation of minimal interventions in logical signaling networks relying on Kleene's three-valued logic and fixpoint semantics. We address this problem within answer set programming and show that it greatly outperforms previous work using dedicated algorithms. T3 - Zweitveröffentlichungen der Universität Potsdam : Mathematisch-Naturwissenschaftliche Reihe - 596 KW - systems biology KW - transduction KW - circuits KW - models KW - sets Y1 - 2019 U6 - http://nbn-resolving.de/urn/resolver.pl?urn:nbn:de:kobv:517-opus4-415704 SN - 1866-8372 IS - 4-5 SP - 675 EP - 690 ER - TY - JOUR A1 - Banbara, Mutsunori A1 - Soh, Takehide A1 - Tamura, Naoyuki A1 - Inoue, Katsumi A1 - Schaub, Torsten H. T1 - Answer set programming as a modeling language for course timetabling JF - Theory and practice of logic programming N2 - The course timetabling problem can be generally defined as the task of assigning a number of lectures to a limited set of timeslots and rooms, subject to a given set of hard and soft constraints. The modeling language for course timetabling is required to be expressive enough to specify a wide variety of soft constraints and objective functions. Furthermore, the resulting encoding is required to be extensible for capturing new constraints and for switching them between hard and soft, and to be flexible enough to deal with different formulations. In this paper, we propose to make effective use of ASP as a modeling language for course timetabling. We show that our ASP-based approach can naturally satisfy the above requirements, through an ASP encoding of the curriculum-based course timetabling problem proposed in the third track of the second international timetabling competition (ITC-2007). Our encoding is compact and human-readable, since each constraint is individually expressed by either one or two rules. Each hard constraint is expressed by using integrity constraints and aggregates of ASP. Each soft constraint S is expressed by rules in which the head is the form of penalty (S, V, C), and a violation V and its penalty cost C are detected and calculated respectively in the body. We carried out experiments on four different benchmark sets with five different formulations. We succeeded either in improving the bounds or producing the same bounds for many combinations of problem instances and formulations, compared with the previous best known bounds. KW - answer set programming KW - educational timetabling KW - course timetabling Y1 - 2013 U6 - https://doi.org/10.1017/S1471068413000495 SN - 1471-0684 VL - 13 IS - 2 SP - 783 EP - 798 PB - Cambridge Univ. Press CY - New York ER - TY - GEN A1 - Banbara, Mutsunori A1 - Soh, Takehide A1 - Tamura, Naoyuki A1 - Inoue, Katsumi A1 - Schaub, Torsten H. T1 - Answer set programming as a modeling language for course timetabling T2 - Postprints der Universität Potsdam : Mathematisch Naturwissenschaftliche Reihe N2 - The course timetabling problem can be generally defined as the task of assigning a number of lectures to a limited set of timeslots and rooms, subject to a given set of hard and soft constraints. The modeling language for course timetabling is required to be expressive enough to specify a wide variety of soft constraints and objective functions. Furthermore, the resulting encoding is required to be extensible for capturing new constraints and for switching them between hard and soft, and to be flexible enough to deal with different formulations. In this paper, we propose to make effective use of ASP as a modeling language for course timetabling. We show that our ASP-based approach can naturally satisfy the above requirements, through an ASP encoding of the curriculum-based course timetabling problem proposed in the third track of the second international timetabling competition (ITC-2007). Our encoding is compact and human-readable, since each constraint is individually expressed by either one or two rules. Each hard constraint is expressed by using integrity constraints and aggregates of ASP. Each soft constraint S is expressed by rules in which the head is the form of penalty (S, V, C), and a violation V and its penalty cost C are detected and calculated respectively in the body. We carried out experiments on four different benchmark sets with five different formulations. We succeeded either in improving the bounds or producing the same bounds for many combinations of problem instances and formulations, compared with the previous best known bounds. T3 - Zweitveröffentlichungen der Universität Potsdam : Mathematisch-Naturwissenschaftliche Reihe - 594 KW - answer set programming KW - educational timetabling KW - course timetabling Y1 - 2019 U6 - http://nbn-resolving.de/urn/resolver.pl?urn:nbn:de:kobv:517-opus4-415469 SN - 1866-8372 IS - 594 SP - 783 EP - 798 ER -