TY - JOUR A1 - Schaub, Torsten H. A1 - Brüning, Stefan A1 - Nicolas, Pascal T1 - XRay : a prolog technology theorem prover for default reasoning: a system description Y1 - 1996 SN - 3-540-61511-3 ER - TY - CHAP A1 - Gebser, Martin A1 - Hinrichs, Henrik A1 - Schaub, Torsten H. A1 - Thiele, Sven T1 - xpanda: a (simple) preprocessor for adding multi-valued propositions to ASP N2 - We introduce a simple approach extending the input language of Answer Set Programming (ASP) systems by multi-valued propositions. Our approach is implemented as a (prototypical) preprocessor translating logic programs with multi-valued propositions into logic programs with Boolean propositions only. Our translation is modular and heavily benefits from the expressive input language of ASP. The resulting approach, along with its implementation, allows for solving interesting constraint satisfaction problems in ASP, showing a good performance. Y1 - 2010 U6 - http://nbn-resolving.de/urn/resolver.pl?urn:nbn:de:kobv:517-opus-41466 ER - TY - JOUR A1 - Anger, Christian A1 - Gebser, Martin A1 - Janhunen, Tomi A1 - Schaub, Torsten H. T1 - What's a head without a body? Y1 - 2006 ER - TY - JOUR A1 - Brain, Martin A1 - Faber, Wolfgang A1 - Maratea, Marco A1 - Polleres, Axel A1 - Schaub, Torsten H. A1 - Schindlauer, Roman T1 - What should an ASP solver output? : a multiple position paper Y1 - 2007 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 - Fandinno, 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 - GEN A1 - Neubauer, Kai A1 - Haubelt, Christian A1 - Wanko, Philipp A1 - Schaub, Torsten H. T1 - Utilizing quad-trees for efficient design space exploration with partial assignment evaluation T2 - 2018 23rd Asia and South Pacific Design Automation Conference (ASP-DAC) N2 - Recently, it has been shown that constraint-based symbolic solving techniques offer an efficient way for deciding binding and routing options in order to obtain a feasible system level implementation. In combination with various background theories, a feasibility analysis of the resulting system may already be performed on partial solutions. That is, infeasible subsets of mapping and routing options can be pruned early in the decision process, which fastens the solving accordingly. However, allowing a proper design space exploration including multi-objective optimization also requires an efficient structure for storing and managing non-dominated solutions. In this work, we propose and study the usage of the Quad-Tree data structure in the context of partial assignment evaluation during system synthesis. Out experiments show that unnecessary dominance checks can be avoided, which indicates a preference of Quad-Trees over a commonly used list-based implementation for large combinatorial optimization problems. Y1 - 2018 SN - 978-1-5090-0602-1 U6 - https://doi.org/10.1109/ASPDAC.2018.8297362 SN - 2153-6961 SP - 434 EP - 439 PB - IEEE CY - New York ER - TY - JOUR A1 - Nicolas, Pascal A1 - Schaub, Torsten H. T1 - Un cadre général pour l'interrogation automatique en logiques des défauts Y1 - 1998 ER - TY - JOUR A1 - Delgrande, James Patrick A1 - Schaub, Torsten H. T1 - Two approaches to merging knowledge bases Y1 - 2004 SN - 3-540-23242-7 ER - TY - JOUR A1 - Borchert, P. A1 - Anger, Christian A1 - Schaub, Torsten H. A1 - Truszczynski, M. T1 - Towards systematic benchmarking in answer set programming : the dagstuhl initiative Y1 - 2004 SN - 3-540- 20721-x ER - TY - JOUR A1 - Cabalar, Pedro A1 - Dieguez, Martin A1 - Schaub, Torsten H. 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 - Delgrande, James Patrick A1 - Schaub, Torsten H. A1 - Tompits, Hans A1 - Wang, Kewen T1 - Towards a classification of preference handling approaches in nonmonotonic reasoning Y1 - 2002 SN - 1-577-35166-5 ER - TY - JOUR A1 - Linke, Thomas A1 - Schaub, Torsten H. T1 - Towards a classification of default logic Y1 - 1997 ER - TY - JOUR A1 - Flöter, André A1 - Nicolas, Jacques A1 - Schaub, Torsten H. A1 - Selbig, Joachim T1 - Threshold extraction in metabolite concentration data N2 - Motivation: Continued development of analytical techniques based on gas chromatography and mass spectrometry now facilitates the generation of larger sets of metabolite concentration data. An important step towards the understanding of metabolite dynamics is the recognition of stable states where metabolite concentrations exhibit a simple behaviour. Such states can be characterized through the identification of significant thresholds in the concentrations. But general techniques for finding discretization thresholds in continuous data prove to be practically insufficient for detecting states due to the weak conditional dependences in concentration data. Results: We introduce a method of recognizing states in the framework of decision tree induction. It is based upon a global analysis of decision forests where stability and quality are evaluated. It leads to the detection of thresholds that are both comprehensible and robust. Applied to metabolite concentration data, this method has led to the discovery of hidden states in the corresponding variables. Some of these reflect known properties of the biological experiments, and others point to putative new states Y1 - 2004 ER - TY - JOUR A1 - Flöter, André A1 - Nicolas, Jacques A1 - Schaub, Torsten H. A1 - Selbig, Joachim T1 - Threshold extraction in metabolite concentration data Y1 - 2003 UR - http://www.cs.uni-potsdam.de/wv/pdfformat/floeterGCB2003.pdf ER - TY - JOUR A1 - Nicolas, Pascal A1 - Schaub, Torsten H. T1 - The XRay system : an implementation platform for local query-answering in default logics Y1 - 1998 SN - 3-540-65312-0 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 - Gebser, Martin A1 - Kaminski, Roland A1 - Kaufmann, Benjamin A1 - Lühne, Patrick A1 - Obermeier, Philipp A1 - Ostrowski, Max A1 - Romero Davila, Javier A1 - Schaub, Torsten H. A1 - Schellhorn, Sebastian A1 - Wanko, Philipp T1 - The Potsdam Answer Set Solving Collection 5.0 JF - Künstliche Intelligenz N2 - The Potsdam answer set solving collection, or Potassco for short, bundles various tools implementing and/or applying answer set programming. The article at hand succeeds an earlier description of the Potassco project published in Gebser et al. (AI Commun 24(2):107-124, 2011). Hence, we concentrate in what follows on the major features of the most recent, fifth generation of the ASP system clingo and highlight some recent resulting application systems. Y1 - 2018 U6 - https://doi.org/10.1007/s13218-018-0528-x SN - 0933-1875 SN - 1610-1987 VL - 32 IS - 2-3 SP - 181 EP - 182 PB - Springer CY - Heidelberg ER - TY - JOUR A1 - Anger, Christian A1 - Gebser, Martin A1 - Linke, Thomas A1 - Neumann, Andre A1 - Schaub, Torsten H. T1 - The nomore++ approach to answer set solving Y1 - 2005 UR - http://www.cs.uni-potsdam.de/wv/pdfformat/angelinesc05c.pdf ER - TY - JOUR A1 - Anger, Christian A1 - Gebser, Martin A1 - Linke, Thomas A1 - Neumann, Andre A1 - Schaub, Torsten H. T1 - The nomore++ approach to answer set solving Y1 - 2005 UR - http://www.cs.uni-potsdam.de/wv/pdfformat/angelinesc05c.pdf ER - TY - JOUR A1 - Gebser, Martin A1 - Liu, Lengning A1 - Namasivayam, Gayathri A1 - Neumann, André A1 - Schaub, Torsten H. A1 - Truszczynski, Miroslaw T1 - The first answer set programming system competition Y1 - 2007 SN - 978-3-540- 72199-4 ER - TY - JOUR A1 - Schaub, Torsten H. T1 - The family of default logics Y1 - 1998 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 - Banbara, Mutsunori A1 - Inoue, Katsumi A1 - Kaufmann, Benjamin A1 - Okimoto, Tenda A1 - Schaub, Torsten H. A1 - Soh, Takehide A1 - Tamura, Naoyuki A1 - Wanko, Philipp T1 - teaspoon BT - solving the curriculum-based course timetabling problems with answer set programming JF - Annals of operation research N2 - Answer Set Programming (ASP) is an approach to declarative problem solving, combining a rich yet simple modeling language with high performance solving capacities. We here develop an ASP-based approach to curriculum-based course timetabling (CB-CTT), one of the most widely studied course timetabling problems. The resulting teaspoon system reads a CB-CTT instance of a standard input format and converts it into a set of ASP facts. In turn, these facts are combined with a first-order encoding for CB-CTT solving, which can subsequently be solved by any off-the-shelf ASP systems. We establish the competitiveness of our approach by empirically contrasting it to the best known bounds obtained so far via dedicated implementations. Furthermore, we extend the teaspoon system to multi-objective course timetabling and consider minimal perturbation problems. KW - Educational timetabling KW - Course timetabling KW - Answer set programming KW - Multi-objective optimization KW - Minimal perturbation problems Y1 - 2018 U6 - https://doi.org/10.1007/s10479-018-2757-7 SN - 0254-5330 SN - 1572-9338 VL - 275 IS - 1 SP - 3 EP - 37 PB - Springer CY - Dordrecht 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 - Gerbser, Martin A1 - Schaub, Torsten H. T1 - Tableau calculi for answer set programming Y1 - 2006 UR - http://www.cs.uni-potsdam.de/wv/pdfformat/gebsch06c.pdf U6 - https://doi.org/10.1007/11799573 SN - 0302-9743 ER - TY - GEN A1 - Schaub, Torsten H. A1 - Woltran, Stefan T1 - Special issue on answer set programming T2 - Künstliche Intelligenz Y1 - 2018 U6 - https://doi.org/10.1007/s13218-018-0554-8 SN - 0933-1875 SN - 1610-1987 VL - 32 IS - 2-3 SP - 101 EP - 103 PB - Springer CY - Heidelberg ER - TY - JOUR A1 - Schaub, Torsten H. A1 - Thielscher, Michael T1 - Skeptical query-answering in constrained default logic Y1 - 1996 SN - 3-540-61313-7 ER - TY - JOUR A1 - Besnard, Philippe A1 - Schaub, Torsten H. T1 - Significant inferences Y1 - 2000 SN - 1-55860-690-4 ER - TY - JOUR A1 - Besnard, Philippe A1 - Schaub, Torsten H. T1 - Signed systems for paraconsistent reasoning Y1 - 1998 ER - TY - JOUR A1 - Besnard, Philippe A1 - Schaub, Torsten H. T1 - Signed systems for paraconsistent reasoning Y1 - 1998 SN - 0168-7433 ER - TY - JOUR A1 - Gebser, Martin A1 - Obermeier, Philipp A1 - Schaub, Torsten H. A1 - Ratsch-Heitmann, Michel A1 - Runge, Mario T1 - Routing driverless transport vehicles in car assembly with answer set programming JF - Theory and practice of logic programming N2 - Automated storage and retrieval systems are principal components of modern production and warehouse facilities. In particular, automated guided vehicles nowadays substitute human-operated pallet trucks in transporting production materials between storage locations and assembly stations. While low-level control systems take care of navigating such driverless vehicles along programmed routes and avoid collisions even under unforeseen circumstances, in the common case of multiple vehicles sharing the same operation area, the problem remains how to set up routes such that a collection of transport tasks is accomplished most effectively. We address this prevalent problem in the context of car assembly at Mercedes-Benz Ludwigsfelde GmbH, a large-scale producer of commercial vehicles, where routes for automated guided vehicles used in the production process have traditionally been hand-coded by human engineers. Such adhoc methods may suffice as long as a running production process remains in place, while any change in the factory layout or production targets necessitates tedious manual reconfiguration, not to mention the missing portability between different production plants. Unlike this, we propose a declarative approach based on Answer Set Programming to optimize the routes taken by automated guided vehicles for accomplishing transport tasks. The advantages include a transparent and executable problem formalization, provable optimality of routes relative to objective criteria, as well as elaboration tolerance towards particular factory layouts and production targets. Moreover, we demonstrate that our approach is efficient enough to deal with the transport tasks evolving in realistic production processes at the car factory of Mercedes-Benz Ludwigsfelde GmbH. KW - automated guided vehicle routing KW - car assembly operations KW - answer set programming Y1 - 2018 U6 - https://doi.org/10.1017/S1471068418000182 SN - 1471-0684 SN - 1475-3081 VL - 18 IS - 3-4 SP - 520 EP - 534 PB - Cambridge Univ. Press CY - New York ER - TY - JOUR A1 - Delgrande, James Patrick A1 - Schaub, Torsten H. T1 - Reasoning with sets of preferences in default logic N2 - We present a general approach for representing and reasoning with sets of defaults in default logic, focusing on reasoning about preferences among sets of defaults. First, we consider how to control the application of a set of defaults so that either all apply (if possible) or none do (if not). From this, an approach to dealing with preferences among sets of default rules is developed. We begin with an ordered default theory, consisting of a standard default theory, but with possible preferences on sets of rules. This theory is transformed into a second, standard default theory wherein the preferences are respected. The approach differs from other work, in that we obtain standard default theories and do not rely on prioritized versions of default logic. In practical terms this means we can immediately use existing default logic theorem provers for an implementation. Also, we directly generate just those extensions containing the most preferred applied rules; in contrast, most previous approaches generate all extensions, then select the most preferred. In a major application of the approach, we show how semimonotonic default theories can be encoded so that reasoning can be carried out at the object level. With this, we can reason about default extensions from within the framework of a standard default logic. Hence one can encode notions such as skeptical and credulous conclusions, and can reason about such conclusions within a single extension Y1 - 2004 SN - 0824-7935 ER - TY - JOUR A1 - Delgrande, James Patrick A1 - Schaub, Torsten H. T1 - Reasoning with sets of preferences in default logic Y1 - 1998 SN - 3-540- 65271-x ER - TY - JOUR A1 - Delgrande, James Patrick A1 - Schaub, Torsten H. T1 - Reasoning credulously and skeptically within a single extension Y1 - 2003 ER - TY - JOUR A1 - Delgrande, James Patrick A1 - Schaub, Torsten H. T1 - Reasoning credulously and skeptically within a single extension Y1 - 2002 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 - 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 - Mileo, Alessandra A1 - Schaub, Torsten H. T1 - Qualitative constraint enforcement in advanced policy specification Y1 - 2007 ER - TY - JOUR A1 - Linke, Thomas A1 - Schaub, Torsten H. T1 - Putting default logics in perspective Y1 - 1996 SN - 3-540-61708-6 ER - TY - JOUR A1 - Schaub, Torsten H. A1 - Brüning, Stefan T1 - Prolog technology for default reasoning : proof theory and compilation techniques Y1 - 1998 ER - TY - JOUR A1 - Schaub, Torsten H. A1 - Brüning, Stefan T1 - Prolog technology for default reasoning Y1 - 1996 SN - 0-471-96809-9 ER - TY - JOUR A1 - Boesel, Andreas A1 - Linke, Thomas A1 - Schaub, Torsten H. T1 - Profiling answer set programming : the visualization component of the noMoRe System Y1 - 2004 SN - 3-540-23242-7 ER - TY - JOUR A1 - Schaub, Torsten H. A1 - Wang, T. T1 - Preferred well-founded semantics for logic programming by alternating fixpoints : preliminary report Y1 - 2002 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 - Gressmann, Jean A1 - Janhunen, Tomi A1 - Mercer, Robert E. A1 - Schaub, Torsten H. A1 - Thiele, Sven A1 - Tichy, Richard T1 - Platypus : a platform for distributed answer set solving Y1 - 2005 UR - http://www.cs.uni-potsdam.de/wv/pdfformat/grjamescthti05a.pdf ER - TY - JOUR A1 - Dimopoulos, Yannis A1 - Gebser, Martin A1 - Lühne, Patrick A1 - Romero Davila, Javier A1 - Schaub, Torsten H. T1 - plasp 3 BT - Towards Effective ASP Planning JF - Theory and practice of logic programming N2 - We describe the new version of the Planning Domain Definition Language (PDDL)-to-Answer Set Programming (ASP) translator plasp. First, it widens the range of accepted PDDL features. Second, it contains novel planning encodings, some inspired by Satisfiability Testing (SAT) planning and others exploiting ASP features such as well-foundedness. All of them are designed for handling multivalued fluents in order to capture both PDDL as well as SAS planning formats. Third, enabled by multishot ASP solving, it offers advanced planning algorithms also borrowed from SAT planning. As a result, plasp provides us with an ASP-based framework for studying a variety of planning techniques in a uniform setting. Finally, we demonstrate in an empirical analysis that these techniques have a significant impact on the performance of ASP planning. KW - knowledge representation and nonmonotonic reasoning KW - technical notes and rapid communications KW - answer set programming KW - automated planning KW - action and change Y1 - 2019 U6 - https://doi.org/10.1017/S1471068418000583 SN - 1471-0684 SN - 1475-3081 VL - 19 IS - 3 SP - 477 EP - 504 PB - Cambridge Univ. Press CY - New York ER - TY - JOUR A1 - Besnard, Philippe A1 - Schaub, Torsten H. A1 - Tompits, Hans A1 - Woltran, Stefan T1 - Paraconsistent reasoning via quantified boolean formulas : Part II: Circumscribing inconsistent theories Y1 - 2003 SN - 3-540- 409494-5 ER - TY - JOUR A1 - Besnard, Philippe A1 - Schaub, Torsten H. A1 - Tompits, Hans A1 - Woltran, Stefan T1 - Paraconsistent reasoning via quantified boolean formulas Y1 - 2002 SN - 3-540-44190-5 ER - TY - JOUR A1 - Besnard, Philippe A1 - Mercer, Robert E. A1 - Schaub, Torsten H. T1 - Optimality Theory via Default Logic Y1 - 2002 ER -