I give a short introduction to Nemo\, a toolkit for rule-based reasoning and data processing that emphasises robustness and ease of use.

\n\nNemo is a scalable and efficient main-memory reasoner that supports an expressive extension of Datalog with support for datatypes\, existential rules\, aggregates\, and (stratified) negation. Built around this core is a versatile system of libraries and applications for interfacing with several data formats and programming languages\, use as a web application\, and IDE integration.

\n\nJoin online: https://bbb.tu-dresden.de/rooms/n5w-ghp-qoq-kts/join

DTSTAMP:20240702T112523 SEQUENCE:39908 END:VEVENT BEGIN:VEVENT SUMMARY:Data Complexity in Expressive Description Logics With Path Expressions URL://iccl.inf.tu-dresden.de/web/Data_Complexity_in_Expressive_Description_Logics_With_Path_Expressions UID://iccl.inf.tu-dresden.de/web/Data_Complexity_in_Expressive_Description_Logics_With_Path_Expressions DTSTART:20240613T110000 DTEND:20240613T120000 LOCATION:APB 3027 DESCRIPTION:In my recent IJCAI paper I established NP-completeness of the satisfiability problem (w.r.t. the data complexity) of the maximal known decidable fragments ZIQ\, ZOQ\, and ZOI of the very description logic ZOIQ (a.k.a. ALCHb^self_regOIQ).\nThe proof uniformly deals with these three logics\, by considering the DL ZOIQ but over forest-like structures dubbed quasi-forests.\nDuring the talk\, I will give a high-level overview of the proof\, and discuss its main ingredients and challenges.\n\nhttps://bbb.tu-dresden.de/rooms/n5w-ghp-qoq-kts/join DTSTAMP:20240613T085309 SEQUENCE:39784 END:VEVENT BEGIN:VEVENT SUMMARY:Musings on Graph Data\, Schemas\, Modality\, and Coinduction URL://iccl.inf.tu-dresden.de/web/Musings_on_Graph_Data,_Schemas,_Modality,_and_Coinduction UID://iccl.inf.tu-dresden.de/web/Musings_on_Graph_Data,_Schemas,_Modality,_and_Coinduction DTSTART:20240606T110000 DTEND:20240606T120000 LOCATION:APB 3027 DESCRIPTION:In this talk\, I'll report on a schema model for graph databases I thought about in late April 2019. The model itself has some nice theoretical and\, admittedly\, some weird practical consequences. The talk will provide some light in both directions. Up until the submission of my PhD thesis in October 2019\, I developed the schema model further and in that very moment\, after the submission\, itself and any continuation on that line of research practically died. This talk will be about its recent revival and potential continuations. DTSTAMP:20240603T115246 SEQUENCE:39746 END:VEVENT BEGIN:VEVENT SUMMARY:Chase Termination Beyond Polynomial Time URL://iccl.inf.tu-dresden.de/web/Chase_Termination_Beyond_Polynomial_Time UID://iccl.inf.tu-dresden.de/web/Chase_Termination_Beyond_Polynomial_Time DTSTART:20240530T110000 DTEND:20240530T120000 LOCATION:APB 3027 DESCRIPTION:The chase is a widely implemented approach to reason with tuple-generating dependencies (tgds\, aka. existential rules)\, used in data exchange\, data integration\, and ontology-based query answering. However\, it is merely a semi-decision procedure\, which may fail to terminate. Many decidable conditions have been proposed for tgds to ensure chase termination\, typically by forbidding some kind of “cycle” in the chase process. We propose a new criterion that explicitly allows some such cycles\, and yet ensures termination of the standard chase under reasonable conditions. This leads to new decidable fragments of tgds that are not only syntactically more general but also strictly more expressive than the fragments defined by prior acyclicity conditions. Indeed\, while known terminating fragments are restricted to PTime data complexity\, our conditions yield decidable languages for any 𝑘-ExpTime. We further refine our syntactic conditions to obtain fragments of tgds for which an optimised chase procedure decides query entailment in PSpace or 𝑘-ExpSpace\, respectively. DTSTAMP:20240429T081337 SEQUENCE:39627 END:VEVENT BEGIN:VEVENT SUMMARY:Minesweeper goes Kaboom (in ASP) - and what makes it difficult URL://iccl.inf.tu-dresden.de/web/Minesweeper_goes_Kaboom_(in_ASP)_-_and_what_makes_it_difficult UID://iccl.inf.tu-dresden.de/web/Minesweeper_goes_Kaboom_(in_ASP)_-_and_what_makes_it_difficult DTSTART:20240516T110000 DTEND:20240516T120000 LOCATION:APB 3027 DESCRIPTION:Kaboom is a fair Minesweeper game. The original Kaboom is implemented with a SAT solver\, and we present an implementation in ASP (Answer Set Programming). We will derive a recommender heuristic and demonstrate the game. At the end we will discuss what makes Minesweeper and Kaboom difficult and how they differ in that regard. DTSTAMP:20240508T143742 SEQUENCE:39669 END:VEVENT BEGIN:VEVENT SUMMARY:An Algebraic Notion of Conditional Independence\, and its Application to Knowledge Representation URL://iccl.inf.tu-dresden.de/web/An_Algebraic_Notion_of_Conditional_Independence,_and_its_Application_to_Knowledge_Representation UID://iccl.inf.tu-dresden.de/web/An_Algebraic_Notion_of_Conditional_Independence,_and_its_Application_to_Knowledge_Representation DTSTART:20240425T110000 DTEND:20240425T120000 LOCATION:APB 3027 DESCRIPTION:Conditional independence is a crucial concept supporting adequate modelling and efficient reasoning in probabilistics. In knowledge representation\, the idea of conditional independence has also been introduced for specific formalisms\, such as propositional logic and belief revision. In this talk\, I show how the notion of conditional independence can be studied in the algebraic framework of approximation fixpoint theory. This gives a language-independent account of conditional independence that can be straightforwardly applied to any logic with fixpoint semantics. It is shown how this notion allows to reduce global reasoning to parallel instances of local reasoning. Furthermore\, relations to existing notions of conditional independence are discussed and the framework is applied to normal logic programming and abstract dialectical frameworks. DTSTAMP:20240408T060609 SEQUENCE:39482 END:VEVENT BEGIN:VEVENT SUMMARY:Fighting my Proof Anxiety with Lean - The Restricted Chase Indeed Yields Universal Models URL://iccl.inf.tu-dresden.de/web/Ighting_my_Proof_Anxiety_with_Lean_-_The_Restricted_Chase_Indeed_Yields_Universal_Models UID://iccl.inf.tu-dresden.de/web/Ighting_my_Proof_Anxiety_with_Lean_-_The_Restricted_Chase_Indeed_Yields_Universal_Models DTSTART:20240418T110000 DTEND:20240418T120000 LOCATION:APB 3027 DESCRIPTION:The restricted chase is a fundamental reasoning algorithm in database theory that can be used for (conjunctive) query answering. For a given pair of a set of existential rules and a database\, the restricted chase yields a so-called universal model. Such a model can be embedded into every (other) model and therefore be used for query answering.\nWe present a formalization of the restricted chase in the interactive theorem proving language "Lean" including a (well-known) proof that the chase indeed yields a universal model. We shine a light on key parts of the formalization and discuss lessons learned in the process. DTSTAMP:20240419T151719 SEQUENCE:39591 END:VEVENT BEGIN:VEVENT SUMMARY:Generating molecule graphs from mass spectrometry results using Answer-Set-Programming URL://iccl.inf.tu-dresden.de/web/Generating_molecule_graphs_from_mass_spectrometry_results_using_Answer-Set-Programming UID://iccl.inf.tu-dresden.de/web/Generating_molecule_graphs_from_mass_spectrometry_results_using_Answer-Set-Programming DTSTART:20240328T110000 DTEND:20240328T120000 LOCATION:APB room 2026 DESCRIPTION:Abstract: Mass spectrometry is a procedure to determine the exact composition of chemicals analytically. However\, chemical properties heavily depend on the structure of the molecules. Therefore it is of interest\, to find possible structure formulas matching a given sum formula. In contrast to prior works on this subject\, we approach this problem with Answer-Set-Programming\, instead of giving a complex imperative implementation. To this end\, various problem encodings for the ASP-solver Clingo will be discussed. Avoiding the emission of isomorphic models\, methods of introducing symmetry-breaking constraints will be compared. Their evaluation focuses on weighting the reduction in undetected isomorphic copies against runtime overhead. Different hand-crafted constraints - adjusted specially for this problem - will be compared against automated methods.\n\nThe talk will take place in a hybrid fashion\, physically in the APB room 2026\, and online through the link: \nhttps://bbb.tu-dresden.de/b/pio-zwt-smp-aus DTSTAMP:20240508T143854 SEQUENCE:39672 END:VEVENT BEGIN:VEVENT SUMMARY:Answer Set Navigation alongside Quantitative Reasoning URL://iccl.inf.tu-dresden.de/web/Answer_Set_Navigation_alongside_Quantitative_Reasoning UID://iccl.inf.tu-dresden.de/web/Answer_Set_Navigation_alongside_Quantitative_Reasoning DTSTART:20240215T110000 DTEND:20240215T120000 LOCATION:APB room 3027 DESCRIPTION:Abstract: This is a so called status talk of PhD student Dominik Rusovac\, supervised by Sarah Alice Gaggl. The main goal of the thesis is to study the concept of answer set navigation. Essentially\, aiming at a systematic framework that consists of efficient and from the ground up characterised methods to deal with a large amount of answer sets (solutions) of a logic program (problem).\n\nThe talk will take place in a hybrid fashion\, physically in the APB room 3027\, and online through the link:\nhttps://bbb.tu-dresden.de/b/pio-zwt-smp-aus DTSTAMP:20240213T190705 SEQUENCE:39401 END:VEVENT BEGIN:VEVENT SUMMARY:SHACL validation over DL-Lite\, ELHI and Horn-SHIQ ontologies (or calculating the core chase layer-by-layer) URL://iccl.inf.tu-dresden.de/web/SHACL_validation_over_DL-Lite,_ELHI_and_Horn-SHIQ_ontologies_(or_calculating_the_core_chase_layer-by-layer) UID://iccl.inf.tu-dresden.de/web/SHACL_validation_over_DL-Lite,_ELHI_and_Horn-SHIQ_ontologies_(or_calculating_the_core_chase_layer-by-layer) DTSTART:20240208T110000 DTEND:20240208T120000 LOCATION:APB room 3027 DESCRIPTION:Abstract: SHACL is a widely used W3C standard to manage RDF data: it is used to express integrity constraints on "complete" data. These constraints may contain recursion and negation and many other kinds of exotic features\, like counting over paths expressed by regular expressions. As SHACL is intended for validation over complete data\, we add ontologies to the RDF data (and create a knowledge base) and ask what it means to combine both: we define validation of SHACL combined with ontologies as SHACL validation over the core chase of this knowledge base. \n\nHowever\, creating the core chase is not feasible in practice. To tackle this\, we propose a way to build the core chase in a layer-by-layer manner\, based on pre-calculated building blocks and without having to look for non-embedding endomorphisms\, as the usual core construction does. We use these building blocks to rewrite SHACL validation in case of ontologies to plain SHACL validation.\n\nThe talk will take place in a hybrid fashion\, physically in the APB room 3027\, and online through the link:\nhttps://bbb.tu-dresden.de/b/pio-zwt-smp-aus DTSTAMP:20240202T155647 SEQUENCE:39391 END:VEVENT BEGIN:VEVENT SUMMARY:ASYDE: An Argumentation-based System for classifYing Driving bEhaviors URL://iccl.inf.tu-dresden.de/web/ASYDE:_An_Argumentation-based_System_for_classifYing_Driving_bEhaviors UID://iccl.inf.tu-dresden.de/web/ASYDE:_An_Argumentation-based_System_for_classifYing_Driving_bEhaviors DTSTART:20240201T110000 DTEND:20240201T120000 LOCATION:APB room 2026 DESCRIPTION:Abstract: \nExamining the influence of human behavior on road safety is a matter of considerable interest. As\nstudies in this field have demonstrated a correlation between driver behavior and road safety over\nthe past decades\, there is a compelling need to develop a software system capable of impartially\nidentifying the typical driving behavior of motorists. The objective of this research is to create one\nor more algorithms capable of recognizing and classifying a driver's typical driving behavior by\nintegrating various data sources. Since different data sources may present conflicting information\ndue to noise errors or failures\, our goal is to resolve such ambiguities by employing artificial\nintelligence paradigms. We are currently exploring the potential use of a well-known AI framework\,\nnamely Dung’s Abstract Argumentation Framework (AAF). Argumentation Frameworks\, indeed\,\nprovide a valuable tool for analyzing and assessing conflicting pieces of information\, enabling us to\ndraw more accurate and dependable conclusions. Our argumentation-based system provides the\nuser with a driving certificate describing their driving behavior. In the certificate\, we outline\, for\neach predefined class C of driving behavior (e.g.\, calm driving\, normal driving\, aggressive driving)\,\nthe minimum and maximum percentage of time points where the driving behavior falls in C. The\nminimum percentage represents the time points where driver behavior has been classified in C\nwithout uncertainty\, whereas the maximum percentage encodes the time points where some other\nclasses in addition to C have been identified\, allowing for multiple interpretations.\nThe experimental evaluation baked up the need for intervals\, as for several time points ambiguity in\nidentifying classes occurred\, due to different measures collected by different sensors leading to\nconflicting information. Therefore\, assigning a single class is not always possible\; instead\, multiple\npossible interpretations need to be considered.\n\nThe talk will take place in a hybrid fashion\, physically in the APB room 2026\, and online through the link:\nhttps://bbb.tu-dresden.de/b/pio-zwt-smp-aus DTSTAMP:20240131T180744 SEQUENCE:39386 END:VEVENT BEGIN:VEVENT SUMMARY:A Logic-based Reasoning Framework for Graph Databases URL://iccl.inf.tu-dresden.de/web/A_Logic-based_Reasoning_Framework_for_Graph_Databases UID://iccl.inf.tu-dresden.de/web/A_Logic-based_Reasoning_Framework_for_Graph_Databases DTSTART:20240118T110000 DTEND:20240118T120000 LOCATION:APB room 3027 DESCRIPTION:In many scientific and industrial applications\, graph databases are gaining momentum thanks to the competitive performance they offer and their flexibility\, not to mention their interpretability. Still\, their uses remain somehow limited due to their lack of consistency-checking strategies. Here\, I introduce a scheme-based access to data in order to assert constraints and keep consistency\, while also opening possibilities for reasoning in logic-based approaches\, in a multi-strategy setting. The possible uses and capabilities are still under investigation\, but the potentialities in almost every domain seem to be promising.\n\nThe talk will take place in a hybrid fashion\, physically in the APB room 3027\, and online through the link:\nhttps://bbb.tu-dresden.de/b/pio-zwt-smp-aus DTSTAMP:20240117T133444 SEQUENCE:39339 END:VEVENT BEGIN:VEVENT SUMMARY:PAC Completion of Description Logic TBoxes URL://iccl.inf.tu-dresden.de/web/PAC_Completion_of_Description_Logic_TBoxes UID://iccl.inf.tu-dresden.de/web/PAC_Completion_of_Description_Logic_TBoxes DTSTART:20240111T110000 DTEND:20240111T120000 LOCATION:APB room 3027 DESCRIPTION:Abstract: In description logic knowledge bases\, there may be a need to ensure that the terminological part of the base is complete in the sense that it captures all relevant relations between concepts. In [1]\, a method was proposed that does this for a user-specified subset of concepts. The method is based on attribute exploration from formal concept analysis [2] and uses queries to acquire knowledge from a domain expert. It may however require an exponential (in the size of the output) number of queries. I will present a probably approximately correct version of the method based on an algorithm for learning propositional Horn formulas [3]. The method works for an arbitrary DL language allowing the bottom concept\, conjunction\, and negation. \nThis is a joint work with Barış Sertkaya (Frankfurt University of Applied Sciences).\n\nThe talk will take place in a hybrid fashion\, physically in the APB room 3027\, and online through the link:\nhttps://bbb.tu-dresden.de/b/pio-zwt-smp-aus DTSTAMP:20240109T194602 SEQUENCE:39267 END:VEVENT BEGIN:VEVENT SUMMARY:Logik geht durch den Magen -- modeling interesting phenomena in (not only) food computing URL://iccl.inf.tu-dresden.de/web/Logik_geht_durch_den_Magen_--_modeling_interesting_phenomena_in_(not_only)_food_computing UID://iccl.inf.tu-dresden.de/web/Logik_geht_durch_den_Magen_--_modeling_interesting_phenomena_in_(not_only)_food_computing DTSTART:20231214T110000 DTEND:20231214T120000 LOCATION:APB room 3027 DESCRIPTION:Abstract: The emerging field of food computing tackles\, among others\, problems of knowledge acquisition\, modeling\, and processing within the culinary domain. Food-related knowledge is often implicit\, contextual\, or culture-dependent. Making at least part of it explicit\, with some formalization\, opens up possibilities to develop intelligent knowledge-based solutions to assist humans in preparing and optimizing food. An interesting and relevant problem is searching for substitutions in food recipes\, a task motivated by different constraints and goals of a person\, and leveraging the knowledge of dieticians and/or food technologists.\nAddressing this challenge\, the following questions emerge: What is relevant knowledge when it comes to food recommendations and AI-based decision support for ingredient substitution? Is there space for knowledge-based systems in the age of large language models? How to formally represent and reason about diets\, allergies\, and other restrictions? What food-related knowledge graphs and ontologies are there and are they useful for practical applications?\nIn this seminar\, I will share my experience from the TAISTI project (“Development of a Technology based on Artificial Intelligence for inferring SubsTitutable recipe Ingredients”\, https://www.taisti.eu/)\, in particular ontology and knowledge graph engineering\, and logical reasoning over integrated knowledge. Apart from practical challenges\, I will also discuss interesting questions about the similarity of entities -- a problem that goes beyond the domain of food. I will present the entity set expansion problem and discuss recent proposals for formally describing the similarity of instances in knowledge bases and retrieving more entities ``of the same kind''.\n\nSpeaker bio: Weronika T. Adrian\, Ph.D. (wta@agh.edu.pl\, http://wtadrian.eu\, http://kraken.edu.pl) is an Assistant Professor and the Deputy Head of the Department of Applied Computer Science\, Faculty of Electrical Engineering\, Automatics\, Computer Science and Biomedical Engineering\, AGH University of Kraków\, Poland. Her research interests cover the theory and practice of semantic technologies\, knowledge graphs\, and logic programming. She (co-)authored nearly 70 publications in the field of AI. Obtained her Ph.D. in Mathematics and Computer Science from the University of Calabria (Italy)\, followed by a 2-year post-doctoral contract in the group of Prof. Nicola Leone. Dr. Adrian has been involved in multiple national and international R&D projects and EU programs. She is a laureate of the “Top 500 Innovators” scholarship at Stanford University (USA). Founder of Creativity and Innovation Lab Foundation\, a founder member of the Polish Artificial Intelligence Society\, and a former member of IEEE.\n\nThe talk will take place in a hybrid fashion\, physically in the APB room 3027\, and online through the link:\nhttps://bbb.tu-dresden.de/b/pio-zwt-smp-aus DTSTAMP:20231208T181548 SEQUENCE:39163 END:VEVENT BEGIN:VEVENT SUMMARY:Notation3 as an Existential Rule Language URL://iccl.inf.tu-dresden.de/web/Notation3_as_an_Existential_Rule_Language UID://iccl.inf.tu-dresden.de/web/Notation3_as_an_Existential_Rule_Language DTSTART:20231116T110000 DTEND:20231116T120000 LOCATION:APB 3027 DESCRIPTION:Abstract: Notation3 Logic (N3) is an extension of RDF that allows the user to write rules introducing new blank nodes to RDF graphs. Many applications (e.g.\, ontology mapping) rely on this feature as blank nodes – used directly or in auxiliary constructs – are omnipresent on the Web. However\, the number of fast N3 reasoners covering this very important feature of the logic is rather limited. On the other hand\, there are engines like VLog or Nemo which do not directly support Semantic Web rule formats but which are developed and optimized for very similar constructs: existential rules. In this paper\, we investigate the relation between N3 rules with blank nodes in their heads and existential rules. We identify a subset of N3 that can be mapped directly to existential rules and define such a mapping preserving the equivalence of N3 formulae. In order to also illustrate that in some cases N3 reasoning could benefit from our translation\, we then employ this mapping in an implementation to compare the performance of the N3 reasoners EYE and cwm to VLog and Nemo on N3 rules and their mapped counterparts. Our tests show that the existential rule reasoners perform particularly well for use cases containing many facts while especially the EYE reasoner is very fast when dealing with a high number of dependent rules. We thus provide a tool enabling the Semantic Web community to directly use existing and future existential rule reasoners and benefit from the findings of this active community.\n\nThe talk will take place in a hybrid fashion\, physically in the APB room 3027\, and online through the link:\nhttps://bbb.tu-dresden.de/b/pio-zwt-smp-aus DTSTAMP:20231114T071956 SEQUENCE:39052 END:VEVENT BEGIN:VEVENT SUMMARY:Abstract Domains for Database Manipulating Processes URL://iccl.inf.tu-dresden.de/web/Abstract_Domains_for_Database_Manipulating_Processes UID://iccl.inf.tu-dresden.de/web/Abstract_Domains_for_Database_Manipulating_Processes DTSTART:20231109T110000 DTEND:20231109T120000 LOCATION:APB room 3027 DESCRIPTION:Database manipulating systems (DMS) formalize operations on relational databases like adding new tuples or deleting existing ones. To ensure sufficient expressiveness for capturing practical database systems\, DMS operations incorporate guarding expressions first-order formulas over countable value domains. Those features impose infinite state\, infinitely branching processes thus making automated reasoning about properties like the reachability of states intractable. Most recent approaches\, therefore\, restrict DMS to obtain decidable fragments. Nevertheless\, a comprehensive semantic framework capturing full DMS\, yet incorporating effective notions of data abstraction and process equivalence is an open issue. In this paper\, we propose DMS process semantics based on principles of abstract interpretation. The concrete domain consists of all valid databases\, whereas the abstract domain employs different constructions for unifying sets of databases being semantically equivalent up to particular fragments of the DMS guard language. The connection between abstract and concrete domains is effectively established by homomorphic mappings whose properties and restrictions depend on the expressiveness of the DMS fragment under consideration. We instantiate our framework for canonical DMS fragments and investigate semantical preservation of abstractions up to bisimilarity\, being one of the strongest equivalence notions for operational process semantics.\n\nThe talk will take place in a hybrid fashion\, physically in the APB room 3027\, and online through the link:\nhttps://bbb.tu-dresden.de/b/pio-zwt-smp-aus DTSTAMP:20231107T114217 SEQUENCE:39024 END:VEVENT BEGIN:VEVENT SUMMARY:Bounded Treewidth and the Infinite Core Chase – Complications and Workarounds toward Decidable Querying URL://iccl.inf.tu-dresden.de/web/Bounded_Treewidth_and_the_Infinite_Core_Chase_%E2%80%93_Complications_and_Workarounds_toward_Decidable_Querying UID://iccl.inf.tu-dresden.de/web/Bounded_Treewidth_and_the_Infinite_Core_Chase_%E2%80%93_Complications_and_Workarounds_toward_Decidable_Querying DTSTART:20231102T110000 DTEND:20231102T120000 LOCATION:APB room 3027 DESCRIPTION:Abstract: The core chase\, a popular algorithm for answering conjunctive queries (CQs) over existential rules\, is guaranteed to terminate and compute a finite universal model whenever one exists\, leading to the equivalence of the universal-model-based and the chase-based definitions of finite expansion sets (fes) – a class of rulesets featuring decidable CQ entailment. In case of non-termination\, however\, it is non-trivial to define a "result" of the core chase\, due to its non-monotonicity. This causes complications when dealing with advanced decidability criteria based on the existence of (universal) models of finite treewidth. For these\, sufficient chase-based conditions have only been established for weaker\, monotonic chase variants.\nThis paper starts out from the – desirable and prima facie plausible – conjecture that the existence of a treewidth-bounded universal model and the existence of a treewidth-bounded core-chase sequence coincide – which would conveniently entail decidable CQ entailment whenever the latter holds. Perhaps surprisingly\, carefully crafted examples show that both directions of this conjectured correspondence fail. On a positive note\, we are still able to define an aggregation scheme for the infinite core chase that preserves treewidth bounds and produces a finitely universal model\, i.e.\, one that satisfies exactly the entailed CQs. This allows us to prove that the existence of a treewidth-bounded core-chase sequence *does* warrant decidability of CQ entailment (yet\, on other grounds than expected). Hence\, for the first time\, we are able to define a chase-based notion of bounded treewidth sets of rules that subsumes fes.\n\nThe talk will take place in a hybrid fashion\, physically in the APB room 3027\, and online through the link:\nhttps://bbb.tu-dresden.de/b/pio-zwt-smp-aus DTSTAMP:20231020T114317 SEQUENCE:38920 END:VEVENT BEGIN:VEVENT SUMMARY:Knowledge graphs: description\, validation and subsetting URL://iccl.inf.tu-dresden.de/web/Knowledge_graphs:_description,_validation_and_subsetting UID://iccl.inf.tu-dresden.de/web/Knowledge_graphs:_description,_validation_and_subsetting DTSTART:20231005T110000 DTEND:20231005T120000 LOCATION:APB room 3027 DESCRIPTION:Abstract: Knowledge graphs like Wikidata have reached great success in the representation and integration of vast amounts of information from different domains. The use of flexible data models\, without predefined schemas facilitates the aggregation of data from heterogeneous sources. However\, the lack of schemas also undermines the quality of the data available in knowledge graphs. Many times\, data curators have an implicit schema that can describe the data and be used to check the conformance of the data. The Shape Expressions (ShEx) language was created with the goal to describe and validate RDF and was adopted by Wikidata in the Entity Schemas namespace. In this talk\, we will briefly present the ShEx language and show some applications. More specifically\, we will show how ShEx can be used to describe and generate Wikidata subsets\, which can help the use of Wikidata as a research source.\n\nThe talk will take place in a hybrid fashion\, physically in the APB room 3027\, and online through the link:\nhttps://bbb.tu-dresden.de/b/pio-zwt-smp-aus DTSTAMP:20231002T140712 SEQUENCE:38736 END:VEVENT BEGIN:VEVENT SUMMARY:Temporal reasoning with DatalogMTL URL://iccl.inf.tu-dresden.de/web/Temporal_reasoning_with_DatalogMTL UID://iccl.inf.tu-dresden.de/web/Temporal_reasoning_with_DatalogMTL DTSTART:20230919T110000 DTEND:20230919T120000 LOCATION:APB room 2026 DESCRIPTION:Abstract: During the talk\, I will present DatalogMTL – an extension of Datalog with operators from metric temporal logic (MTL) – and our research on this formalism. DatalogMTL allows for performing complex temporal reasoning tasks over the rational timeline\, which makes it suitable for many practical applications. However\, performing the main reasoning tasks in this setting is computationally expensive\, e.g.\, fact entailment is EXPSPACE-complete in combined and PSPACE-complete in data complexity. High complexity\, together with the need of performing reasoning over infinite temporal structures\, makes developing practical algorithms for DatalogMTL challenging. I will describe our approaches to address these difficulties\, and discuss their experimental evaluation.\n\n\nThe talk will take place in a hybrid fashion\, physically in the APB room 2026\, and online through the link:\nhttps://bbb.tu-dresden.de/b/pio-zwt-smp-aus DTSTAMP:20230918T130921 SEQUENCE:38715 END:VEVENT BEGIN:VEVENT SUMMARY:Representative Answer Sets: Collecting Something of Everything URL://iccl.inf.tu-dresden.de/web/Representative_Answer_Sets:_Collecting_Something_of_Everything UID://iccl.inf.tu-dresden.de/web/Representative_Answer_Sets:_Collecting_Something_of_Everything DTSTART:20230914T110000 DTEND:20230914T120000 LOCATION:APB room 3027 DESCRIPTION:Title: Representative Answer Sets: Collecting Something of Everything\n\nAbstract: Answer set programming (ASP) is a popular problem\nsolving paradigm with applications in planning and configuration.\nIn practice\, the number of answer sets can be overwhelmingly high\,\nwhich naturally causes interest in a concise characterisation of the\nsolution space in terms of representative answer sets. We establish\na notion of representativeness that refers to the entropy of specified\ntarget atoms within a collection of answer sets. Accordingly\, we pro-\npose different approaches for collecting such representative answer\nsets\, based on answer set navigation. Finally\, we conduct experi-\nments using our prototypical implementation\, which reveals promis-\ning results.\n\nThe talk will take place in a hybrid fashion\, physically in the APB room 3027\, and online through the link:\nhttps://bbb.tu-dresden.de/b/pio-zwt-smp-aus DTSTAMP:20230911T151551 SEQUENCE:38697 END:VEVENT BEGIN:VEVENT SUMMARY:Formalizing "Formale Systeme" URL://iccl.inf.tu-dresden.de/web/Formalizing_%22Formale_Systeme%22 UID://iccl.inf.tu-dresden.de/web/Formalizing_%22Formale_Systeme%22 DTSTART:20230831T110000 DTEND:20230831T120000 LOCATION:APB room 3027 DESCRIPTION:Abstract: In undergraduate theoretical computer science courses\, students\nencounter many new concepts along with techniques to prove theorems\nabout those with mathematical rigour. Most of those definitions and\nproofs are both constructive in nature and fairly self contained\, since\nthey depend on only very few mathematical facts. This makes formalising\nthem in an automated theorem prover feasible and educational. The\nobjective of this project was to formalize a subset of the two lectures\n"Formale Systeme" and "Theoretische Informatik und Logik"\, serving both\nas a reference for students and as a starting point for future\nformalisations.\n\nThe LEAN theorem prover and programming language is a project under\nactive development with a large\, community maintained library of\nmathematical definitions and theorems called "mathlib". This makes it a\ngood fit for formalising the undergraduate computer science lectures.\nLEAN also incorporates interesting and convenient features\, notably a\nHaskell inspired type class resolution\, a first-class support for\nquotients and the ability to very easily extend the language with new\nnotations or tactics.\n\nWhile there has already been some effort to formalizing "Formale\nSysteme"\, most has been reimplemented to make the definitions easier to\nwork with\, taking special care to end up with small and reusable proofs.\nOverall the focus has been on regular languages\, where the equivalence\nof DFAs\, NFAs and regular grammars among each other is the major\nimplemented result.\n\nIn this talk I will give a short introduction to LEAN and outline the\ndefinitions and theorems that have been formalized as a part of this\nproject.\n\nThe talk will take place in a hybrid fashion\, physically in the APB room 3027\, and online through the link:\nhttps://bbb.tu-dresden.de/b/pio-zwt-smp-aus DTSTAMP:20230825T155022 SEQUENCE:38609 END:VEVENT BEGIN:VEVENT SUMMARY:On the Abstract Expressive Power of Description Logics with Concrete Domains URL://iccl.inf.tu-dresden.de/web/On_the_Abstract_Expressive_Power_of_Description_Logics_with_Concrete_Domains UID://iccl.inf.tu-dresden.de/web/On_the_Abstract_Expressive_Power_of_Description_Logics_with_Concrete_Domains DTSTART:20230824T110000 DTEND:20230824T120000 LOCATION:APB room 3027 DESCRIPTION:The talk will take place in a hybrid fashion\, physically in the APB room 3027\, and online through the link:\nhttps://bbb.tu-dresden.de/b/pio-zwt-smp-aus\n\nAbstract: Concrete domains have been introduced in Description Logic (DL) to\nenable reference to concrete objects (such as numbers) and predefined\npredicates on these objects (such as numerical comparisons) when\ndefining concepts. The main emphasis of research in this context was on\nfinding restrictions on the concrete domain such that its integration\ninto certain DLs preserves decidability. In particular\, it was shown\nthat ω-admissible concrete domains can be integrated into the DL ALC\nwithout causing undecidability.\n\nIn this paper\, we concentrate on investigating the expressive power of\nDLs with concrete domains. Basically\, their semantics is defined using\nfirst-order interpretations as abstract domains extended with partial\nfunctions from the abstract domain into the concrete domain.\nThe abstract expressive power of a given classical logic (first-order\nlogic or DL) extended with a concrete domain is determined by which\nclasses of first-order interpretations (i.e.\, abstract domains where we\nforget the partial functions and their values) can be expressed.\n\nTo show that such a class is not first-order definable\, one can try to\nuse a compactness argument\, i.e.\, prove that first-order definability\nwould lead to a contradiction to compactness of first-order logic (FO).\nIn the first part of the paper\, we will show that extensions of FO or\nALC with a homomorphism ω-compact concrete domain share many formal\nproperties with FO\, such as the compactness and the downward\nLöwenheim-Skolem property. Nevertheless\, their abstract expressive power\nneed not be contained in that of FO. Note that any ω-admissible concrete\ndomain is homomorphism ω-compact.\n\nIn the second part of the paper\, we investigate whether finitely-bounded\nhomogeneous structures\, which preserve decidability if employed as\nconcrete domains\, can be used to express certain universal first-order\nsentences\, which then could be added to knowledge bases without\ndestroying decidability. We will see that this requires rather strong\nconditions on the universal first-order sentences or an extended scheme\nfor integrating the concrete domain. DTSTAMP:20230821T104147 SEQUENCE:38603 END:VEVENT BEGIN:VEVENT SUMMARY:Do Repeat Yourself: Understanding Sufficient Conditions for Restricted Chase Non-Termination URL://iccl.inf.tu-dresden.de/web/Do_Repeat_Yourself:_Understanding_Sufficient_Conditions_for_Restricted_Chase_Non-Termination UID://iccl.inf.tu-dresden.de/web/Do_Repeat_Yourself:_Understanding_Sufficient_Conditions_for_Restricted_Chase_Non-Termination DTSTART:20230727T110000 DTEND:20230727T120000 LOCATION:APB room 3027 DESCRIPTION:Abstract: The disjunctive restricted chase is a sound and complete procedure for solving boolean conjunctive query entailment over knowledge bases of disjunctive existential rules. Alas\, this procedure does not always terminate and checking if it does is undecidable. However\, we can use acyclicity notions (sufficient conditions that imply termination) to effectively apply the chase in many real-world cases. To know if these conditions are as general as possible\, we can use cyclicity notions (sufficient conditions that imply non-termination). In this paper\, we discuss some issues with previously existing cyclicity notions\, propose some novel notions for non-termination by dismantling the original idea\, and empirically verify the generality of the new criteria.\n\nThe talk will take place in a hybrid fashion\, physically in the APB room 3027\, and online through the link:\nhttps://bbb.tu-dresden.de/b/pio-zwt-smp-aus DTSTAMP:20230724T172459 SEQUENCE:38568 END:VEVENT BEGIN:VEVENT SUMMARY:How I made my research more VISIBLE? Undecidability Results for ALC Extended with Visibly Pushdown Path Expressions. URL://iccl.inf.tu-dresden.de/web/How_I_made_my_research_more_VISIBLE%3F_Undecidability_Results_for_ALC_Extended_with_Visibly_Pushdown_Path_Expressions. UID://iccl.inf.tu-dresden.de/web/How_I_made_my_research_more_VISIBLE%3F_Undecidability_Results_for_ALC_Extended_with_Visibly_Pushdown_Path_Expressions. DTSTART:20230713T110000 DTEND:20230713T120000 LOCATION:APB room 3027 DESCRIPTION:Abstract: We investigate the impact of non-regular path expressions on the decidability of satisfiability checking and querying in description logics. Our primary object of interest is ALCvpl\, an extension of ALC with path expressions using visibly-pushdown languages\, which was shown to be decidable by Löding et al. in 2007. We prove that decidability of ALCvpl is preserved when enriching the logic with functionality\, but decidability is lost upon adding the seemingly innocent Self operator. We also consider the simplest non-regular (visibly-pushdown) language r#s# := {r^n s^n : n ∈ N}. We establish undecidability of the satisfiability problem for ALC extended with nominals and r#s#\, as well as the query entailment problem\, where such non-regular atoms are present in queries.\nThis work is based on the paper accepted to JELIA 2023\, which is going to be submitted to Logical Methods in Computer Science next week.\n\nThe talk will take place in a hybrid fashion\, physically in the APB room 3027\, and online through the link:\nhttps://bbb.tu-dresden.de/b/pio-zwt-smp-aus DTSTAMP:20230710T192135 SEQUENCE:38488 END:VEVENT BEGIN:VEVENT SUMMARY:Investigating the finite-cliquewidth-model property of C². URL://iccl.inf.tu-dresden.de/web/Navigating_ASP_Solution_Spaces UID://iccl.inf.tu-dresden.de/web/Navigating_ASP_Solution_Spaces DTSTART:20230706T110000 DTEND:20230706T120000 LOCATION:APB room 3027 DESCRIPTION:Abstract: I will try to explain to you the results of my internship on 2-variable logics (with counters) and how it interfaces with the cliquewidth notion. \n\nThe talk will take place in a hybrid fashion\, physically in the APB room 3027\, and online through the link:\nhttps://bbb.tu-dresden.de/b/pio-zwt-smp-aus DTSTAMP:20230706T073233 SEQUENCE:38479 END:VEVENT BEGIN:VEVENT SUMMARY:To Lead or to be Led: A Generalized Condorcet Jury Theorem under Dependence URL://iccl.inf.tu-dresden.de/web/To_Lead_or_to_be_Led:_A_Generalized_Condorcet_Jury_Theorem_under_Dependence UID://iccl.inf.tu-dresden.de/web/To_Lead_or_to_be_Led:_A_Generalized_Condorcet_Jury_Theorem_under_Dependence DTSTART:20230629T110000 DTEND:20230609T120000 LOCATION:APB room 3027 DESCRIPTION:Abstract: Aggregating pieces of information or beliefs held by (abstract) agents is central to a variety of belief merging applications. When the merging process aims at retrieving an underlying ground truth\, the Condorcet Jury Theorem (CJT) allows identifying voting rules that almost surely track the true piece of information for large groups of agents\, given that specific conditions are met. As essential assumptions\, the CJT relies on all agents being equally competent as well as independent from one another. In the search for a generalization of the CJT applicable to real-world scenarios\, both aforementioned assumptions were weakened separately. In this work\, we provide a generalization of the CJT that allows\, at the same time\, for heterogeneous competence levels across agents as well as a degree of dependence modeled through an opinion leader exerting influence on the electorate. Additionally\, we derive a concrete bound on the number of agents necessary to successfully track the underlying ground truth\, and examine the bound's tightness by means of statistical simulations.\n\nThe talk will take place in a hybrid fashion\, physically in the APB room 3027\, and online through the link:\nhttps://bbb.tu-dresden.de/b/pio-zwt-smp-aus DTSTAMP:20230623T151719 SEQUENCE:38412 END:VEVENT BEGIN:VEVENT SUMMARY:Deontic Explanations via Logical Argumentation. URL://iccl.inf.tu-dresden.de/web/Deontic_Explanations_via_Logical_Argumentation. UID://iccl.inf.tu-dresden.de/web/Deontic_Explanations_via_Logical_Argumentation. DTSTART:20230615T110000 DTEND:20230615T120000 LOCATION:APB room 3027 DESCRIPTION:Abstract: In many normative reasoning contexts\, one is not merely interested in knowing whether an obligation holds\, but also in why it holds despite other norms to the contrary. Answers to such why questions are deontic explanations. They not only lead to a better understanding of normative reasoning\, they also motivate compliance and collaboration. The importance of such explanations increases with the development of AI systems that need to comply with normative codes. The study of explanation is growing rapidly but\, so far\, little to no formal work has been done in the intersection of explanation and normative reasoning. What is more\, existing approaches in deontic logic do not make explicit the reasons why certain obligations do and do not hold given a normative system\, and are\, therefore\, not yet suitable for deontic explanations. In collaboration with Christian Strasser\, we developed Deontic Argumentation Calculi (DAC): Sequent-style proof systems tailored to the construction of deontic explanations. DAC generate transparent arguments that provide explicit reasons why certain obligations hold and why certain norms are inapplicable. We prove that Formal Argumentation (FA) frameworks instantiated with DAC arguments are sound and complete with respect to the nonmonotonic inference relation of the class of constrained Input/Output (I/O) logics\, a renowned formalism for defeasible reasoning with norms and their conflicts. We demonstrate how to employ DAC to generate deontic explanations using general tools from the FA literature. In particular\, we use these tools to generate deontic explanations as answers to contrastive questions of the form “Why am I obliged to ϕ\, despite ψ?”\n\nThe talk will take place in a hybrid fashion\, physically in the APB room 3027\, and online through the link:\nhttps://bbb.tu-dresden.de/b/pio-zwt-smp-aus DTSTAMP:20230613T100051 SEQUENCE:38351 END:VEVENT BEGIN:VEVENT SUMMARY:Querying Wikidata with GraphQL URL://iccl.inf.tu-dresden.de/web/Querying_Wikidata_with_GraphQL UID://iccl.inf.tu-dresden.de/web/Querying_Wikidata_with_GraphQL DTSTART:20230608T110000 DTEND:20230608T120000 LOCATION:APB room 3027 DESCRIPTION:Abstract: Knowledge graphs like Wikidata are widely used in commercial and\nresearch domains. They represent knowledge that conveys information\nabout the real world in the form of graphs. Often they are modelled\nusing directed-edge labelled graphs using the Resource Description\nFramework (RDF). RDF is a framework that represents information in the\nform of Linked Data. SPARQL is a protocol and query language for RDF. It\nis based on matching graph patterns and is used to query RDF graphs.\nSPARQL is a powerful query language as it is expressive\, and provides\nmany features to retrieve and manipulate data. However\, SPARQL queries\nare complex in nature and have a steep learning curve. There are few\ntools and libraries available to developers for working with SPARQL.\nGraphQL is a popular query language for working with APIs. It is a\nflexible query language and is designed to have a human-oriented syntax.\nThis makes it easy for developers to learn and implement it in\napplications. Moreover\, there are many supporting resources that help\nthe integration of GraphQL into the development of such systems.\n\nThe purpose of our work is to show ways of querying the knowledge graph\,\nWikidata\, using GraphQL queries. This helps avoid the complexity of\ndealing with SPARQL queries\, and makes use of the flexibility and\nfeatures offered by GraphQL. In this work\, we show some key differences\nbetween GraphQL and SPARQL. We show some existing commercial and\nopen-source solutions to query RDF data via GraphQL. Our main focus is\nto introduce two existing open-source solutions\, GraphQL-LD and\nHyperGraphQL\, that can be used to query Wikidata via GraphQL queries.\nBoth these approaches use GraphQL queries to act as layer of abstraction\nthat hides the complexity of SPARQL queries. We show extensively how\nthese approaches operate and the respective features that they offer. We\nprovide details on how we can use GraphQL-LD and HyperGraphQL to fetch\ndata from Wikidata and demonstrate the results. Since they are\nopen-source\, we made appropriate changes to the source code to implement\nthe approaches on Wikidata. The changes were also made to help analyse\nthe steps in the implementation and facilitate querying. Our results\nshow that some key differences between GraphQL-LD and HyperGraphQL exist\nin terms of implementation and features. We demonstrate these in this\nwork extensively and compare them via examples against standard GraphQL\nand SPARQL features.\n\nThe talk will take place in a hybrid fashion\, physically in the APB room 3027\, and online through the link:\nhttps://bbb.tu-dresden.de/b/pio-zwt-smp-aus DTSTAMP:20230605T112940 SEQUENCE:38277 END:VEVENT BEGIN:VEVENT SUMMARY:Database-Inspired Reasoning Problems in Description Logics With Path Expressions URL://iccl.inf.tu-dresden.de/web/Database-Inspired_Reasoning_Problems_in_Description_Logics_With_Path_Expressions UID://iccl.inf.tu-dresden.de/web/Database-Inspired_Reasoning_Problems_in_Description_Logics_With_Path_Expressions DTSTART:20230601T110000 DTEND:20230601T120000 LOCATION:APB room 3027 DESCRIPTION:This is a status talk (i.e. pre-PHD-defense talk) for the ongoing PHD thesis of Bartosz Bednarczyk\, supervised by Sebastian Rudolph (TU Dresden) and Emanuel Kieroński (University of Wrocław). The main goal of the thesis is to study database-inspired reasoning problems (e.g. satisfiability\, query entailment or query containment problems) for the very expressive family Z of description logics.\n\n\nThe talk will take place in a hybrid fashion\, physically in the APB room 3027\, and online through the link:\nhttps://bbb.tu-dresden.de/b/pio-zwt-smp-aus DTSTAMP:20230529T143105 SEQUENCE:38255 END:VEVENT BEGIN:VEVENT SUMMARY:Decidable (Ac)counting with Parikh and Muller: Adding Presburger Arithmetic to Monadic Second-Order Logic over Tree-Interpretable Structures URL://iccl.inf.tu-dresden.de/web/Decidable_(Ac)counting_with_Parikh_and_Muller:_Adding_Presburger_Arithmetic_to_Monadic_Second-Order_Logic_over_Tree-Interpretable_Structures UID://iccl.inf.tu-dresden.de/web/Decidable_(Ac)counting_with_Parikh_and_Muller:_Adding_Presburger_Arithmetic_to_Monadic_Second-Order_Logic_over_Tree-Interpretable_Structures DTSTART:20230525T110000 DTEND:20230525T120000 LOCATION:APB room 3027 DESCRIPTION:Abstract: We propose ωMSO⋈BAPA\, an expressive logic for describing countable structures\, which subsumes and transcends both Counting Monadic Second-Order Logic (CMSO) and Boolean Algebra with Presburger Arithmetic (BAPA). We show that satisfiability of ωMSO⋈BAPA is decidable over the class of labeled infinite binary trees. This result is established by an elaborate multi-step transformation into a particular normal form\, followed by the deployment of Parikh-Muller Tree Automata\, a novel kind of automaton for infinite labeled binary trees\, integrating and generalizing both Muller and Parikh automata while still exhibiting a decidable (in fact PSpace-complete) emptiness problem. By means of MSO-interpretations\, we lift the decidability result to all tree-interpretable classes of structures\, including the classes of finite/countable structures of bounded treewidth/cliquewidth/partitionwidth. We observe that satisfiability over (finite or infinite) labeled trees becomes undecidable even for a rather mild extension of ωMSO⋈BAPA.\n\nThe talk will take place in a hybrid fashion\, physically in the APB room 3027\, and online through the link:\nhttps://bbb.tu-dresden.de/b/pio-zwt-smp-aus DTSTAMP:20230517T121003 SEQUENCE:38185 END:VEVENT BEGIN:VEVENT SUMMARY:Discrete Linear Dynamical Systems: The Introduction. URL://iccl.inf.tu-dresden.de/web/Discrete_Linear_Dynamical_Systems:_The_Introduction. UID://iccl.inf.tu-dresden.de/web/Discrete_Linear_Dynamical_Systems:_The_Introduction. DTSTART:20230512T110000 DTEND:20230512T120000 LOCATION:APB room 2026 DESCRIPTION:Abstract: Linear Dynamical systems are a fundamental modelling paradigm in many branches of science\, and have been the subject of extensive research for many decades and are of profound interest\, both from a theoretical and a practical standpoint. For example\, reachability problems for linear dynamical systems attract attention due to their frequent occurrence in practice and their deep and wide-ranging connections with other fascinating areas of study\, such as problems on Markov chains\, quantum automata. In this presentation we are going to motivate the topic\, give the basic definitions and will consider some famous problems.\n\nThe talk will take place in a hybrid fashion\, physically in the APB room 3027\, and online through the link:\nhttps://bbb.tu-dresden.de/b/pio-zwt-smp-aus\n\nPlease take a note that the seminar will be held on Friday. DTSTAMP:20230509T113046 SEQUENCE:38143 END:VEVENT BEGIN:VEVENT SUMMARY:Can AI explanations skew our causal intuitions about the world? If so\, can we correct for that? URL://iccl.inf.tu-dresden.de/web/Can_AI_explanations_skew_our_causal_intuitions_about_the_world%3F_If_so,_can_we_correct_for_that%3F UID://iccl.inf.tu-dresden.de/web/Can_AI_explanations_skew_our_causal_intuitions_about_the_world%3F_If_so,_can_we_correct_for_that%3F DTSTART:20230504T110000 DTEND:20230504T120000 LOCATION:Online DESCRIPTION:Abstract: Explainable Artificial Intelligence provides methods for bringing in transparency into black-box artificial intelligence (AI) systems. These methods produce explanations of AI systems’ predictions that are aimed at increasing the understanding of the AI systems’ behavior and help us to appropriately calibrate our trust in these systems. In this talk\, I will explore some of the potential undesirable effects of providing explanations of AI systems to human users and ways to mitigate such effects. I start from the observation that most AI systems capture correlations and associations in data and not causal relationships. Explanations of the AI systems’ predictions would make the correlations more transparent. They would not\, however\, make the explained relationships causal. In four experiments\, I show how providing counterfactual explanations of AI systems’ predictions unjustifiably changes people’s beliefs about causal relationships in the real world. I also show how we may go about preventing such a change in beliefs and hope to open doors for further exploration into psychological effects of AI explanations on human recipients.\n\nThe talk will take place virtually through the link:\nhttps://bbb.tu-dresden.de/b/pio-zwt-smp-aus DTSTAMP:20230428T131233 SEQUENCE:38097 END:VEVENT BEGIN:VEVENT SUMMARY:A Pitch Rich with Width-Witchcraft – Model-Theoretic Criteria for Decidable Query Entailment URL://iccl.inf.tu-dresden.de/web/A_Pitch_Rich_with_Width-Witchcraft_%E2%80%93_Model-Theoretic_Criteria_for_Decidable_Query_Entailment UID://iccl.inf.tu-dresden.de/web/A_Pitch_Rich_with_Width-Witchcraft_%E2%80%93_Model-Theoretic_Criteria_for_Decidable_Query_Entailment DTSTART:20230420T110000 DTEND:20230420T120000 LOCATION:APB room 3027 DESCRIPTION:Abstract: Decidability of inferencing is commonly considered a very important property of logic-based knowledge representation formalisms\, required for the algorithmization and automation of reasoning. Yet\, oftentimes\, the corresponding (un)decidability arguments are idiosyncratic and do not shed much light on the underlying principles governing the divide.\nIn my talk\, I will review generic model-theoretic criteria for decidability of querying in fragments of first-order logic. I will describe a general framework by means of which decidability of query entailment can be established based on the existence of countermodels with certain structural properties. These properties depend on the ontology and query language used and range from finite domain over forest-like shape to width-finiteness employing width notions like treewidth and cliquewidth.\n\nThe talk will take place in a hybrid fashion\, physically in the APB room 3027\, and online through the link:\nhttps://bbb.tu-dresden.de/b/pio-zwt-smp-aus DTSTAMP:20230413T135216 SEQUENCE:38013 END:VEVENT BEGIN:VEVENT SUMMARY:Adventures in Computer Science -- Grades 1 & 2 URL://iccl.inf.tu-dresden.de/web/Adventures_in_Computer_Science_--_Grades_1_%26_2 UID://iccl.inf.tu-dresden.de/web/Adventures_in_Computer_Science_--_Grades_1_%26_2 DTSTART:20230330T110000 DTEND:20230330T120000 LOCATION:APB room 3027 DESCRIPTION:Have you sorted you toys at home by color or by size? Have you\never looked for this one particular pencil? Have you asked yourself\, why\ndid this search take so long or how can it be faster? The "World of\nAlgorithms" (German: Die Welt der Algorithmen) provides some useful\ntools for you to achieve your goals as quick as possible. This includes\nproblems that never crossed your minds before. We are going to look at\ncertain problems and their (algorithmic) solutions. It is our goal the\nlearn about the strategies leading to the solutions. We are also facing\nproblems that are so hard to solve for which a quick solutions is out of\nreach\, even for a modern computer.\n\nThis is a translation of the advertisement I provided for pupils at the\n39th Primary School here at Dresden for a so-called "Ganztagsangebot"\n(GTA for short) which is basically a 1 hour/week course\ninstitutionalized as afternoon activity. My target group has been\nchildren at the level of 1st and 2nd grade (ages 6 to 8). In this talk\,\nI will briefly explain what I planned to do\, what I did and what I'm\nplanning to do in this GTA. I will mainly elaborate on the experiences I\ngathered in teaching 6-8 year-olds over the course of this school year.\n\nThe talk will take place in a hybrid fashion\, physically in the APB room 3027\, and online through the link:\nhttps://bbb.tu-dresden.de/b/pio-zwt-smp-aus DTSTAMP:20230327T211414 SEQUENCE:37949 END:VEVENT BEGIN:VEVENT SUMMARY:Static Program Analysis in Datalog URL://iccl.inf.tu-dresden.de/web/Static_Program_Analysis_in_Datalog UID://iccl.inf.tu-dresden.de/web/Static_Program_Analysis_in_Datalog DTSTART:20230323T110000 DTEND:20230323T110000 LOCATION:APB room 3027 DESCRIPTION:Abstract: Doop is a framework for Program Analysis of Java code. It utilizes the Datalog engine Souffle to run high-speed analyses on an Intermediate Code Representation. Existing analyses mainly deal with larger-scope Pointer Analysis\, but not with local optimization possibilities. In this talk\, I focus on the implementation of local static analyses like Constant Folding\, Liveness and Available Expressions in Doop. I will give an introduction into the related frameworks\, and point out benefits and limitations of Doop and Souffle regarding each analysis. Furthermore I will compare my results to existing tools for static code analysis and give an outlook whether Doop is suitable for local static analysis.\n\nThe talk will take place in a hybrid fashion\, physically in the APB room 3027\, and online through the link:\nhttps://bbb.tu-dresden.de/b/pio-zwt-smp-aus DTSTAMP:20230320T112131 SEQUENCE:37925 END:VEVENT BEGIN:VEVENT SUMMARY:Relating Description Complexity to Entropy URL://iccl.inf.tu-dresden.de/web/Relating_Description_Complexity_to_Entropy UID://iccl.inf.tu-dresden.de/web/Relating_Description_Complexity_to_Entropy DTSTART:20230316T110000 DTEND:20230316T120000 LOCATION:APB room 3027 DESCRIPTION:We demonstrate some novel links between entropy and description complexity\, a notion referring to the minimal formula length for specifying given properties. Let MLU be the logic obtained by extending propositional logic with the universal modality\, and let GMLU be the corresponding extension with the ability to count. In the finite\, MLU is expressively complete for specifying sets of variable assignments\, while GMLU is expressively complete for multisets. We show that for MLU\, the model classes with maximal Boltzmann entropy are the ones with maximal description complexity. Concerning GMLU\, we show that expected Boltzmann entropy is asymptotically equivalent to expected description complexity multiplied by the number of proposition symbols considered. To contrast these results\, we prove that this link breaks when we move to considering first-order logic FO over vocabularies with higher-arity relations. To establish the aforementioned result\, we show that almost all finite models require relatively large FO-formulas to define them. Our results relate to links between Kolmogorov complexity and entropy\, demonstrating a way to conceive such results in the logic-based scenario where relational structures are classified by formulas of different sizes.\n\nThe talk will take place in a hybrid fashion\, physically in the APB room 3027\, and online through the link:\nhttps://bbb.tu-dresden.de/b/pio-zwt-smp-aus DTSTAMP:20230313T182807 SEQUENCE:37902 END:VEVENT BEGIN:VEVENT SUMMARY:From Provenance Polynomials to Provenance Patterns: More Mileage for Mere Mortals URL://iccl.inf.tu-dresden.de/web/From_Provenance_Polynomials_to_Provenance_Patterns:_More_Mileage_for_Mere_Mortals UID://iccl.inf.tu-dresden.de/web/From_Provenance_Polynomials_to_Provenance_Patterns:_More_Mileage_for_Mere_Mortals DTSTART:20230309T110000 DTEND:20230309T120000 LOCATION:APB room 3027 DESCRIPTION:Abstract: \nIt is well known that the commutative semiring of integer polynomials N[X] provides an elegant unifying framework (a.k.a. how-provenance) for a number of earlier provenance approaches in databases. A provenance-annotated answer A’ to a query Q reveals how outputs depend on inputs from the annotated database D′ and thus it can be used to answer strictly more questions than the original answer A = Q(D) without provenance. We propose to use provenance patterns\, a related notion implicit in earlier work\, to support answering additional questions\, not answerable by A′ alone. We show that the pattern-enhanced answer A* can be easily obtained as a by-product of computing A or A’. Using a detailed running example\, we illustrate questions that can and cannot be answered using A\, A′\, and A*\, respectively. Time allowing\, I’d also like to touch upon related research in answering why-not provenance questions. \n\nAbout the speaker:\nBertram Ludäscher is a professor at the School of Information Sciences at the University of Illinois\, Urbana-Champaign\, where he is also a faculty affiliate with the National Center for Supercomputing Applications (NCSA) and the CS department. Prior to joining UIUC\, he was a professor at the CS department and the UC Davis Genome Center at the University of California\, Davis. His research interests range from practical questions in scientific data management and workflow automation\, to database theory\, and knowledge representation & reasoning. Before his faculty appointments\, he was a research scientist at the San Diego Supercomputer Center (SDSC) and an adjunct faculty at the CSE department at UCSD. He holds a M.S. (Dipl.-Inform.) in CS from the University of Karlsruhe (K.I.T.) and a PhD (Dr. rer. nat.) from the University of Freiburg.\n\nThe talk will take place in a hybrid fashion\, physically in the APB room 3027\, and online through the link:\nhttps://bbb.tu-dresden.de/b/pio-zwt-smp-aus DTSTAMP:20230303T202039 SEQUENCE:37892 END:VEVENT BEGIN:VEVENT SUMMARY:Tunas - Fishing for Diverse Answer Sets: A Multi-Shot Trade up Strategy URL://iccl.inf.tu-dresden.de/web/Tunas_-_Fishing_for_Diverse_Answer_Sets:_A_Multi-Shot_Trade_up_Strategy UID://iccl.inf.tu-dresden.de/web/Tunas_-_Fishing_for_Diverse_Answer_Sets:_A_Multi-Shot_Trade_up_Strategy DTSTART:20230302T110000 DTEND:20230302T120000 LOCATION:APB room 2026 DESCRIPTION:Abstract: Answer set programming (ASP) solvers have advanced in recent years\, with a variety of different specialisation and overall development. Thus\, even more complex and detailed programs can be solved. A side effect of this development are growing solution spaces and the problem of how to find those answer sets one is interested in. One general approach is to give an overview in form of a small number of highly diverse answer sets. By choosing a favourite and repeating the process\, the user is able to leap through the solution space. But finding highly diverse answer sets is computationally expensive. In this paper we introduce a new approach called Tunas for Trade Up Navigation for Answer Sets to find diverse answer sets by reworking existing solution collections. The core idea is to collect diverse answer sets one after another by iteratively solving and updating the program. Once no more answer sets can be added to the collection\, the program is allowed to trade answer sets from the collection for different answer sets\, as long as the collection grows and stays diverse. Elaboration of the approach is possible in three variations\, which we implemented and compared to established methods in an empirical evaluation. The evaluation shows that the Tunas approach is competitive with existing methods\, and that efficiency of the approach is highly connected to the underlying logic program.\n\nThe talk will take place in a hybrid fashion\, physically in the APB room 3027\, and online through the link:\nhttps://bbb.tu-dresden.de/b/pio-zwt-smp-aus DTSTAMP:20230221T172612 SEQUENCE:37858 END:VEVENT BEGIN:VEVENT SUMMARY:Multilinguality in Knowledge Graphs URL://iccl.inf.tu-dresden.de/web/Multilinguality_in_Knowledge_Graphs UID://iccl.inf.tu-dresden.de/web/Multilinguality_in_Knowledge_Graphs DTSTART:20230216T110000 DTEND:20230216T120000 LOCATION:APB 3027 DESCRIPTION:Abstract: In this talk\, I will give an overview of my work in the domain of\nmultilingual knowledge graphs with a focus on Wikidata.\nI will speak about how well knowledge graphs are covered in terms of\nmultilingual information\, how to measure and increase their\nmutlilinguality\, and finally about the reuse of the multilingual\ninformation.\nIn particular\, I introduce a framework to measure knowledge graphs'\nlabels and language information for reuse in applications. Then\, I will\ngive an overview of the topic of machine translation of knowledge graph\nlabels. Further\, we explore the generation of multilingual text from\ntriples.\nI will tie in my most recent work on language models with regard to\nmultilingual and cross-cultural understanding.\n\nThe talk will take place in a hybrid fashion\, physically in the APB room 3027\, and online through the link:\nhttps://bbb.tu-dresden.de/b/pio-zwt-smp-aus DTSTAMP:20230208T210700 SEQUENCE:37838 END:VEVENT BEGIN:VEVENT SUMMARY:Strong Equivalence in Non-monotonic Reasoning URL://iccl.inf.tu-dresden.de/web/Strong_Equivalence_in_Non-monotonic_Reasoning UID://iccl.inf.tu-dresden.de/web/Strong_Equivalence_in_Non-monotonic_Reasoning DTSTART:20230119T110000 DTEND:20230119T120000 LOCATION:APB room 3027 DESCRIPTION:Abstract: In classical logic\, when two theories have the same models\, they are\nmutually replaceable in arbitrary contexts. This is not the case in\nvarious non-monotonic formalisms\, e.g. logic programs under the stable\nmodel semantics\, or abstract argumentation frameworks. There\, two\ntheories (programs/frameworks) can have the same models (stable\nmodels/extensions)\, but yet differ in their semantics when both are\nextended with the same third theory. To obtain mutual replaceability\, a\nstronger notion is needed – this equivalence across all possible\nextensions is known as strong equivalence.\n\nWe address the question on how non-monotonicity is related to this\ndivergence of standard and strong equivalence\, show examples of how\nstrong equivalence for concrete formalisms is analysed in the\nliterature\, and finally preview an abstract\, algebraic approach to\ncharacterising strong equivalence model-theoretically. DTSTAMP:20230116T210853 SEQUENCE:37756 END:VEVENT BEGIN:VEVENT SUMMARY:Efficient Dependency Analysis for Rule-Based Ontologies URL://iccl.inf.tu-dresden.de/web/Efficient_Dependency_Analysis_for_Rule-Based_Ontologies UID://iccl.inf.tu-dresden.de/web/Efficient_Dependency_Analysis_for_Rule-Based_Ontologies DTSTART:20230112T110000 DTEND:20230112T120000 LOCATION:APB room 3027 DESCRIPTION:Several types of dependencies have been proposed for the static analysis of existential rule ontologies\, promising insights about computational properties and possible practical uses of a given set of rules\, e.g.\, in ontology-based query answering. Unfortunately\, these dependencies are rarely implemented\, so their potential is hardly realised in practice. We focus on two kinds of rule dependencies - positive reliances and restraints - and design and implement optimised algorithms for their efficient computation. Experiments on real-world ontologies of up to more than 100\,000 rules show the scalability of our approach\, which lets us realise several previously proposed applications as practical case studies. In particular\, we can analyse to what extent rule-based bottom-up approaches of reasoning can be guaranteed to yield redundancy-free "lean" knowledge graphs (so-called cores) on practical ontologies. DTSTAMP:20230106T113352 SEQUENCE:37707 END:VEVENT BEGIN:VEVENT SUMMARY:Nested Sequents for First-Order Modal Logics via Reachability Rules URL://iccl.inf.tu-dresden.de/web/Nested_Sequents_for_First-Order_Modal_Logics_via_Reachability_Rules UID://iccl.inf.tu-dresden.de/web/Nested_Sequents_for_First-Order_Modal_Logics_via_Reachability_Rules DTSTART:20221215T110000 DTEND:20221215T120000 LOCATION:APB room 3027 DESCRIPTION:In this talk\, we present cut-free nested sequent calculi for first-order modal logics. We consider a diverse class of first-order modal logics obtained by imposing certain Horn conditions on the relational and domain structure of QK models. Labeled sequent calculi are then obtained via standard techniques from the semantics of these logics. We show how to derive nested calculi from labeled via the 'structural refinement' technique\, which consists of eliminating structural rules\, introducing reachability rules\, and translating notation. The reachability rules obtained via this method possess a unique functionality\, consisting of propagating and/or checking if data exists along certain paths within a nested sequent. We demonstrate how such rules operate and touch on the significance of the nested sequent formulation (in the first-order setting) which emerges naturally from the structural refinement methodology. DTSTAMP:20221211T170759 SEQUENCE:37645 END:VEVENT BEGIN:VEVENT SUMMARY:The Relevance of Formal Logics for Cognitive Logics\, and Vice Versa URL://iccl.inf.tu-dresden.de/web/The_Relevance_of_Formal_Logics_for_Cognitive_Logics,_and_Vice_Versa UID://iccl.inf.tu-dresden.de/web/The_Relevance_of_Formal_Logics_for_Cognitive_Logics,_and_Vice_Versa DTSTART:20221214T110000 DTEND:20221214T120000 LOCATION:APB room 2026 DESCRIPTION:Classical logics like propositional or predicate logic have been considered as the gold standard for rational human reasoning\, and hence as a solid\, desirable norm on which all human knowledge and decision making should be based\, ideally. For instance\, Boolean logic was set up as kind of an arithmetic framework that should help make rational reasoning computable in an objective way\, similar to the arithmetics of numbers. Computer scientists adopted this view to (literally) implement objective knowledge and rational deduction\, in particular for AI applications. Psychologists have used classical logics as norms to assess the rationality of human commonsense reasoning. However\, both disciplines could not ignore the severe limitations of classical logics\, e.g.\, computational complexity and undecidedness\, failures of logic-based AI systems in practice\, and lots of psychological paradoxes. Many of these problems are caused by the inability of classical logics to deal with uncertainty in an adequate way. Both disciplines have used probabilities as a way out of this dilemma\, hoping that numbers and the Kolmogoroff axioms can do the job (somehow). However\, psychologists have been observing also lots of paradoxes here (maybe even more).\n\nSo then\, are humans hopelessly irrational? Is human reasoning incompatible with formal\, axiomatic logics? In the end\, should computer-based knowledge and information processing be considered as superior in terms of objectivity and rationality?\n\nCognitive logics aim at overcoming the limitations of classical logics and resolving the observed paradoxes by proposing logic-based approaches that can model human reasoning consistently and coherently in benchmark examples. The basic idea is to reverse the normative way of assessing human reasoning in terms of logics resp. probabilities\, and to use typical human reasoning patterns as norms for assessing the cognitive quality of logics. Cognitive logics explore the broad field of logic-based approaches between the extreme points marked by classical logics and probability theory with the goal to find more suitable logics for AI applications\, on the one hand\, and to gain more insights into the rational structures of human reasoning\, on the other. DTSTAMP:20221211T104845 SEQUENCE:37643 END:VEVENT BEGIN:VEVENT SUMMARY:IASCAR: Incremental Answer Set Counting by Anytime Refinement URL://iccl.inf.tu-dresden.de/web/IASCAR:_Incremental_Answer_Set_Counting_by_Anytime_Refinement UID://iccl.inf.tu-dresden.de/web/IASCAR:_Incremental_Answer_Set_Counting_by_Anytime_Refinement DTSTART:20221124T110000 DTEND:20221124T120000 LOCATION:APB room 3027 DESCRIPTION:Answer set programming (ASP) is a popular declarative programming paradigm with various applications. Programs can easily have so many answer sets that they cannot be enumerated in practice\, but counting still allows to quantify solution spaces. If one counts under assumptions on literals\, one obtains a tool to comprehend parts of the solution space\, so called answer set navigation. But navigating through parts of the solution space requires counting many times\, which is expensive in theory. There\, knowledge compilation compiles instances into representations on which counting works in polynomial time. However\, these techniques exist only for CNF formulas and compiling ASP programs into CNF formulas can introduce an exponential overhead. In this paper\, we introduce a technique to iteratively count answer sets under assumptions on knowledge compilations of CNFs that encode supported models. Our anytime technique uses the principle of inclusion-exclusion to systematically improve bounds by over- and undercounting. In a preliminary empirical analysis we demonstrate promising results. After compiling the input (offline phase) our approach quickly (re)counts. DTSTAMP:20221119T115255 SEQUENCE:37564 END:VEVENT END:VCALENDAR