BEGIN:VCALENDAR
PRODID:-//SMW Project//Semantic Result Formats
VERSION:2.0
METHOD:PUBLISH
X-WR-CALNAME:ICCL Events
X-WR-CALDESC:
BEGIN:VTIMEZONE
TZID:Europe/Berlin
BEGIN:DAYLIGHT
DTSTART:20240625T133000
TZOFFSETFROM:+0200
TZOFFSETTO:+0200
TZNAME:CEST
END:DAYLIGHT
END:VTIMEZONE
BEGIN:VEVENT
SUMMARY:TBA10
URL://iccl.inf.tu-dresden.de/web/TBA10
UID://iccl.inf.tu-dresden.de/web/TBA10
DTSTART:20260430T110000
DTEND:20260430T120000
LOCATION:APB-2026
DESCRIPTION:In modern AI the aim of a system is to address the problem requirements directly from the natural language description of the problem.  Clearly\, such a problem specification is expressed under human reasoning and hence a problem solving system would be advantageous if it could also operate under a formalism that is close to human reasoning. The recent development of Large Language Models (LLMs) offers such a possibility as these systems appear to handle natural language in a human-like fashion. But their reliability is under question as is their ability to reason underneath their process of constructing well-formed sentences in order to explain and argue for their solutions to problems. The question the arises: do we develop and train LLMs as reasoners or do we connect these to other formal (symbolic) reasoners who do not suffer from the above shortcomings? In this talk\, the speaker will present a neuro-symbolic framework\, based on the integration of the Natural Language capabilities of LLMs with Argumentation-based Reasoning. In this approach\, instead of the LLM carrying out the reasoning\, this is delegated to COGNICA\, a Cognitive Argumentation system\, which carries out the reasoning within a Controlled Natural Language. Specifically\, LLM-COGNICA is a hybrid neural-symbolic framework for reasoning under a decision policy specified within Natural Language and executed via Explainable Argumentation. This offers the reliability of formal problem solving and allows the human developer and problem solver to be in control of the system development process. The talk will present the Argumentation foundations and Argumentation Technology underlying the neuro-symbolic integration of the LLM-COGNICA framework and describe how this can be employed to build reliable real-life application systems.\n\n\nBBB room for online attendees: https://bbb.tu-dresden.de/rooms/sqo-ezi-97u-sry/join
DTSTAMP:20260420T140552
SEQUENCE:44319
END:VEVENT
BEGIN:VEVENT
SUMMARY:Recurring Problems: Decidability\, Sufficient Conditions and Formal Verification for Chase Termination
URL://iccl.inf.tu-dresden.de/web/Recurring_Problems:_Decidability,_Sufficient_Conditions_and_Formal_Verification_for_Chase_Termination
UID://iccl.inf.tu-dresden.de/web/Recurring_Problems:_Decidability,_Sufficient_Conditions_and_Formal_Verification_for_Chase_Termination
DTSTART:20260326T110000
DTEND:20260326T130000
LOCATION:APB-2026
DESCRIPTION:The chase is a sound and complete but possibly non-terminating procedure for query answering over ontologies that feature existential rules (aka. tuple-generating dependencies)\, a highly expressive knowledge representation language. Termination of the procedure is undecidable in the general case but for some language fragments the problem becomes decidable. A fruitful line of research has established many sufficient conditions for termination and non-termination of the chase. Despite these efforts\, our collective understanding seems to be misled by deceptive intuitions at times. In this status talk\, the speaker will summarize his involvement in recent contributions to the research area of chase termination\, focusing mainly on insights into (un)decidability\, improved sufficient conditions for (non-)termination\, and an attempt at formally verifying the latter while introducing additional generalizations.\n\n\nBBB room for online attendees: https://bbb.tu-dresden.de/rooms/sqo-ezi-97u-sry/join
DTSTAMP:20260320T124327
SEQUENCE:44214
END:VEVENT
BEGIN:VEVENT
SUMMARY:Recurring Problems: Decidability\, Sufficient Conditions and Formal Verification for Chase Termination2
URL://iccl.inf.tu-dresden.de/web/Recurring_Problems:_Decidability,_Sufficient_Conditions_and_Formal_Verification_for_Chase_Termination2
UID://iccl.inf.tu-dresden.de/web/Recurring_Problems:_Decidability,_Sufficient_Conditions_and_Formal_Verification_for_Chase_Termination2
DTSTART:20260320T123805
DTEND:20260320T123805
DTSTAMP:20260320T124255
SEQUENCE:44212
END:VEVENT
BEGIN:VEVENT
SUMMARY:Declarative Debugging for Datalog with Aggregation
URL://iccl.inf.tu-dresden.de/web/Declarative_Debugging_for_Datalog_with_Aggregation
UID://iccl.inf.tu-dresden.de/web/Declarative_Debugging_for_Datalog_with_Aggregation
DTSTART:20260319T110000
DTEND:20260319T120000
LOCATION:APB-2026
DESCRIPTION:This talk will propose summary proof trees as a way for explaining derivations in Datalog programs with aggregation. These combine structurally similar parts of proof trees into a single\, easier to understand structure. It will show how to query for such summaries\, discuss the implementation in the rule engine Nemo\, and empirically establish the feasibility of the method. It will also briefly introduce a graphical interface for editing these proof queries and visualising the results.\n\n\nBBB room for online attendees: https://bbb.tu-dresden.de/rooms/sqo-ezi-97u-sry/join
DTSTAMP:20260313T124913
SEQUENCE:44176
END:VEVENT
BEGIN:VEVENT
SUMMARY:Rule Rewriting Revisited: A Fresh Look at Static Filtering for Datalog and ASP
URL://iccl.inf.tu-dresden.de/web/Rule_Rewriting_Revisited:_A_Fresh_Look_at_Static_Filtering_for_Datalog_and_ASP
UID://iccl.inf.tu-dresden.de/web/Rule_Rewriting_Revisited:_A_Fresh_Look_at_Static_Filtering_for_Datalog_and_ASP
DTSTART:20260312T110000
DTEND:20260312T120000
LOCATION:APB-2026
DESCRIPTION:Static filtering is a data-independent optimisation method for Datalog\, which generalises algebraic query rewriting techniques from relational databases. In spite of its early discovery by Kifer and Lozinskii in 1986\, the method has been overlooked in recent research and system development\, and special cases are being rediscovered independently. The talk will therefore recall the original approach\, using updated terminology and more general filter predicates that capture features of modern systems\, and it will show how to extend its applicability to answer set programming (ASP). The outcome is strictly more general but also more complex than the classical approach: double exponential in general and single exponential even for predicates of bounded arity. As a solution\, tractable approximations of the algorithm will be proposed that can still yield much improved logic programs in typical cases\, e.g.\, it can improve the performance of rule systems over real-world data in the order of magnitude.\n\n\nBBB room for online attendees: https://bbb.tu-dresden.de/rooms/sqo-ezi-97u-sry/join
DTSTAMP:20260309T163516
SEQUENCE:44123
END:VEVENT
BEGIN:VEVENT
SUMMARY:TBA9
URL://iccl.inf.tu-dresden.de/web/TBA9
UID://iccl.inf.tu-dresden.de/web/TBA9
DTSTART:20260219T110000
DTEND:20260219T120000
LOCATION:APB-2026
DESCRIPTION:The ability to recognize and manage (in)dependence is crucial in symbolic reasoning \, it plays a major part in causal reasoning [Pearl\, 2009]\, e.g.\, in probabilistic models\, where (in)dependence between variables of interest is built into graphical representations such as Bayesian networks. The ability to determine independence contributes to the explainability and trustworthiness of reasoning systems\, while also improving efficiency by empowering breaking problems down so that they can be managed more effectively. The speaker will present some recent work on notions of conditional independence in computational argumentation. Two prominent areas of computational models of argument are abstract argumentation [Dung 1995]\, and structured argumentation. Unlike abstract argumentation\, where arguments are considered abstract\, structured argumentation frameworks focus on the inner structure of the arguments\, enabling a finer-grained analysis of the arguments and relations. Assumption-based argumentation (ABA) [Bondarenko et al.\, 1997] is a well-known form of structured argumentation\, whose building blocks are assumptions (defeasible elements) and inference rules. In both frameworks argumentation semantics provide methods for evaluating acceptance\, and it is wrt. argumentation semantics that [Rienstra et al.\, 2020] propose a notion of conditional independence for Abstract Argumentation\, which recently was extended to independence between assumptions in Flat ABA-Frameworks [Blümel et al.\, 2025]. However\, in both frameworks other concepts of conditional independence are conceivable\, especially in ABA\, where assumptions are not the only structural objects under investigation. Furthermore\, the current notion has proven computationally challenging. In the second part of the talk the speaker will discuss some ideas regarding further investigations along these lines.\n\n\nBBB room for online attendees: https://bbb.tu-dresden.de/rooms/sqo-ezi-97u-sry/join
DTSTAMP:20260304T210855
SEQUENCE:44115
END:VEVENT
BEGIN:VEVENT
SUMMARY:News from Knowledge-aware AI
URL://iccl.inf.tu-dresden.de/web/News_from_Knowledge-aware_AI
UID://iccl.inf.tu-dresden.de/web/News_from_Knowledge-aware_AI
DTSTART:20260205T110000
DTEND:20260205T120000
LOCATION:APB-2026
DESCRIPTION:In this talk\, the speaker will summarize developments from last year\, in particular\, GPTKB version v1.5 (won the ISWC best demo award)\, and the EACL 2026 paper "Foundations of LLM Knowledge Materialization: Termination\, Reproducibility\, Robustness". The talk will also give an outlook on recent research towards statistical estimation of the scale of LLM knowledge\, knowledge materialization with disambiguated entities\, classes\, and relations\, and unstructured materialization in the style of Grokipedia.\n\n\nBBB room for online attendees: https://bbb.tu-dresden.de/rooms/sqo-ezi-97u-sry/join
DTSTAMP:20260304T210821
SEQUENCE:44114
END:VEVENT
BEGIN:VEVENT
SUMMARY:Interactive Exploration of Plan Spaces
URL://iccl.inf.tu-dresden.de/web/Interactive_Exploration_of_Plan_Spaces
UID://iccl.inf.tu-dresden.de/web/Interactive_Exploration_of_Plan_Spaces
DTSTART:20260122T110000
DTEND:20260122T120000
LOCATION:APB-2026
DESCRIPTION:Many planning applications require not only a single solution but benefit substantially from having a set of possible plans from which users can select\, for example\, when explaining plans. For decades\, research in classical AI planning has primarily focused on quickly finding single plans. Only recently researchers have started to investigate preferences\, enumerate plans by top-k planning\, or count plans to reason about the plan space. Unfortunately\, reasoning about the plan space is computationally extremely hard and feeding many similar plans to the user is hardly practical. To circumvent computational shortcomings while still being able to reason about variability in plans\, faceted actions have been introduced very recently. These are meaningful actions that can be used by some plan but are not required by all plans. Enforcing or forbidding such facets allows for navigating even large plan spaces while ensuring desired properties quickly and step by step. This talk will illustrate an industrial challenge\, the Beluga logistics problem of Airbus\, where reasoning with facets enables targeted plan space navigation. It will present an approach to handle large plan spaces iteratively and present a tool that the authors call planpilot.\n\n\nBBB room for online attendees: https://bbb.tu-dresden.de/rooms/sqo-ezi-97u-sry/join
DTSTAMP:20260119T094936
SEQUENCE:43934
END:VEVENT
BEGIN:VEVENT
SUMMARY:TBA8
URL://iccl.inf.tu-dresden.de/web/TBA8
UID://iccl.inf.tu-dresden.de/web/TBA8
DTSTART:20260115T110000
DTEND:20260115T120000
LOCATION:APB-2026
DESCRIPTION:The importance of taking individual\, potentially conflicting perspectives into account when dealing with knowledge has been widely recognised. Many existing knowledge management approaches fully merge knowledge perspectives\, which may require weakening in order to maintain consistency\; others represent the distinct views in an entirely detached way. This talk will present an alternative\, referred to as Standpoint Logic\, a simple\, yet versatile multi-modal logic “add-on” for existing logical languages – including Description Logics – intended for the integrated representation of domain knowledge relative to diverse standpoints\, which can be hierarchically organised\, combined\, and put in relation with each other. It will introduce the general logical framework of Standpoint Logic and discuss variations which differ in expressivity and computational complexity of automated reasoning.\n\n\nBBB room for online attendees: https://bbb.tu-dresden.de/rooms/sqo-ezi-97u-sry/join
DTSTAMP:20260119T094902
SEQUENCE:43933
END:VEVENT
BEGIN:VEVENT
SUMMARY:A Basis for Defeasible Reasoning
URL://iccl.inf.tu-dresden.de/web/A_Basis_for_Defeasible_Reasoning
UID://iccl.inf.tu-dresden.de/web/A_Basis_for_Defeasible_Reasoning
DTSTART:20251211T110000
DTEND:20251211T120000
LOCATION:APB-2026
DESCRIPTION:Formal Concept Analysis (FCA) provides a framework for studying Boolean data through concepts and their corresponding structures. The implication logic underlying FCA is relatively simple - analogous to propositional Horn\, and is monotonic. As a result\, FCA is largely unable to reason through exceptions that may exist in given data\, impeding the discovery of partially holding\, but useful\, rules. We explore how the style of non-monotonic reasoning developed by Kraus\, Lehmann\, and Magidor (1990) (frequently initialised to the KLM framework)\, and more generally preferential semantics\, may be introduced to FCA\, and what becomes of the (defeasible) implication logic\, as well as how the notions of formal concepts may be reframed to accommodate the aforementioned preferential semantics.\n\n\nBBB room for online attendees: https://bbb.tu-dresden.de/rooms/sqo-ezi-97u-sry/join
DTSTAMP:20251204T175527
SEQUENCE:43714
END:VEVENT
BEGIN:VEVENT
SUMMARY:Defeasible Standpoint Logics
URL://iccl.inf.tu-dresden.de/web/Defeasible_Standpoint_Logics
UID://iccl.inf.tu-dresden.de/web/Defeasible_Standpoint_Logics
DTSTART:20251204T110000
DTEND:20251204T120000
LOCATION:APB-2026
DESCRIPTION:The production of commercial aircrafts is a complex undertaking that requires meticulous planning. While ensuring that all demands within the network are satisfied\, industrial architectures must also aim to minimise the overall cost of the network. This problem is referred to as the Multi-Network Batch Scheduling (MNBS) problem. Previous work has investigated this using linear programming (LP) techniques. This talk will outline a proposal for a hybrid column-generation approach\, in which the restricted master problem is handled using LP\, while the pricing problem is modelled and solved using Answer Set Programming (ASP). \n\n\nBBB room for online attendees: https://bbb.tu-dresden.de/rooms/sqo-ezi-97u-sry/join
DTSTAMP:20251203T144004
SEQUENCE:43704
END:VEVENT
BEGIN:VEVENT
SUMMARY:Defeasible Conditionals using Answer Set Programming
URL://iccl.inf.tu-dresden.de/web/Defeasible_Conditionals_using_Answer_Set_Programming
UID://iccl.inf.tu-dresden.de/web/Defeasible_Conditionals_using_Answer_Set_Programming
DTSTART:20251127T110000
DTEND:20251127T120000
LOCATION:APB-2026
DESCRIPTION:Standpoint logics are a recent family of modal logics introduced to KR\, which provide a mechanism for representing potentially conflicting beliefs of different viewpoints into a single logical framework. In the classical setting\, standpoint logics allows for one to express information about beliefs which are necessary or possible to a given standpoint. However\, this case is not sufficiently expressive but to reason about the prototypical (or usual) behaviour and beliefs of a given standpoint. This talk will introduce Propositional Defeasible Standpoint Logic (PDSL) which extends propositional standpoint logics with KLM style defeasible modalities and implications\, allowing us to reason about standpoints’ prototypical behaviours. The authors define a semantics and a notion of preferential entailment for PDSL\, and show that satisfiability and preferential entailment can be computed using a semantic tableaux algorithm. They also consider an alternative means of incorporating KLM-style defeasibility\, in which standpoints can hold defeasible beliefs\, rather than exhibit defeasible behaviours.\n\n\nBBB room for online attendees: https://bbb.tu-dresden.de/rooms/sqo-ezi-97u-sry/join
DTSTAMP:20251124T134532
SEQUENCE:43636
END:VEVENT
BEGIN:VEVENT
SUMMARY:Exception Closed Conjunctive Rule Sets (ECCRS) for Prediction
URL://iccl.inf.tu-dresden.de/web/Exception_Closed_Conjunctive_Rule_Sets_(ECCRS)_for_Prediction
UID://iccl.inf.tu-dresden.de/web/Exception_Closed_Conjunctive_Rule_Sets_(ECCRS)_for_Prediction
DTSTART:20251113T110000
DTEND:20251113T120000
LOCATION:APB-2026
DESCRIPTION:In this talk\, Exception Closed Conjunctive Rule Sets (ECCRS) will be presented as a transparent rule based classifier with explicit exceptions. Exception closure induces laminarity among opposite label rules\, so prediction follows a clear most specific wins principle. The learning pipeline builds minimal decisive rule bodies from training examples\, enforces comparability with opposite rules\, and can apply a strict global closure that yields a canonical order independent model. Two base preserving completions resolve undecided cases only when required. On standard binary classification benchmarks ECCRS is competitive and often comparable to symbolic and non symbolic baselines. Models are compact with direct reasons per decision. An ablation quantifies the trade off between closure level\, model size\, and time.\n\n\nBBB room for online attendees: https://bbb.tu-dresden.de/rooms/sqo-ezi-97u-sry/join
DTSTAMP:20251203T144037
SEQUENCE:43705
END:VEVENT
BEGIN:VEVENT
SUMMARY:TBA7
URL://iccl.inf.tu-dresden.de/web/TBA7
UID://iccl.inf.tu-dresden.de/web/TBA7
DTSTART:20251106T110000
DTEND:20251106T120000
LOCATION:APB-2026
DESCRIPTION:The chase is a ubiquitous algorithm in database theory. However\, for existential rules (aka tuple-generating dependencies)\, its termination is not guaranteed\, and even undecidable in general. The problem of termination becomes particularly difficult for the restricted (or standard) chase\, for which the order of rule application matters. Thus\, decidability of restricted chase termination is still open for many well-behaved classes such as linear or guarded multi-headed rules. We make a step forward by showing that all-instances restricted chase termination is decidable in the linear multi-headed case.\n\n\nBBB room for online attendees: https://bbb.tu-dresden.de/rooms/sqo-ezi-97u-sry/join
DTSTAMP:20251103T130806
SEQUENCE:43485
END:VEVENT
BEGIN:VEVENT
SUMMARY:Grounding Rule-Based Argumentation Using Datalog
URL://iccl.inf.tu-dresden.de/web/Grounding_Rule-Based_Argumentation_Using_Datalog
UID://iccl.inf.tu-dresden.de/web/Grounding_Rule-Based_Argumentation_Using_Datalog
DTSTART:20251030T110000
DTEND:20251030T120000
LOCATION:APB-2026
DESCRIPTION:Although first-order rules are commonly used in ASPIC+ examples\, most existing approaches to reason over rule-based argumentation only support propositional rules. To enable reasoning over first-order instances\, a preliminary grounding step is required. As groundings can lead to an exponential increase in size of the program\, intelligent procedures are needed. However\, there is a lack of dedicated solutions for ASPIC+. Therefore\, we propose an intelligent grounding procedure that keeps the size of the grounding manageable while preserving the correctness of the reasoning process. To this end\, we translate the first-order ASPIC+ instance into a Datalog program and query a Datalog engine to obtain ground substitutions to perform the grounding of rules and contraries. Additionally\, we propose simplifications specific to the ASPIC+ formalism to avoid unnecessary grounding of rules that won’t influence the complete extensions of the instance. Finally\, we performed an empirical evaluation of the prototypical implementation to show scalability.
DTSTAMP:20251013T134319
SEQUENCE:43308
END:VEVENT
BEGIN:VEVENT
SUMMARY:Verifying Datalog Reasoning with Lean
URL://iccl.inf.tu-dresden.de/web/Verifying_Datalog_Reasoning_with_Lean
UID://iccl.inf.tu-dresden.de/web/Verifying_Datalog_Reasoning_with_Lean
DTSTART:20251023T110000
DTEND:20251023T120000
LOCATION:APB-2026
DESCRIPTION:Datalog is an essential logical rule language with many applications\, and modern rule engines compute logical consequences for Datalog with high performance and scalability. While Datalog is rather simple and\, in principle\, explainable by design\, such sophisticated implementations and optimizations are hard to verify. We therefore propose a certificate-based approach to validate results of Datalog reasoners in a formally verified checker for Datalog proofs. Using the proof assistant Lean\, we implement such a checker and verify its correctness against direct formalizations of the Datalog semantics. We propose two JSON encodings for Datalog proofs: one using the widely supported Datalog proof trees\, and one using directed acyclic graphs for succinctness. To evaluate the practical feasibility and performance of our approach\, we validate proofs that we obtain by converting derivation traces of an existing Datalog reasoner into our tool-independent format.
DTSTAMP:20251017T070646
SEQUENCE:43338
END:VEVENT
BEGIN:VEVENT
SUMMARY:Software Verification in Ada/SPARK
URL://iccl.inf.tu-dresden.de/web/Software_Verification_in_Ada/SPARK
UID://iccl.inf.tu-dresden.de/web/Software_Verification_in_Ada/SPARK
DTSTART:20251016T110000
DTEND:20251016T120000
LOCATION:APB 2026
DESCRIPTION:Formal software verification seeks to establish logical properties of programs with mathematical rigor\, rather than relying solely on empirical testing. Ada/SPARK provides a verification-oriented programming environment in which contracts (preconditions\, postconditions\, invariants) serve as logical specifications embedded in the code. These contracts enable modular reasoning about subprograms and allow the GNATprove tool to discharge proofs of safety properties\, functional correctness and termination. I will outline this verification\nworkflow\, illustrate typical classes of provable properties and discuss current industrial applications.
DTSTAMP:20251009T091031
SEQUENCE:43279
END:VEVENT
BEGIN:VEVENT
SUMMARY:Supporting Risk Management for Medical Devices via the Riskman Ontology and Shapes
URL://iccl.inf.tu-dresden.de/web/Supporting_Risk_Management_for_Medical_Devices_via_the_Riskman_Ontology_and_Shapes
UID://iccl.inf.tu-dresden.de/web/Supporting_Risk_Management_for_Medical_Devices_via_the_Riskman_Ontology_and_Shapes
DTSTART:20250925T110000
DTEND:20250925T120000
LOCATION:APB 3027
DESCRIPTION:We propose the Riskman ontology and shapes for representing and analysing information about risk management for medical devices. Risk management is concerned with taking necessary precautions to ensure that a medical device does not cause harms for users or the environment. To date\, risk management documentation is submitted to notified bodies (for certification) in the form of semi-structured natural language text. We propose to use terms from the Riskman ontology to provide a formal\, logical underpinning for risk management documentation\, and to use the included SHACL constraints to check whether the provided data is in accordance with the requirements of the two relevant norms\, i.e. ISO 14971 and VDE Spec 90025.
DTSTAMP:20250923T051939
SEQUENCE:43073
END:VEVENT
BEGIN:VEVENT
SUMMARY:Reliance-based Static Analysis of Existential Rules
URL://iccl.inf.tu-dresden.de/web/Reliance-based_Static_Analysis_of_Existential_Rules
UID://iccl.inf.tu-dresden.de/web/Reliance-based_Static_Analysis_of_Existential_Rules
DTSTART:20250918T080000
DTEND:20250918T090000
LOCATION:APB 3027
DESCRIPTION:Cores are universal models of existential rules knowledge bases that have no redundant facts. They can be determined with the core chase\, but this is expensive. Recent work suggested special positive and restraint reliance relations between rules to assess whether applying a rule can activate another and whether a rule should be preferred over another to avoid introducing unnecessary facts into the chase result. They give rise to core-stratifiable rulesets\, which are susceptible to a rule-based selection strategy for the restricted chase that does not violate restraints and thus produces a core with certainty. However\, there are still many practically relevant rulesets which are not core-stratifiable whilst still supporting core computation with a specialized selection strategy for the restricted chase.\n\nWe examine such cases to propose a new class of rulesets\, which we call SCC-contraction core-stratifiable\, that broadens the applicability of the restricted chase to compute cores. It is based on deputizing positive reliances by sets of contracted rules\, which are formed by syntactically intersecting unifiable parts of the second rule’s body and the first rule’s head to attain the combined effect of applying two respective triggers in succession. Then\, rulesets are contraction core-stratifiable iff they have no cycle in the restraints of the contracted reliance graph. We evaluate a prototype implementation on a subset of the Oxford Ontology Repository\, revealing that a significant portion is covered by our analysis.
DTSTAMP:20250916T044250
SEQUENCE:42885
END:VEVENT
BEGIN:VEVENT
SUMMARY:Linear Ghost Types Are All You Need -- An Introduction to Proof-Oriented Programming in Verus
URL://iccl.inf.tu-dresden.de/web/Linear_Ghost_Types_Are_All_You_Need_--_An_Introduction_to_Proof-Oriented_Programming_in_Verus
UID://iccl.inf.tu-dresden.de/web/Linear_Ghost_Types_Are_All_You_Need_--_An_Introduction_to_Proof-Oriented_Programming_in_Verus
DTSTART:20250911T110000
DTEND:20250911T120000
LOCATION:APB 3027
DESCRIPTION:Previously in this seminar\, we introduced a concurrent separation logic (IRIS) to verify the memory safety of unsafe code inside Rust's standard library. Conversely\, the observation that the safe subset of Rust can be efficiently encoded into constraint horn clauses has led to highly automated\, SMT-solver based tools for the verification of this subset of rust. Naturally\, the next question is how to automate the verification of Rust programs that do use unsafe code. Linear ghost types offer a simple yet powerful solution: We can reuse the borrow checking that is already performed by the Rust compiler to automate a separation logic built into the source code\, allowing for a "proof oriented programming" style. In this talk\, we show how linear ghost types relate to the broader landscape of verification tools for Rust and how to use them for the verification of low level data structures -- an application which might be useful for nemo\, the Rust-based logic reasoner developed in our group.
DTSTAMP:20250909T051254
SEQUENCE:42808
END:VEVENT
BEGIN:VEVENT
SUMMARY:A Crash Course in Determinacy
URL://iccl.inf.tu-dresden.de/web/A_Crash_Course_in_Determinacy
UID://iccl.inf.tu-dresden.de/web/A_Crash_Course_in_Determinacy
DTSTART:20250821T110000
DTEND:20250821T120000
LOCATION:APB 3027
DESCRIPTION:This talk offers a (short) crash course in Determinacy - a classical problem in database theory\, and with multiple connections to KR.\n\nAt its core\, the determinacy problem asks: given a query Q and a set of queries {V_1\, V_2\, ...\, V_n}\, can the answer to Q(D) be recovered solely from the answers to V_1(D)\, V_2(D)\, ...\, V_n(D) no matter the database D?\n\nWe will explore the problem\, its key variants\, and the connections to query rewritability\, existential rules\, and the chase procedure. The presentation will be grounded in examples\, making the concepts as concrete and intuitive as possible.\n\nThe presentation will be given on the board\, so do feel encouraged to join the talk in person if possible. We will provide the usual hybrid setup but it will likely be hard to see what is written on the board online. Sorry for the inconvenience!
DTSTAMP:20250820T055743
SEQUENCE:42697
END:VEVENT
BEGIN:VEVENT
SUMMARY:LogAI-Seminar-2025-08-14
URL://iccl.inf.tu-dresden.de/web/LogAI-Seminar-2025-08-14
UID://iccl.inf.tu-dresden.de/web/LogAI-Seminar-2025-08-14
DTSTART:20250814T110000
DTEND:20250814T120000
LOCATION:APB 3027
DESCRIPTION:In epistemic voting\, multiple agents vote over a set of alternatives\, with the goal of identifying the one that corresponds to the ground truth. The Condorcet Jury Theorem (CJT) is a foundational result in this context\, offering probabilistic guarantees for truth-tracking\, albeit under restrictive assumptions. This talk has two main objectives. First\, we generalize the CJT by relaxing its core assumptions and provide novel probabilistic bounds for successful truth identification. Second\, we introduce a new aggregation method\, Voting for Bins\, grounded in the epistemic voting framework\, designed for aggregating interval-valued probabilistic beliefs. Each of these contributions is tied to a key application: for the generalized CJT\, we formalize and bound conditions under which diversity can outperform ability\, offering a rigorous formulation of the Diversity-Trumps-Ability Theorem. For Voting for Bins\, we address the problem of dilation in imprecise belief aggregation.
DTSTAMP:20250725T085613
SEQUENCE:42621
END:VEVENT
BEGIN:VEVENT
SUMMARY:LogAI-Seminar-2025-06-19
URL://iccl.inf.tu-dresden.de/web/LogAI-Seminar-2025-06-19
UID://iccl.inf.tu-dresden.de/web/LogAI-Seminar-2025-06-19
DTSTART:20250731T110000
DTEND:20250731T120000
LOCATION:APB 3027
DESCRIPTION:Fuzzy logic programming is an established approach for reasoning under uncertainty.\nSeveral semantics from classical\, two-valued logic programming have been generalized to the case of fuzzy logic programs.\nIn this paper\, we show that two of the most prominent classical semantics\, namely the stable model and the well-founded semantics\, can be reconstructed within the general framework of approximation fixpoint theory (AFT).\n\nThis not only widens the scope of AFT from two- to many-valued logics\, but allows a wide range of existing AFT results to be applied to fuzzy logic programming.\nAs first examples of such applications\, we clarify the formal relationship between existing semantics\, generalize the notion of stratification from classical to fuzzy logic programs\, and devise “more precise” variants of the semantics.
DTSTAMP:20250728T125929
SEQUENCE:42625
END:VEVENT
BEGIN:VEVENT
SUMMARY:Satisfying Rationality Postulates of Structured Argumentation through Deductive Support
URL://iccl.inf.tu-dresden.de/web/Satisfying_Rationality_Postulates_of_Structured_Argumentation_through_Deductive_Support
UID://iccl.inf.tu-dresden.de/web/Satisfying_Rationality_Postulates_of_Structured_Argumentation_through_Deductive_Support
DTSTART:20250724T110000
DTEND:20250724T120000
LOCATION:APB 3027
DESCRIPTION:ASPIC-style structured argumentation frameworks provide a formal basis for reasoning in artificial intelligence by combining internal argument structure with abstract argumentation semantics. A key challenge in these frameworks is ensuring compliance with five critical rationality postulates: closure\, direct consistency\, indirect consistency\, non-interference\, and crash-resistance. Recent approaches\, including ASPIC⊖ and Deductive ASPIC-\, have made significant progress but fall short of meeting all postulates simultaneously under a credulous semantics (e.g. preferred) in the presence of undercuts. We introduce Deductive ASPIC⊖\, a novel framework that integrates gen-rebuttals from ASPIC⊖ with the Joint Support Bipolar Argumentation Frameworks (JSBAFs) of Deductive ASPIC-\, incorporating preferences. We show that Deductive ASPIC⊖ satisfies all five rationality postulates under a version of preferred semantics.
DTSTAMP:20250721T141923
SEQUENCE:42616
END:VEVENT
BEGIN:VEVENT
SUMMARY:LogAI-Seminar-2025-07-03
URL://iccl.inf.tu-dresden.de/web/LogAI-Seminar-2025-07-03
UID://iccl.inf.tu-dresden.de/web/LogAI-Seminar-2025-07-03
DTSTART:20250703T110000
DTEND:20250703T120000
LOCATION:APB 3027
DESCRIPTION:Standpoint logics offer unified modal logic-based formalisms for representing multiple heterogeneous viewpoints. At the same time\, many non-monotonic reasoning frameworks can be naturally captured using modal logics — in particular using the modal logic S4F. In this work\, we propose a novel formalism called S4F Standpoint Logic\, which generalizes both S4F and standpoint propositional logic and is therefore capable of expressing multi-viewpoint\, non-monotonic semantic commitments. We define its syntax and semantics and analyze its computational complexity\, obtaining the result that S4F Standpoint Logic is not computationally harder than its constituent logics\, whether in monotonic or non-monotonic form. We also outline mechanisms for credulous and skeptical acceptance and illustrate the framework with a worked example.
DTSTAMP:20250701T050854
SEQUENCE:42555
END:VEVENT
BEGIN:VEVENT
SUMMARY:LogAI-Seminar-2025-06-26
URL://iccl.inf.tu-dresden.de/web/LogAI-Seminar-2025-06-26
UID://iccl.inf.tu-dresden.de/web/LogAI-Seminar-2025-06-26
DTSTART:20250626T110000
DTEND:20250626T120000
LOCATION:APB 3027
DESCRIPTION:AI models are often developed to solve reasoning problems optimally. In contrast\, cognitive models focus on explaining and predicting replicative cognitive patterns of human information processing. And while many of the theories aim to explain an assumed ‘general’ human reasoner\, only few are aimed at the individual. This talk will address the challenge of the latter by presenting the automatic generation of individualised predictive algorithms using transformer-based models. These models which have been trained on huge amounts of human data\, potentially exhibit built-in cognitive patterns. Leveraging such characteristics and architecture of transformer-based models\, a generalised methodology for establishing a Human-AI collaborative framework will be outlined\, which can be used to generate explainable and reproducible algorithms with cross-domain applicability. While predictive accuracy and generalisability pose less of a problem\, the bigger challenges in using machine learning approaches or transformer-based models may be explainability and replicability. Hence\, instead of ‘just’ using such a model for directly fitting the data\, it is used to extract features and to propose cognitive algorithms that are executable in systems outside of the model. Using two datasets pertaining to syllogistic and spatial reasoning\, the predictive algorithms thus generated applying the presented framework\, achieve mean accuracies of 68% and 81%\, respectively. Both algorithms outperform other established\, state-of-the-art cognitive models by far\, surpassing the (previously) best state-of-the art models in syllogistic and spatial human reasoning by 19% and 13%\, respectively.
DTSTAMP:20250620T051619
SEQUENCE:42489
END:VEVENT
BEGIN:VEVENT
SUMMARY:LogAI-Seminar-2025-06-05
URL://iccl.inf.tu-dresden.de/web/LogAI-Seminar-2025-06-05
UID://iccl.inf.tu-dresden.de/web/LogAI-Seminar-2025-06-05
DTSTART:20250605T110000
DTEND:20250605T120000
LOCATION:APB 3027
DESCRIPTION:Querying data sometimes calls for a logical layer between the user and the data to address challenges arising from distributed datasets\, overly specific vocabulary\, or incompleteness. Existential rules form an expressive knowledge representation language used for this purpose. However\, query answering in the presence of existential rules presents several challenges.  \n\nOne such challenge is undecidability\, which is addressed through various approaches\, including query rewriting. We define FUS as the class of existential rule sets for which query rewriting successfully determines entailment. Another challenge arises from the distinction between entailment over finite and infinite models: these two semantics differ\, yet most tools are designed with infinite models in mind\, whereas finite models better reflect actual databases. We call an existential rule set finitely controllable (FC) if the two semantics coincide.  \n\nA natural question\, and a long-standing open conjecture\, is whether FUS implies FC. We take a step toward a positive resolution of this conjecture by showing that universal models generated by FUS rule sets cannot contain arbitrarily large cliques without entailing a loop query. This simple yet elegant result narrows the space of potential counterexamples to the FUS/FC conjecture.
DTSTAMP:20250603T070035
SEQUENCE:42450
END:VEVENT
BEGIN:VEVENT
SUMMARY:Defeasible Reasoning in Formal Concept Analysis
URL://iccl.inf.tu-dresden.de/web/Defeasible_Reasoning_in_Formal_Concept_Analysis
UID://iccl.inf.tu-dresden.de/web/Defeasible_Reasoning_in_Formal_Concept_Analysis
DTSTART:20250522T110000
DTEND:20250522T120000
LOCATION:APB 3027
DESCRIPTION:Formal Concept Analysis (FCA) provides a framework for understanding dependencies between attributes through implications. However\, classical implications fall short when dealing with noisy or exception-prone data. In this talk\, we explore how the well-established KLM framework for defeasible reasoning can be adapted to FCA. We introduce defeasible conditionals—statements like "normally\, A implies B"—into the FCA setting via a typicality ordering over objects. This ordering can be either specified upfront or derived from background knowledge. The resulting framework preserves the rationality postulates of KLM and supports context-sensitive inference grounded in the structure of the data.\n\nJoint work with Lucas Carr\, Nicholas Leisegang\, and Thomas Meyer (University of Cape Town and CAIR\, South Africa)
DTSTAMP:20250520T075923
SEQUENCE:42401
END:VEVENT
BEGIN:VEVENT
SUMMARY:Model Checking Linear Temporal Logic with Standpoint Modalities
URL://iccl.inf.tu-dresden.de/web/Model_Checking_Linear_Temporal_Logic_with_Standpoint_Modalities
UID://iccl.inf.tu-dresden.de/web/Model_Checking_Linear_Temporal_Logic_with_Standpoint_Modalities
DTSTART:20250515T110000
DTEND:20250515T120000
LOCATION:APB 3027
DESCRIPTION:Standpoint linear temporal logic (SLTL) is a recently introduced extension of classical linear temporal logic (LTL) with standpoint modalities. Intuitively\, these modalities allow to express that\, from agent a's standpoint\, it is conceivable that a given formula holds. Besides the standard interpretation of the standpoint modalities\, we introduce four new semantics\, which differ in the information an agent can extract from the history. We provide a general model checking algorithm applicable to SLTL under any of the five semantics. Furthermore\, we analyze the computational complexity of the corresponding model checking problems\, obtaining PSPACE-completeness in three cases\, which stands in contrast to the known EXPSPACE-completeness of the SLTL satisfiability problem.
DTSTAMP:20250512T091236
SEQUENCE:42325
END:VEVENT
BEGIN:VEVENT
SUMMARY:Restricted Chase Termination: You Want More than Fairness
URL://iccl.inf.tu-dresden.de/web/Restricted_Chase_Termination:_You_Want_More_than_Fairness
UID://iccl.inf.tu-dresden.de/web/Restricted_Chase_Termination:_You_Want_More_than_Fairness
DTSTART:20250508T110000
DTEND:20250508T120000
LOCATION:APB 3027
DESCRIPTION:The chase is a fundamental algorithm with ubiquitous uses in database theory. Given a database and a set of existential rules (aka tuple-generating dependencies)\, it iteratively extends the database to ensure that the rules are satisfied in a most general way. This process may not terminate\, and a major problem is to decide whether it does. This problem has been studied for a large number of chase variants\, which differ by the conditions under which a rule is applied to extend the database. Surprisingly\, the complexity of the universal termination of the restricted (aka standard) chase is not fully understood. We close this gap by placing universal restricted chase termination in the analytical hierarchy. This higher hardness is due to the fairness condition\, and we propose an alternative condition to reduce the hardness of universal termination.\n\n\nThis is joint work with David Carral\, Lucas Larroque\, and Michaël Thomazo.
DTSTAMP:20250506T050542
SEQUENCE:42284
END:VEVENT
BEGIN:VEVENT
SUMMARY:On Explicit Solutions to Fixed-Point Equations in Propositional Dynamic Logic
URL://iccl.inf.tu-dresden.de/web/On_Explicit_Solutions_to_Fixed-Point_Equations_in_Propositional_Dynamic_Logic
UID://iccl.inf.tu-dresden.de/web/On_Explicit_Solutions_to_Fixed-Point_Equations_in_Propositional_Dynamic_Logic
DTSTART:20250403T110000
DTEND:20250403T120000
LOCATION:APB 3027
DESCRIPTION:Propositional dynamic logic (PDL) is an important modal logic used to specify and reason about the behavior of programs. A challenging problem in the context of PDL is solving fixed-point equations\, i.e.\, formulae of the form x ≡ ϕ(x) such that x is a propositional variable and ϕ(x) is a formula containing x. A solution to such an equation is a formula ψ that omits x and satisfies ψ ≡ ϕ(ψ)\, where ϕ(ψ) is obtained by replacing all occurrences of x with ψ in ϕ(x). In this short talk\, we discuss PDL\, fixed-point equations\, and identify a class of PDL formulae arranged into two dual hierarchies for which every fixed-point equation x ≡ ϕ(x) has a solution.
DTSTAMP:20250401T053129
SEQUENCE:42102
END:VEVENT
BEGIN:VEVENT
SUMMARY:Formalizing Possibly Infinite Trees of Bounded Degree
URL://iccl.inf.tu-dresden.de/web/Formalizing_Possibly_Infinite_Trees_of_Bounded_Degree
UID://iccl.inf.tu-dresden.de/web/Formalizing_Possibly_Infinite_Trees_of_Bounded_Degree
DTSTART:20250306T110000
DTEND:20250306T120000
LOCATION:APB 3027
DESCRIPTION:As Lean does not support coinductive types directly\, formalizing infinite lists and infinite trees requires some "creativity". As a byproduct of one of our ongoing works\, we formalized possibly infinite trees of bounded degree in Lean. In this workshop\, we will reproduce this idea and present the definition from scratch (even without mathlib). We will work towards showing a special case of König’s Lemma: if each branch in such a tree is finite\, then there are only finitely many branches.\n\nThis is going to be an interactive talk so feel free to bring your machine with Lean installed!
DTSTAMP:20250228T100201
SEQUENCE:41535
END:VEVENT
BEGIN:VEVENT
SUMMARY:Description Logic with Abstraction and Refinement
URL://iccl.inf.tu-dresden.de/web/Description_Logic_with_Abstraction_and_Refinement
UID://iccl.inf.tu-dresden.de/web/Description_Logic_with_Abstraction_and_Refinement
DTSTART:20250206T110000
DTEND:20250206T120000
LOCATION:APB 3027
DESCRIPTION:Ontologies often require knowledge representation on multiple levels of abstraction\, but description logics (DLs) are not well-equipped for supporting this. We propose an extension of DLs in which abstraction levels are first-class citizens and which provides explicit operators for the abstraction and refinement of concepts and roles across multiple abstraction levels\, based on conjunctive queries. We prove that reasoning in the resulting family of DLs is decidable while several seemingly harmless variations turn out to be undecidable. We also pinpoint the precise complexity of our logics and several relevant fragments.
DTSTAMP:20250127T153039
SEQUENCE:40812
END:VEVENT
BEGIN:VEVENT
SUMMARY:GPTKB: Comprehensively Materializing Factual LLM Knowledge
URL://iccl.inf.tu-dresden.de/web/GPTKB:_Comprehensively_Materializing_Factual_LLM_Knowledge
UID://iccl.inf.tu-dresden.de/web/GPTKB:_Comprehensively_Materializing_Factual_LLM_Knowledge
DTSTART:20250116T110000
DTEND:20250116T120000
LOCATION:APB 3027
DESCRIPTION:LLMs have majorly advanced NLP and AI\, and next to their ability to perform a wide range of procedural tasks\, a major success factor is their internalized factual knowledge. Since (Petroni et al.\, 2019)\, analyzing this knowledge has gained attention. However\, most approaches investigate one question at a time via modest-sized pre-defined samples\, introducing an availability bias (Tversky and Kahnemann\, 1973) that prevents the discovery of knowledge (or beliefs) of LLMs beyond the experimenter's predisposition.\n\nTo address this challenge\, we propose a novel methodology to comprehensively materialize an LLM's factual knowledge through recursive querying and result consolidation.\n\nAs a prototype\, we employ GPT-4o-mini to construct GPTKB\, a large-scale knowledge base (KB) comprising 105 million triples for over 2.9 million entities - achieved at 1% of the cost of previous KB projects. This work potentially marks a milestone in two areas: (1) For LLM research\, for the first time\, it provides constructive insights into the scope and structure of LLMs' knowledge (or beliefs). For KB construction\, it pioneers new pathways for the long-standing challenge of general-domain KB construction. GPTKB is accessible at https://gptkb.org.
DTSTAMP:20250107T144837
SEQUENCE:40711
END:VEVENT
BEGIN:VEVENT
SUMMARY:Tree Automata with Global and Non-Global Counting
URL://iccl.inf.tu-dresden.de/web/Tree_Automata_with_Global_and_Non-Global_Counting
UID://iccl.inf.tu-dresden.de/web/Tree_Automata_with_Global_and_Non-Global_Counting
DTSTART:20241212T110000
DTEND:20241212T120000
LOCATION:APB 3027
DESCRIPTION:Similar to the case of finite string automata\, there is a long tradition of adding counting mechanisms to finite tree automata in order to increase their expressiveness\, resulting in two interesting models (among others): Parikh tree automata (PTA) increment a number of counters when computing a tree and eventually test their membership in a semilinear set. On the other hand\, one-counter tree automata (OCTA) use only one counter that can be incremented\, decremented and tested for zero during a computation. The calculation principles for the counting mechanisms work orthogonally in both approaches – while OCTA split their computations at each node and execute them pathwise\, PTA allow a global view: their counters are incremented over the whole input tree. When comparing the expressive power of the two models\, one will find differences that stem not only from the specific storage types used\, but also from the global or non-global view of the input.\n\nThis talk will report on two recent works\, where we exchanged the computation mode of both tree automata models:\n\nWe introduce global one-counter tree automata (GOCTA) deviating from OCTA by working on one counter which is passed through the tree in lexicographical order\, rather than duplicating the counter at every branching position. When comparing the capabilities of GOCTA and OCTA\, we obtain that their classes of recognizable tree languages are incomparable. Moreover\, we show that the non-emptiness problem of GOCTA is undecidable while\, in stark contrast\, their membership problem is in P.\n\nIn a similar spirit\, we define a non-global version of Parikh tree automata. Here\, we copy and distribute the current configuration at each node to all its children\, incrementing the counters pathwise\, and check the arithmetic constraint at each leaf. Again we obtain that\, in contrast to the original definition of PTA\, non-emptiness becomes undecidable if we allow the automaton to use at least three counters. However\, we can prove decidability of non-emptiness for a (still powerful) restriction of the model.
DTSTAMP:20241209T151105
SEQUENCE:40646
END:VEVENT
BEGIN:VEVENT
SUMMARY:Towards Understanding Brain Function by Uncovering the Conceptual Structure of C.elegans Sensorium
URL://iccl.inf.tu-dresden.de/web/Towards_Understanding_Brain_Function_by_Uncovering_the_Conceptual_Structure_of_C.elegans_Sensorium
UID://iccl.inf.tu-dresden.de/web/Towards_Understanding_Brain_Function_by_Uncovering_the_Conceptual_Structure_of_C.elegans_Sensorium
DTSTART:20241205T110000
DTEND:20241205T120000
LOCATION:APB 3027
DESCRIPTION:The framework of Embodied and Embedded cognition suggests that animals engage in a continuous sensory-motor feedback loop with their environment\, mediated by their nervous systems. A significant challenge in the study of nervous systems lies in the lack of a comprehensive model for the sensorium - the mechanism by which organisms perceive their surroundings.\nIn this presentation\, I will introduce two information theory-based approaches that enable exploration of the sensorium of Caenorhabditis elegans\, examining its connectivity\, responsiveness\, and neuronal characterization.\nThe first approach demonstrates how K-Formal Concept Analysis (K-FCA)\, an information-theoretical tool\, can be applied for Exploratory Data Analysis (EDA) of this sensorium.\nThrough K-FCA\, we can identify specific neurons’ responses to various odorants in an immediate and visual manner. Additionally\, this method allows us to observe clusters of neurons based on responsiveness to odorants\, as well as clusters of odorants according to their perceptual representations within the nematode’s sensorium.\nThe second approach focuses on characterizing neurons based on their neural traces\, using Convolutional Neural Networks (CNNs)\, Explainability techniques\, and FCA. Although this approach remains a work in progress\, I will present preliminary findings on how neurons can be characterized through their neural traces\, revealing distinct neuronal profiles that enable their identification.\nOverall\, this talk will showcase tools from Information Theory\, Deep Learning\, and Artificial Intelligence in general\, to support the exploration\, analysis\, and understanding of the structural organization of C. elegans’ sensorium. This will\, therefore\, allow us to begin to deeply understand brain functioning.
DTSTAMP:20241111T064103
SEQUENCE:40484
END:VEVENT
BEGIN:VEVENT
SUMMARY:The RustBelt and its Separation Logic
URL://iccl.inf.tu-dresden.de/web/The_RustBelt_and_its_Separation_Logic
UID://iccl.inf.tu-dresden.de/web/The_RustBelt_and_its_Separation_Logic
DTSTART:20241128T110000
DTEND:20241128T120000
LOCATION:APB 3027
DESCRIPTION:Rust is a systems-programming language whose expressive type system centers around the concept of ownership enabling both stronger\, statically verified safety guarantees as well as lower level control compared to more mainstream "safe" languages. The RustBelt project provided some formal verification for those claims using a seperation logic for modelling rusts typing rules. In this seminar we aim at giving an introduction into the features of Rust's type system as well as into the stack of logical tools used to verify the properties it promises.
DTSTAMP:20241125T122826
SEQUENCE:40567
END:VEVENT
BEGIN:VEVENT
SUMMARY:Tsetlin Machine\, A Game Theoretic Bandit Driven Approach to Optimal Pattern Recognition with Propositional Logic
URL://iccl.inf.tu-dresden.de/web/Tsetlin_Machine,_A_Game_Theoretic_Bandit_Driven_Approach_to_Optimal_Pattern_Recognition_with_Propositional_Logic
UID://iccl.inf.tu-dresden.de/web/Tsetlin_Machine,_A_Game_Theoretic_Bandit_Driven_Approach_to_Optimal_Pattern_Recognition_with_Propositional_Logic
DTSTART:20241121T110000
DTEND:20241121T120000
LOCATION:APB 3027
DESCRIPTION:This is a talk about a paper [1] with the following abstract:\n\nAlthough simple individually\, artificial neurons provide state-of-the-art performance when interconnected in deep networks. Arguably\, the Tsetlin Automaton is an even simpler and more versatile learning mechanism\, capable of solving the multi-armed bandit problem. Merely by means of a single integer as memory\, it learns the optimal action in stochastic environments through increment and decrement operations. In this paper\, we introduce the Tsetlin Machine\, which solves complex pattern recognition problems with propositional formulas\, composed by a collective of Tsetlin Automata. To eliminate the longstanding problem of vanishing signal-to-noise ratio\, the Tsetlin Machine orchestrates the automata using a novel game. Further\, both inputs\, patterns\, and outputs are expressed as bits\, while recognition and learning rely on bit manipulation\, simplifying computation. Our theoretical analysis establishes that the Nash equilibria of the game align with the propositional formulas that provide optimal pattern recognition accuracy. This translates to learning without local optima\, only global ones. In five benchmarks\, the Tsetlin Machine provides competitive accuracy compared with SVMs\, Decision Trees\, Random Forests\, Naive Bayes Classifier\, Logistic Regression\, and Neural Networks. We further demonstrate how the propositional formulas facilitate interpretation. In conclusion\, we believe the combination of high accuracy\, interpretability\, and computational simplicity makes the Tsetlin Machine a promising tool for a wide range of domains.\n\n[1] https://arxiv.org/abs/1804.01508
DTSTAMP:20241121T075858
SEQUENCE:40539
END:VEVENT
BEGIN:VEVENT
SUMMARY:Bypassing the ASP Bottleneck: Hybrid Grounding by Splitting and Rewriting
URL://iccl.inf.tu-dresden.de/web/Bypassing_the_ASP_Bottleneck:_Hybrid_Grounding_by_Splitting_and_Rewriting
UID://iccl.inf.tu-dresden.de/web/Bypassing_the_ASP_Bottleneck:_Hybrid_Grounding_by_Splitting_and_Rewriting
DTSTART:20241114T110000
DTEND:20241114T120000
LOCATION:APB 3027
DESCRIPTION:Answer Set Programming (ASP) is a key paradigm for problems in artificial intelligence and industrial contexts. In ASP\, problems are modeled via a set of rules. Over the time this paradigm grew into a rich language\, enabling complex rule types like aggregate expressions. Most practical ASP systems follow a ground-and-solve pattern\, where rule schemes are grounded and resulting rules are solved. There\, the so-called grounding bottleneck may prevent from solving\, due to sheer grounding sizes. Recently\, body-decoupled grounding (BDG) [1] demonstrated how to reduce grounding sizes by delegating effort to solving. However\, BDG provides limited interoperability with traditional grounders and only covers simple rule types.  \nHybrid Grounding\, which we presented at IJCAI24 [2]\, enables interoperability by the introduction of a novel splitting theorem that allows the free combination of BDG with traditional grounders. Further\, we extended the handled rule types with aggregates.\n\nIn this talk\, we will (i) provide an overview of BDG and Hybrid Grounding\, along with examples demonstrating the practical benefits of Hybrid Grounding. Further\, we (ii) delve into the specifics of BDG\, and (iii) finally discuss how Hybrid Grounding achieves interoperability between BDG and state-of-the-art methods.\n\n[1] Viktor Besin\, Markus Hecher\, and Stefan Woltran. „Body-Decoupled Grounding via Solving: A Novel Approach on the ASP Bottleneck“. In: IJCAI22 (2022).  \n[2] Alexander Beiser\, Markus Hecher\, Kaan Unalan\, and Stefan Woltran. „Bypassing the ASP Bottleneck: Hybrid Grounding by Splitting and Rewriting“. In: IJCAI24 (2024).
DTSTAMP:20241111T063724
SEQUENCE:40479
END:VEVENT
BEGIN:VEVENT
SUMMARY:Cyclic Proof Theory
URL://iccl.inf.tu-dresden.de/web/Cyclic_Proof_Theory
UID://iccl.inf.tu-dresden.de/web/Cyclic_Proof_Theory
DTSTART:20241024T110000
DTEND:20241024T120000
LOCATION:APB 3027
DESCRIPTION:Proofs are a central tool in mathematics and a core concept in the study of formal reasoning. Traditionally\, a proof is conceived as a finite object which is used to certify the correctness of our mathematical structures and their properties. Less common are so called cyclic proofs which\, although infinitary\, exhibit periodic patterns. Cyclic proof systems have proven to be a remarkably useful alternative in the mathematical study of computational systems\, particularly in connection with algorithms\, databases and programs. In this talk we will introduce cyclic proofs and study the extent to which these classes of proofs lend themselves to traditional proof theoretic techniques.
DTSTAMP:20241020T173522
SEQUENCE:40335
END:VEVENT
BEGIN:VEVENT
SUMMARY:Knowledge-aware Artificial Intelligence or How to Rock Your CS@TUD Studies with chatGPT
URL://iccl.inf.tu-dresden.de/web/Knowledge-aware_Artificial_Intelligence_or_How_to_Rock_Your_CS@TUD_Studies_with_chatGPT
UID://iccl.inf.tu-dresden.de/web/Knowledge-aware_Artificial_Intelligence_or_How_to_Rock_Your_CS@TUD_Studies_with_chatGPT
DTSTART:20241022T164000
DTEND:20241022T174000
LOCATION:APB E023
DESCRIPTION:In the first part of this inaugural lecture\, I will provide an overview of the field of knowledge-aware artificial intelligence\, with a focus on two pillars of AI knowledge\, knowledge graphs (KGs) and large language models (LLMs). The second part will highlight key areas of my research\, including knowledge estimation\, knowledge extraction\, and commonsense knowledge.\nI will also provide a recipe for successfully completing CS studies at TUD with chatGPT
DTSTAMP:20241022T081735
SEQUENCE:40370
END:VEVENT
BEGIN:VEVENT
SUMMARY:Navigating ASP Solution Spaces2
URL://iccl.inf.tu-dresden.de/web/Navigating_ASP_Solution_Spaces2
UID://iccl.inf.tu-dresden.de/web/Navigating_ASP_Solution_Spaces2
DTSTART:20241017T110000
DTEND:20241017T120000
LOCATION:APB 3027
DESCRIPTION:'''This talk has been canceled. There will be no seminar on Oct 17.'''\n\nA wide range of combinatorial search problems can be modelled and solved with Answer Set Programming (ASP). While modern ASP solvers allow to quickly enumerate solutions\, the user faces the problem of dealing with a possibly exponential number of solutions\, which may easily go into millions and beyond. To still be able to reach an understanding of the answer set space\, we propose navigation approaches to reach subspaces that fulfill desirable criteria. We start with an iterative approach to compute a diverse collection of answer sets that allows to exchange some answer sets to improve the size and diversity of the whole collection. Then\, we propose an approach to collect representative answer sets that\, in contrast to diverse collections\, do not require to \nspecify a diversity measure. With weighted faceted answer set navigation we allow for a quantitative understanding of the answer set space. Weights can be assigned to atoms depending on how much they restrict the remaining solution space\, either by counting the number of answer sets (resp. supported models) or counting the number of atoms still available to choose. Finally\, we will present a visual approach to explore solution spaces and apply it to the domain of abstract argumentation.
DTSTAMP:20241022T050232
SEQUENCE:40364
END:VEVENT
BEGIN:VEVENT
SUMMARY:Adding Circumscription to Decidable Fragments of First-Order Logic: A Complexity Rollercoaster
URL://iccl.inf.tu-dresden.de/web/Adding_Circumscription_to_Decidable_Fragments_of_First-Order_Logic:_A_Complexity_Rollercoaster
UID://iccl.inf.tu-dresden.de/web/Adding_Circumscription_to_Decidable_Fragments_of_First-Order_Logic:_A_Complexity_Rollercoaster
DTSTART:20241010T110000
DTEND:20241010T120000
LOCATION:Https://bbb.tu-dresden.de/rooms/n5w-ghp-qoq-kts/join
DESCRIPTION:We study extensions of expressive decidable fragments of first-order logic with circumscription\, in particular the two-variable fragment FO2\, its extension C2 with counting quantifiers\, and the guarded fragment GF. We prove that if only unary predicates are minimized (or fixed) during circumscription\, then decidability of logical consequence is preserved. For FO2 the complexity increases from coNExp to coNExp^NP-complete\, for GF it (remarkably!) increases from 2Exp to Tower-complete\, and for C2 the complexity remains open. We also consider querying circumscribed knowledge bases whose ontology is a GF sentence\, showing that the problem is decidable for unions of conjunctive queries\, Tower-complete in combined complexity\, and Elementary in data complexity. Already for atomic queries and ontologies that are sets of guarded existential rules\, however\, for every k ≥ 0 there is an ontology and query that are k-Exp-hard in data complexity.
DTSTAMP:20240930T124624
SEQUENCE:40165
END:VEVENT
BEGIN:VEVENT
SUMMARY:Winning Snake: Design Choices in Multi-Shot ASP
URL://iccl.inf.tu-dresden.de/web/Winning_Snake:_Design_Choices_in_Multi-Shot_ASP
UID://iccl.inf.tu-dresden.de/web/Winning_Snake:_Design_Choices_in_Multi-Shot_ASP
DTSTART:20240926T110000
DTEND:20240926T120000
LOCATION:APB 3027
DESCRIPTION:Answer set programming is a well-understood and established problem-solving and knowledge representation paradigm. It has become more prominent amongst a wider audience due to its multiple applications in science and industry. The constant development of advanced programming and modeling techniques extends the toolset for developers and users regularly. This paper demonstrates different techniques to reuse logic program parts (multi-shot) by solving the arcade game snake. This game is particularly interesting because a victory can be assured by solving the underlying NP-hard problem of Hamiltonian Cycles. We will demonstrate five hands-on implementations in clingo and compare their performance in an empirical evaluation. In addition\, our implementation utilizes clingraph to generate a simple yet informative image representation of the game’s progress.
DTSTAMP:20240916T052211
SEQUENCE:40116
END:VEVENT
BEGIN:VEVENT
SUMMARY:Characterizing common argumentation semantics using branch evaluations for justification systems
URL://iccl.inf.tu-dresden.de/web/Characterizing_common_argumentation_semantics_using_branch_evaluations_for_justification_systems
UID://iccl.inf.tu-dresden.de/web/Characterizing_common_argumentation_semantics_using_branch_evaluations_for_justification_systems
DTSTART:20240815T110000
DTEND:20240815T120000
LOCATION:APB 3027
DESCRIPTION:First introduced in 2015 by Denecker\, Brewka and Strass\, justification theory is formalism providing a new way of characterizing semantics for both logic programs and Dung style argumentation frameworks. Justification theory uses branch evaluation functions operating on a body of rules and an interpretation to define a set of justified facts. Fixpoints of the branch evaluation function on a given body of rules are called justified interpretations. Common semantics for argumentation frameworks can be obtained using these justified interpretations. In this work we characterize these semantics using branch evaluations with the goal of characterizing exactly the desired semantics with no additional conditions imposed on the justified interpretations.\nWe present a grounded branch evaluation yielding grounded semantics for argumentation. This grounded branch evaluation coincides with the branch evaluations providing well founded and Kripke-Kleene semantics for logic programming. Furthermore we show that for admissible\, preferred and stable argumentation semantics an exact characterization in the general case is not possible.
DTSTAMP:20240624T061542
SEQUENCE:39845
END:VEVENT
BEGIN:VEVENT
SUMMARY:Multi-Cultural Commonsense Knowledge Base Construction
URL://iccl.inf.tu-dresden.de/web/Multi-Cultural_Commonsense_Knowledge_Base_Construction
UID://iccl.inf.tu-dresden.de/web/Multi-Cultural_Commonsense_Knowledge_Base_Construction
DTSTART:20240808T110000
DTEND:20240808T120000
LOCATION:APB 3027
DESCRIPTION:Commonsense knowledge (CSK) about concepts and their properties is useful for AI applications such as robust dialogue. Prior works like ConceptNet\, TupleKB and others compiled noteworthy commonsense knowledge bases (CSKBs)\, but are restricted in their expressiveness to subject-predicate-object (SPO) triples with simple concepts for S and monolithic strings for P and O. Also\, these projects have either prioritized precision or recall\, but hardly reconcile these complementary goals. In this talk I will present several of our CSKB construction works (DICE\, ASCENT\, CANDLE\, MANGO)\, where we automatically build large-scale CSKBs with advanced expressiveness and both better precision and recall than prior works.\n\nIn DICE\, we introduce multi-faceted scoring\, and joint reasoning for consistency and corroboration. With ASCENT\, we go beyond triples by capturing composite concepts with subgroups and aspects\, and by refining assertions with semantic facets. CANDLE focuses on multi-cultural CSK\, while MANGO unifies the entity-centric model of ASCENT and the culture-centric model of CANDLE.\n\nThe works rely on a combination of textual information extraction and knowledge distillation from LLMs. Intrinsic evaluation shows the superior size and quality of our CSKBs\, and extrinsic use cases prove their utility for retrieval-augmented generation.\n\nLinks:\n\nProject overview: https://www.mpi-inf.mpg.de/commonsense\n\nAscent: https://ascent.mpi-inf.mpg.de\n\nCandle: https://candle.mpi-inf.mpg.de\n\nMango: https://bit.ly/cultural-csk
DTSTAMP:20240808T110807
SEQUENCE:40015
END:VEVENT
BEGIN:VEVENT
SUMMARY:Algebraic Aspects of Propositional Logic\, and Future Work in Defeasibile Reasoning
URL://iccl.inf.tu-dresden.de/web/Algebraic_Aspects_of_Propositional_Logic,_and_Future_Work_in_Defeasibile_Reasoning
UID://iccl.inf.tu-dresden.de/web/Algebraic_Aspects_of_Propositional_Logic,_and_Future_Work_in_Defeasibile_Reasoning
DTSTART:20240718T110000
DTEND:20240718T120000
LOCATION:APB 3027
DESCRIPTION:This talk will consist of two parts. In the first part\, I will discuss work from my masters thesis on algebraic aspects of propositional logic. In particular\, I will provide a brief introduction into universal algebra\, and describe how a propositional theory of logic corresponds to a variety of universal algebra in a generalized setting. Using this correspondence and certain examples\, we will then characterise a notion of completeness in an algebraic setting for propositional logics.\n\nIn the second part of the talk\, I will talk a little bit about the area of interest and the central questions for my PhD studies. Specifically\, I will give a brief introduction to KLM style defeasibility and introduce the problems I am working on with regards to introducing KLM-style reasoning into more expressive logics.
DTSTAMP:20240716T052500
SEQUENCE:39966
END:VEVENT
BEGIN:VEVENT
SUMMARY:Finite Groundings for ASP with Functions: A Journey through Consistency
URL://iccl.inf.tu-dresden.de/web/Finite_Groundings_for_ASP_with_Functions:_A_Journey_through_Consistency
UID://iccl.inf.tu-dresden.de/web/Finite_Groundings_for_ASP_with_Functions:_A_Journey_through_Consistency
DTSTART:20240711T110000
DTEND:20240711T120000
LOCATION:APB 3027
DESCRIPTION:Answer set programming (ASP) is a logic programming formalism used in various areas of artificial intelligence like combinatorial problem solving and knowledge representation and reasoning. It is known that enhancing ASP with function symbols makes basic reasoning problems highly undecidable. However\, even in simple cases\, state of the art reasoners\, specifically those relying on a ground-and-solve approach\, fail to produce a result. Therefore\, we reconsider consistency as a basic reasoning problem for ASP. We show reductions that give an intuition for the high level of undecidability. These insights allow for a more fine-grained analysis where we characterize ASP programs as "frugal" and "non-proliferous". For such programs\, we are not only able to semi-decide consistency but we also propose a grounding procedure that yields finite groundings on more ASP programs with the concept of "forbidden" facts.
DTSTAMP:20240709T061437
SEQUENCE:39935
END:VEVENT
BEGIN:VEVENT
SUMMARY:Research Lightning Talks
URL://iccl.inf.tu-dresden.de/web/Research_Lightning_Talks
UID://iccl.inf.tu-dresden.de/web/Research_Lightning_Talks
DTSTART:20240627T110000
DTEND:20240627T120000
LOCATION:APB 3027
DESCRIPTION:In this seminar session\, three of our guest students will present their recent and ongoing research in three short talks.\n\n\n1. Aidan Bailey will show two applications of ASP. On one hand\, the generation of propositional formulas\, and by extension knowledge bases\, adhering to specified properties. On the other hand\, graph drawing via placements of nodes and edges adhering to constraints and optimised on specific criteria promoting usability\, understandability and aesthetics.\n\n2. Lucas Carr will present an idea for a notion of defeasible implications in formal concept analysis\, which is currently being developed. Formal concept analysis allows us to model hierarchies between concepts\, where concepts are defined by a relation between objects which fall into the concept\, and properties these objects share. A clear notion of implication exists within FCA\, which can be loosely characterised as saying attributes X imply attributes Y\, if every object with X also has Y. The focus of my work will be to try introduce a notion of defeasibility\, which would enable us to say attributes X imply attributes Y within some frame of preference\, or typicality. The motivation for this is to allow to recognise relations in data which do not strictly hold\, but are still potentially useful.\n\n3. Luke Slater will talk about knowledge compilation for ranking functions. Ranking functions are essential in various domains of defeasible reasoning\, such as belief revision. These functions operate by dividing the space of Boolean valuations into a totally ordered partition\, necessitating separate SAT solving steps for inference at each rank. This research aims to develop a method to compile a ranking function into a single structure\, facilitating inference through a single query.
DTSTAMP:20240625T053839
SEQUENCE:39868
END:VEVENT
BEGIN:VEVENT
SUMMARY:PhD Defense of Bartosz Bednarczyk
URL://iccl.inf.tu-dresden.de/web/PhD_Defense_of_Bartosz_Bednarczyk
UID://iccl.inf.tu-dresden.de/web/PhD_Defense_of_Bartosz_Bednarczyk
DTSTART:20240625T133000
DTEND:20240625T150000
LOCATION:APB 1004
DESCRIPTION:The public defence of the doctoral dissertation titled "Database-Inspired Reasoning Problems in Description Logics With Path Expressions" by Bartosz Bednarczyk (supervised by prof. Sebastian Rudolph and prof. Emanuel Kieroński) will take place on the 25th of June at 01:30 p.m. (APB 1004).  \n\nThe draft of the thesis is available here: https://iccl.inf.tu-dresden.de/web/Phdthesis3021/en\n\nThe defence starts at 13:30 in APB 1004. It will also be streamed via Zoom. \nhttps://tu-dresden.zoom-x.de/j/65979593638?pwd=LVdbGbkGy2aQnFijO28tqYkfshU23d.1
DTSTAMP:20240625T032807
SEQUENCE:39858
END:VEVENT
END:VCALENDAR