TY  - JOUR
A1  - Gebser, Martin
A1  - Schaub, Torsten H.
A1  - Thiele, Sven
A1  - Veber, Philippe
T1  - Detecting inconsistencies in large biological networks with answer set programming
JF  - Theory and practice of logic programming
N2  - We introduce an approach to detecting inconsistencies in large biological networks by using answer set programming. To this end, we build upon a recently proposed notion of consistency between biochemical/genetic reactions and high-throughput profiles of cell activity. We then present an approach based on answer set programming to check the consistency of large-scale data sets. Moreover, we extend this methodology to provide explanations for inconsistencies by determining minimal representations of conflicts. In practice, this can be used to identify unreliable data or to indicate missing reactions.
KW  - answer set programming
KW  - bioinformatics
KW  - consistency
KW  - diagnosis
Y1  - 2011
U6  - https://doi.org/10.1017/S1471068410000554
SN  - 1471-0684
VL  - 11
IS  - 5-6
SP  - 323
EP  - 360
PB  - Cambridge Univ. Press
CY  - New York
ER  - 
TY  - JOUR
A1  - Gebser, Martin
A1  - Kaufmann, Benjamin
A1  - Kaminski, Roland
A1  - Ostrowski, Max
A1  - Schaub, Torsten H.
A1  - Schneider, Marius
T1  - Potassco the Potsdam answer set solving collection
JF  - AI communications : AICOM ; the European journal on artificial intelligence
N2  - This paper gives an overview of the open source project Potassco, the Potsdam Answer Set Solving Collection, bundling tools for Answer Set Programming developed at the University of Potsdam.
KW  - Answer set programming
KW  - declarative problem solving
Y1  - 2011
U6  - https://doi.org/10.3233/AIC-2011-0491
SN  - 0921-7126
VL  - 24
IS  - 2
SP  - 107
EP  - 124
PB  - IOS Press
CY  - Amsterdam
ER  - 
TY  - JOUR
A1  - Gebser, Martin
A1  - Sabuncu, Orkunt
A1  - Schaub, Torsten H.
T1  - An incremental answer set programming based system for finite model computation
JF  - AI communications : AICOM ; the European journal on artificial intelligence
N2  - We address the problem of Finite Model Computation (FMC) of first-order theories and show that FMC can efficiently and transparently be solved by taking advantage of a recent extension of Answer Set Programming (ASP), called incremental Answer Set Programming (iASP). The idea is to use the incremental parameter in iASP programs to account for the domain size of a model. The FMC problem is then successively addressed for increasing domain sizes until an answer set, representing a finite model of the original first-order theory, is found. We implemented a system based on the iASP solver iClingo and demonstrate its competitiveness by showing that it slightly outperforms the winner of the FNT division of CADE's 2009 Automated Theorem Proving (ATP) competition on the respective benchmark collection.
KW  - Incremental answer set programming
KW  - finite model computation
Y1  - 2011
U6  - https://doi.org/10.3233/AIC-2011-0496
SN  - 0921-7126
VL  - 24
IS  - 2
SP  - 195
EP  - 212
PB  - IOS Press
CY  - Amsterdam
ER  - 
TY  - JOUR
A1  - Lindauer, Marius
A1  - Hoos, Holger H.
A1  - Hutter, Frank
A1  - Schaub, Torsten H.
T1  - An automatically configured algorithm selector
JF  - The journal of artificial intelligence research
N2  - Algorithm selection (AS) techniques - which involve choosing from a set of algorithms the one expected to solve a given problem instance most efficiently - have substantially improved the state of the art in solving many prominent AI problems, such as SAT, CSP, ASP, MAXSAT and QBF. Although several AS procedures have been introduced, not too surprisingly, none of them dominates all others across all AS scenarios. Furthermore, these procedures have parameters whose optimal values vary across AS scenarios. This holds specifically for the machine learning techniques that form the core of current AS procedures, and for their hyperparameters. Therefore, to successfully apply AS to new problems, algorithms and benchmark sets, two questions need to be answered: (i) how to select an AS approach and (ii) how to set its parameters effectively. We address both of these problems simultaneously by using automated algorithm configuration. Specifically, we demonstrate that we can automatically configure claspfolio 2, which implements a large variety of different AS approaches and their respective parameters in a single, highly-parameterized algorithm framework. Our approach, dubbed AutoFolio, allows researchers and practitioners across a broad range of applications to exploit the combined power of many different AS methods. We demonstrate AutoFolio can significantly improve the performance of claspfolio 2 on 8 out of the 13 scenarios from the Algorithm Selection Library, leads to new state-of-the-art algorithm selectors for 7 of these scenarios, and matches state-of-the-art performance (statistically) on all other scenarios. Compared to the best single algorithm for each AS scenario, AutoFolio achieves average speedup factors between 1.3 and 15.4.
Y1  - 2015
SN  - 1076-9757
SN  - 1943-5037
VL  - 53
SP  - 745
EP  - 778
PB  - AI Access Foundation
CY  - Marina del Rey
ER  - 
TY  - JOUR
A1  - Hoos, Holger
A1  - Kaminski, Roland
A1  - Lindauer, Marius
A1  - Schaub, Torsten H.
T1  - aspeed: Solver scheduling via answer set programming
JF  - Theory and practice of logic programming
N2  - Although Boolean Constraint Technology has made tremendous progress over the last decade, the efficacy of state-of-the-art solvers is known to vary considerably across different types of problem instances, and is known to depend strongly on algorithm parameters. This problem was addressed by means of a simple, yet effective approach using handmade, uniform, and unordered schedules of multiple solvers in ppfolio, which showed very impressive performance in the 2011 Satisfiability Testing (SAT) Competition. Inspired by this, we take advantage of the modeling and solving capacities of Answer Set Programming (ASP) to automatically determine more refined, that is, nonuniform and ordered solver schedules from the existing benchmarking data. We begin by formulating the determination of such schedules as multi-criteria optimization problems and provide corresponding ASP encodings. The resulting encodings are easily customizable for different settings, and the computation of optimum schedules can mostly be done in the blink of an eye, even when dealing with large runtime data sets stemming from many solvers on hundreds to thousands of instances. Also, the fact that our approach can be customized easily enabled us to swiftly adapt it to generate parallel schedules for multi-processor machines.
KW  - algorithm schedules
KW  - answer set programming
KW  - portfolio-based solving
Y1  - 2015
U6  - https://doi.org/10.1017/S1471068414000015
SN  - 1471-0684
SN  - 1475-3081
VL  - 15
SP  - 117
EP  - 142
PB  - Cambridge Univ. Press
CY  - New York
ER  - 
TY  - JOUR
A1  - Schaub, Torsten H.
A1  - Wang, Kewen
T1  - A comparative study of logic programs with preference
Y1  - 2001
ER  - 
TY  - JOUR
A1  - Delgrande, James Patrick
A1  - Schaub, Torsten H.
T1  - How to reason credulously and skeptically within a single extension.
Y1  - 2001
SN  - 3-540- 42464-4
ER  - 
TY  - JOUR
A1  - Delgrande, James Patrick
A1  - Schaub, Torsten H.
A1  - Tompits, Hans
T1  - A generic compiler for ordered logic programs
Y1  - 2001
SN  - 3-540-42593-4
ER  - 
TY  - JOUR
A1  - Schaub, Torsten H.
A1  - Wang, Kewen
T1  - A comparative study of logic programs with preference
Y1  - 2001
SN  - 1-558-60777-3
SN  - 1045-0823
ER  - 
TY  - JOUR
A1  - Delgrande, James Patrick
A1  - Schaub, Torsten H.
T1  - How to reason credulously and skeptically within a single extension
Y1  - 2001
ER  - 
TY  - JOUR
A1  - Besnard, Philippe
A1  - Schaub, Torsten H.
T1  - Significant inferences
Y1  - 2000
SN  - 1-55860-690-4
ER  - 
TY  - JOUR
A1  - Linke, Thomas
A1  - Schaub, Torsten H.
T1  - Alternative foundations for Reiter's default logic.
Y1  - 2000
SN  - 0004-3702
ER  - 
TY  - JOUR
A1  - Besnard, Philippe
A1  - Schaub, Torsten H.
T1  - What is a (non-constructive) non-monotone logical system?
Y1  - 2000
SN  - 0304-3975
ER  - 
TY  - JOUR
A1  - Delgrande, James Patrick
A1  - Schaub, Torsten H.
T1  - The role of default logic in knowledge representation
Y1  - 2000
SN  - 0-7923-7224-7
ER  - 
TY  - JOUR
A1  - Delgrande, James Patrick
A1  - Schaub, Torsten H.
T1  - Expressing preferences in default logic
Y1  - 2000
SN  - 0004-3702
ER  - 
TY  - JOUR
A1  - Delgrande, James Patrick
A1  - Schaub, Torsten H.
A1  - Tompits, Hans
T1  - A compilation of Brewka and Eiter's approach to prioritizationtion
Y1  - 2000
SN  - 3-540-41131-3
ER  - 
TY  - JOUR
A1  - Delgrande, James Patrick
A1  - Schaub, Torsten H.
T1  - A consistency-based model for belief change: preliminary report
Y1  - 2000
SN  - 0-262-51112-6
ER  - 
TY  - JOUR
A1  - Delgrande, James Patrick
A1  - Schaub, Torsten H.
A1  - Tompits, Hans
T1  - Logic programs with compiled preferences
Y1  - 2000
SN  - 1-58603-013-2
ER  - 
TY  - JOUR
A1  - Delgrande, James Patrick
A1  - Schaub, Torsten H.
A1  - Tompits, Hans
T1  - Logic programs with compiled preferences
Y1  - 2000
UR  - http://xxx.lanl.gov/abs/cs.AI/0003028
ER  - 
TY  - JOUR
A1  - Delgrande, James Patrick
A1  - Schaub, Torsten H.
T1  - A consistency-based model for belief change: preliminary report
Y1  - 2000
UR  - http://xxx.lanl.gov/abs/cs.AI/0003052
ER  - 
TY  - JOUR
A1  - Delgrande, James Patrick
A1  - Schaub, Torsten H.
A1  - Tompits, Hans
T1  - A compiler for ordered logic programs
Y1  - 2000
UR  - http://arxiv.org/abs/cs.AI/0003024
ER  - 
TY  - JOUR
A1  - Brüning, Stefan
A1  - Schaub, Torsten H.
T1  - A connection calculus for handling incomplete information
Y1  - 2000
ER  - 
TY  - JOUR
A1  - Brüning, Stefan
A1  - Schaub, Torsten H.
T1  - Avoiding non-ground variables
Y1  - 1999
SN  - 3-540-66131-x
ER  - 
TY  - JOUR
A1  - Benhammadi, Farid
A1  - Nicolas, Pascal
A1  - Schaub, Torsten H.
T1  - Query-answering in prioritized default logic
Y1  - 1999
SN  - 3-540-66131-X
ER  - 
TY  - BOOK
A1  - Schaub, Torsten H.
T1  - The automation of reasoning with incomplete information : from semantic foundations to efficient computation
T3  - Lecture notes in computer science
Y1  - 1999
SN  - 3-540-64515-2
U6  - https://doi.org/10.1007/BFb0054963
VL  - 1409
PB  - Springer
CY  - Berlin
ER  - 
TY  - JOUR
A1  - Benhammadi, Farid
A1  - Nicolas, Pascal
A1  - Schaub, Torsten H.
T1  - Query-answering in prioritized default logic
Y1  - 1999
SN  - 3-540-66131-X
ER  - 
TY  - JOUR
A1  - Brüning, Stefan
A1  - Schaub, Torsten H.
T1  - A voiding non-ground variables
Y1  - 1999
ER  - 
TY  - JOUR
A1  - Linke, Thomas
A1  - Schaub, Torsten H.
T1  - On bottom-up pre-processing techniques for automated default reasoning
Y1  - 1999
SN  - 3-540-66131-x
ER  - 
TY  - JOUR
A1  - Brewka, Gerhard
A1  - Ellmauthaler, Stefan
A1  - Kern-Isberner, Gabriele
A1  - Obermeier, Philipp
A1  - Ostrowski, Max
A1  - Romero, Javier
A1  - Schaub, Torsten H.
A1  - Schieweck, Steffen
T1  - Advanced solving technology for dynamic and reactive applications
JF  - Künstliche Intelligenz
Y1  - 2018
U6  - https://doi.org/10.1007/s13218-018-0538-8
SN  - 0933-1875
SN  - 1610-1987
VL  - 32
IS  - 2-3
SP  - 199
EP  - 200
PB  - Springer
CY  - Heidelberg
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  - Bosser, Anne-Gwenn
A1  - Cabalar, Pedro
A1  - Dieguez, Martin
A1  - Schaub, Torsten H.
T1  - Introducing temporal stable models for linear dynamic logic
T2  - 16th International Conference on Principles of Knowledge Representation and Reasoning
N2  - We propose a new temporal extension of the logic of Here-and-There (HT) and its equilibria obtained by combining it with dynamic logic over (linear) traces. Unlike previous temporal extensions of HT based on linear temporal logic, the dynamic logic features allow us to reason about the composition of actions. For instance, this can be used to exercise fine grained control when planning in robotics, as exemplified by GOLOG. In this paper, we lay the foundations of our approach, and refer to it as Linear Dynamic Equilibrium Logic, or simply DEL. We start by developing the formal framework of DEL and provide relevant characteristic results. Among them, we elaborate upon the relationships to traditional linear dynamic logic and previous temporal extensions of HT.
Y1  - 2018
UR  - https://www.dc.fi.udc.es/~cabalar/del.pdf
SP  - 12
EP  - 21
PB  - ASSOC Association for the Advancement of Artificial Intelligence
CY  - Palo Alto
ER  - 
TY  - JOUR
A1  - Fandiño, Jorge
A1  - Lifschitz, Vladimir
A1  - Lühne, Patrick
A1  - Schaub, Torsten H.
T1  - Verifying tight logic programs with Anthem and Vampire
JF  - Theory and practice of logic programming
N2  - This paper continues the line of research aimed at investigating the relationship between logic programs and first-order theories. We extend the definition of program completion to programs with input and output in a subset of the input language of the ASP grounder gringo, study the relationship between stable models and completion in this context, and describe preliminary experiments with the use of two software tools, anthem and vampire, for verifying the correctness of programs with input and output. Proofs of theorems are based on a lemma that relates the semantics of programs studied in this paper to stable models of first-order formulas.
Y1  - 2020
U6  - https://doi.org/10.1017/S1471068420000344
SN  - 1471-0684
SN  - 1475-3081
VL  - 20
IS  - 5
SP  - 735
EP  - 750
PB  - Cambridge Univ. Press
CY  - Cambridge [u.a.]
ER  - 
TY  - JOUR
A1  - Cabalar, Pedro
A1  - Fandiño, Jorge
A1  - Garea, Javier
A1  - Romero, Javier
A1  - Schaub, Torsten H.
T1  - Eclingo
BT  - a solver for epistemic logic programs
JF  - Theory and practice of logic programming
N2  - We describe eclingo, a solver for epistemic logic programs under Gelfond 1991 semantics built upon the Answer Set Programming system clingo. The input language of eclingo uses the syntax extension capabilities of clingo to define subjective literals that, as usual in epistemic logic programs, allow for checking the truth of a regular literal in all or in some of the answer sets of a program. The eclingo solving process follows a guess and check strategy. It first generates potential truth values for subjective literals and, in a second step, it checks the obtained result with respect to the cautious and brave consequences of the program. This process is implemented using the multi-shot functionalities of clingo. We have also implemented some optimisations, aiming at reducing the search space and, therefore, increasing eclingo 's efficiency in some scenarios. Finally, we compare the efficiency of eclingo with two state-of-the-art solvers for epistemic logic programs on a pair of benchmark scenarios and show that eclingo generally outperforms their obtained results.
KW  - Answer Set Programming
KW  - Epistemic Logic Programs
KW  - Non-Monotonic
KW  - Reasoning
KW  - Conformant Planning
Y1  - 2020
U6  - https://doi.org/10.1017/S1471068420000228
SN  - 1471-0684
SN  - 1475-3081
VL  - 20
IS  - 6
SP  - 834
EP  - 847
PB  - Cambridge Univ. Press
CY  - New York
ER  - 
TY  - JOUR
A1  - Cabalar, Pedro
A1  - Fandiño, Jorge
A1  - Schaub, Torsten H.
A1  - Schellhorn, Sebastian
T1  - Gelfond-Zhang aggregates as propositional formulas
JF  - Artificial intelligence
N2  - Answer Set Programming (ASP) has become a popular and widespread paradigm for practical Knowledge Representation thanks to its expressiveness and the available enhancements of its input language. One of such enhancements is the use of aggregates, for which different semantic proposals have been made. In this paper, we show that any ASP aggregate interpreted under Gelfond and Zhang's (GZ) semantics can be replaced (under strong equivalence) by a propositional formula. Restricted to the original GZ syntax, the resulting formula is reducible to a disjunction of conjunctions of literals but the formulation is still applicable even when the syntax is extended to allow for arbitrary formulas (including nested aggregates) in the condition. Once GZ-aggregates are represented as formulas, we establish a formal comparison (in terms of the logic of Here-and-There) to Ferraris' (F) aggregates, which are defined by a different formula translation involving nested implications. In particular, we prove that if we replace an F-aggregate by a GZ-aggregate in a rule head, we do not lose answer sets (although more can be gained). This extends the previously known result that the opposite happens in rule bodies, i.e., replacing a GZ-aggregate by an F-aggregate in the body may yield more answer sets. Finally, we characterize a class of aggregates for which GZ- and F-semantics coincide.
KW  - Aggregates
KW  - Answer Set Programming
Y1  - 2019
U6  - https://doi.org/10.1016/j.artint.2018.10.007
SN  - 0004-3702
SN  - 1872-7921
VL  - 274
SP  - 26
EP  - 43
PB  - Elsevier
CY  - Amsterdam
ER  - 
TY  - GEN
A1  - Cabalar, Pedro
A1  - Fandiño, Jorge
A1  - Schaub, Torsten H.
A1  - Schellhorn, Sebastian
T1  - Lower Bound Founded Logic of Here-and-There
T2  - Logics in Artificial Intelligence
N2  - A distinguishing feature of Answer Set Programming is that all atoms belonging to a stable model must be founded. That is, an atom must not only be true but provably true. This can be made precise by means of the constructive logic of Here-and-There, whose equilibrium models correspond to stable models. One way of looking at foundedness is to regard Boolean truth values as ordered by letting true be greater than false. Then, each Boolean variable takes the smallest truth value that can be proven for it. This idea was generalized by Aziz to ordered domains and applied to constraint satisfaction problems. As before, the idea is that a, say integer, variable gets only assigned to the smallest integer that can be justified. In this paper, we present a logical reconstruction of Aziz’ idea in the setting of the logic of Here-and-There. More precisely, we start by defining the logic of Here-and-There with lower bound founded variables along with its equilibrium models and elaborate upon its formal properties. Finally, we compare our approach with related ones and sketch future work.
Y1  - 2019
SN  - 978-3-030-19570-0
SN  - 978-3-030-19569-4
U6  - https://doi.org/10.1007/978-3-030-19570-0_34
SN  - 0302-9743
SN  - 1611-3349
VL  - 11468
SP  - 509
EP  - 525
PB  - Springer
CY  - Cham
ER  -