Attribut:Beschreibung DE
Aus International Center for Computational Logic
Dies ist eine Eigenschaft des Typs Text.
"
(joint work with Jakub Michaliszyn from University of Wrocław)
Linear 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.
The talk will take approximately 30 minutes and will be held online via BigBlueButton. To access the room, take one of the following links:
with ZIH-login:
https://selfservice.zih.tu-dresden.de/l/link.php?m=67110&p=dbb695ef
without ZIH-login:
https://selfservice.zih.tu-dresden.de/link.php?m=67110&p=cf01a562 +
1
'''Themen und Arbeitsort:''' In [https://www.secai.org SECAI] arbeiten Forscher/innen unterschiedlicher Fachrichtungen gemeinsam an der Weiterentwicklung der Künstlichen Intelligenz. Die Bandbreite der angebotenen Themen reicht dabei von Kerngebieten der Informatik und Elektronik über medizinische Anwendungen bis zu gesellschaftlichen Aspekten der KI. Besondere Schwerpunkte in SECAI sind:
* ''Composite AI:'' Wie kann man Maschinelles Lernen und symbolische KI-Methoden verbinden?
* ''AI Compute Paradigms:'' Wie wird die KI-Hardware der Zukunft aussehen und funktionieren?
* ''Intelligent Medical Devices:'' Wie kann KI cybermedizinsiche Systeme voranbringen?
* ''AI Methods for Health:'' Wie hilft Informationsverarbeitung mit KI in Therapie und Diagnostik?
* ''Societal Framework of AI:'' Wie kann KI rechtssicher und vertrauenswert werden?
Der Arbeitsort (Dresden oder Leipzig) ist abhängig von dem der Stelle zugeordneten Forschungsthema. Informationen zu den verfügbaren Themen und Betreuer/innen finden Sie unter https://secai.org/topics.
'''Aufgaben:''' Als Mitglied der SECAI Graduate School verwirklichen Sie herausfordernde Forschungsvorhaben unter der fachlichen Betreuung führender KI-Expert/innen und gemeinsam im Team mit anderen Forscher/innen in Dresden und Leipzig. Sie entwickeln Ihr Forschungsprofil, publizieren und präsentieren Ihre Ergebnisse und vernetzten sich mit der internationalen Community.
'''Chancen:''' SECAI bietet ein erstklassiges Umfeld zur Entwicklung Ihrer Karriere. Sie arbeiten mit international hervorragend ausgewiesenen Forscher/innen und profitieren von der starken Vernetzung der School mit Industrie und Wissenschaft. Die Ausbildung hervorragend qualifizierter Nachwuchswissenschaftler/innen ist ein wesentliches Projektziel in SECAI und Promovierende werden bei Forschungs- und Karriereplanung durch vielfältige Angebote unterstützt.
'''Voraussetzungen:''' sehr guter wiss. Hochschulabschluss in einer für die Forschungsthemen in SECAI relevanten Fachrichtung (z.B. Informatik, Mathematik, Elektrotechnik, Medizintechnik, Bioinformatik oder Rechtswissenschaften); sehr gute Englischkenntnisse. Kreativität, Freude am Forschen sowie ein Sinn für wissenschaftliche Qualität und ethisches Verhalten in der Forschung sind von Vorteil. Bitte geben Sie an, für welche der unter https://secai.org/topics angegebenen Themen Sie sich bewerben möchten.
Am 11. und 12. Februar fand der 11. Workshop der EMCL-Studenten in Wien statt.
Der Workshop wurde durch die Studenten des Europäischem Master Programm in Computational Logic der Universitäten Bozen, Dresden, Wien und Lissabon selbst organisiert und beinhaltete Vorträge der Studierenden, Alumni, Doktoranten und anderer Wissenschaftler über ihre Forschungsprojekte.
Am Workshop nahmen Studenten aus mehr als 21 Nationen teil.
Dabei wurde der Best Master Thesis Award 2015 an Adrian Rebola Pardo für seine Arbeit über die Generierung von Beweisen in SAT Solvern verliehen.
Abgerundet wurde der Workshop mit einer Tour durch die Stadt zur Domkirche St. Stephan und einem gemeinsamen Abendessen in dem ansässigen Lokal Die Halle.
[http://www.emcl-study.eu www.emcl-study.eu] +
Logics have, for many years, laid claim to providing a formal basis for the study and development of applications and systems in Artificial Intelligence. With the depth and maturity of formalisms, methodologies and logic-based systems today, this claim is stronger than ever.
The European Conference on Logics in Artificial Intelligence (or Journées Européennes sur la Logique en Intelligence Artificielle - JELIA) began back in 1988, as a workshop, in response to the need for a European forum for the discussion of emerging work in this field. Since then, JELIA has been organised biennially, with English as official language, and with proceedings published in Springer-Verlag's Lecture Notes in Artificial Intelligence. Previous meetings took place in Roscoff, France (1988), Amsterdam, Netherlands (1990), Berlin, Germany (1992), York, UK (1994), Évora, Portugal (1996), Dagstuhl, Germany (1998), Málaga, Spain (2000), Cosenza, Italy (2002), Lisbon, Portugal (2004), and Liverpool, UK (2006).
The increasing interest in this forum, its international level with growing participation from researchers outside Europe, and the overall technical quality, has turned JELIA into a major biennial forum for the discussion of logic-based approaches to artificial intelligence. +
Am 20. und 21. Februar findet der 12. Workshop der EMCL-Studenten in Dresden statt.
Der Workshop wird durch die Studenten des Europäischem Master Programm in Computational Logic der Universitäten Bozen, Dresden, Wien und Lissabon selbst organisiert und beinhaltet Vorträge der Studierenden, Alumni, Doktoranten und anderer Wissenschaftler über ihre Forschungsprojekte. Dabei wird der Best Master Thesis Award 2017 verliehen. +
Logische Programmierung ist eine besonders weitgehende Art, Probleme deklarativ zu spezifizieren. In der Form von Prolog geschieht das durch den Einsatz eines Fragments der Logik. Weitergehende Konzepte integrieren in dieses ursprünglich rein relationale Konzept auch Funktionen und Constraints. In den vergangenen Jahren hat dieses Paradigma eine hohe Attraktivität erworben, u.a. in den Bereichen Datenbanken und Verarbeitung von natürlicher Sprache und bei der Modellierung und Bearbeitung komplexer kombinatorischer Probleme. Die Logikprogrammierung ist somit ein aktives Gebiet geblieben, das sich zunehmend auch den schwierigen Thematiken der Integration in die übrige Softwarelandschaft, der Behandlung von Dynamik und des Umgangs mit Kommunikation stellt. +
2
The workshops on (constraint) logic programming are the annual meeting of the Society of Logic Programming (GLP e.V.) and bring together researchers interested in logic programming, constraint programming, and related areas like databases and artificial intelligence. Previous workshops have been held in Germany, Austria and Switzerland. The technical program of the workshop will include invited talks, presentations of refereed papers and demo presentations. +
The Workshops on (Constraint) Logic Programming are the annual meeting of the German Society of Logic Programming Gesellschaft für Logische Programmierung e.V. (GLP) and brings together researchers interested in logic programming, constraint programming, answer set programming, and related areas like databases and artificial intelligence (not only from Germany).
The workshops provide a forum for exchanging ideas on declarative logic programming, nonmonotonic reasoning and knowledge representation, and facilitate interactions between research in theoretical foundations and in the design and implementation of logic-based programming systems.
The technical program of the workshop will include invited talks, presentations of refereed papers, and system demonstrations. +
The Workshops on (Constraint) Logic Programming are the annual meeting of the German Society of Logic Programming Gesellschaft für Logische Programmierung e.V. (GLP) and brings together researchers interested in logic programming, constraint programming, answer set programming, and related areas like databases and artificial intelligence (not only from Germany).
The workshops provide a forum for exchanging ideas on declarative logic programming, nonmonotonic reasoning and knowledge representation, and facilitate interactions between research in theoretical foundations and in the design and implementation of logic-based programming systems.
The technical program of the workshop will include invited talks, presentations of refereed papers, and system demonstrations. +
3
Im September 2015 findet die jährliche [http://www.tu-dresden.de/inf/ki2015 KI Konferenz] in Dresden inklusive mehrerer Workshops statt. Die Konferenz wird von vielen Mitgliedern des ICCL organisiert. +
KI 2015 is the 38th edition of the German Conference on Artificial Intelligence, which traditionally brings together academic and industrial researchers from all areas of AI, providing a premier forum for exchanging news and research results on theory and applications of intelligent system technology.
In September 2015, prior to the conference, there is an international summer school on reasoning organized by the international center of computational logic. +
8
[https://scads.ai/ ScaDS.AI] veranstaltet vom 11.07. bis 15.07.2022 die [https://scads.ai/education/summer-schools/scads-ai-summer-school-2022/ 8th International Summer School on AI and Big Data].
<br><br>
[https://scads.ai/ ScaDS.AI] (Center for Scalable Data Analytics and Artificial Intelligence) Dresden/Leipzig ist ein Zentrum für Data Science, Artificial Intelligence und Big Data mit Standorten in Dresden und Leipzig. Es ist eines von fünf neuen KI-Zentren in Deutschland, die im Rahmen der KI-Strategie der Bundesregierung gefördert werden, und soll als dauerhafte Forschungseinrichtung etabliert werden.
<br><br>
Die Themen für dieses Jahr sind u.a. Datenintegration und KI, NLP und KI, Datenschutz und vertrauenswürdige KI, KI in der Medizin/den Lebenswissenschaften und KI in den Geo- und Umweltwissenschaften.
<br><br>
Die Sommerschule richtet sich an Masterstudierende, Doktoranden, Forscher sowie Berufstätige, die in den Bereichen maschinelles Lernen, künstliche Intelligenz und/oder Big Data tätig sind oder werden. +
9
Multi-Agent Systems are communities of problem-solving entities that can perceive and act upon their environment in order to achieve both their individual goals and their joint goals. The work on such systems integrates many technologies and concepts from artificial intelligence and other areas of computing as well as other disciplines. Over recent years, the agent paradigm gained popularity, due to its applicability to a full spectrum of domains, such as search engines, recommendation systems, educational support, e-procurement, simulation and routing, electronic commerce and trade, etc. Computational logic provides a well-defined, general, and rigorous framework for studying the syntax, semantics and procedures for the various tasks in individual agents, as well as the interaction between, and integration amongst, agents in multi-agent systems. It also provides tools, techniques and standards for implementations and environments, for linking specifications to implementations, and for the verification of properties of individual agents, multi-agent systems and their implementations. +
A
In a previous paper [1], we have shown that clause sets belonging to the Horn Bernays-Schönfinkel fragment over simple linear arithmetic (HBS(SLA)) can be translated into HBS clause sets over a finite set of first-order constants.
HBS clause sets are also called Datalog programs and HBS(SLA) can be seen as an extension of Datalog programs that allow simple arithmetic inequalities in the bodies of rules. The translation from HBS(SLA) to HBS preserves validity and satisfiability and it is still applicable if we extend our input with positive universally or existentially quantified verification conditions (conjectures). We call this translation a Datalog hammer. The combination of its implementation in SPASS-SPL with the Datalog reasoner VLog establishes an effective way of deciding verification conditions in the Horn fragment. As a result, we were able to verify supervisor code for two examples: a lane change assistant in a car and an electronic control unit of a supercharged combustion engine.
In this talk, we present several new improvements to our Datalog hammer: we have generalized it to mixed real-integer arithmetic and finite first-order sorts; we extended the class of acceptable inequalities beyond variable bounds and positively grounded inequalities, and we significantly reduced the size of the hammer output by a soft typing discipline. We call the result the sorted Datalog hammer. It not only allows us to handle more complex supervisor code and to model already considered supervisor code more concisely, but it also improves our performance on real-world benchmark examples.
References:
[1] Bromberger, M., Dragoste, I., Faqeh, R., Fetzer, C., Krötzsch, M., Weidenbach, C.: A Datalog hammer for supervisor verification conditions modulo simple linear arithmetic. In: Reger, G.,Konev, B. (eds.) Frontiers of Combining Systems - 13th International Symposium, FroCoS 2021, Birmingham, United Kingdom, September 8-10, 2021. Proceedings. Lecture Notes in Computer Science, vol. 12941, pp. 3–24. Springer (2021)
Online talk link:
https://bbb.tu-dresden.de/b/ali-zgz-l8d-52n
Regular path queries (RPQs) are a central component of graph databases. We investigate decision- and enumeration problems concerning the evaluation of RPQs under several semantics that have recently been considered: arbitrary paths, shortest paths, and simple paths.
Whereas arbitrary and shortest paths can be enumerated in polynomial delay, the situation is much more intricate for simple paths. For instance, already the question if a given graph contains a simple path of a certain length has cases with highly non-trivial solutions and cases that are long-standing open problems. We study RPQ evaluation for simple paths from a parameterized complexity perspective and define a class of simple transitive expressions that is prominent in practice and for which we can prove a dichotomy for the evaluation problem. We observe that, even though simple path semantics is intractable for RPQs in general, it is feasible for the vast majority of RPQs that are used in practice. At the heart of our study on simple paths is a result of independent interest: the two disjoint paths problem in directed graphs is W[1]-hard if parameterized by the length of one of the two paths.
'''Bio:''' Wim Martens is a professor for Theoretical Computer Science at the University of Bayreuth. He is interested in theoretical aspects of data management, formal language theory, logic, and complexity. He was an invited speaker at STOC 2017 and his research received several awards, including the ACM SIGMOD research highlight award and the Dissertation Award for Computer Science, Belgium. Currently, he is on the editorial board of ACM TODS and he is chairing the ICDT Council. His talk reports about research for which he recently received the Best Paper Award of the International Conference on Database Theory 2018. +
Abstract:
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.
However, Eyal and Sirer introduced a strategy for a miner to time the publishing of blocks that will give them a significant edge in profits.
This 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.
Bio:
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. +
Model counting (#SAT) asks to compute the number of satisfying assignments for a propositional formula. The decision version (SAT) received widespread interest in computational complexity, formed many applications in modern combinatorial problem solving, and can be solved effectively for millions of variables on structured instances. #SAT is much harder than SAT and requires more elaborate solving techniques. In this talk, we revisit the problem, its complexity, and explain its connection to quantitative AI. We briefly overview solving techniques and illustrate a parameterized algorithm and implementation to tackle the problem. While purely parameterized approaches from theory often suffer practical limitations, we elaborate that a parameterized algorithm can be successful when combining it with modern hardware that takes advantage of parallelism. +
In many scientific and industrial applications, graph databases are gaining momentum thanks to the competitive performance they offer and their flexibility, not to mention their interpretability. Still, their uses remain somehow limited due to their lack of consistency-checking strategies. Here, I introduce a scheme-based access to data in order to assert constraints and keep consistency, while also opening possibilities for reasoning in logic-based approaches, in a multi-strategy setting. The possible uses and capabilities are still under investigation, but the potentialities in almost every domain seem to be promising.
The talk will take place in a hybrid fashion, physically in the APB room 3027, and online through the link:
https://bbb.tu-dresden.de/b/pio-zwt-smp-aus +
Abstract: Decidability of inferencing is commonly considered a very important property of logic-based knowledge representation formalisms, required for the algorithmization and automation of reasoning. Yet, oftentimes, the corresponding (un)decidability arguments are idiosyncratic and do not shed much light on the underlying principles governing the divide.
In my talk, I will review generic model-theoretic criteria for decidability of querying in fragments of first-order logic. I will describe a general framework by means of which decidability of query entailment can be established based on the existence of countermodels with certain structural properties. These properties depend on the ontology and query language used and range from finite domain over forest-like shape to width-finiteness employing width notions like treewidth and cliquewidth.
The talk will take place in a hybrid fashion, physically in the APB room 3027, and online through the link:
https://bbb.tu-dresden.de/b/pio-zwt-smp-aus +
The Shapes Constraint Language (SHACL) was recommended by the W3C in 2017 for describing constraints on RDF graphs and validating them. As it turns out, SHACL is closely related to Description Logics and to monadic Datalog, both familiar KR languages. Building on these connections, we introduce SHACL and its main reasoning problems in familiar KR terms. We discuss in particular the different approaches to the semantics of recursive SHACL, and the complexity of validation in some important fragments. Then we will recap some recent and ongoing research work on SHACL, and point to some of the many interesting open challenges, shedding light on how ideas and techniques from familiar KR areas can help develop SHACL further. +
