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 -