BEGIN:VCALENDAR
PRODID:-//SMW Project//Semantic Result Formats
VERSION:2.0
METHOD:PUBLISH
X-WR-CALNAME:ICCL Events
BEGIN:VEVENT
SUMMARY:Tuple-Generating Dependencies Capture Complex Values
URL://iccl.inf.tu-dresden.de/web/Tuple-Generating_Dependencies_Capture_Complex_Values
UID://iccl.inf.tu-dresden.de/web/Tuple-Generating_Dependencies_Capture_Complex_Values
DTSTART:20220120T110000
DTEND:20220120T120000
LOCATION:Online
DESCRIPTION:We formalise a variant of Datalog that allows complex values constructed by nesting elements of\nthe input database in sets and tuples. We study its complexity and give a translation into sets\nof tuple-generating dependencies (TGDs) for which the standard chase terminates on any input\ndatabase. We identify a fragment for which reasoning is tractable. As membership is undecidable\nfor this fragment\, we develop decidable sufficient conditions. \n\nThe talk is about an accepted paper with Markus in ICDT 2022.\n\nLink to the online talk:\nhttps://bbb.tu-dresden.de/b/ali-zgz-l8d-52n
DTSTAMP:20220106T094428
SEQUENCE:35517
END:VEVENT
BEGIN:VEVENT
SUMMARY:An Introduction to Proof Theory II: More on the Sequent Calculus
URL://iccl.inf.tu-dresden.de/web/An_Introduction_to_Proof_Theory_II:_More_on_the_Sequent_Calculus
UID://iccl.inf.tu-dresden.de/web/An_Introduction_to_Proof_Theory_II:_More_on_the_Sequent_Calculus
DTSTART:20220113T110000
DTEND:20220113T120000
LOCATION:Online
DESCRIPTION:This talk is a sequel to the first lecture "An Introduction to Proof Theory I: Sequent Calculus\," which can be found at the following link: https://www.youtube.com/watch?v=grjMRgmjddE. In this talk\, we will briefly review notions introduced in the first talk such as what a sequent is\, types of inference rules\, and types of rule redundancy. Building off these notions\, we will then look at invertible rules\, cut-elimination\, and touch on how logics can be shown decidable via proof-search. All such concepts will be introduced within the framework of a sequent calculus for classical propositional logic. \n\nThe talk is online via BigBlueButton.\n\nLink:\nhttps://bbb.tu-dresden.de/b/ali-zgz-l8d-52n
DTSTAMP:20220107T142732
SEQUENCE:35524
END:VEVENT
BEGIN:VEVENT
SUMMARY:Answering Queries with Negation over Existential Rules
URL://iccl.inf.tu-dresden.de/web/Answering_Queries_with_Negation_over_Existential_Rules
UID://iccl.inf.tu-dresden.de/web/Answering_Queries_with_Negation_over_Existential_Rules
DTSTART:20220106T110000
DTEND:20220106T120000
LOCATION:Online
DESCRIPTION:Ontology-based query answering with existential rules is well understood and implemented for positive queries\, in particular conjunctive queries. The situation changes drastically for queries with negation\, where there is no agreed-upon semantics or standard implementation. Stratification\, as used for Datalog\, is not enough for existential rules\, since the latter still admit multiple universal models that can differ on negative queries. We\, therefore\, propose universal core models as a basis for meaningful (non-monotonic) semantics for queries with negation. Since cores are hard to compute\, we identify syntactic descriptions of queries that can equivalently be answered over other types of models. This leads to fragments of queries with negation that can safely be evaluated by current chase implementations. We establish new techniques to estimate how the core model differs from other universal models\, and we incorporate our findings into a new reasoning approach for existential rules with negation.\n\nThe talk is about an upcoming publication in AAAI 2022 by Stefan Ellmauthaler\, Markus Krötzsch\, Stephan Mennicke\n\nThe talk is online\,\nLink: https://bbb.tu-dresden.de/b/ali-zgz-l8d-52n
DTSTAMP:20220103T134220
SEQUENCE:35513
END:VEVENT
BEGIN:VEVENT
SUMMARY:Reliance-Based Optimization of Existential Rule Reasoning
URL://iccl.inf.tu-dresden.de/web/Reliance-Based_Optimization_of_Existential_Rule_Reasoning
UID://iccl.inf.tu-dresden.de/web/Reliance-Based_Optimization_of_Existential_Rule_Reasoning
DTSTART:20211209T094500
DTEND:20211209T104500
LOCATION:Online
DESCRIPTION:Existential rules is a powerful formalism for describing implicit knowledge contained within a dataset. Extracting such knowledge can be achieved with the chase\, which is a well-known algorithm for computing universal models. This is done by exhaustively calculating the consequences of each given rule. However\, the order in which the rules are selected can have a significant impact on the run time of the procedure as well as the number of derived facts. It was discovered in recent work that core-stratified rule sets allow for a selection strategy that is guaranteed to produce so-called core models\, which\, in the finite case\, correspond to the smallest possible universal models. The strategy is based on considering certain syntactic relationships between the rules called reliances. These indicate whether it is possible for a rule to produce facts used by another or if selecting a rule in the wrong order may introduce redundant facts into the result.\n\nIn this work\, we utilize these reliances to devise rule application strategies that optimize the chase procedure based on the following criteria: First\, we try to minimize the number of times rules are applied during the chase\, aiming to improve run times. Second\, we want to avoid applying rules in a way which introduces redundant facts. The goal here is to minimize the size of the resulting model\, ideally producing a core. While it is always possible to derive a core model in core-stratified rule sets\, we show situations where our approach is guaranteed to produce cores even if the rule set is not stratified. Moreover\, we give a detailed description of the algorithms necessary for detecting a reliance relationship between two given rules as well as prove their correctness. We implement our approach into the rule reasoning engine VLog and evaluate its effectiveness on several knowledge bases used for benchmarking as well as some real-world datasets. We find a significant improvement in the run times for a small portion of the considered knowledge bases and are able to match VLog in the remaining ones.\n\nThis is a diploma defense\, the talk is online.\nLink: https://bbb.tu-dresden.de/b/ali-zgz-l8d-52n
DTSTAMP:20211202T142824
SEQUENCE:35364
END:VEVENT
BEGIN:VEVENT
SUMMARY:Capturing Homomorphism-Closed Decidable Queries with Existential Rules
URL://iccl.inf.tu-dresden.de/web/Capturing_Homomorphism-Closed_Decidable_Queries_with_Existential_Rules
UID://iccl.inf.tu-dresden.de/web/Capturing_Homomorphism-Closed_Decidable_Queries_with_Existential_Rules
DTSTART:20211202T110000
DTEND:20211202T120000
LOCATION:Online
DESCRIPTION:Existential rules are a very popular ontology-mediated query language for which the chase represents a generic computational approach for query answering. It is straightforward that existential rule queries exhibiting chase termination are decidable and can only recognize properties that are preserved under homomorphisms. In this paper\, we show the converse: every decidable query that is closed under homomorphism can be expressed by an existential rule set for which the standard chase universally terminates. Membership in this fragment is not decidable\, but we show via a diagonalization argument that this is unavoidable.\nThis work has been presented in a relatively short presentation at KR 2021. This extended talk will have room for more in-depth explanations and discussions.\n\nThe talk is via BigBlueButton\, link:\nhttps://bbb.tu-dresden.de/b/ali-zgz-l8d-52n
DTSTAMP:20211125T120927
SEQUENCE:35320
END:VEVENT
BEGIN:VEVENT
SUMMARY:On Classical Decidable Logics extended with Percentage Quantifiers and Arithmetics
URL://iccl.inf.tu-dresden.de/web/On_Classical_Decidable_Logics_extended_with_Percentage_Quantifiers_and_Arithmetics
UID://iccl.inf.tu-dresden.de/web/On_Classical_Decidable_Logics_extended_with_Percentage_Quantifiers_and_Arithmetics
DTSTART:20211125T110000
DTEND:20211125T120000
LOCATION:Online
DESCRIPTION:The talk is based on my forthcoming FSTTCS'21 paper (https://iccl.inf.tu-dresden.de/web/Inproceedings3301/en) with the eponymous title\, co-authored with my two bachelor students (Anna Pacanowska and Maja Orłowska) and my college Tony Tan from Taiwan.\nIn this work we investigated the extensions of classical decidable logics with percentage quantifiers\, specifying how frequently a formula is satisfied in the indented model. We showed\, surprisingly\, that both the two-variable logic and the guarded fragment become undecidable under such extension\, sharpening the existing results in the literature. Our negative results are supplemented by decidability of the two-variable guarded fragment with even more expressive counting\, namely Presburger constraints. Our results can be applied to infer decidability of various modal and description logics\, e.g. Presburger Modal Logics with Converse or ALCI\, with expressive cardinality constraints.\n\nThe talk is online\, link to the talk:\n\nhttps://bbb.tu-dresden.de/b/ali-zgz-l8d-52n
DTSTAMP:20211122T135932
SEQUENCE:35311
END:VEVENT
BEGIN:VEVENT
SUMMARY:Flexible Dispute Derivations with Forward and Backward Arguments for Assumption-Based Argumentation
URL://iccl.inf.tu-dresden.de/web/Flexible_Dispute_Derivations_with_Forward_and_Backward_Arguments_for_Assumption-Based_Argumentation
UID://iccl.inf.tu-dresden.de/web/Flexible_Dispute_Derivations_with_Forward_and_Backward_Arguments_for_Assumption-Based_Argumentation
DTSTART:20211118T110000
DTEND:20211118T120000
LOCATION:Online
DESCRIPTION:Assumption-based argumentation (ABA) is one of the main general frameworks for structured argumentation. Dispute derivations for ABA allow for evaluating claims in a dialectical manner: i.e. on the basis of an exchange of arguments and counter-arguments for a claim between a proponent and an opponent of the claim. Current versions of dispute derivations are geared towards determining (credulous) acceptance of claims w.r.t. the admissibility-based semantics that ABA inherits from abstract argumentation. Relatedly\, they make use of backwards or top down reasoning for constructing arguments. In this work we define flexible dispute derivations with forward as well as backward reasoning allowing us\, in particular\, to also have dispute derivations for finding admissible\, complete\, and stable assumption sets rather than only determine acceptability of claims. We give an argumentation-based definition of such dispute derivations and a more implementation friendly alternative representation in which disputes involve exchange of claims and rules rather than arguments. These can be seen as elaborations on\, in particular\, existing graph-based dispute derivations on two fronts: first\, in also allowing for forward reasoning\; second\, in that all arguments put forward in the dispute are represented by a graph and not only the proponents.\nor check:\nhttps://link.springer.com/chapter/10.1007/978-3-030-89391-0_9\n\nThe talk is online\, the room link for the talk:\nhttps://bbb.tu-dresden.de/b/ali-zgz-l8d-52n
DTSTAMP:20211115T093925
SEQUENCE:35280
END:VEVENT
BEGIN:VEVENT
SUMMARY:Admissibility in Probabilistic Argumentation
URL://iccl.inf.tu-dresden.de/web/Admissibility_in_Probabilistic_Argumentation
UID://iccl.inf.tu-dresden.de/web/Admissibility_in_Probabilistic_Argumentation
DTSTART:20211104T110000
DTEND:20211104T120000
LOCATION:Online
DESCRIPTION:Abstract argumentation is a prominent reasoning framework. It comes with a variety of semantics and has lately been enhanced by probabilities to enable a quantitative treatment of argumentation. While admissibility is a fundamental notion in the classical setting\, it has been merely reflected so far in the probabilistic setting. In this paper\, we address the quantitative treatment of argumentation based on probabilistic notions of admissibility in a way that they form fully conservative extensions of classical notions. In particular\, our building blocks are not the beliefs regarding single arguments. Instead\, we start from the fairly natural idea that whatever argumentation semantics is to be considered\, semantics systematically induces constraints on the joint probability distribution on the sets of arguments. In some cases there might be many such distributions\, even infinitely many ones\, in other cases\, there may be one or none. Standard semantic notions are shown to induce such sets of constraints\, and so do their probabilistic extensions. This allows them to be tackled by SMT solvers\, as we demonstrate by a proof-of-concept implementation. We present a taxonomy of semantic notions\, also in relation to published work\, together with a running example illustrating our achievements.\n\nThis is a talk regarding the paper at KR 2021. The talk will be given online via BigBlueButton. To access the room\, use the following link:\n\nRoom Link: \nhttps://bbb.tu-dresden.de/b/ali-zgz-l8d-52n
DTSTAMP:20211029T233155
SEQUENCE:35133
END:VEVENT
BEGIN:VEVENT
SUMMARY:Indexing for Datalog Materialisation with Leapfrog Triejoin
URL://iccl.inf.tu-dresden.de/web/Indexing_for_Datalog_Materialisation_with_Leapfrog_Triejoin
UID://iccl.inf.tu-dresden.de/web/Indexing_for_Datalog_Materialisation_with_Leapfrog_Triejoin
DTSTART:20211028T110000
DTEND:20211028T120000
LOCATION:Online
DESCRIPTION:Datalog is a well-understood relational query language and there are efficient reasoners based on different concepts and technologies. Nevertheless\, the search for faster and more efficient reasoners continues. A promising approach for further performance improvements is the so-called leapfrog triejoin by Veldhuizen. Leapfrog triejoin is a variable-oriented join algorithm\, similar to an ordered merge join\, and it computes the matches of a Datalog rule as a result trie following a previously defined variable order. The literature about leapfrog triejoin focuses on its application to a single join or\, respectively\, Datalog rule. Unfortunately\, applying leapfrog triejoin to whole Datalog programs during materialization yields new challenges. We concentrate on these challenges as well as on potential solutions.\n\nAs leapfrog triejoin requires suitable data structures for each rule\, it is prone to be inefficient when considering the rules of a program in isolation\, as this might introduce avoidable redundancy. Moreover\, the choice of ‘good’ variable orders is crucial for the performance of leapfrog triejoin. Hence\, we propose criteria for the quality of variable orders. For finding good variable orders\, we propose an optimal approach based on Answer Set Programming as well as a heuristic approach. Furthermore\, we show the trade-off between the optimality of the ASP approach and the required time in an evaluation.\n\nMoreover\, we generalize leapfrog triejoin to use partial variable orders. We discuss the resulting generalization of the data structures\, i.e.\, f-representations instead of tries\, and we show how to efficiently prepare them for leapfrog triejoin. To realize the potential of considering independent variables separately and the more succinct representation of relations\, we adapt leapfrog triejoin for partial variable orders. We show that\, on a set of benchmarks\, partial variable orders are of higher quality than total ones w.r.t. our optimization criteria.\n\nThis is a Diploma project defense and will be given online via BigBlueButton. To access the room\, use one of the following links:\n\nWith ZIH-Login:\nhttps://selfservice.zih.tu-dresden.de/l/link.php?m=154204&p=b7e638fd\n\nWithout ZIH-Login:\nhttps://selfservice.zih.tu-dresden.de/link.php?m=154204&p=19a754b0
DTSTAMP:20211022T141110
SEQUENCE:34970
END:VEVENT
BEGIN:VEVENT
SUMMARY:Ongoing Research in the NAVAS Project
URL://iccl.inf.tu-dresden.de/web/Ongoing_Research_in_the_NAVAS_Project
UID://iccl.inf.tu-dresden.de/web/Ongoing_Research_in_the_NAVAS_Project
DTSTART:20211021T110000
DTEND:20211021T120000
LOCATION:Online
DESCRIPTION:This talk provides an insight into the latest research of answer set navigation methods.
DTSTAMP:20211015T152537
SEQUENCE:34885
END:VEVENT
BEGIN:VEVENT
SUMMARY:Seminar 07.10.2021
URL://iccl.inf.tu-dresden.de/web/Seminar_07.10.2021
UID://iccl.inf.tu-dresden.de/web/Seminar_07.10.2021
DTSTART:20211007T130000
DTEND:20211007T143000
LOCATION:Online
DESCRIPTION:Datalog boundedness is the property of a Datalog rule set that its recursion depth is independent of the database during query answering. This property is known to be undecidable and has been extensively studied. We give an overview of different perspectives on boundedness and relate boundedness to first-order rewritability. To build a strong intuition for the nature of boundnedness\, we define a new fragment of bounded Datalog rule sets and show its place amidst other bounded fragments.\n\n\nThis is a project defence and will be given online via BigBlueButton. To access the room\, use one of the following links:\n\nwith ZIH-login: \n\nhttps://selfservice.zih.tu-dresden.de/l/link.php?m=147898&p=494d5a1d\n\nwithout ZIH-login (i.e. external participants):\nhttps://selfservice.zih.tu-dresden.de/link.php?m=147898&p=2f89586e
DTSTAMP:20210917T062746
SEQUENCE:34583
END:VEVENT
BEGIN:VEVENT
SUMMARY:Seminar 23.09.2021
URL://iccl.inf.tu-dresden.de/web/Seminar_23.09.2021
UID://iccl.inf.tu-dresden.de/web/Seminar_23.09.2021
DTSTART:20210923T130000
DTEND:20210923T143000
LOCATION:Online
DESCRIPTION:Abstract argumentation and Dung’s framework is popular for modeling and evaluating arguments in artificial intelligence. Recently\, counting problems in abstract argumentation became of increasing interest visible by the 2021 ICCMA competition\, which asked to solve counting problems despite the high computational complexity. In this paper\, we consider various counting problems in abstract argumentation under practical aspects. We revisit previous theoretical algorithms\, present formulations in relational algebra\, and an implementation employing the DPDB framework for solving problems using dynamic programming on tree decompositions. Thereby\, we establish an implementation for counting extensions of abstract argumentation frameworks under admissible\, stable\, and complete semantics. We provide a thorough empirical evaluation that also incorporates less known approaches to solve counting questions in argumentation. Finally\, we show that our approach can be particularly well suited for instances of low treewidth and is quite useful in a portfolio-based solving approach.\n\n\nThis is a project presentation and with an approximate duration of 30 minutes and a 15 minutes Q&A session. It will be given online via BigBlueButton. To access the room\, use one of the following links:\n\nwith ZIH-login:\n\nhttps://selfservice.zih.tu-dresden.de/l/link.php?m=147897&p=76c02e6b\n\nwithout ZIH-login:\nhttps://selfservice.zih.tu-dresden.de/link.php?m=147897&p=05cc674a
DTSTAMP:20210916T083715
SEQUENCE:34580
END:VEVENT
BEGIN:VEVENT
SUMMARY:Seminar 16.09.2021
URL://iccl.inf.tu-dresden.de/web/Seminar_16.09.2021
UID://iccl.inf.tu-dresden.de/web/Seminar_16.09.2021
DTSTART:20210916T130000
DTEND:20210916T143000
LOCATION:Online
DESCRIPTION:The chase is a well studied sound and complete algorithm for computing universal models of knowledge bases that consist of an existential rule set and a set of facts. Since universal models can be used to solve generally undecidable reasoning tasks like BCQ entailment\, it is no surprise that termination of the chase is undecidable as well. While conditions for termination and non-termination of variants like the skolem- or restricted-chase have been studied extensively\, similar conditions for the core chase rarely exist. In practice\, the core chase does not seem to be feasible. Still\, compared to the other chase variants\, the core chase not only yields a universal model but even a core\, which intuitively is the smallest universal model that exists (up to isomorphism). Thus\, the core chase terminates if and only if the given knowledge base has a finite universal model. In recent work\, it has been shown that for rule sets that are “core-stratified”\, the restricted chase also yields universal models that are cores if it terminates.\nIn our work\, we strengthen the existing result and proof that restricted and core chase termination exactly coincide for core-stratified rule sets. This also implies that we can use sufficient conditions for restricted chase non-termination as sufficient conditions for the non-existence of finite universal models. We also find a new fragment of existential rules for which core chase termination is decidable based on an existing result that shows decidability of restricted chase termination for the same fragment and we conjecture that this even holds for a slightly larger fragment by generalizing the so-called Fairness Theorem\, which is a key part of the decidability proof. For non-core-stratified rule sets\, we investigate a possible heuristic for core computation and introduce the hybrid chase as a mixture of restricted and core chase as a new chase variant equivalent to the core chase.\n\n\nThis is a diploma thesis defence. It will be given online via BigBlueButton. To access the room\, use one of the following links:\n\nwith ZIH-login:\n\nhttps://selfservice.zih.tu-dresden.de/l/link.php?m=140092&p=6a50295d\n\nwithout ZIH-login:\nhttps://selfservice.zih.tu-dresden.de/link.php?m=140092&p=ea2e02f3
DTSTAMP:20210910T163925
SEQUENCE:34557
END:VEVENT
BEGIN:VEVENT
SUMMARY:Seminar 09.09.2021
URL://iccl.inf.tu-dresden.de/web/Seminar_09.09.2021
UID://iccl.inf.tu-dresden.de/web/Seminar_09.09.2021
DTSTART:20210909T130000
DTEND:20210909T143000
LOCATION:Online
DESCRIPTION:Ontologies and knowledge bases encode\, to a certain extent\, the stand-points or perspectives of their creators. As differences and conflicts between stand-points should be expected in multi-agent scenarios\, this will pose challenges for shared creation and usage of knowledge sources.\nOur work pursues the idea that\, in some cases\, a framework that can handle diverse and possibly conflicting standpoints is more useful and versatile than forcing their unification\, and avoids common compromises required for their merge. Moreover\, in analogy to the notion of family resemblance concepts\, we propose that a collection of standpoints can provide a simpler yet more faithful and nuanced representation of some domains.\nTo this end\, we present standpoint logic\, a multi-modal framework that is suitable for expressing information with semantically heterogeneous vocabularies\, where a standpoint is a partial and acceptable interpretation of the domain. Standpoints can be organised hierarchically and combined\, and complex correspondences can be established between them. We provide a formal syntax and semantics\, outline the complexity for the propositional case\, and explore the representational capacities of the framework in relation to standard techniques in ontology integration\, with some examples in the Bio-Ontology domain.\n\n\nThis is a test talk for a presentation at FOIS 2021. Thus it will have a duration of 15 minutes after which questions can be asked. The talk will be given online via BigBlueButton. To access the room\, use one of the following links:\n\nwith ZIH-login:\n\nhttps://selfservice.zih.tu-dresden.de/l/link.php?m=145027&p=4d1d790d\n\nwithout ZIH-login:\nhttps://selfservice.zih.tu-dresden.de/link.php?m=145027&p=93e20500
DTSTAMP:20210901T210024
SEQUENCE:34553
END:VEVENT
BEGIN:VEVENT
SUMMARY:Seminar 12.08.2021
URL://iccl.inf.tu-dresden.de/web/Seminar_12.08.2021
UID://iccl.inf.tu-dresden.de/web/Seminar_12.08.2021
DTSTART:20210812T130000
DTEND:20210812T143000
LOCATION:Online
DESCRIPTION:Although logical inferences are interpretable\, actually explaining them to a user is still a challenging task. While sometimes it may be enough to point out the axioms from the ontology that lead to the consequence of interest\, more complex inferences require proofs with intermediate steps that the user can follow. Our main hypothesis is that different users need different representations of proofs for optimal understanding. To this end\, we undertook some user experiments related to logical proofs. In particular\, we compared tree-shaped representations with linear\, text-based ones\, and for each we offered an interactive and a static version. The results of the experiment and the lessons learned will be reported in the talk.\n\n\nThis talk will take place online via BigBlueButton. To access the room\, use one of the following links:\n\nwith ZIH-login: \n\nhttps://selfservice.zih.tu-dresden.de/l/link.php?m=142879&p=5d643238\n\nwithout ZIH-login:\nhttps://selfservice.zih.tu-dresden.de/link.php?m=142879&p=911ffc8d
DTSTAMP:20210804T121824
SEQUENCE:34496
END:VEVENT
BEGIN:VEVENT
SUMMARY:Seminar 29.07.2021
URL://iccl.inf.tu-dresden.de/web/Seminar_29.07.2021
UID://iccl.inf.tu-dresden.de/web/Seminar_29.07.2021
DTSTART:20210729T130000
DTEND:20210729T143000
DESCRIPTION:Datalog is a well-understood relational query language and there are efficient implementations\, based on different concepts and technologies. Nevertheless\, the search for faster and more efficient reasoners continues. A promising approach for further improvements is the so-called leapfrog triejoin by Veldhuizen. Leapfrog triejoin is a variable-oriented join algorithm and computes the matches of a Datalog rule as a result tree following a previously defined variable order. Leapfrog triejoin is worst-case optimal w.r.t. the AGM bound\, which provides a tight bound on the maximum result size of full conjunctive queries\, and empirical evaluations suggest that leapfrog triejoin is relevant in practice\, too.\n\nThe focus of the current research concerning leapfrog triejoin lies on the theoretical and practical aspects of computing a single join. Implementing a Datalog reasoner based on leapfrog triejoin\, however\, requires to compute the consequences of a Datalog program with several rules and\, thus\, several joins. The main task is to find variable orders for all the joins that are both locally and globally good. We discuss challenges\, which arise naturally in this setting\, as well as potential approaches.\n\n\nThis talk will take place online via BigBlueButton. To access the room\, take one of the following links:\n\nwith ZIH-login: \n\nhttps://selfservice.zih.tu-dresden.de/l/link.php?m=136288&p=07d4d73e\n\nwithout ZIH-login:\nhttps://selfservice.zih.tu-dresden.de/link.php?m=136288&p=788f2a1a
DTSTAMP:20210729T123250
SEQUENCE:34489
END:VEVENT
BEGIN:VEVENT
SUMMARY:Seminar 22.07.2021
URL://iccl.inf.tu-dresden.de/web/Seminar_22.07.2021
UID://iccl.inf.tu-dresden.de/web/Seminar_22.07.2021
DTSTART:20210722T130000
DTEND:20210722T143000
LOCATION:Online
DESCRIPTION:Abstract dialectical frameworks (ADFs) are a formalism for representing knowledge about abstract arguments and various logical relationships between them. This talk presents an overview of some of our results on ADFs.\n\nFirstly\, we use the framework of approximation fixpoint theory to define various semantics that are known from related knowledge representation formalisms also for ADFs.\n\nWe then analyse the computational complexity of a variety of reasoning problems related to ADFs.\n\nAfterwards\, we also analyse the formal expressiveness in terms of realisable sets of interpretations and show how ADFs fare in comparison to other formalisms.\n\nFinally\, we show how ADFs can be put to use in instantiated argumentation\, where researchers try to assign meaning to sets of defeasible and strict rules.\n\nThe main outcomes of our work show that in particular the sublanguage of *bipolar* ADFs are a useful knowledge representation formalism with meaningful representational capabilities and acceptable computational properties. \n\n\n'''Short Bio:''' The speaker is a research associate in the Computational Logic Group. He obtained his BSc in Computer Science in 2006\, his (European) MSc in Computational Logic in 2008\, both from TUD\; his PhD about Non-monotonic Reasoning in Action Theories in 2012\, his Habilitation about the topic of this talk in 2017\, both from Leipzig University. Most recently\, he worked at compl3te GmbH in Leipzig dealing with automated problem solving\, before he joined TUD again.\n\n\nThis talk will take place online via BigBlueButton. To access the room\, take one of the following links:\n\nwith ZIH-login:\n\nhttps://selfservice.zih.tu-dresden.de/l/link.php?m=139679&p=9e3a0a4a\n\nwithout ZIH-login:\nhttps://selfservice.zih.tu-dresden.de/link.php?m=139679&p=7cb3769c
DTSTAMP:20210719T075225
SEQUENCE:34452
END:VEVENT
BEGIN:VEVENT
SUMMARY:Seminar 15.07.2021
URL://iccl.inf.tu-dresden.de/web/Seminar_15.07.2021
UID://iccl.inf.tu-dresden.de/web/Seminar_15.07.2021
DTSTART:20210715T130000
DTEND:20210715T143000
LOCATION:Online
DESCRIPTION:Datalog extended with existential rules is important for many reasoning tasks. To evaluate a Datalog program\, its rules are applied until no new facts can be derived. Crucially\, their execution order might significantly impact runtime\, memory consumption and even the number of derived facts. Our goal is to find an optimal execution strategy by analysing the relationship between the rules of a given program. We implemented our approach in VLog -- a Datalog rule execution engine -- and measured its impact on performance on several databases.\n\n\nThis talk will take place online via BigBlueButton. To access the room\, take one of the following links:\n\nwith ZIH-login: \n\nhttps://selfservice.zih.tu-dresden.de/l/link.php?m=133369&p=679d54f7\n\nwithout ZIH-login:\nhttps://selfservice.zih.tu-dresden.de/link.php?m=133369&p=e19bcdf1
DTSTAMP:20210706T143404
SEQUENCE:34170
END:VEVENT
BEGIN:VEVENT
SUMMARY:Seminar 08.07.2021
URL://iccl.inf.tu-dresden.de/web/Seminar_08.07.2021
UID://iccl.inf.tu-dresden.de/web/Seminar_08.07.2021
DTSTART:20210708T130000
DTEND:20210708T143000
LOCATION:Online
DESCRIPTION:The fluted fragment is a fragment of first-order logic in which the order of quantification of variables coincides with the order in which those variables appear as arguments of predicates. It is known that the fluted fragment possesses the finite model property. In this talk\, we extend the fluted fragment by the addition of counting quantifiers. We show that the resulting logic retains the finite model property\, and that the satisfiability problem for its (m+1)-variable sub-fragment is in m-NExpTime for all positive m. We also consider the satisfiability and finite satisfiability problems for the extension of any of these fragments in which the fluting requirement applies only to sub-formulas having at least three free variables.\n\nThis talk is based on the speakers paper [https://drops.dagstuhl.de/opus/volltexte/2021/14210/pdf/LIPIcs-ICALP-2021-141.pdf Fluted Logic with Counting] accepted at ICALP 2021.\n\n\n'''Short bio:''' Ian Pratt-Hartmann studied mathematics and philosophy at [http://www.bnc.ox.ac.uk Brasenose College\, Oxford]\, and philosophy at [http://www.princeton.edu/main/ Princeton] and [http://www.stanford.edu/ Stanford] Universities\, gaining his PhD. from Princeton. He is currently Senior Lecturer in the Department of Computer Science at the [http://www.manchester.ac.uk/ University of Manchester]. Since February\, 2014\, Dr. Pratt-Hartmann has held a joint appointment in the [http://informatyka.wmfi.uni.opole.pl/ Institute of Computer Science] at the [http://www.uni.opole.pl/ University of Opole]. His academic interests range widely over computational logic\, natural language semantics and artificial intelligence.\n\n\nThis talk will take place online via BigBlueButton. To access the room\, take one of the following links:\n\nwith ZIH-login:\n\nhttps://selfservice.zih.tu-dresden.de/l/link.php?m=128251&p=5a1cd43c\n\nwithout ZIH-login:\nhttps://selfservice.zih.tu-dresden.de/link.php?m=128251&p=14fd82b8
DTSTAMP:20210707T141757
SEQUENCE:34188
END:VEVENT
BEGIN:VEVENT
SUMMARY:Seminar 24.06.2021
URL://iccl.inf.tu-dresden.de/web/Seminar_24.06.2021
UID://iccl.inf.tu-dresden.de/web/Seminar_24.06.2021
DTSTART:20210624T130000
DTEND:20210624T143000
LOCATION:Online
DESCRIPTION:Concrete domains have been introduced in the area of Description Logic to enable reference to concrete objects (such as numbers) and predefined predicates on these objects (such as numerical comparisons) when defining concepts. Unfortunately\, in the presence of general concept inclusions (GCIs)\, which are supported by all modern DL systems\, adding concrete domains may easily lead to undecidability. To regain decidability of the DL ALC in the presence of GCIs\, quite strong restrictions\, in sum called omega-admissibility\, were imposed on the concrete domain. On the one hand\, we generalize the notion of omega-admissibility from concrete domains with only binary\npredicates to concrete domains with predicates of arbitrary arity. On the other hand\, we relate omega-admissibility to well-known notions from model theory. In particular\, we show that finitely bounded homogeneous structures yield omega-admissible concrete domains. This allows us to show omega-admissibility of concrete domains using existing results from model theory. When integrating concrete domains into lightweight DLs of the EL family\, achieving decidability is not enough. One wants reasoning in the resulting DL to be tractable. This can be achieved by using so-called p-admissible concrete domains and restricting the interaction between the DL and the concrete domain. We investigate p-admissibility from an algebraic point of view. Again\, this yields strong algebraic tools for demonstrating p-admissibility. In particular\, we obtain an expressive numerical p-admissible concrete domain based on the rational numbers. Although omega-admissibility and p-admissibility are orthogonal conditions that are almost exclusive\, our algebraic characterizations of these two properties allow us to locate an infinite class of p-admissible concrete domains whose integration into ALC yields decidable DLs.\n\n\nThis talk will take place online via BigBlueButton. To access the room\, take one of the following links:\n\nwith ZIH-login: \n\nhttps://selfservice.zih.tu-dresden.de/l/link.php?m=128250&p=cc3d308c\n\nwithout ZIH-login:\n\nhttps://selfservice.zih.tu-dresden.de/link.php?m=128250&p=0d4fa104
DTSTAMP:20210617T092039
SEQUENCE:34042
END:VEVENT
BEGIN:VEVENT
SUMMARY:Seminar 17.06.2021
URL://iccl.inf.tu-dresden.de/web/Seminar_17.06.2021
UID://iccl.inf.tu-dresden.de/web/Seminar_17.06.2021
DTSTART:20210617T130000
DTEND:20210617T140000
LOCATION:Online
DESCRIPTION:The Triguarded Fragment (TGF) is among the most expressive decidable fragments of first-order logic\, subsuming both its two-variable and guarded fragments without equality. We show that the TGF has the finite model property (providing a tight doubly exponential bound on the model size) and hence finite satisfiability coincides with satisfiability known to be N2ExpTime-complete. Using similar constructions\, we also establish 2ExpTime-completeness for finite satisfiability of the constant-free (tri)guarded fragment with transitive guards.\n\n\nThis talk will take place online via BigBlueButton. To access the room\, take one of the following links:\n\nwith ZIH-login: \n\nhttps://selfservice.zih.tu-dresden.de/l/link.php?m=128248&p=fac3a576\n\nwithout ZIH-login:\n\nhttps://selfservice.zih.tu-dresden.de/link.php?m=128248&p=9f228a78
DTSTAMP:20210610T111239
SEQUENCE:34011
END:VEVENT
BEGIN:VEVENT
SUMMARY:Enterprise Management in the Presence of Data
URL://iccl.inf.tu-dresden.de/web/Enterprise_Management_in_the_Presence_of_Data
UID://iccl.inf.tu-dresden.de/web/Enterprise_Management_in_the_Presence_of_Data
DTSTART:20210527T130000
DTEND:20210527T143000
LOCATION:Online
DESCRIPTION:This presentation discusses the two research lines of my work\, namely Enterprise Modelling and Knowledge Representation\, and their synergies. In the first line\, my PhD work has been structured around understanding\, clarifying and making use of the interconnections between the enterprise motivational and behavioural ontologies in Enterprise Computing. My research questions addressed the investigation of the suitable abstractions for the specification of motivational and behavioural concepts and their interconnections to allow synchronized movements between both structures. With the advent of Big data\, I became interested in combining such enterprise ontologies with data. My postdoctoral work uses the Ontology Based Data Access (OBDA) paradigm from Semantic Web to connect elements from the behavioural ontology with timestamped relational data sources. This approach allows business users to gain insights from data\, by allowing the reconstruction and querying of the state of behavioural elements using ontology as an intermediate layer in a vocabulary which is close to business users.\n\n\nShort Bio: Evellin Cardoso is currently a Post-Doctoral fellow at the KRDB Research Centre for Knowledge and Data\, at Free University of Bolzano working in the field of Process Mining\, Artificial Intelligence and Databases. She holds a PhD in Computer Science from University of Trento\, where she worked in the field of Information Systems\, more specifically Enterprises Architectures.\n\n\nThis talk will take place online via BigBlueButton. To access the room\, take one of the following links:\n\nwith ZIH-login:\n\nhttps://selfservice.zih.tu-dresden.de/l/link.php?m=115791&p=68e311bf\n\nwithout ZIH-login:\n\nhttps://selfservice.zih.tu-dresden.de/link.php?m=115791&p=37e2d8b6
DTSTAMP:20210504T073058
SEQUENCE:33833
END:VEVENT
BEGIN:VEVENT
SUMMARY:Seminar 20.05.2021
URL://iccl.inf.tu-dresden.de/web/Seminar_20.05.2021
UID://iccl.inf.tu-dresden.de/web/Seminar_20.05.2021
DTSTART:20210520T130000
DTEND:20210520T143000
LOCATION:Online
DESCRIPTION:We give a brief account of the Shapley value\, which is a powerful and elegant formalism aimed at distributing a surplus achieved jointly by a group of agents to the individual members.\nIt was first studied in theoretical economics\, but has since influenced many domains.\nUsing this concept\, we derive a notion of importance of states in a system with respect to satisfying a given temporal logic specification.\nThe aim is to measure how much the nondeterministic choices of a state influence the capacity of the system as a whole to satisfy the specification.\nWe will mainly consider linear temporal logic\, for which we study the exact complexity of determining the importance value.\nFinally\, we discuss how the formalism can be applied to computation tree logic and what additional challenges that brings.\n\n\nThis talk will have a duration of approximately 30 minutes and takes place online via BigBlueButton. To access the room\, take one of the following links:\n\nwith ZIH-login:\n\nhttps://selfservice.zih.tu-dresden.de/l/link.php?m=115787&p=a346519e\n\nwithout ZIH-login:\nhttps://selfservice.zih.tu-dresden.de/link.php?m=115787&p=c9c0523a
DTSTAMP:20210514T055922
SEQUENCE:33892
END:VEVENT
BEGIN:VEVENT
SUMMARY:Exploiting forwardness: Satisfiability and Query-Entailment in Forward Guarded Fragment
URL://iccl.inf.tu-dresden.de/web/Exploiting_forwardness:_Satisfiability_and_Query-Entailment_in_Forward_Guarded_Fragment
UID://iccl.inf.tu-dresden.de/web/Exploiting_forwardness:_Satisfiability_and_Query-Entailment_in_Forward_Guarded_Fragment
DTSTART:20210506T130000
DTEND:20210506T143000
LOCATION:Online
DESCRIPTION:We study the complexity of two standard reasoning problems for Forward Guarded Logic (FGF)\, obtained as a restriction of the Guarded Fragment in which variables appear in atoms in a specific order. We show that FGF enjoys the higher-arity-forest-model property\, which results in ExpTime-completeness of its (finite) knowledge-base satisfiability problem. Moreover\, we show that FGF is well-suited for knowledge representation. By employing a generalisation of the spoiler technique\, we prove that the conjunctive query entailment problem for FGF remains in ExpTime. We believe that our results are quite unusual as FGF is\, up to our knowledge\, the first decidable fragment of First-Order Logic\, extending standard description logics\, that offers unboundedly many variables and higher-arity relations while keeping its complexity surprisingly low.\n\n\nThis talk is based on an accepted paper submission to JELIA 2021 and will take approximately 30 minutes. It will take place online via BigBlueButton. To access the room\, take one of the following links: \n\n\nwith ZIH-login:\n\nhttps://selfservice.zih.tu-dresden.de/l/link.php?m=86974&p=57992a96\n\n\nwithout ZIH-login:\n\nhttps://selfservice.zih.tu-dresden.de/link.php?m=86974&p=f38fa613
DTSTAMP:20210223T085257
SEQUENCE:33120
END:VEVENT
BEGIN:VEVENT
SUMMARY:Seminar 29.04.2021
URL://iccl.inf.tu-dresden.de/web/Seminar_29.04.2021
UID://iccl.inf.tu-dresden.de/web/Seminar_29.04.2021
DTSTART:20210429T143000
DTEND:20210429T160000
LOCATION:Online
DESCRIPTION:Modern applications like recommender systems and question answering systems can leverage models beyond traditional data representations. These novel applications build upon knowledge\, which cannot be easily captured with relational data models used in databases. Instead\, Knowledge Graphs (KGs) allow for modeling\, in a semi-structured way\, inter-connected facts or statements annotated with semantics. In KGs\, concepts and entities correspond to nodes while their connections are modeled as directed and labeled edges\, creating a graph.\nWhile the models for representing relational data and KGs differ considerably\, the architecture for querying databases have served as a foundation for querying KGs. However\, not all the advancements in databases can be directly applied to KGs. This lecture will present some necessary extensions as well as successful applications of database techniques to efficiently execute queries over KGs. First\, I will introduce the problem of query optimization and present extensions to traditional optimizers to cope with the semi- structured nature of KGs. Then\, I will present the application of adaptive execution techniques to handle unexpected conditions when querying decentralized KGs. I will conclude with an outlook on future research directions\, which include preliminary results on applying Deep Learning to the problem of query optimization for KGs.\n\n\nMaribel Acosta studied Computer Science at the Universidad Simon Bolivar in Venezuela\, where she started working on Heterogeneous Databases and the Semantic Web. In 2017\, she finished her PhD in the Knowledge Management group at the Karlsruhe Institute of Technology (KIT) on the topic "Query Processing over Graph-structured Data on the Web". After that\, she was a postdoc and a lecturer (Akademische Rätin) at the Web Science group also at KIT. She has participated as a Track Chair of several international Semantic Web conferences and also as a reviewer in international conferences on the Web (WWW) and Artificial Intelligence (AAAI\, NEURIPS). Since October 2020\, Maribel is an Assistant Professor at the Ruhr University Bochum\, where she will hold lectures about Databases\, Information Systems\, and Knowledge Graphs. \n\n\nThis talk will take place online via BigBlueButton. To access the room\, take one of the following links: \n\nwith ZIH-login:\n\nhttps://selfservice.zih.tu-dresden.de/l/link.php?m=94316&p=76ddab55\n\n\nwithout ZIH-login:\n\nhttps://selfservice.zih.tu-dresden.de/link.php?m=94316&p=7b2c73ef
DTSTAMP:20210426T185728
SEQUENCE:33800
END:VEVENT
BEGIN:VEVENT
SUMMARY:A Semantic Characterization of Belief Base Revision for Arbitrary Monotonic Logics
URL://iccl.inf.tu-dresden.de/web/A_Semantic_Characterization_of_Belief_Base_Revision_for_Arbitrary_Monotonic_Logics
UID://iccl.inf.tu-dresden.de/web/A_Semantic_Characterization_of_Belief_Base_Revision_for_Arbitrary_Monotonic_Logics
DTSTART:20210422T130000
DTEND:20210422T143000
LOCATION:Online
DESCRIPTION:The AGM postulates by Alchourron\, Gärdenfors\, and Makinson continue to represent a cornerstone in research related to belief change. We generalize the approach of Katsuno and Mendelzon (KM) for characterizing AGM base revision from propositional logic to the setting of (multiple) base revision in arbitrary monotonic logics. Our core result is a representation theorem using the assignment of total – yet not transitive – “preference” relations to belief bases. We also provide a characterization of all logics for which our result can be strengthened to preorder assignments (as in KM’s original work).\n\n\nThis talk will take place online via BigBlueButton. To access the room\, take one of the following links:\n\nwith ZIH-login: \n\nhttps://selfservice.zih.tu-dresden.de/l/link.php?m=103268&p=3fab0d1a\n\nwithout ZIH-login:\n\nhttps://selfservice.zih.tu-dresden.de/link.php?m=103268&p=c61bdf2f
DTSTAMP:20210407T151457
SEQUENCE:33607
END:VEVENT
BEGIN:VEVENT
SUMMARY:Seminar 15.04.2021
URL://iccl.inf.tu-dresden.de/web/Seminar_15.04.2021
UID://iccl.inf.tu-dresden.de/web/Seminar_15.04.2021
DTSTART:20210415T130000
DTEND:20210415T143000
LOCATION:Online
DESCRIPTION:Proof theory is an important branch of mathematical logic that is primarily concerned with the study and application of mathematical proofs. One of the preferred formalisms in proof theory for building deductive systems is Gerhard Gentzen's sequent calculus formalism. This talk is intended as an introduction to proof theory and will introduce a variant of Gentzen's sequent calculus for classical propositional logic. Moreover\, the sequent calculus will be used to demonstrate and define fundamental proof theoretic notions such as sequents\, types of inference rules\, methods of soundness and completeness\, and properties of calculi.\n\n\nThis lecture will take place online via BigBlueButton. To access the room\, take one of the following links:\n\nwith ZIH-login:\n\nhttps://selfservice.zih.tu-dresden.de/l/link.php?m=88852&p=57980ee1\n\nwithout ZIH-login:\n\nhttps://selfservice.zih.tu-dresden.de/link.php?m=88852&p=7788afd1
DTSTAMP:20210407T194406
SEQUENCE:33610
END:VEVENT
BEGIN:VEVENT
SUMMARY:Seminar 08.04.2021
URL://iccl.inf.tu-dresden.de/web/Seminar_08.04.2021
UID://iccl.inf.tu-dresden.de/web/Seminar_08.04.2021
DTSTART:20210408T130000
DTEND:20210408T143000
LOCATION:Online
DESCRIPTION:For reasoning over ontologies\, (finite) universal models play an important role in tasks like conjunctive query answering\, which is undecidable. The (restricted) chase is a sound and complete algorithm for computing (finite) universal models of ontologies featuring existential rules. Termination of the chase is undecidable and various sufficient conditions for termination and non-termination have been studied. If the chase terminates\, we obtain a finite universal model. However\, if the chase does not terminate\, a finite universal model may still exist. In recent work\, it has been shown that for certain ontologies for which the chase terminates\, there exists a chase sequence that yields a universal model that is a core and therefore is the smallest universal model for the given rule set up to isomorphism. We extend this result to non-terminating chase sequences. By that\, we are able to introduce a sufficient condition for the existence of an infinite universal model that is a core which in turn implies that no finite universal model exists.\n\nNote that this talk acts as a colloquium/examination for the module INF-PM-FPG. It will take place online via BigBlueButton. To access the room\, take one of the following links: \n\nwith ZIH-login:\n\nhttps://selfservice.zih.tu-dresden.de/l/link.php?m=86971&p=30896df0\n\nwithout ZIH-login:\n\nhttps://selfservice.zih.tu-dresden.de/link.php?m=86971&p=83001746
DTSTAMP:20210301T092106
SEQUENCE:33385
END:VEVENT
BEGIN:VEVENT
SUMMARY:Using Datalog to Ground ASP Programs
URL://iccl.inf.tu-dresden.de/web/Using_Datalog_to_Ground_ASP_Programs
UID://iccl.inf.tu-dresden.de/web/Using_Datalog_to_Ground_ASP_Programs
DTSTART:20210401T130000
DTEND:20210401T143000
LOCATION:Online
DESCRIPTION:Answer Set Programming (ASP) is a powerful tool in Knowledge Representation and Reasoning. The typical approach to find the answer sets of an ASP program is a ground-and-solve approach\, where a grounder transforms an input program with variables into a ground program without variables and a solver computes the answer sets of the ground program. To be feasible\, this requires an intelligent grounding phase to keep the grounding relatively small.\nThe relational query language Datalog is related to ASP and has some similarities to it. Even though they arise from the same origin\, there might be recent progress in the development of fast Datalog reasoners\, which might be beneficial for grounding ASP programs. Thus\, we present an approach for an ASP grounder that uses a Datalog reasoner. We then implement this approach by using the Datalog reasoner VLog\, and we show that our implementation is competitive with state-of-the-art grounders. \n\n\nNote that this talk is a defence of a "Belegarbeit". It will take place online via BigBlueButton. To access the room\, take one of the following links: \n\n\nwith ZIH-login:\n\nhttps://selfservice.zih.tu-dresden.de/l/link.php?m=86969&p=6e64180f\n\n\nwithoput ZIH-login:\n\nhttps://selfservice.zih.tu-dresden.de/link.php?m=86969&p=94b73c2d
DTSTAMP:20210223T085215
SEQUENCE:33118
END:VEVENT
BEGIN:VEVENT
SUMMARY:"Most of" leads to undecidability: Failure of adding frequencies to LTL.
URL://iccl.inf.tu-dresden.de/web/%22Most_of%22_leads_to_undecidability:_Failure_of_adding_frequencies_to_LTL.
UID://iccl.inf.tu-dresden.de/web/%22Most_of%22_leads_to_undecidability:_Failure_of_adding_frequencies_to_LTL.
DTSTART:20210325T130000
DTEND:20210325T143000
LOCATION:Online
DESCRIPTION:(joint work with Jakub Michaliszyn from University of Wrocław)\n\nLinear Temporal Logic (LTL) interpreted on finite traces is a robust specification framework popular in formal verification. However\, despite the high interest in the logic in recent years\, the topic of their quantitative extensions is not yet fully explored. The main goal of this work is to study the effect of adding weak forms of percentage constraints (e.g. that most of the positions in the past satisfy a given condition\, or that sigma is the most-frequent letter occurring in the past) to fragments of LTL. Such extensions could potentially be used for the verification of influence networks or statistical reasoning. Unfortunately\, as we prove in the paper\, it turns out that percentage extensions of even tiny fragments of LTL have undecidable satisfiability and model-checking problems. Our undecidability proofs not only sharpen most of the undecidability results on logics with arithmetics interpreted on words known from the literature\, but also are fairly simple. We also show that the undecidability can be avoided by restricting the allowed usage of the negation\, and briefly discuss how the undecidability results transfer to first-order logic on words.\n\nThe talk will take approximately 30 minutes and will be held online via BigBlueButton. To access the room\, take one of the following links: \n\n\nwith ZIH-login:\n\nhttps://selfservice.zih.tu-dresden.de/l/link.php?m=67110&p=dbb695ef\n\nwithout ZIH-login:\n\nhttps://selfservice.zih.tu-dresden.de/link.php?m=67110&p=cf01a562
DTSTAMP:20210319T114641
SEQUENCE:33518
END:VEVENT
BEGIN:VEVENT
SUMMARY:Seminar 18.03.2021
URL://iccl.inf.tu-dresden.de/web/Seminar_18.03.2021
UID://iccl.inf.tu-dresden.de/web/Seminar_18.03.2021
DTSTART:20210318T130000
DTEND:20210318T143000
LOCATION:Online
DESCRIPTION:The chase is a well-studied\, sound and complete algorithm that is used in different variants as a basis for reasoning tasks over (disjunctive) existential rules. Since termination of the chase is undecidable\, acyclicity notions\, i.e. sufficient conditions for termination\, like model faithful acyclicity (MFA) for the skolem chase and restricted model faithful acyclicity (RMFA) for the restricted chase are introduced. The recently developed acyclicity notion disjunctive model faithful acyclicity (DMFA) for the disjunctive skolem chase promises improvements for detecting termination over existing notions like MFA in theory. We further know that RMFA captures DFMA while RMFA itself is not sound for the disjunctive skolem chase. We evaluate the generality of DMFA in practice compared to MFA and RMFA on rule sets that we obtain from real-world OWL ontologies in the Oxford ontology repository (OXFD) and the dataset of the OWL reasoner evaluation 2015 (ORE15). Our results show that DMFA achieves practical improvements over MFA that narrow the gap towards RMFA. Our findings motivate further research regarding the disjunctive skolem chase in general and the development of sufficient conditions for non-termination of the disjunctive skolem chase in particular.\n\n\nNote that this talk acts as a colloquium/examination for the module INF-PM-FPG. It will take place online via BigBlueButton. To access the room\, take one of the following links: \n\nwith ZIH-login:\n\nhttps://selfservice.zih.tu-dresden.de/l/link.php?m=86967&p=b14dca92\n\nwithout ZIH-login:\n\nhttps://selfservice.zih.tu-dresden.de/link.php?m=86967&p=00922683
DTSTAMP:20210301T091808
SEQUENCE:33383
END:VEVENT
BEGIN:VEVENT
SUMMARY:Solving Datalog(S) Problems with Lazy-Grounding ASP Solving
URL://iccl.inf.tu-dresden.de/web/Solving_Datalog(S)_Problems_with_Lazy-Grounding_ASP_Solving
UID://iccl.inf.tu-dresden.de/web/Solving_Datalog(S)_Problems_with_Lazy-Grounding_ASP_Solving
DTSTART:20210304T130000
DTEND:20210304T143000
LOCATION:Online
DESCRIPTION:Datalog(S) extends Datalog with support for sets\, and it can be captured in a decidable fragment of existential rules. We show that it can also be captured by Answer Set Programming (ASP) with function symbols. The traditional ground-and-solve approach for ASP\, however\, is insufficient\, as it computes the grounding in a first step before solving. Thus\, the introduction of function symbols can lead to infinite groundings\, even though a finite one would be sufficient\, since grounding and solving are separated and the obtained grounding is an over-approximation of the smallest possible one. We therefore propose the use of ASP systems with lazy-grounding\, i.e.\, systems that interleave grounding and solving\, to solve Datalog(S) programs as they guarantee termination. We show empirically that the lazy-grounding ASP solver Alpha can solve practical Datalog(S) problems. \n\n\nNote that this talk acts as a colloquium/examination for the module INF-PM-FPG.\nIt will take place online via BigBlueButton. To access the room\, take one of the following links: \n\n\nwith ZIH-login:\n\nhttps://selfservice.zih.tu-dresden.de/l/link.php?m=86965&p=58febf13\n\n\nwithout ZIH-login:\n\nhttps://selfservice.zih.tu-dresden.de/link.php?m=86965&p=35a69ec8
DTSTAMP:20210223T085148
SEQUENCE:33117
END:VEVENT
BEGIN:VEVENT
SUMMARY:Knowledge Graphs for AI: Wikidata and Beyond
URL://iccl.inf.tu-dresden.de/web/Knowledge_Graphs_for_AI:_Wikidata_and_Beyond
UID://iccl.inf.tu-dresden.de/web/Knowledge_Graphs_for_AI:_Wikidata_and_Beyond
DTSTART:20210211T130000
DTEND:20210211T143000
LOCATION:Online
DESCRIPTION:Abstract:\n"Wikidata\, the knowledge graph of Wikimedia\, has successfully grown from an experimental “data wiki” to a well-organized reference knowledge base with a large and active editor community as well as many academic and industrial uses. It is also a key ingredient of popular AI applications\, most prominently of intelligent agents such as Apple's Siri or Amazon's Alexa. Of course\, human knowledge is fully expected to be in high demand in this time of rapidly advancing AI. And yet\, the fact that modern AI relies on the manual labor of thousands of human knowledge modelers is in stark contrast to the common narrative of AI in popular media\, which tells us that methods of pattern recognition and statistical function approximation can produce intelligent behavior from unstructured data without much human intervention. However\, Wikidata is not a singular exception to the trend but rather a specific solution to a general need of AI: the need for knowledge that is understandable to humans and accessible to computers. Almost every major AI application incorporates such knowledge\, and organizations long have realized the need to acquire and develop knowledge resources as part of their AI strategy. The next frontier in AI is the ability of systems to explain and justify their behavior. There\, too\, we can see the need for knowledge-based technologies as a bridge between human understanding and computational mechanisms\, but the task goes far beyond the realms of knowledge representation or machine learning\, and will require the effort of all of AI and maybe all of computer science.\n\nIn my talk\, I will give an overview of Wikidata and other knowledge-based technologies in AI\, and outline some ongoing research efforts that combine knowledge representation with other methods towards the creation of (more) understandable and accountable AI."\n\n\n\nThis talk will have a duration of approximately 45 minutes and takes place via BigBlueButton. To access the room\, use one of the following links: \n\nwith ZIH-Login:\n\nhttps://selfservice.zih.tu-dresden.de/l/link.php?m=82158&p=3d86e9c8\n\nwithout ZIH-Login:\n\nhttps://selfservice.zih.tu-dresden.de/link.php?m=82158&p=506714c8
DTSTAMP:20210205T091100
SEQUENCE:32692
END:VEVENT
BEGIN:VEVENT
SUMMARY:Codifying Logical Fragments in ASP - A General Knowledge Base Approach
URL://iccl.inf.tu-dresden.de/web/Codifying_Logical_Fragments_in_ASP_-_A_General_Knowledge_Base_Approach
UID://iccl.inf.tu-dresden.de/web/Codifying_Logical_Fragments_in_ASP_-_A_General_Knowledge_Base_Approach
DTSTART:20210204T130000
DTEND:20210204T143000
LOCATION:Online
DESCRIPTION:The study of logic fragments\, their limitations and expressive properties is and has been an important field for topics such as Knowledge Representation\, Model Checking and even Human Reasoning. Many different research fields have found properties for different logic fragments and drawn links between these fragments. In this project\, we have aimed to build a general framework for representing these different fragments\, their properties and for inferring new results from their relative expressivity. Using Answer Set Programming (ASP) for its useful computational properties\, we have implemented this knowledge base and provide ways to query it or find explanations for any inferred results.\n\nThis talk will be a project defence and takes place via BigBlueButton. To access the room\, take one of the following links:\n\nwith ZIH-Login:\n\nhttps://selfservice.zih.tu-dresden.de/l/link.php?m=79924&p=e5e8bd36\n\nwithout ZIH-Login:\n\nhttps://selfservice.zih.tu-dresden.de/link.php?m=79924&p=e66e7dfe
DTSTAMP:20210203T093942
SEQUENCE:32628
END:VEVENT
BEGIN:VEVENT
SUMMARY:Integration and Evaluation of an ASP-Solver as an Alternative Reasoning Backend in the Rulewerk Toolkit
URL://iccl.inf.tu-dresden.de/web/Integration_and_Evaluation_of_an_ASP-Solver_as_an_Alternative_Reasoning_Backend_in_the_Rulewerk_Toolkit
UID://iccl.inf.tu-dresden.de/web/Integration_and_Evaluation_of_an_ASP-Solver_as_an_Alternative_Reasoning_Backend_in_the_Rulewerk_Toolkit
DTSTART:20201217T130000
DTEND:20201217T143000
LOCATION:Online
DESCRIPTION:This talk will be a BA thesis defence.\n\nRulewerk is a Java API\, that is build to abstract the access to data sources for the rule-based reasoner VLog. Since the VLog reasoner is actively developed\, there is always a need to evaluate potential improvements and to compare VLogs performance to other systems. A good way to make it way easier to compare multiple reasoners is to provide them easy access to the same and also diverse data sources.\nA potential first alternative reasoning backend is the ASP system Clingo. In this thesis I present a translation form the datalog-based input language of Rulewerk into the ASP-based input language of Clingo. I also show a direct comparison of the performance of both backends.\n\n\nThis talk will take place via BigBlueButton. To access the room\, take one of the following links:\n\nwith ZIH-Login:\n\nhttps://selfservice.zih.tu-dresden.de/l/link.php?m=56216&p=bb0e03e2\n\n\nwithout ZIH-Login:\n\nhttps://selfservice.zih.tu-dresden.de/link.php?m=56216&p=6efb2684
DTSTAMP:20201216T070540
SEQUENCE:32258
END:VEVENT
BEGIN:VEVENT
SUMMARY:Positivity-Hardness and Saturation Points in Markov Decision Processes
URL://iccl.inf.tu-dresden.de/web/Positivity-Hardness_and_Saturation_Points_in_Markov_Decision_Processes
UID://iccl.inf.tu-dresden.de/web/Positivity-Hardness_and_Saturation_Points_in_Markov_Decision_Processes
DTSTART:20201105T130000
DTEND:20201105T143000
LOCATION:Online
DESCRIPTION:The Positivity problem for linear recurrence sequences is a number-theoretic decision problem whose decidability has been open for many decades. We show that this Positivity problem can be encoded into several optimization problems on Markov decision processes\, a standard model combining non-deterministic and probabilistic behavior. This reduction demonstrates the inherent mathematical difficulty of various problems in the formal verification of probabilistic systems.\nFor naturally restricted versions of most of these problems\, we can nevertheless establish decidability. The key ingredient is the existence of so-called saturation points which can be seen as bounds on the memory required for an optimal strategy in the Markov decision process.\n\n\nThe talk will be approximately 45 minutes long and takes place online. To access the talk use the following links:\n\nIf you have a ZIH-login:\n\nhttps://selfservice.zih.tu-dresden.de/l/link.php?meeting_id=42224&pin=4c120949\n\n\nIf you do not have a ZIH-login:\n\nhttps://selfservice.zih.tu-dresden.de/link.php?meeting_id=42224&pin=d3219e91
DTSTAMP:20201030T155351
SEQUENCE:31781
END:VEVENT
BEGIN:VEVENT
SUMMARY:TBA6
URL://iccl.inf.tu-dresden.de/web/TBA6
UID://iccl.inf.tu-dresden.de/web/TBA6
DTSTART:20201029T130000
DTEND:20201029T143000
LOCATION:Online
DESCRIPTION:The field of artificial intelligence and knowledge representation (KR) has originated a high variety of formalisms\, notions\, languages\, and formats during the past decades. Each approach has been motivated and designed with specific applications in mind. Nowadays\, in the century of Industry 4.0\, the Internet of Things\, and Smart-devices\, we are interested in ways to connect the various approaches and allow them to distribute and exchange their knowledge and beliefs in an uniform way. In addition most information is provided continuously over time in streams of data. This leads to the problem that these sophisticated knowledge representation approaches cannot understand each others point of views\, their positions on semantics are not necessarily compatible either\, and most formalisms are designed as one-shot computations. These three problems between different KR-formalisms has been tackled by the concept of stream-aware Multi-Context Systems\, which allow methods to transfer information under a strong and generalised notion of semantics over time.\n\n\nStefan Ellmauthaler is a post-doctoral researcher in the group of Gerhard Brewka in Leipzig. He received his B.Sc. in 'Medicine and Computer Science' and his diploma in 'Computational Intelligence' at the Vienna University of Technology. His doctoral thesis 'Multi-Context Reasoning in Continuous Data-Flow Environments' has been supervised by Gerhard Brewka at the Leipzig University. Currently his research fields are abstract argumentation\, logic programming\, multi-context systems\, and hybrid reasoning approaches like stream reasoning and reactive reasoning.\n\n\nThe talk will take place online. If there is any interest in attending\, please send an e-mail to thomas.feller@tu-dresden.de.
DTSTAMP:20201020T122226
SEQUENCE:31570
END:VEVENT
BEGIN:VEVENT
SUMMARY:TBA5
URL://iccl.inf.tu-dresden.de/web/TBA5
UID://iccl.inf.tu-dresden.de/web/TBA5
DTSTART:20201027T111500
DTEND:20201027T124500
LOCATION:Online
DESCRIPTION:Whereas the operation of forgetting has recently seen a considerable amount of attention in the context of Answer Set Programming (ASP)\, most of it has focused on theoretical aspects\, leaving the practical issues largely untouched. Recent studies include results about what sets of properties operators should satisfy\, as well as the abstract characterization of several operators and their theoretical limits. However\, no concrete operators have been investigated.\nWe address this issue by presenting the first concrete operator that satisfies strong persistence (SP) - a property that seems to best capture the essence of forgetting in the context of ASP - whenever this is possible\, and many other important properties. The operator is syntactic\, limiting the computation of the forgetting result to manipulating the rules in which the atoms to be forgotten occur\, naturally yielding a forgetting result that is close to the original program. \nWhenever (SP) cannot be satisfied\, it is inevitable to break some relations between the atoms not to be forgotten.\nTherefore\, an alternative to satisfying (SP) only when possible is to enhance the logical language so that all such relations can be maintained after the forgetting operation.\nWe borrow from the recently introduced notion of fork – a conservative extension of Equilibrium Logic and its monotonic basis\, the logic of Here-and-There – which has been shown to be sufficient to overcome the problems related to satisfying (SP). We map this notion into the language of logic programs\, enhancing it with so-called anonymous cycles\, and we introduce a concrete syntactical forgetting operator over this enhanced language that we show to always obey strong persistence.\nResearch of forgetting in the context of Dung-style argumentation frameworks (AFs) is much less developed. For example\, properties that forgetting operators over AFs should satisfy have only been compiled this year. We provide a summery of relevant results and preliminary thoughts on how to proceed in the field.\n\n\nShort-Bio:\nMatti Berthold received his B.Sc. in Computer Science at the University of Leipzig\, before studying Computational Logic at TU Dresden and FCT NOVA Lisbon. During his studies he had the chance to assist and conduct teaching and publish and present the results of both his theses.\n\n\nThe talk will take place online. If there is any interest in attending\, please send an e-mail to thomas.feller@tu-dresden.de.
DTSTAMP:20201020T122044
SEQUENCE:31569
END:VEVENT
BEGIN:VEVENT
SUMMARY:Inconsistency Values for Logic Programs under Answer Set Semantics
URL://iccl.inf.tu-dresden.de/web/Inconsistency_Values_for_Logic_Programs_under_Answer_Set_Semantics
UID://iccl.inf.tu-dresden.de/web/Inconsistency_Values_for_Logic_Programs_under_Answer_Set_Semantics
DTSTART:20201022T130000
DTEND:20201022T143000
LOCATION:Online
DESCRIPTION:The proposition that conflicting pieces of information cannot exist together appears to be too simplistic for developing intelligent systems. Knowledge representation tools such as ASP (Answer Set Programming) rely on non-monotonic reasoning\, i.e.\, programs may contain inconsistent information without collapsing. While measuring inconsistency in monotonic formalisms has been investigated for some time now\, my master thesis addresses the issue of measuring inconsistency in ASP in order to provide an approach for analysing and resolving inconsistency in logic-based knowledge representation. Taking nonmonotonicity into account demands for a generalisation of the notion of inconsistency\, namely Strong Inconsistency [2]. Aiming to generalise A. Hunter's and S. Konieczny's\napproach [1] to non-monotonic formalisms\, the key idea is to characterise and use Minimal Strong Inconsistency Values for inducing a game in coalitional form on a knowledge base\, and to then use the Shapley Value in\norder to obtain a solution to this sort of blame game\, which reflects the impact of each element on the overall inconsistency in the base. Based on the latter I characterise the Minimal Strong Inconsistency Shapley Strong\nInconsistency (MSISSI) value and the MSISSI measure\, which provide an approach to describing inconsistency in ASP and allow for repairing inconsistent knowledge bases.\n\n[1] Anthony Hunter and Sébastien Konieczny. "On the measure of conflicts: Shapley inconsistency values". In: Artifcial Intelligence 174.14 (2010)\, pp. 1007-1026.\n\n[2] Markus Ulbricht\, Matthias Thimm\, and Gerhard Brewka. "Measuring Strong Inconsistency." In: AAAI. 2018\, pp. 1989-1996.\n\n\nDominik Rusovac was born in Vienna and studied Philosophy at the University of Vienna. Then he studied Logic at the University of Leipzig\, focussing on knowledge representation and formal systems. After graduating in 2019 he has been working since January 2020 as a software developer.\n\n\nThe talk will take around 45 minutes after which there will be the opportunity to ask questions and it will take place online. If there is any interest in attending\, please send an e-mail to thomas.feller@tu-dresden.de.
DTSTAMP:20201016T090429
SEQUENCE:31550
END:VEVENT
BEGIN:VEVENT
SUMMARY:Termination of the Skolem Chase on Disjunctive Existential Rules
URL://iccl.inf.tu-dresden.de/web/Termination_of_the_Skolem_Chase_on_Disjunctive_Existential_Rules
UID://iccl.inf.tu-dresden.de/web/Termination_of_the_Skolem_Chase_on_Disjunctive_Existential_Rules
DTSTART:20201008T130000
DTEND:20201008T143000
LOCATION:Online
DESCRIPTION:Disjunctive Existential Rules are a fragment of first order logic that is already expressive enough to capture many description logics. Conjunctive Query answering is an important reasoning task over such rules. Although this problem is undecidable\, different variants of the chase provide sound and complete algorithms that can be used as a reasoning basis. Since it is undecidable if these algorithms terminate for a specific rule set\, sufficient conditions for termination\, called acyclicity notions\, are introduced. We develop Disjunctive Model Faithful Acyclicity (DMFA) as a novel acyclicity notion for the disjunctive skolem chase variant by using ideas from Model Faithful Acyclicity (MFA) for the non-disjunctive skolem chase and Restricted Model Faithful Acyclicity (RMFA) for the restricted chase. Our research shows that our notion captures MFA and is able give a better approximation for termination on disjunctive existential rules. Acyclicity notions for the restricted chase like RMFA still capture DMFA but these notions are not sound for the disjunctive skolem chase. Our results encourage the use of the disjunctive skolem chase in practical applications\, which is implementable using well optimized ASP solvers.\n\n\nThis talk is a defence of the speakers "Großer Beleg".\nFurthermore it will be held online and take approximately 45 minutes which consist of an uninterrupted talk and a following question and answers part. If there is any interest in attending\, please send an e-mail to thomas.feller@tu-dresden.de.
DTSTAMP:20201002T175430
SEQUENCE:31420
END:VEVENT
BEGIN:VEVENT
SUMMARY:Smoke Test Planning using Answer Set Programming
URL://iccl.inf.tu-dresden.de/web/Smoke_Test_Planning_using_Answer_Set_Programming
UID://iccl.inf.tu-dresden.de/web/Smoke_Test_Planning_using_Answer_Set_Programming
DTSTART:20200910T130000
DTEND:20200910T143000
LOCATION:Online
DESCRIPTION:Smoke testing is an important method to increase stability and reliability of hardware-depending systems. Due to concurrent access to the same physical resource and the impracticality of the use of virtualization\, smoke testing requires some form of planning. In this paper\, we propose to decompose test cases in terms of atomic actions consisting of preconditions and effects. We present a solution based on answer set programming with multi-shot solving that automatically generates short parallel test plans. Experiments suggest that the approach is feasible for non-inherently sequential test cases and scales up to thousands of test cases.\n\n\nThis talk will be held online and take approximately 30 minutes after which questions can be asked. If there is any interest in attending\, please send an e-mail to thomas.feller@tu-dresden.de.
DTSTAMP:20200910T121605
SEQUENCE:31266
END:VEVENT
BEGIN:VEVENT
SUMMARY:Notation3 Logic: From informal to formal semantics
URL://iccl.inf.tu-dresden.de/web/Notation3_Logic:_From_informal_to_formal_semantics
UID://iccl.inf.tu-dresden.de/web/Notation3_Logic:_From_informal_to_formal_semantics
DTSTART:20200730T130000
DTEND:20200730T143000
LOCATION:Online
DESCRIPTION:Notation3 Logic is a rule-based extension of RDF. Since its invention\, the logic has been refined and applied in several reasoning engines like for example EYE\, Cwm and FuXi. But despite these developments\, a clear formal definition of Notation3’s semantics is still missing and the details of the logic are only defined in an informal way. This lack of formalisation does not only cause theoretical problems - the relationship to other logics cannot be investigated - it also has practical consequences: in many cases the interpretations of the same formula differ between reasoning engines. In this talk\, I will explain these differences and discuss how the formal semantics of the logic can be defined based on the informal specifications and the implementations.\n\n\nThis talk will be held online. If there is any interest in attending\, please send an e-mail to thomas.feller@tu-dresden.de.
DTSTAMP:20200727T072445
SEQUENCE:31071
END:VEVENT
BEGIN:VEVENT
SUMMARY:On the Complexity of Synthesis of nop-Free Boolean Petri Nets.
URL://iccl.inf.tu-dresden.de/web/On_the_Complexity_of_Synthesis_of_nop-Free_Boolean_Petri_Nets.
UID://iccl.inf.tu-dresden.de/web/On_the_Complexity_of_Synthesis_of_nop-Free_Boolean_Petri_Nets.
DTSTART:20200724T130000
DTEND:20200724T143000
LOCATION:Online
DESCRIPTION:In a Boolean Petri net\, the interaction nop allows places and transitions to be independent\, so that the firing of a transition does not affect the marking of a place\, and vice versa. Recently\, the complexity of synthesis of nets equipped with nop has been investigated thoroughly\, while the question for the rest 128 types of nets remains open. This work tackles the case of nop-free nets synthesis\, that is\, the Boolean nets where places and transitions are always related via interactions that are able to modify the marking of a place. In this paper\, we show that\, for nop-free nets\, the absence of swap leads always to a polynomial time synthesis procedure. Moreover\, we give a first hint\, that the presence of swap might make the synthesis for these types NP-complete.\n\n\nThis talk will be held online. If there is any interest in attending\, please send an e-mail to thomas.feller@tu-dresden.de.
DTSTAMP:20200722T203026
SEQUENCE:31066
END:VEVENT
BEGIN:VEVENT
SUMMARY:Imprecise Probabilities in Decision-making
URL://iccl.inf.tu-dresden.de/web/Imprecise_Probabilities_in_Decision-making
UID://iccl.inf.tu-dresden.de/web/Imprecise_Probabilities_in_Decision-making
DTSTART:20200709T130000
DTEND:20200709T143000
LOCATION:Online
DESCRIPTION:An agent’s beliefs come in different strengths. We understand her degree of belief in a\nproposition as a measure of the strength of her belief in that proposition. According to the\northodox Bayesian picture\, an agent's degree of belief is best represented by a single probability\nfunction. In particular\, the Bayesian claims that agents must assign numerically precise\nprobabilities to every proposition that they can entertain. On an alternative account\, an agent’s\nbeliefs ought to be modeled based on imprecise probabilities. With that\, imprecise degrees of\nbelief can be represented by a set of probability functions.\nRecently\, however\, imprecise probabilities have come under attack. Adam Elga (2010) claims\nthat there is no adequate account of the way they can be manifested in decision-making. In\nresponse to Elga\, more elaborate accounts of the imprecise framework have been developed. One\nof them is based on Supervaluationism\, originally\, a semantic approach to vague predicates. Still\,\nSeamus Bradley (2019) shows that those accounts that solve Elga’s problem\, have a more severe\ndefect: they undermine a central motivation to introduce imprecise probabilities in the first place.\nThe aim of my presentation is to modify the supervaluationist approach in such a way that it\naccounts for both Elga’s and Bradley’s challenges to the imprecise framework.\n\n\nThis talk will be held digitally. If there is any interest in attending\, please write an e-mail to thomas.feller@tu-dresden.de.
DTSTAMP:20200706T044025
SEQUENCE:30938
END:VEVENT
BEGIN:VEVENT
SUMMARY:ASNP: a tame fragment of existential second-order logic
URL://iccl.inf.tu-dresden.de/web/ASNP:_a_tame_fragment_of_existential_second-order_logic
UID://iccl.inf.tu-dresden.de/web/ASNP:_a_tame_fragment_of_existential_second-order_logic
DTSTART:20200625T130000
DTEND:20200625T143000
LOCATION:Digital
DESCRIPTION:Amalgamation SNP (ASNP) is a fragment of existential second-order logic that strictly contains binary connected MMSNP of Feder and Vardi and binary connected guarded monotone SNP of Bienvenu\, ten Cate\, Lutz\, and Wolter\; it is a promising candidate for an expressive subclass of NP that exhibits a complexity dichotomy. We show that ASNP has a complexity dichotomy if and only if the infinite-domain dichotomy conjecture holds for constraint satisfaction problems for first-order reducts of binary finitely bounded homogeneous structures. For such CSPs\, powerful universal-algebraic hardness conditions are known that are conjectured to describe the border between NP-hard and polynomial-time tractable CSPs. The connection to CSPs also implies that every ASNP sentence can be evaluated in polynomial time on classes of finite structures of bounded treewidth. We show that the syntax of ASNP is decidable. The proof relies on the fact that for classes of finite binary structures given by finitely many forbidden substructures\, the amalgamation property is decidable.\n\n\nThis will be a test talk for the presentation of an eponymous paper consisting of the 20 minute long prerecorded talk (like it will be presented at the conference) which will be followed up with a Q&A session to the talk where questions will be answered by Simon Knäuer\, one of the authors. Feedback and suggestions in preperation for the conference talk are heavily encouraged.\n\nThis talk will be held digitally. If there is any interest in attending\, please write an e-mail to thomas.feller@tu-dresden.de.
DTSTAMP:20200622T054325
SEQUENCE:30849
END:VEVENT
BEGIN:VEVENT
SUMMARY:The Method of Refinement: Deriving Proof-Calculi from Semantics for Multi-Modal Logics
URL://iccl.inf.tu-dresden.de/web/The_Method_of_Refinement:_Deriving_Proof-Calculi_from_Semantics_for_Multi-Modal_Logics
UID://iccl.inf.tu-dresden.de/web/The_Method_of_Refinement:_Deriving_Proof-Calculi_from_Semantics_for_Multi-Modal_Logics
DTSTART:20200611T130000
DTEND:20200611T143000
LOCATION:Digital
DESCRIPTION:In this talk\, we look at how to derive nested calculi from labelled calculi for multi-modal logics\, thus connecting the general results for labelled calculi with the more refined formalism of nested sequents. Since labelled calculi are constructed by transforming the semantics of a logic into a proof system\, the method of refinement shows how one can derive simplified calculi from the semantics of a logic. The extraction of nested calculi from labelled calculi obtains via considerations pertaining to the elimination of structural rules in labelled derivations. As a consequence of the extraction process\, each nested calculus inherits fundamental proof-theoretic properties from its associated labelled calculus and is suitable for applications such as decidability and interpolation.\n\nTim is currently working at the informatics faculty of the TU Wien in Vienna as a PreDoc Researcher in the research unit "Theory and Logic".\n\nThis talk will be held digitally. If there is any interest in attending\, please write an e-mail to thomas.feller@tu-dresden.de.
DTSTAMP:20200520T082459
SEQUENCE:30588
END:VEVENT
BEGIN:VEVENT
SUMMARY:Compositional Matrix-Space Models: Learning Methods and Evaluation
URL://iccl.inf.tu-dresden.de/web/Compositional_Matrix-Space_Models:_Learning_Methods_and_Evaluation
UID://iccl.inf.tu-dresden.de/web/Compositional_Matrix-Space_Models:_Learning_Methods_and_Evaluation
DTSTART:20200528T130000
DTEND:20200528T143000
LOCATION:Digital
DESCRIPTION:There has been a lot of research on machine-readable representations of words for natural\nlanguage processing (NLP). One mainstream paradigm for the word meaning representation\ncomprises vector-space models obtained from the distributional information of words in\nthe text. Machine learning techniques have been proposed to produce such word representations\nfor computational linguistic tasks. Moreover\, the representation of multi-word\nstructures\, such as phrases\, in vector space can arguably be achieved by composing the distributional\nrepresentation of the constituent words. To this end\, mathematical operations have\nbeen introduced as composition methods in vector space. An alternative approach to word\nrepresentation and semantic compositionality in natural language has been compositional\nmatrix-space models. In this thesis\, two research directions are considered. In the first\,\nconsidering compositional matrix-space models\, we explore word meaning representations\nand semantic composition of multi-word structures in matrix space. The main motivation\nfor working on these models is that they have shown superiority over vector-space models\nregarding several properties. The most important property is that the composition operation\nin matrix-space models can be defined as standard matrix multiplication\; in contrast to\ncommon vector space composition operations\, this is sensitive to word order in language. We\ndesign and develop machine learning techniques that induce continuous and numeric representations\nof natural language in matrix space. The main goal in introducing representation\nmodels is enabling NLP systems to understand natural language to solve multiple related\ntasks. Therefore\, first\, different supervised machine learning approaches to train word\nmeaning representations and capture the compositionality of multi-word structures using\nthe matrix multiplication of words are proposed. The performance of matrix representation\nmodels learned by machine learning techniques is investigated in solving two NLP tasks\,\nnamely\, sentiment analysis and compositionality detection. Then\, learning techniques for\nlearning matrix-space models are proposed that introduce generic task-agnostic representation\nmodels\, also called word matrix embeddings. In these techniques\, word matrices are\ntrained using the distributional information of words in a given text corpus. We show the\neffectiveness of these models in the compositional representation of multi-word structures in\nnatural language.\nThe second research direction in this thesis explores effective approaches for evaluating\nthe capability of semantic composition methods in capturing the meaning representation of\ncompositional multi-word structures\, such as phrases. A common evaluation approach is\nexamining the ability of the methods in capturing the semantic relatedness between linguistic\nunits. The underlying assumption is that the more accurately a method of semantic composition\ncan determine the representation of a phrase\, the more accurately it can determine the\nrelatedness of that phrase with other phrases. To apply the semantic relatedness approach\,\ngold standard datasets have been introduced. In this thesis\, we identify the limitations of\nthe existing datasets and develop a new gold standard semantic relatedness dataset\, which\naddresses the issues of the existing datasets. The proposed dataset allows us to evaluate\nmeaning composition in vector- and matrix-space models.\n\nThe presentation will take 45 minutes without questions. Afterwards there will be Q&A.\nThis talk will be held digitally. If there is any interest in attending\, please write an e-mail to thomas.feller@tu-dresden.de.
DTSTAMP:20200508T121859
SEQUENCE:30495
END:VEVENT
BEGIN:VEVENT
SUMMARY:Tracking False Information Online
URL://iccl.inf.tu-dresden.de/web/Tracking_False_Information_Online
UID://iccl.inf.tu-dresden.de/web/Tracking_False_Information_Online
DTSTART:20200227T161500
DTEND:20200227T174500
LOCATION:APB 1004
DESCRIPTION:Digital media enables fast sharing of information and discussions among users. While this comes with many benefits to today’s society\, such as broadening information access\, the manner in which information is disseminated also has obvious downsides. Since fast access to information is expected by many users and news outlets are often under financial pressure\, speedy access often comes at the expense of accuracy\, which leads to misinformation. Moreover\, digital media can be misused by campaigns to intentionally spread false information\, i.e. disinformation\, about events\, individuals or governments. In this talk\, I will present on different ways false information is spread online\, including misinformation and disinformation. I will then report findings from our recent and ongoing work on automatic fact checking\, stance detection and framing attitudes.
DTSTAMP:20200220T161257
SEQUENCE:30135
END:VEVENT
BEGIN:VEVENT
SUMMARY:A Distributed Blockchain Model of Selfish Mining
URL://iccl.inf.tu-dresden.de/web/A_Distributed_Blockchain_Model_of_Selfish_Mining
UID://iccl.inf.tu-dresden.de/web/A_Distributed_Blockchain_Model_of_Selfish_Mining
DTSTART:20200226T123000
DTEND:20200226T140000
LOCATION:APB 3027
DESCRIPTION:Abstract:\n Bitcoin is currently still the most widely used cryptocurrency\, judging from its market cap and trade volume. A big part of Bitcoin's appeal is the mining process\, which makes sure that new transactions are being validated and processed in a distributed fashion\, maintaining a distributed ledger known as the blockchain. Miners receive a fee for every block of transactions that they mine\, as an incentive for their computational effort. In the long run\, they can expect a reward proportional to the computational power they provide to the network.\nHowever\, Eyal and Sirer introduced a strategy for a miner to time the publishing of blocks that will give them a significant edge in profits. \nThis talk will present a model for the behaviour of honest and selfish mining pools in UPPAAL\, that can be used for analysing properties of the mining process in the presence of network delay\, and taking into account the distributed nature of the process. The analysis shows what effects selfish mining would have on the share of profits\, but also on the number of orphaned blocks in the blockchain. This analysis also allows us to compares those results to real-world data\, to establish if there is evidence for the presence of selfish miners.\n\nBio:\n Ansgar Fehnker is Associate Professor for Programming Education at the Faculty of Electrical Engineeering\, Mathematics\, and Computer Science\, at the University of Twente. He is part of the Formal Methods and Tools group and has been previously professor at the University of the South Pacific and researcher at Australia's ICT research centre NICTA\, working on static analysis for C/C++ and on analysis of wireless network protocols with model checking. Prior to joining NICTA he was a PostDoc in the model-checking teams at Carnegie Mellon University\, US. He received his PhD from the Radboud University Nijmegen on verification of real-time and hybrid systems.
DTSTAMP:20200217T091734
SEQUENCE:30129
END:VEVENT
BEGIN:VEVENT
SUMMARY:Knowledge Graph Curation and Reasoning using the Example of the Scholarly Domain
URL://iccl.inf.tu-dresden.de/web/Knowledge_Graph_Curation_and_Reasoning_using_the_Example_of_the_Scholarly_Domain
UID://iccl.inf.tu-dresden.de/web/Knowledge_Graph_Curation_and_Reasoning_using_the_Example_of_the_Scholarly_Domain
DTSTART:20200130T130000
DTEND:20200130T143000
LOCATION:APB 3027
DESCRIPTION:Knowledge graphs allow organisations and enterprises to integrate their internal and external heterogeneous sources of information into a unified form and enable analytics and discovery of unknown knowledge. To exploit the information encoded in knowledge graphs\, analysis of the graph structure as well as the semantics of the represented relations\, is required. I will show this using the scholarly domain as an example. The heterogeneity of scholarly artifacts and their metadata spread over different Web data sources serve as a great use case platform for data analytics and reasoning methods. In this talk\, I will first have a look into major challenges of this domain using KG creation and curation leveraging semantic Web technologies. I will further showcase the application of Knowledge Graph Embedding models for link prediction scenarios of this domain.
DTSTAMP:20200123T134125
SEQUENCE:30034
END:VEVENT
END:VCALENDAR