Large language models (LLMs) such as ChatGPT that have an amazing facility with language have recently appeared. These LLMs have tremendous commercial potential, and companies are racing to get ahead in this area. However, there are obvious deficiencies in such programs, and these deficiencies have been widely reported. One such deficiency of ChatGPT is that it sometimes fabricates facts that are plausible but not true. This makes one question whether ChatGPT and other such large language models have any concept of truth and falsehood. Because of this, adding better reasoning facilities to large language models is an active area of research. Our community can help in this area. However, a real solution to this problem seems a long way off. Despite the problems, people still find ChatGPT to be helpful in summarizing large quantities of text and creating text.
Progress in other areas of AI
Other areas of AI are also seeing spectacular success. I remember playing Greenblatt’s chess program in the old days and winning, despite not being very good at chess. However, chess programs have become so powerful that they can now defeat any human being. The program AlphaZero learned to play chess purely from the rules of the game by playing itself millions of times without any input of knowledge from humans. It beat the previous computer chess champion Stockfish in a couple of matches in 2017 and 2018. It frequently permits itself to have a material disadvantage in order to gain a positional advantage. Its style of chess playing has amazed human experts in the field. Go programs have also reached a level above the best human Go players.
Reasons for progress in some areas of AI
What explains the amazing progress in some areas of AI? Deep learning is behind much of it. It reminds me of my first reaction to seeing neural networks with only two or three layers. “Why aren’t there more layers?” I remember John McCarthy in the old days commenting on what artificial intelligence needed to make real progress: “Ten good ideas.” Deep learning is one of these. Neural networks operate essentially by gradient descent, which is able to find local minima. Apparently this is enough in many areas. Transformers are apparently another good idea that have contributed to the success of LLMs. They are a way to organize neural networks to process sequential data that permits a large degree of concurrency.
Areas that are not making such progress
However, not all areas of artificial intelligence are making such spectacular progress. It is strange that AI programs can be so good in chess, Go, and language processing and yet we still don’t have self-driving cars. For people, learning to drive is a lot easier than learning Go and chess at an expert level. Also, AI programs are not good at common sense reasoning. Perhaps the automated deduction community can contribute to areas of AI such as common sense reasoning where AI seems to be having problems.
History of AI
In 1957 Newell Shaw and Simon developed the General Problem Solver program that was intended to be able to reason and achieve goals in many different areas. However, its performance was poor. There was also early enthusiasm for resolution theorem proving as a general reasoning method. Progress with such approaches was difficult, and attention then shifted to expert systems that achieved human level performance in a narrow area. I remember that in the early days Stanford emphasized logical approaches to AI and MIT emphasized procedural approaches. At the moment with deep learning the procedural side is making spectacular progress, though the logical approach is also making great strides as we all know. Some combination of the two seems to be necessary for a general AI system.
Problems with deep learning and AI in general
There are some general problems with neural networks, however. We don’t really understand what they are doing, and it is hard to have confidence in them especially in areas that are safety critical. Sometimes neural networks can be brittle and be confused by small changes in their input. There is a need for verifiable AI to increase our confidence in AI systems. Developing verifiable AI is an active area of research that our community can contribute to. Of course, we often don’t understand people either, but we manage to get along with one another most of the time.
Dangers of AI
There are also dangers of AI programs becoming so intelligent that they become smarter than we are, we lose control of the programs, and they begin to act in ways that are harmful. More than 1000 researchers and others including Elon Musk and Geoffrey Hinton have called for a pause in the development of AI systems (especially LLMs) until we can better decide how to handle the situation. This is similar to early warnings about the dangers of atomic weapons. There is also a concern about large language models taking away many jobs from humans. The development of AI also has obvious implications for the military. In fact, Vladimir Putin famously stated that the nation that gets ahead in AI “will be the ruler of the world.”
Automated deduction
Our own field of automated deduction may not be making progress as spectacular as AI, but it is making good progress, perhaps not sufficiently appreciated in the computer science community as a whole. Automated deduction is impacting many practical and theoretical areas of computer science and mathematics. In fact, our field is hot enough that funding should become easier, especially in applied areas. Considering the situation with AI, perhaps we should ask if we need to be concerned about the social effects of the field of mechanical theorem proving. And there are other connections between AI and theorem proving besides those that have been mentioned. Deep learning is already being used to increase the effectiveness of automated theorem provers. In addition, it would be good to use natural language interfaces to improve the input and explain the output of theorem provers. Another research area is developing neural networks that are adapted to mathematical notation. Also, perhaps using theorem provers, we can revive the idea of a general problem solver in some form. However, one thing that is certain is that there will be surprises in future advances in AI and automated deduction as there have been in these and other areas in the past.
This article is a précis of a paper with the same title, presented at the 14th International Workshop on the Implementation of Logics, held at the 24th International Conference on Logic for Programming Artificial Intelligence and Reasoning (LPAR-24).
Given all the excitement around ChatGPT, Bard, Bing, etc., we decided to test Bard’s logical reasoning powers. Bard was given the English description of the TPTP problem PUZ001+1 - “Who Killed Aunt Agatha?”, modified to really ask that question. Here’s what was given as the prompt ...
... and here’s what Bard replied ...
From point 4, we know Agatha hates Charles. Since Charles hates no one that Aunt Agatha
hates (point 3), Charles does not hate Aunt Agatha. Thus, Charles cannot be the killer since a
killer hates his victim. From points 5 and 6, we know the butler hates everyone not richer than
Aunt Agatha and everyone that Aunt Agatha hates. Since Agatha hates everyone except the
butler (point 4), the butler hates Charles. According to point 7, no one hates everyone, so the
butler doesn’t hate Agatha. The only person left is Aunt Agatha. Since we know that Charles
and the butler cannot be the killers, and Agatha is not Charles and Charles is not the butler, it
implies that Agatha must have killed herself.
So, the answer was right, but it’s not hard to see that the reasoning is wrong. Bard’s reasoning was encoded in the TPTP format for derivations, and displayed using the IDV derivation viewing tool. That didn’t make the reasoning mistakes obvious, so the GDV derivation verification tool was used to isolate the unsound inferences...
{ ! [X] : ( hates(agatha,X) => ~ hates(charles,X) ), hates(agatha,charles) } |= ~ hates(charles,agatha)
... and...
{ ! [X] : ? [Y] : ~ hates(X,Y), hates(butler,charles) } |= ~ hates(butler,agatha)
The conclusions Charles does not hate Aunt Agatha and the butler doesn’t hate Agatha are wrong.
Bard was given a chance to redeem itself, by giving the prompt What is the logical mistake in your reasoning?, which produced a fallacious excuse. As a test for any reasoning capability in Bard, the problem was obfuscated by a consistent replacement of words, e.g., “Splot, Split, and Splat move diagonally in the plain, and are the only things that move in such a way.” replaced “Agatha, the butler, and Charles live in Dreadbury Mansion, and are the only people who live therein.”. Unsurprisingly, Bard got it wrong, by concluding that Split bamboozled Splot (the butler killed Agatha).
There are well understood reasons why generative AI should not be expected to give sound answers to reasoning tasks like the one described and analysed in this paper. Other people might not know that danger, and might trust such AI tools to give sound answers. There’s an opportunity here for Automated Reasoning... in the last decade many researchers have been developing ways to use machine learning to guide the actions (axiom selection, given clause selection, lemma retention, etc.) of Automated Theorem Provers. The toy experiment described above exemplifies what some people in the community have been saying for quite a while... (i) symbolic reasoning systems should be usefully integrated in complex reasoning systems; (ii) symbolic reasoning systems should be used to verify and point out errors in results produced by subsymbolic systems. Or as a 10 year old might cry out...
The affairs of CADE are managed by its Board of Trustees. This includes the selection of CADE (IJCAR) co-chairs, the selection of CADE venues, choosing the Herbrand, Bill McCune, and Skolem Award selection committee, instituting new awards, etc.
Nominations for three CADE trustee positions are being sought, in preparation for the elections to be held after CADE-29.
The current members of the board of trustees are (in alphabetical order):
The terms of Marijn Heule, Andrew Reynolds, and Renate Schmidt end. Renate Schmidt may be nominated for a second term, whereas Marijn Heule and Andrew Reynolds have already served two consecutive terms and cannot be nominated this year.
The term of office of Brigitte Pientka as CADE-29 programme chair ends after the CADE conference. As outgoing ex-officio trustee, Brigitte Pientka is eligible to be nominated as elected trustee.
In summary, we are seeking to elect three trustees.
Nominations can be made by any CADE member, either by e-mail or at the CADE business meeting at CADE-29; since nominators must be CADE members, they must have participated at at least one of the CADE or IJCAR conferences in the years 2020-2023. Two members, a principal nominator and a second, are required to make a nomination, and it is their responsibility to ask people's permission before nominating them. A member may nominate or second only one candidate. For further details please see the CADE Inc. bylaws at the CADE web site.
E-mail nominations can be provided up to the upcoming CADE business meeting, via email to
Jürgen Giesl, President of CADE Inc.with copies to
Philipp Rümmer, Secretary of CADE Inc.
We invite proposals for sites around the world to host the International Conference on Automated Deduction (CADE) to be held in summer 2025. CADE typically merges into IJCAR (the International Joint Conference on Automated Reasoning) in even years, and meets as an independent conference in odd years. For odd years, both proposals to host CADE alone or CADE co-located with other conferences are welcome.
The deadline for proposals is 31 August 2023.
CADE's/IJCAR's recent location history is as follows:
The upcoming CADE/IJCAR events will be:
We encourage proposers to register their intention informally as soon as possible. We will try to do the final selection of the site within two months after the proposal deadline.
Proposals should address the following points that also represent criteria for evaluation:
Prospective organizers are encouraged to get in touch with the CADE Secretary and the CADE President for informal discussion, and to study the CADE management notes. If the host institution is not actually located at the proposed site, then one or more visits to the site by the proposers are encouraged.
The International Conference on Automated Deduction (CADE) Herbrand Award for Distinguished Contributions to Automated Reasoning is presented to
in recognition of his many foundational contributions to logic and automated reasoning, in particular automata-based verification methods, constraint solving, and knowledge representation.
Presented at CADE-29, the 29th International Conference on Automated Deduction.
The Herbrand Award Committee 2023 consisted of Aart Middeldorp (Chair), Tobias Nipkow, Andre Platzer, Viorica Sofronie-Stokkermans.
The International Conference on Automated Deduction (CADE) Bill McCune PhD Award in Automated Reasoning is presented to
for his dissertation “SMT-based Safety Verification of Data-Aware Processes: Foundations and Applications”” supervised by Prof. Marco Montali and Prof. Silvio Ghilardi. The thesis was selected for its contributions to the field of Automated Reasoning, with the development of a general framework for automating safety verification of both processes and data. The thesis introduces new foundations for the integration and extension of infinite-state model checkers which are needed for the successful and scalable verification of data-aware processes. Beyond the limits of the intended application, it brings novel theoretical results on model completion and uniform interpolation for SMT theories and their combinations, which are of general interest. The theoretical results are accompanied by the introduction of automated reasoners which show the effectiveness of these developments in practice.
Presented at CADE-29, the 29th International Conference on Automated Deduction.
The McCune award committee 2023 consisted of Cláudia Nalon (chair), Pascal Fontaine, Carsten Fuhs, Marijn Heule, Laura Kovács, Andrew Reynolds, Philipp Rümmer, Martina Seidl, Viorica Sofronie-Stokkermans.
CADE-6: International Conference on Automated Deduction (CADE) Skolem Award for a CADE paper that has Passed the Test of Time, by being a Most Influential Paper in the field. Presented to
CADE-12: International Conference on Automated Deduction (CADE) Skolem Award for a CADE paper that has Passed the Test of Time, by being a Most Influential Paper in the field. Presented to
CADE-18: International Conference on Automated Deduction (CADE) Skolem Award for a CADE paper that has Passed the Test of Time, by being a Most Influential Paper in the field. Presented to
CADE-24: International Conference on Automated Deduction (CADE) Skolem Award for a CADE paper that has Passed the Test of Time, by being a Most Influential Paper in the field. Presented to
These awards will be presented at CADE-29, the 29th International Conference on Automated Deduction.
The Skolem Award Committee consisted of Franz Baader (chair), Clare Dixon, Pascal Fontaine, Martin Giese, Konstantin Korovin, Tobias Nipkow, and Sarah M. Winkler.
Nominations are invited for the 2023 Ackermann Award. PhD dissertations in topics specified by the CSL and LICS conferences, which were formally accepted as PhD theses at a university or equivalent institution between 1 January 2022 and 31 December 2022 are eligible for nomination for the award.
The deadline for submission is 1 July 2023.
Nominations should be submitted by the candidate or the supervisor via Easychair.
Please submit a pdf file containing:
The Award The 2023 Ackermann award will be presented to the recipient(s) at CSL 2024, the annual conference of the EACSL.
The award consists of a certificate, an invitation to present the thesis at the CSL conference, the publication of the laudatio in the CSL proceedings, an invitation to publish the thesis in the FoLLI subseries of Springer LNCS, and financial support to attend the conference.
Ackermann Jury
The jury consists of:
For more information please contact Maribel Fernandez.
CADE is the major international forum for presenting research on all aspects of automated deduction.
FSCD covers all aspects of formal structures for computation and deduction from theoretical foundations to applications. Building on two communities, RTA (Rewriting Techniques and Applications) and TLCA (Typed Lambda Calculi and Applications), FSCD embraces their core topics and broadens their scope to closely related areas in logic, models of computation, semantics and verification in new challenging areas.
The following workshops and competitions are affiliated with FSCD and CADE in 2023:
The Women in Logic workshop (WiL) provides an opportunity to increase awareness of the valuable contributions made by women in the area of logic in computer science. Its main purpose is to promote the excellent research done by women, with the ultimate goal of increasing their visibility and representation in the community. Our aim is to:
The aim of WPTE is to bring together the researchers working on program transformations, evaluation, and operationally based programming language semantics, using rewriting methods, in order to share the techniques and recent developments and to exchange ideas to encourage further activation of research in this area.
The workshop aims at bringing together researchers who are currently developing theory and applications of linear logic as a technical tool or a methodological guideline, to foster their interaction and provide a forum for presenting new ideas and work in progress, and enable newcomers to learn about current activities in this area. Linear Logic is a key feature in both theoretical and practical approaches to computer science, and the goal of this workshop is to present work exploring the theory of Linear Logic so as its applications.
Logical and semantic frameworks are formal languages used to represent logics, languages and systems. These frameworks provide foundations for the formal specification of systems and programming languages, supporting tool development and reasoning.
The aim of this series is bringing together theoreticians and practitioners to promote new techniques and results, from the theoretical side, and feedback on the implementation and use of such techniques and results, from the practical side. LSFA includes areas such as proof and type theory, equational deduction and rewriting systems, automated reasoning and concurrency theory.
The aim of this workshop is to bring together researchers who are currently developing new computation models or new features for traditional computation models, in order to foster their interaction, to provide a forum for presenting new ideas and work in progress, and to enable newcomers to learn about current activities in this area.
Logical frameworks and meta-languages form a common substrate for representing, implementing and reasoning about a wide variety of deductive systems of interest in logic and computer science. Their design, implementation and their use in reasoning tasks, ranging from the correctness of software to the properties of formal systems, have been the focus of considerable research over the last two decades. This workshop will bring together designers, implementors and practitioners to discuss various aspects impinging on the structure and utility of logical frameworks, including the treatment of variable binding, inductive and co-inductive reasoning techniques and the expressiveness and lucidity of the reasoning process.
Unification is concerned with the problem of identifying terms, finding solutions for equations, or making formulas equivalent. It is a fundamental process used in a number of fields of computer science, including automated reasoning, term rewriting, logic programming, natural language processing, program analysis, types, etc.
In order to stimulate ATP research and system development, and to expose ATP systems within and beyond the ATP community, the CADE ATP System Competition (CASC) is held at each CADE and IJCAR conference.
CASC evaluates the performance of sound, fully automatic, ATP systems. The evaluation is in terms of:
HOR is a forum to present work concerning all aspects of higher-order rewriting. The aim is to provide an informal and friendly setting to discuss recent work and work in progress.
IFIP Working Group 1.6 is one of the working groups of the Technical Committee 1 of the International Federation for Information Processing (IFIP). IFIP is the leading multinational, apolitical organization in Information & Communications Technologies and Sciences.
The purpose of this workshop is to bring together researchers who work in machine learning and automated deduction. The targets of the workshop will be: to apply automated deduction methods to machine learning, to produce objects recognizable by automated deduction tools by machine learning methods, to enhance explainable artificial intelligence coupled with machine learning by automated deduction tools, and to consider further developments in the intersection of both research areas.
Computer Theorem Proving is becoming a paradigm as well as a technological base for a new generation of educational software in science, technology, engineering and mathematics. The workshop brings together experts in automated deduction with experts in education in order to further clarify the shape of the new software generation and to discuss existing systems.
The workshop addresses recent trends in implementing first-order theorem provers, and focus on new challenges and application areas. The workshop also discusses the development and use of the first-order theorem prover Vampire, and its potential use cases and interaction with other systems.
Determining the satisfiability of first-order formulas modulo background theories, known as the Satisfiability Modulo Theories (SMT) problem, has proved to be an enabling technology for verification, synthesis, test generation, compiler optimization, scheduling, and other areas. The success of SMT techniques depends on the development of both domain-specific decision procedures for each background theory (e.g., linear arithmetic, the theory of arrays, or the theory of bit-vectors) and combination methods that allow one to obtain more versatile SMT tools. These ingredients together make SMT techniques well-suited for use in larger automated reasoning and verification efforts. The aim of the workshop is to bring together researchers and users of SMT tools and techniques.
Dates
The LICS Symposium is an annual international forum on theoretical and practical topics in computer science that relate to logic, broadly construed.
Workshops:
More information is available on the symposium's web page.
The ITP conference series is concerned with all aspects of interactive theorem proving, ranging from theoretical foundations to implementation aspects and applications in program verification, security, and the formalization of mathematics.
Affiliated workshops:
More information is available on the conference's web page.
Modern society is increasingly dependent on software systems that are becoming larger and more complex. This poses new challenges to the various aspects of software engineering, for instance, software dependability in trusted computing, interaction with physical components in cyber physical systems, quality assurance in AI systems, distribution in cloud computing applications, security and privacy in general. Hence, new concepts and methodologies are required to enhance the development of software engineering from theoretical aspects.
TASE 2023 aims to provide a forum for people from academia and industry to communicate their latest results on innovative advances in software engineering.
The conference is now accepting registration!
More information is available on the symposium's web page.
Since the first conference held in Marseille in 1982, ICLP has been the premier international event for presenting research in logic programming. Contributions include all areas of logic programming, such as:
Program
Registration is open.
More information is available on the conference's web page.
CiE 2023 is the 19th conference organized by CiE (Computability in Europe), a European association of mathematicians, logicians, computer scientists, philosophers, physicists and others interested in new developments in computability and their underlying significance for the real world.
Format
The conference will have a hybrid format.
At the same time, we strongly encourage in-person participation for a richer
experience: There are direct flights to Batumi from Istanbul and Tel Aviv, among
other airports. Hotels can be booked directly on the
conference website at a reduced rate.
Batumi is located on the Black Sea coast close to the Turkish border.
We suggest to book hotels as soon as possible, since Batumi is a
well-appreciated touristic location, especially in July.
Numerous travel advisory websites currently rank travel to Georgia as very safe.
More information is available on the conference's web page.
Symbolic computation (SC) aims at providing algorithmic solutions to problems dealing with symbolic objects such as terms, formulas, programs, representations of algebraic objects, etc. Algorithms and methods developed for the major subfields of SC (computer algebra, computational logic, automatic programming) have found successful applications in various areas.
From the beginning, SC was also considered a major approach to "artificial intelligence", since the problems solved by SC, typically, are problems that were considered hard for "human intelligence" (like symbolic integration, theorem proving, SAT/SMT solving, program verification, hardware verification, etc.).
Meanwhile, recent advances in artificial intelligence methods have provided new exciting opportunities in science and industry, being more and more integrated into most aspects of life. Machine learning (ML) methods, developed in parallel to symbolic methods for solving hard "artificial intelligence" problems, achieved spectacular results in numerous applications in recent years.
This special issue is dedicated to the interaction of symbolic computation and machine learning methods seen as the two major approaches to "artificial intelligence". We expect dramatic advances from a much closer interaction of the SC and the ML approaches to artificial intelligence. This interplay is, in fact, essential in the current scenario where the economy and society demand the development of complex, data-intensive, trustable, and high-performant computational systems that accompany humans in more and more facets of their daily life.
The special issue is organized as a follow-up of the 24th International Symposium on Symbolic and Numeric Algorithms for Scientific Computing, SYNASC 2022. Participants of the symposium, as well as other authors, are invited to submit contributions. We welcome submissions describing the interaction of SC and ML methods, techniques, and tools, and their applications in AI.
Submission deadline: August 14, 2023
About Protests in Peru
We are continuously monitoring the political situation in the host country Peru,
which faced violent protests in 2022 also affecting travelers. To the best of our
knowledge, this situation has calmed down. If protests erupt again, we will work
closely with the ICTAC Steering Committee to choose the best feasible solution.
Scope
The ICTAC conference series aims at bringing together researchers
and practitioners from academia, industry, and government to present
research and exchange ideas and experiences within theoretical aspects
of computing through methods and tools for system development.
ICTAC also aims to promote research cooperation between developing
and industrial countries.
Topics
The conference concerns all aspects of theoretical computer science,
including, but not limited to:
Important Dates
More information is available on the conference's web page.
Principles of Programming Languages (POPL) is a forum for the discussion of all aspects of programming languages and programming systems. Both theoretical and experimental papers are welcome. We seek submissions that make principled, enduring contributions to the theory, design, understanding, implementation, or application of programming languages.
Important Dates
All the times/deadlines below are Anywhere on Earth (AoE) in 2023.
More information is available on the conference's web page.
FSTTCS 2023 is a forum for presenting original results in foundational aspects of Computer Science and Software Technology.
Topics
Track A
Important Dates (all dates are AoE)
More information is available on the conference's web page.
Computer Science Logic (CSL) is the annual conference of the European Association for Computer Science Logic (EACSL). It is an interdisciplinary conference, spanning across both basic and application oriented research in mathematical logic and computer science.
List of topics:
The following list is not exhaustive but indicates the scope of interest for CSL'23:
Important dates:
More information is available on the conference's web page.
SBMF 2023 is the twenty-sixth of a series of events devoted to the development, dissemination, and use of formal methods for the construction of high-quality computational systems. It is now a well-established event with an international reputation. It regularly receives submissions and participants from all over the world.
Scope and Topics
The aim of SBMF is to provide a venue for the presentation and
discussion of high-quality work in formal methods. The topics include,
but are not limited to, the following:
Important Dates
More information is available on the symposium's web page.
The International Conference on Knowledge Capture, K-CAP, aims at bringing together an interdisciplinary group of researchers on a diverse set of topics with an interest in the development of knowledge capture. This involves the design and development of formalisms, methods, and tools that enable efficient and precise extraction and organization of knowledge from different sources and for different modalities of use including, for example, automated reasoning, machine learning, and human-machine teaming.
Topics of interest
Areas of interest for submissions to K-CAP 23 include, but are not limited to, the following topics:
Important Dates:
More information is available on the conference's web page.
The Second Workshop on the Implementation of Type Systems (WITS 2023) will be held on August 28, 2023, in Braga, Portugal, co-located with IFL 2023. The goal of this workshop is to bring together the implementors of a variety of languages with advanced type systems. The main focus is on the practical issues that come up in the implementation of these systems, rather than the theoretical frameworks that underlie them. In particular, we want to encourage exchanging ideas between the communities around specific systems that would otherwise be accessible to only a very select group. The workshop will have a mix of invited and contributed talks, organized discussion times, and informal collaboration time. We invite participants to share their experiences, study differences among the implementations, and generalize lessons from those. We also want to promote the creation of a shared vocabulary and set of best practices for implementing type systems.
Here are a few examples of topics we are interested to discuss:
Important Dates
More information is available on the workshop's web page.
Concurrency and Logics are two of the most active research areas in the theoretical computer science domain. The literature in these fields is extensive and provides a plethora of logics and models for reasoning about intelligent and distributed systems. More recently, the interplay of concurrency and logic with areas such as:
The workshop aims to bring together researchers working on different aspects of logic and concurrency in AI, multi-agent systems, and computer science, both from a theoretical and a practical point of view. Besides, it aims to promote research on Foundation of AI in other research communities that are traditionally Theoretical Computer Science-oriented.
The topics covered by the workshop include, but are not limited to, the following:
Important Dates
More information is available on the workshop's web page.
The EXPRESS/SOS workshop series aims at bringing together researchers interested in the formal semantics of systems and programming concepts, and in the expressiveness of computational models.
Topics of interest for EXPRESS/SOS 2023 include, but are not limited to:
Important Dates
More information is available on the workshop's web page.
The annual meeting Deduktionstreffen is the prime activity of the Interest Group for Deduction Systems (FGDedSys) of the AI Chapter (FB KI) of the German Society of Informatics (Gesellschaft für Informatik). It is a meeting with a familiar, friendly atmosphere, where everyone (not only the German community) interested in deduction can report on their work in an informal setting.
A special focus of the Deduktionstreffen is on young researchers and students, who are particularly encouraged to present their ongoing research projects to a wider audience. Another goal of the meeting is to stimulate networking effects and to foster collaborative research projects.
Topics include, but are not limited to:
Important dates
More information is available on the workshop's web page.
Doctoral Concortium Format
There will be a PhD workshop with keynote and oral presentations during the KI conference, providing an opportunity for obtaining feedback on PhD projects. Doctoral students may also participate in a mentoring program that will connect students with experienced researchers in their field. The organizers will try to schedule personal meetings between mentors and students. Students can indicate their interest in this program when submitting their contribution, or directly by contacting the organizers. The schedule of the meetings will be announced ahead of the event. The organizers plan to publish extended abstracts as proceedings of the PhD workshop, probably with the GI-DL (GI Digital Library).
Additionally, there will be the opportunity to participate in the main conference poster session where the participants will have the chance to present their research to a larger audience.
Important Dates
More information is available on the consortium's web page.
Ontology matching is a key interoperability enabler for the Semantic Web, as well as a useful technique in some classical data integration tasks dealing with the semantic heterogeneity problem. It takes ontologies as input and determines as output an alignment, that is, a set of correspondences between the semantically related entities of those ontologies. These correspondences can be used for various tasks, such as ontology merging, data interlinking, query answering or navigation over knowledge graphs. Thus, matching ontologies enables the knowledge and data expressed with the matched ontologies to interoperate.
The workshop has three goals:
Topics of interest include but are not limited to:
Dates for Technical Papers and Posters:
More information is available on the workshop's web page.
CCC is a workshop series that brings together researchers applying logical methods to the development of algorithms, with a particular focus on computation with infinite data, where issues of continuity, computability and constructivity play major roles. Specific topics include exact real number computation, computable analysis, effective descriptive set theory, constructive analysis, and related areas. The overall aim is to apply logical methods in these disciplines to provide a sound foundation for obtaining exact and provably correct algorithms for computations with real numbers and other continuous data, which are of increasing importance in safety critical applications and scientific computation.
Topics
constructive mathematics, constructive analysis, computable analysis, exact real number computation
Contributions
The workshop invites all contributions relating to computation where issues of
continuity, computability and constructivity play major roles. Specific areas
of interest include:
Participation is open both in presence and online.
Deadline for Submissions July 31, 2023
More information is available on the workshop's web page.
The 15th edition of the Summer School on Verification Technology, Systems and Applications (VTSA) will be organized by Inria Nancy - Grand Est in cooperation with Max-Planck-Institute for Informatics Saarbruecken, the University of Liege, and the University of Luxembourg. The school will take place from August 28 to September 1, 2023 at Inria Nancy - Grand Est / LORIA, France.
The following speakers have accepted to give courses at VTSA 2022:
Participation is free (except for travel and accommodation costs) and open to anybody holding at least a bachelor degree or equivalent in computer science. It includes the lectures, daily coffee breaks and lunches as well as a school dinner. Attendance is limited to 40 participants. Please apply electronically by sending to Jennifer Müller:
The deadline for application is July 9, 2023. Notification of acceptance will be given by July 12, 2023.
Full details are available here
The purpose of the Reasoning Web Summer School is to disseminate recent advances on reasoning techniques and related issues that are of particular interest to Semantic Web and Linked Data applications. It is primarily intended for postgraduate (PhD or MSc) students, postdocs, young researchers, and senior researchers wishing to deepen their knowledge. In 2023, the broad theme of the school is: “Declarative Artificial Intelligence: Knowledge, Rules, Logic”
As in the previous years, lectures in the summer school will be given by a distinguished group of expert lecturers.
Confirmed Lectures
Applications
The number of attendees will be limited and participation will depend on submitting an application which will undergo a reviewing process. Accepted participants will receive a registration link, meanwhile please see the registration page for fee and other relevant information.
Applications must be submitted by filling the form.
Important Dates
More information is available on the school's web page.
Synthesis is a fundamental problem in computer science and mathematics, concerned with automatically generating programs that satisfy a given logical specification. Its applications span a range of domains, including model-based system design, software engineering, and automated theorem proving. For instance, designing a controller that guides the behavior of a reactive system, that is, a system that continually interacts with its environment, can be framed as a synthesis problem. Similarly, the design and verification of a distributed system often depend on distributed synthesis, which finds programs that enforce correct component interaction and satisfy desired specifications.
The third edition of the Summer School on Formal Methods for Cyber-Physical Systems offers an in-depth exploration of reactive synthesis, a topic that was already introduced in the first edition of the school. The lecturers will provide a systematic account of the main achievements and the current trends of research in reactive synthesis, covering both theory and applications.
The course will begin with an overview of the classical synthesis problem in the finite-state setting, as originally formulated by Church and solved by Buechi and Landweber. This introductory part will introduce the terminology of infinite two-player games, explain the automatic construction of winning strategies in “regular games”, and address history of the subject, discussing extensions and open problems. From there, the course will investigate approaches for making reactive synthesis more efficient and practical, including techniques for solving the synthesis problem in restricted settings, for decomposing the problem into subproblems, and for employing algorithms, data structures, and heuristics to manage complexity. Variants of the synthesis problem will also be explored, such as control strategies for hybrid and distributed systems, monitor synthesis, synthesis under incomplete information, distributed synthesis, and symmetric synthesis. The implementation of synthesis tools will also receive significant attention, with a focus on recent advances and applications of UPPAAL Stratego and the SYNTCOMP reactive synthesis competition.
The summer school will conclude with a workshop on emerging research trends in synthesis, monitoring, and learning, which showcases some exciting interactions between formal methods and machine learning. Distinguished invited speakers will lead the workshop. Participants will also have the opportunity to engage with peers from around the world and may propose to deliver short research talks voluntarily.
Deadline for online application is August 18, 2023.
More information is available on the school's web page.
The Computer Science Department of the University of Verona invites ex- pressions of interest for open-rank tenured positions (either Associate Professor (PA) or Professor (PO)) in computer science (Settore Scientifico Disciplinare - SSD: INF/01) .
We are looking for candidates with an excellent publication record, an inter- nationally visible research profile, a clear potential to promote and lead research activities, and an interest in teaching students at all levels (BS, MS, PhD). We aim at recruiting a researcher with a strong background in one of the following areas: Artificial Intelligence, Theory, Software Engineering and Security (see here for a description of the themes).
Verona is a charmingly beautiful, well-connected city of Roman origin, with an exceptonally high quality of life, and a strategic position between central Europe and the Mediterranean.
Applications (and questions regarding the application process) should be sent by email, by June 30, 2023 (the sooner the better), and must contain:
Based on the received expressions of interest, the Department will decide whether to open an official call and which selection procedure to follow, in- cluding direct recruitment procedures (e.g., Law 240, art. 7, comma 5bis). All expressions of interest will be given proper consideration. The Department of Computer Science of the University of Verona adheres to EU and Italian laws against discrimination based on sex, gender, age, ethnicity, sexual orientation, marital status, disability, or religion, and it appreciates and welcomes diversity and inclusion in all forms.
The group of André Platzer, the Alexander von Humboldt Professor for Logic of Autonomous Dynamical Systems, in the Computer Science Department at KIT, Karlsruhe, is recruiting a PhD Student / Doctoral Researcher (full-time, about €4200-€4800 gross by TVL E13 depending on experience). Exceptionally qualified applicants for postdoc positions may be considered as well.
Our research group develops the logical foundations for cyber-physical systems and practical theorem proving tools such as KeYmaera X for analyzing and correctly building such systems. Our techniques are used to analyze the safety of autonomous cars, airplanes and collision avoidance protocols in aerospace applications, robotics, and train control as well as for provably safe AI. Your exciting mathematical research can have a direct impact on making the world a better place.
More details here.
The BINSEC team opens postdoc, PhD student and research intern positions in software security and program analysis.
Our Team - The BINary-level SECurity research group (BINSEC) is a dynamic team of a dozen of researchers, which offers a stimulating and open-minded work environment in English. The group has frequent publications in top-tier security, formal methods and software engineering conferences. It is part of CEA (one of the main French research organisations, employing more than 20k researchers and persistently ranked as a top global innovator) and of Université Paris-Saclay (the world’s 16th and European Union’s 1st university, according to the Shanghai ARWU Ranking in 2022).
Our Work - The team has strong expertise in several code analysis approaches, namely symbolic execution, abstract interpretation and fuzzing. We apply these techniques to improve software security, covering notably vulnerability detection and analysis, code (de)obfuscation and formal verification. See our website for additional information.
APPLICATION - Candidates should send a CV by email as soon as possible. Applications will be reviewed as they arrive (first come, first served), depending on our availability, and additional information may be requested from you. Please read the detailed job offer to prepare your application in the best way.
We are offering a 2-year engineering position in formal methods inside the LiberAbaci project, that aims at improving the access of the Coq proof assistant for mathematics students at the beginning of university. The engineer will work on the coq-num-analysis library in order to improve its software development and its practicality, especially for first-years university students to use part of it.
More information here in French (translation upon request).
Interested people should send a CV before July 30th to Sylvie Boldo, François Clément and Miceala Mayero. Applications will be examined over time.
Deducteam is offering a 3-year engineering position to help develop, test and maintain tools for proof system interoperability (continuous integration, proof libraries management, searching tools, VSCode interface, etc.). Net taxable monthly salary between 2148 and 4412 euros depending on experience.
Interested people should send their CV to Frédéric Blanqui before 30 July 2023. Applications will be examined over time.
A Post-Doctoral position is available as part of the funded ANR project CoMeMoV between the LIFO (University of Orleans, France), CEA List and Thales Research and Technology.
Frama-C is an extensible and collaborative open-source platform dedicated to source-code analysis of C software. If offers a specification language and various analyzers in the form of separate plugins. The WP plugin of Frama-C can be used to prove that a given C program respects its specification. WP provides a combination of different memory models that collaborate together thanks to a smart but simple partitioning of the memory. On moderately complex, industrial-strength programs, this combination already makes WP mature enough to be deployed for proving critical industrial embedded software. However, several theoretical and practical issues still persist. The goal of CoMeMoV is to tackle these issues to allow deductive verification with WP to better scale on complex industrial programs.
The work of the successful candidate will mainly focus on the formalization and proof of correctness of the proposed collaborative memory models for deductive verification.
Application requirements:
This is a research-only position, for 21 months.
Please send the application materials or any questions to Frederic Loulergue.
The Université de Montpellier is funding an 18-month post-doctoral position at the LIRMM research department, to start in September 2023.
The position is open to candidates who hold (or will soon complete) a PhD in computer science, with a research background in automated reasoning, program verification, programming languages, or algorithms.
For more details about the project and the position see here.
To apply, please send a mail to Simon Robillard with a resume. Application is open until June 23rd.
The faculty of Sciences at Vrije Universiteit Amsterdam is offering a PhD position on explainable AI for stream reasoning. Motivated by applications in AI, the project will involve research in the area of knowledge representation and automated reasoning, more specifically involving description logics and/or rule-based formalisms, applied to temporal data.
The application deadline is 10/07/2023.
More information can be found in the official advertisement.