TY - GEN A1 - Cabalar, Pedro A1 - Fandiño, Jorge A1 - Schaub, Torsten 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 - TY - JOUR A1 - Cabalar, Pedro A1 - Dieguez, Martin A1 - Schaub, Torsten A1 - Schuhmann, Anna T1 - Towards metric temporal answer set programming JF - Theory and practice of logic programming N2 - We elaborate upon the theoretical foundations of a metric temporal extension of Answer Set Programming. In analogy to previous extensions of ASP with constructs from Linear Temporal and Dynamic Logic, we accomplish this in the setting of the logic of Here-and-There and its non-monotonic extension, called Equilibrium Logic. More precisely, we develop our logic on the same semantic underpinnings as its predecessors and thus use a simple time domain of bounded time steps. This allows us to compare all variants in a uniform framework and ultimately combine them in a common implementation. Y1 - 2020 U6 - https://doi.org/10.1017/S1471068420000307 SN - 1471-0684 SN - 1475-3081 VL - 20 IS - 5 SP - 783 EP - 798 PB - Cambridge Univ. Press CY - Cambridge [u.a.] ER - TY - JOUR A1 - Pearce, David A1 - Sarsakov, Vladimir A1 - Schaub, Torsten A1 - Tompits, Hans A1 - Woltran, Stefan T1 - A polynomial translation of logic programs with nested expressions into disjunctive logic programs Y1 - 2002 SN - 3-540-43930-7 ER - TY - JOUR A1 - Anger, Christian A1 - Gebser, Martin A1 - Janhunen, Tomi A1 - Schaub, Torsten T1 - What's a head without a body? Y1 - 2006 ER - TY - JOUR A1 - Mileo, Alessandra A1 - Schaub, Torsten T1 - Qualitative constraint enforcement in advanced policy specification Y1 - 2007 ER - TY - JOUR A1 - Durzinsky, Markus A1 - Marwan, Wolfgang A1 - Ostrowski, Max A1 - Schaub, Torsten A1 - Wagler, Annegret T1 - Automatic network reconstruction using ASP JF - Theory and practice of logic programming N2 - Building biological models by inferring functional dependencies from experimental data is an important issue in Molecular Biology. To relieve the biologist from this traditionally manual process, various approaches have been proposed to increase the degree of automation. However, available approaches often yield a single model only, rely on specific assumptions, and/or use dedicated, heuristic algorithms that are intolerant to changing circumstances or requirements in the view of the rapid progress made in Biotechnology. Our aim is to provide a declarative solution to the problem by appeal to Answer Set Programming (ASP) overcoming these difficulties. We build upon an existing approach to Automatic Network Reconstruction proposed by part of the authors. This approach has firm mathematical foundations and is well suited for ASP due to its combinatorial flavor providing a characterization of all models explaining a set of experiments. The usage of ASP has several benefits over the existing heuristic algorithms. First, it is declarative and thus transparent for biological experts. Second, it is elaboration tolerant and thus allows for an easy exploration and incorporation of biological constraints. Third, it allows for exploring the entire space of possible models. Finally, our approach offers an excellent performance, matching existing, special-purpose systems. Y1 - 2011 U6 - https://doi.org/10.1017/S1471068411000287 SN - 1471-0684 VL - 11 SP - 749 EP - 766 PB - Cambridge Univ. Press CY - New York ER - TY - JOUR A1 - Gebser, Martin A1 - Schaub, Torsten 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 - Ostrowski, Max A1 - Schaub, Torsten T1 - ASP modulo CSP The clingcon system JF - Theory and practice of logic programming N2 - We present the hybrid ASP solver clingcon, combining the simple modeling language and the high performance Boolean solving capacities of Answer Set Programming (ASP) with techniques for using non-Boolean constraints from the area of Constraint Programming (CP). The new clingcon system features an extended syntax supporting global constraints and optimize statements for constraint variables. The major technical innovation improves the interaction between ASP and CP solver through elaborated learning techniques based on irreducible inconsistent sets. A broad empirical evaluation shows that these techniques yield a performance improvement of an order of magnitude. Y1 - 2012 U6 - https://doi.org/10.1017/S1471068412000142 SN - 1471-0684 VL - 12 SP - 485 EP - 503 PB - Cambridge Univ. Press CY - New York 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 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 - Gebser, Martin A1 - Schaub, Torsten A1 - Thiele, Sven T1 - GrinGo : a new grounder for answer set programming Y1 - 2007 SN - 978-3-540- 72199-4 ER -