Attribut:Beschreibung EN
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
'''Topics and Work Location:''' Researchers of several disciplines are collaborating in [https://www.secai.org SECAI] on advancing AI. The spectrum of available topics ranges from core areas of computer science and electronics over medical applications to societal aspects of AI. SECAI’s main research focus areas are:
* ''Composite AI:'' How can machine learning and symbolic AI methods be combined?
* ''AI Compute Paradigms:'' How will future AI hardware look and how will it be used?
* ''Intelligent Medical Devices:'' How can AI advance cybermedical systems?
* ''AI Methods for Health:'' How can AI methods support therapy and diagnostis?
* ''Societal Framework of AI:'' How can AI become trustworthy and free of legal risks?
The location of work (Dresden or Leipzig) depends on the topic assigned for each position. Information about the available topics and supervisors can be found at https://secai.org/topics/.
'''Tasks:''' As a member of the SECAI graduate school, you are answering challenging research questions under the supervision of leading researchers and together with other teams members from Dresden and Leipzig. You develop your own research profile, publish and present your findings are international venues, and network with the international research community.
'''Opportunities:''' SECAI offers a first-class environment for advancing your career. You can work with internationally renowned researchers and benefit from the school’s strong networks in industry and research. The graduation of highly qualified researchers is a central project goal in SECAI and doctoral students receive strong support for their professional and personal development.
Requirements: very good research-oriented university degree in a discipline that is relevant to SECAI’s research fields (e.g., computer science, mathematics, electronics, medical devices, bioinformatics, or law); fluency in English. Creativity, taking pleasure in research, and a sense for research quality and ethical behavior in research are an advantage. Please specify for which of the topics found at https://secai.org/topics/ you would like to apply.
On the 11th and 12th February, the 11th EMCL student workshop took place in Vienna (see http://www.logic.at/emcl2016/).
Students in the European Master's Program in Computational Logic of the universities in Bozen, Dresden, Vienna, and Lisbon organized the workshop.
The program contains presentations by the students suggested for master theses, presentations by alumni about their continued education in PhD programs or in industry, and research talks by the partner universities.
Students from more than 21 nations participated.
During the workshop, the Best Master Thesis Award 2015 was given to Adrian Rebola Pardo for his thesis about the generation of proofs in SAT solvers.
The social program included a city tour to St. Stephen's Cathedral, ice skating and a dinner at 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. +
On the 20th and 21th February, the 12th EMCL student workshop takes place in Dresden (see http://www.pk.workshop.computational-logic.org/).
Students in the European Master's Program in Computational Logic of the universities in Bozen, Dresden, Vienna, and Lisbon organize the workshop.
The program contains presentations by the students suggested for master theses, presentations by alumni about their continued education in PhD programs or in industry, and research talks by the partner universities. During the workshop, the Best Master Thesis Award 2017 will be given. +
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
In September 2015, the 38th German Conference on AI, [http://www.tu-dresden.de/inf/ki2015 KI 2015], will take place in Dresden. The conference is co-organized by many members of the ICCL. +
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] will host the [https://scads.ai/education/summer-schools/scads-ai-summer-school-2022/ 8th International Summer School on AI and Big Data] from from 11.07 to 15.07.2022.
<br><br>
[https://scads.ai/ ScaDS.AI] (Center for Scalable Data Analytics and Artificial Intelligence) Dresden/Leipzig is a center for Data Science, Artificial Intelligence and Big Data with locations in Dresden and Leipzig. It is one of five new AI centers in Germany funded under the federal government’s AI strategy and is to be established as a permanent research facility.
<br><br>
The topics for this year are related but not limited to Data Integration and AI, NLP and AI, Privacy and trushworthy AI, AI in Medicine/ Life Science and AI in Earth and Environmental Sciences
<br><br>
The summer school aims at graduate students, Ph.D. students, researchers as well as practitioners starting or being active in the areas of Machine Learning, Artificial Intelligence and/or Big Data. +
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. +
