@misc{SchaubWoltran2018, author = {Schaub, Torsten H. and Woltran, Stefan}, title = {Special issue on answer set programming}, series = {K{\"u}nstliche Intelligenz}, volume = {32}, journal = {K{\"u}nstliche Intelligenz}, number = {2-3}, publisher = {Springer}, address = {Heidelberg}, issn = {0933-1875}, doi = {10.1007/s13218-018-0554-8}, pages = {101 -- 103}, year = {2018}, language = {en} } @misc{FrankKreitz2018, author = {Frank, Mario and Kreitz, Christoph}, title = {A theorem prover for scientific and educational purposes}, series = {Electronic proceedings in theoretical computer science}, journal = {Electronic proceedings in theoretical computer science}, number = {267}, publisher = {Open Publishing Association}, address = {Sydney}, issn = {2075-2180}, doi = {10.4204/EPTCS.267.4}, pages = {59 -- 69}, year = {2018}, abstract = {We present a prototype of an integrated reasoning environment for educational purposes. The presented tool is a fragment of a proof assistant and automated theorem prover. We describe the existing and planned functionality of the theorem prover and especially the functionality of the educational fragment. This currently supports working with terms of the untyped lambda calculus and addresses both undergraduate students and researchers. We show how the tool can be used to support the students' understanding of functional programming and discuss general problems related to the process of building theorem proving software that aims at supporting both research and education.}, language = {en} } @misc{SchaepersNiemuellerLakemeyeretal.2018, author = {Sch{\"a}pers, Bj{\"o}rn and Niemueller, Tim and Lakemeyer, Gerhard and Gebser, Martin and Schaub, Torsten H.}, title = {ASP-Based Time-Bounded Planning for Logistics Robots}, series = {Twenty-Eighth International Conference on Automated Planning and Scheduling (ICAPS 2018)}, journal = {Twenty-Eighth International Conference on Automated Planning and Scheduling (ICAPS 2018)}, publisher = {ASSOC Association for the Advancement of Artificial Intelligence}, address = {Palo Alto}, issn = {2334-0835}, pages = {509 -- 517}, year = {2018}, abstract = {Manufacturing industries are undergoing a major paradigm shift towards more autonomy. Automated planning and scheduling then becomes a necessity. The Planning and Execution Competition for Logistics Robots in Simulation held at ICAPS is based on this scenario and provides an interesting testbed. However, the posed problem is challenging as also demonstrated by the somewhat weak results in 2017. The domain requires temporal reasoning and dealing with uncertainty. We propose a novel planning system based on Answer Set Programming and the Clingo solver to tackle these problems and incentivize robot cooperation. Our results show a significant performance improvement, both, in terms of lowering computational requirements and better game metrics.}, language = {en} } @misc{BordihnNagyVaszil2018, author = {Bordihn, Henning and Nagy, Benedek and Vaszil, Gy{\"o}rgy}, title = {Preface: Non-classical models of automata and applications VIII}, series = {RAIRO-Theoretical informatics and appli and applications}, volume = {52}, journal = {RAIRO-Theoretical informatics and appli and applications}, number = {2-4}, publisher = {EDP Sciences}, address = {Les Ulis}, issn = {0988-3754}, doi = {10.1051/ita/2018019}, pages = {87 -- 88}, year = {2018}, language = {en} } @misc{LifschitzSchaubWoltran2018, author = {Lifschitz, Vladimir and Schaub, Torsten H. and Woltran, Stefan}, title = {Interview with Vladimir Lifschitz}, series = {K{\"u}nstliche Intelligenz}, volume = {32}, journal = {K{\"u}nstliche Intelligenz}, number = {2-3}, publisher = {Springer}, address = {Heidelberg}, issn = {0933-1875}, doi = {10.1007/s13218-018-0552-x}, pages = {213 -- 218}, year = {2018}, abstract = {This interview with Vladimir Lifschitz was conducted by Torsten Schaub at the University of Texas at Austin in August 2017. The question set was compiled by Torsten Schaub and Stefan Woltran.}, language = {en} } @misc{BrewkaSchaubWoltran2018, author = {Brewka, Gerhard and Schaub, Torsten H. and Woltran, Stefan}, title = {Interview with Gerhard Brewka}, series = {K{\"u}nstliche Intelligenz}, volume = {32}, journal = {K{\"u}nstliche Intelligenz}, number = {2-3}, publisher = {Springer}, address = {Heidelberg}, issn = {0933-1875}, doi = {10.1007/s13218-018-0549-5}, pages = {219 -- 221}, year = {2018}, abstract = {This interview with Gerhard Brewka was conducted by correspondance in May 2018. The question set was compiled by Torsten Schaub and Stefan Woltran.}, language = {en} } @misc{NeubauerHaubeltWankoetal.2018, author = {Neubauer, Kai and Haubelt, Christian and Wanko, Philipp and Schaub, Torsten H.}, title = {Utilizing quad-trees for efficient design space exploration with partial assignment evaluation}, series = {2018 23rd Asia and South Pacific Design Automation Conference (ASP-DAC)}, journal = {2018 23rd Asia and South Pacific Design Automation Conference (ASP-DAC)}, publisher = {IEEE}, address = {New York}, isbn = {978-1-5090-0602-1}, issn = {2153-6961}, doi = {10.1109/ASPDAC.2018.8297362}, pages = {434 -- 439}, year = {2018}, abstract = {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.}, language = {en} } @misc{BosserCabalarDieguezetal.2018, author = {Bosser, Anne-Gwenn and Cabalar, Pedro and Dieguez, Martin and Schaub, Torsten H.}, title = {Introducing temporal stable models for linear dynamic logic}, series = {16th International Conference on Principles of Knowledge Representation and Reasoning}, journal = {16th International Conference on Principles of Knowledge Representation and Reasoning}, publisher = {ASSOC Association for the Advancement of Artificial Intelligence}, address = {Palo Alto}, pages = {12 -- 21}, year = {2018}, abstract = {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.}, language = {en} } @misc{SahlmannSchwotzer2018, author = {Sahlmann, Kristina and Schwotzer, Thomas}, title = {Ontology-based virtual IoT devices for edge computing}, series = {Proceedings of the 8th International Conference on the Internet of Things}, journal = {Proceedings of the 8th International Conference on the Internet of Things}, publisher = {Association for Computing Machinery}, address = {New York}, isbn = {978-1-4503-6564-2}, doi = {10.1145/3277593.3277597}, pages = {1 -- 7}, year = {2018}, abstract = {An IoT network may consist of hundreds heterogeneous devices. Some of them may be constrained in terms of memory, power, processing and network capacity. Manual network and service management of IoT devices are challenging. We propose a usage of an ontology for the IoT device descriptions enabling automatic network management as well as service discovery and aggregation. Our IoT architecture approach ensures interoperability using existing standards, i.e. MQTT protocol and SemanticWeb technologies. We herein introduce virtual IoT devices and their semantic framework deployed at the edge of network. As a result, virtual devices are enabled to aggregate capabilities of IoT devices, derive new services by inference, delegate requests/responses and generate events. Furthermore, they can collect and pre-process sensor data. These tasks on the edge computing overcome the shortcomings of the cloud usage regarding siloization, network bandwidth, latency and speed. We validate our proposition by implementing a virtual device on a Raspberry Pi.}, language = {en} } @misc{BoehneKreitz2018, author = {B{\"o}hne, Sebastian and Kreitz, Christoph}, title = {Learning how to prove}, series = {Electronic proceedings in theoretical computer science}, journal = {Electronic proceedings in theoretical computer science}, number = {267}, publisher = {Open Publishing Association}, address = {Sydney}, issn = {2075-2180}, doi = {10.4204/EPTCS.267.1}, pages = {1 -- 18}, year = {2018}, abstract = {We have developed an alternative approach to teaching computer science students how to prove. First, students are taught how to prove theorems with the Coq proof assistant. In a second, more difficult, step students will transfer their acquired skills to the area of textbook proofs. In this article we present a realisation of the second step. Proofs in Coq have a high degree of formality while textbook proofs have only a medium one. Therefore our key idea is to reduce the degree of formality from the level of Coq to textbook proofs in several small steps. For that purpose we introduce three proof styles between Coq and textbook proofs, called line by line comments, weakened line by line comments, and structure faithful proofs. While this article is mostly conceptional we also report on experiences with putting our approach into practise.}, language = {en} }