# Association for Automated Reasoning

February 2020

## From the AAR President, Larry Wos

When I was a grad student in mathematics, the proofs I usually saw in class were what I think of as forward proofs. Such a proof begins with its assumptions, axioms of the field under study, and zero or more additional hypotheses.

In contrast to a forward proof, I cannot recall seeing in any of my graduate courses in mathematics what I term a backward proof. Such a proof begins with the denial of the theorem to be proved and works backward, eventually producing the negation (or denial) of some axiom or additional assumption for the theorem in focus. A so-called bidirectional proof also exists; again, I never saw one in my graduate mathematics courses. Such a proof includes statements some of which follow from axioms and, if present, hypotheses of the theorem in focus, while others follow from the denial or negation of the goal.

At this point I will concentrate on forward proofs, but the observations and challenges that follow apply also to so-called backward proofs and bidirectional proofs.

Implicit steps, demodulation, and automated reasoning
Often, many steps in a mathematical proof -- especially in a paper intended for publication -- are omitted from the proof. The referee has to (in effect) guess at the missing steps, and sometimes the verification by the referee of the proposed proof is indeed difficult. For a trivial example, applying associativity implicitly and repeatedly to obtain a third step from two others in a problem from group theory can present difficulty and can be easily overlooked. Much subtler is the implicit use of some lemma or theorem proved earlier in the intended publication. Such implicit and hidden aspects are often treated as obvious; that is, the parents may be cited, but other aspects are not.

In automated reasoning, the object that corresponds to such an implicit use in mathematics is a demodulator -- an equality that encodes, for example, associativity. In OTTER, such an equality is referenced by its number. And the number of demodulators cited with a single derived equation in the proof can make a huge difference in the reading of the proof. Let me give you an example.

Many years ago, William McCune (the developer of the automated reasoning program OTTER) proved the Robbins conjecture true -- that is, he produced a proof from a program he authored, a program different from OTTER. Among his other successes, some of the proofs he obtained with OTTER offered single lines depending on a large number of demodulators. When I showed that proof to the mathematician Ken Kunen, he commented that the huge set of demodulators, for a single line of the proof was too much to cope with. Indeed, he found the resulting equation difficult to verify because of so many implicit moves that were (in effect) made after the two parents were treated with paramodulation -- moves implicitly made because of many lines of numbers corresponding to demodulators.

Challenges in group theory
With this background, I now offer shortly several relevant challenges, challenges taken from group theory. Since the axioms for a group are vital to the challenges issued here, I give these and the definition of commutator, where the function f denotes product, the constant e denotes identity, the function g denotes inverse, and the function h denotes commutator.

``` f(e,x) = x.                       % left identity
f(x,e) = x.                       % right identity
f(g(x),x) = e.                    % left inverse
f(x,g(x)) = e.                    % right inverse
f(f(x,y),z) = f(x,f(y,z)).        % associativity
h(x,y) = f(x,f(y,f(g(x),g(y)))).  % definition of commutator
```
In particular I focus on a theorem of Levi, in which he asserts the equivalence of the following two properties in group theory, not assuming that either holds for all groups.
``` h(h(x,y),z = h(x,h(y,z)),  commutator is associative, property 1
f(h(x,y),z) = f(z,h(x,y)), commutator has the property of nilpotent class 2, property 3
```
As it turns out, if I have been informed correctly, a third property (the following) is equivalent to each of the two cited properties.
``` f(h(x,z),h(y,z)) = h(f(x,y),z), commutator distributes over product, property 2
```
And now for the challenges.

In the first challenge I ask you to prove the equivalence of all three properties. In other words, find six proofs: prove property 2 from property 1, 3 from 1, 3 from 2, 1 from 2, 2 from 3, and finally 1 from 3.

In the second challenge, I ask you to find a circle of pure proofs for the three. Specifically, I am asking you to find a set of three proofs consisting of a proof that the second property follows from the first in which the third property does not occur; a proof that the third is provable from the second with the first not occurring in the proof; and a proof that the first is provable from the third with the second property excluded from the proof.

When and if you succeed, I offer more difficult challenges. In particular, for each of the six proofs you have found, you are to find (1) a forward proof, (2) a proof free of demodulators, and (3) a forward proof for each that is also free of demodulators. In cases in which the proof you may have found is backward or bidirectional, and in the case in which demodulators are present, I believe you will find that two rather disconnected procedures are required, one for producing a forward proof and one for removing demodulators.

A research challenge
For those of you ready to face a challenge that is more a type of research, I offer the following. Specifically, you are asked to find methods to convert bidirectional or backward proofs to forward and to find a procedure to remove any and all demodulators from proofs that rely on such. Should you wish some insight into the possible difficulty regarding demodulation removal, I include the following lines taken from a 197-step OTTER proof proving that property 1 implies property 3.

``` 934 [back_demod,476,demod,809,383,383,383,797,797,797,797,797,797,418,418,
418,383,383,383,383,383,383,383,383,383,383,809,383,383,383,383,383,383,383,
383,383,383,383,383,383,383]  f(h(x,h(y,z)),f(u,f(z,f(x,f(y,f(g(x),f(g(y),
f(g(z),f(y,f(x,f(g(y),f(g(x),g(u)))))))))))))=h(x,h(y,h(z,u))).
383,382 [] f(f(x,y),z)=f(x,f(y,z)).
797,796 [para_from,434.1.1,392.1.1.2,flip.1] g(f(x,y))=f(g(y),g(x)).
```
As line 934 indicates, the proof relies on 38 demodulators, where 383 corresponds to the associativity of product, in the function f, and 797 is a step occurring earlier in the proof, a step you might view as a lemma if written out for a detailed paper being submitted for publication.

If you find six proofs each of which is a forward proof free of demodulation, I would very much enjoy the opportunity to examine that proof. My e-mail address is wos@mcs.anl.gov.

## Guest Column: on Zohar Manna

Nachum Dershowitz and Richard Waldinger

An extended version, including a list of publications, appears in Formal Aspects of Computing (2019)

Zohar Manna, founding father of the study and application of formal methods for software and hardware verification, died peacefully at his home in Netanya, Israel on August 30, 2018, after a long and marvelously productive career. He is survived by his wife Nitza and their four children and five grandchildren. He was 79.

Over a career spanning nearly half a century, Zohar had profound impact on most aspects of formal methods and automated reasoning. He was a deep thinker who laid the foundations for tools that are now coming into widespread use. He pioneered program verification and program synthesis, two fields that were then at the theoretical edge of computing, but which today help form the foundations of artificial intelligence and help assure the reliability of extraordinarily complex software. His work has inspired several generations of researchers. His manifold research interests included, in particular, the design and verification of concurrent, reactive and hybrid systems. His students and colleagues dedicated their research careers to the hardest problems in automated reasoning, including program semantics, partial correctness, termination, invariant generation, program synthesis, program transformation, planning, proof methodology, temporal reasoning, natural language understanding, non-clausal proof search, and decision procedures. Each of these activities is today a thriving independent field of research.

Zohar received his bachelor’s and master’s degrees in mathematics from the Technion in Haifa in 1961 and 1965, respectively, serving as a scientific programmer in the Israel Defense Forces from 1962 to 1964. Afterwards, he attended Carnegie Mellon University in Pittsburgh (together with one of us, Richard), where he earned his Ph.D. in computer science in the spring of 1968 under the guidance of Robert W Floyd and Alan J. Perlis both Turing Award recipients. Upon graduating CMU, Zohar joined Stanford University as an assistant professor of computer science, where, among other activities, he worked with John McCarthy. Zohar returned to Israel in 1972 to the Department of Applied Mathematics at the Weizmann Institute of Science in Rehovot, first as an associate professor and from 1976 on as full professor (where he supervised the dissertation of the other one of us, Nachum). In 1978, he was recruited back to Stanford as a full professor (taking Nachum along with him), dividing his time between Stanford and Weizmann until 1995, at which point he resigned the latter appointment. He remained at Stanford University until his retirement in 2010.

Zohar’s 1968 dissertation, entitled Termination of Programs, used second-order logic to formalize the problem of termination for abstract programs and demonstrate decidable subclasses of the termination program. Whereas Floyd’s own approach to termination required the invention of inductive assertions and well-founded orderings, Zohar’s approach made stronger demands on the theorem prover, which had to be second order. Richard Lipton calls it “one of the coolest PhD theses ever.” He authored or coauthored 9 books and close to 200 scholarly articles, plus more than 50 technical reports (Weizmann, Stanford, SRI), which served as a rapid mode of dissemination of pre-publication cutting-edge research. All are all models of clarity and comprehensiveness. His magnificent textbook, Mathematical Theory of Computation (1974), was extraordinarily influential; it was translated into Bulgarian, Czech, Hungarian, Italian, Japanese, and Russian. It pioneered the logical analysis of programs for correctness vis-à-specifications and for termination properties. For very many of today’s computer scientists, this book was their introduction to formal methods.

Richard Waldinger was Zohar’s chief collaborator on program synthesis. In 1970, they published a groundbreaking paper, “Toward automatic program synthesis” (CACM ). Eventually they moved to a purely “deductive” approach in which, to construct a program meeting a desired condition for a given input, one proves the existence of an output entity that satisfies that condition. The proof is restricted to be sufficiently constructive so that a program that computes the satisfying output can be extracted. Conditional expressions are introduced via case analysis in the proof; recursion is introduced by application of recursion induction. Perhaps the most practical application of deductive program synthesis came from its use by NASA in the Amphion project, which synthesized programs for analysis of data from interplanetary missions. Zohar and Richard also developed a non-clausal reasoner that better served the need for doing an inductive proof in a resolution-theorem-proving framework. This collaboration culminated in the two-volume book, The Logical Basis for Computer Programming (1985 and 1990).

Zohar played a central rôle in the study of applications of temporal logic. His most cited works are on the formal analysis of reactive systems, much of which was done in collaboration with Amir Pnueli. In the late seventies, the two of them embarked on their seminal study of applications of temporal modal logics to verification of concurrent programs. This long-term collaboration culminated in two landmark volumes and in the STeP prover.

Zohar was universally acclaimed and deeply appreciated as a consummate teacher. Even as a graduate student, his first talk, describing his thesis research, was polished and professional. The courses he taught include “Logic and Automated Reasoning” and “Formal Methods for Concurrent and Reactive Systems.” Moshe Vardi has divulged that “His course was one of my favorite all-time computer science courses. It convinced me that logic has a real place in computer science.”

When Nachum took Zohar’s course at Weizmann in 1974, Mathematical Theory of Computation was in galley proofs, and exercises were assigned from them. Besides laboring to solve the problems, Nachum would take pleasure in proofreading for errors and typos, for which Zohar was quite grateful. Later, when preparing their textbooks, Zohar and Richard would give students handouts in which three small errors had been deliberately introduced into each chapter. As part of their homework, students were asked to find these errors. If they found more than the three, so much the better. This worked well as long as Zohar and Richard kept good records of where the errors had been secreted, so they could be removed prior to publication. For several years, students would read successive versions of the manuscript, sprinkled with deliberately introduced errors.

Zohar’s international cachet is reflected in the honors he accrued, including: the ACM Programming Systems and Languages Award (1974); a Guggenheim Fellowship (1981); the F. L. Bauer Prize from the Technical University Munich (1992); Fellowship in the ACM (1993); doctor honoris causa from École nor- male supérieure de Cachan (2002); and a Fulbright Fellowship (2002). In 2016, he (together with Richard Waldinger) received the Herbrand Award for Distinguished Contributions to Automated Reasoning from CADE “for his pioneering research and pedagogical contributions to automated reasoning, program synthe- sis, planning, and formal methods.” He was also associate editor of Acta Informatica and of Theoretical Computer Science and a board member of the International Institute for Software Technology of the United Nations University in Macao. His fifty coauthors and collaborators read like a computer-science hall of fame. When he turned sixty-four in 2003, many of his graduate students, research collaborators, and computer- science colleagues gathered in Sicily for a symposium on subjects related to Zohar’s manifold contributions in the field. Their breadth and depth serve as a tribute to Zohar’s lasting impact on the field. In addition, a liber amicorum was prepared in tribute: Verification – Theory and Practice (2003).

Zohar and Nitza’s children recall a house full of life and guests, and Friday night family dinners, but most of all, they remember the family camping trips. They toured the world extensively, paying special attention to nature reserves and beaches. There are dozens of albums with Zohar’s exquisite photography, another one of his many talents. A more mathematical talent of Zohar’s was counting cards at blackjack, leading to his being blacklisted by some casinos. “He laughed that it was one of his greatest achievements,” his son recalls. Above all, family and friends remember a person who enjoyed the fullness of life, was humble despite his accomplishments, and was devoted to all who came into his orbit. He will be sorely missed.

## Results of the CADE Trustee Elections

Philipp Rümmer

An election was held from November 16 to November 30 2019 to fill four positions on the board of trustees of CADE, Inc.

Six candidates were nominated (in alphabetical order): Maria Paola Bonacina, Pascal Fontaine, Laura Kovács, Aart Middeldorp, Renate Schmidt, and Christoph Weidenbach.

The participants of the last three CADE/IJCAR conferences were invited to vote, and a total of 240 ballots were sent by electronic mail on November 16. By November 30, 83 valid ballots had been returned, which translates to a participation rate of 34.5% (as compared to 21.1% in 2018, 9.1% in 2017, 11.2% in 2016, 11.0% in 2015, 10.0% in 2014, 11.8% in 2013, 13.0% in 2012, 16.2% in 2011).

The four candidates elected are Pascal Fontaine, Laura Kovács, Aart Middeldorp, and Christoph Weidenbach.

The counting of the votes according to the single transferable vote algorithm described in the CADE Bylaws is detailed near the end of this newsletter.

After this election, the following people (listed alphabetically) are serving on the board of trustees of CADE Inc.:

On behalf of the AAR and CADE Inc., I would like to thank Jasmin Blanchette and Renate Schmidt for their service on the board of trustees since 2016, and Maria Paola Bonacina for running in the election.

Congratulations to Laura Kovács and Christoph Weidenbach, who were re-elected, and to Pascal Fontaine and Aart Middeldorp, who will join the board as new members!

## A Change to the CADE STV Algorithm

Christoph Weidenbach
Philipp Rümmer
Secretary of AAR and CADE Inc.

In conjunction with the 2019 CADE trustee elections, a vote on a motion brought forward by the CADE trustees was held. The CADE trustees suggested to move from the CADE STV algorithm to a standard algorithm that is supported by automatic voting platforms, and to change the CADE bylaws as follows:

1. Changing Article (IV) Section 2.3 of the bylaws from
(CURRENT)
Subsection 2.3 Election of Trustees
Elected members of the Board of Trustees shall be elected via email by the entire CADE membership using the Single Transferrable Vote system. The election will be held within thirty days of the business meeting that marks the close of nominations and shall be binding on the Trustees.
to
(NEW)
Subsection 2.3 Election of Trustees
Elected members of the Board of Trustees shall be elected electronically by the entire CADE membership. The CADE trustees decide on a voting procedure for the trustee election. The procedure will be published on the CADE homepage. The election will be held within thirty days of the business meeting that marks the close of nominations and shall be binding on the Trustees.
2. Remove the CADE STV algorithm from the bylaws.

The 240 ballots sent out to the CADE members on November 16 included a question about this change. By November 30, 84 valid answers had been sent back for the question, while one person preferred to abstain:

• YES (adopt the change): 80
• NO (keep the bylaws as they are): 4
• Abstain: 1

This means that more than 30% of the people voted on the question, and more than two-third voted in favor of the proposed change.

By Article IX of the bylaws, the change has therefore been accepted, and the bylaws have been updated accordingly.

## Invitation to the Zulip chat

the Zipperposition team

Zulip is successfully used by the Lean community to communicate. It bridges the gap between long-form mailing lists and interactive messaging, with excellent support for threading (which allows to follow in-depth discussions without drowning in unrelated noise), streams and topics, and the convenience of quick messages and replies when needed.

We have an instance of zulip which is used for Matryoshka and Zipperposition development, and would like to open it further to the wider ATP community. Streams allow sub-communities to have their own space (e.g. a Vampire specific stream, or one for CASC). The lean zulip server demonstrates that good communication tools can help communities thrive, make it easier for newcomers to ask questions, and lower friction for discussions.

## Calls for Award Nominations

### 2020 Alonzo Church Award

An annual award, called the Alonzo Church Award for Outstanding Contributions to Logic and Computation, was established in 2015 by the ACM Special Interest Group for Logic and Computation (SIGLOG), the European Association for Theoretical Computer Science (EATCS), the European Association for Computer Science Logic (EACSL), and the Kurt Gödel Society (KGS). The award is for an outstanding contribution represented by a paper or by a small group of papers published within the past 25 years. This time span allows the lasting impact and depth of the contribution to have been established. The award can be given to an individual, or to a group of individuals who have collaborated on the research. For the rules governing this award, see: here, here and here.

The 2019 Alonzo Church Award was given jointly to Murdoch J. Gabbay and Andrew M. Pitts for their ground-breaking work introducing the theory of nominal representations. Previous awardees are listed here.

Eligibility and Nominations
The contribution must have appeared in a paper or papers published within the past 25 years. Thus, for the 2020 award, the cut-off date is January 1, 1995. When a paper has appeared in a conference and then in a journal, the date of the journal publication will determine the cut-off date. In addition, the contribution must not yet have received recognition via a major award, such as the Turing Award, the Kanellakis Award, or the Gödel Prize. (The nominee(s) may have received such awards for other contributions.) While the contribution can consist of conference or journal papers, journal papers will be given a preference.

Nominations for the 2020 award are now being solicited. The nominating letter must summarize the contribution and make the case that it is fundamental and outstanding. The nominating letter can have multiple co-signers. Self-nominations are excluded. Nominations must include: a proposed citation (up to 25 words); a succinct (100-250 words) description of the contribution; and a detailed statement (not exceeding four pages) to justify the nomination. Nominations may also be accompanied by supporting letters and other evidence of worthiness.

Nominations should be submitted to Thomas Eiter by April 1, 2020.

Presentation of the Award The 2020 award will be presented at CSL 2021, the annual conference of the European Association for Computer Science Logic, which is scheduled to take place in Athens in January 2021. The award will be accompanied by an invited lecture by the award winner, or by one of the award winners. The awardee(s) will receive a certificate and a cash prize of USD 2,000. If there are multiple awardees, this amount will be shared.

Award Committee
The 2020 Alonzo Church Award Committee consists of the following five members: Mariangiola Dezani, Thomas Eiter (chair), Javier Esparza, Radha Jagadeesan, Natarajan Shankar

### Ackermann Award 2020

Nominations are now invited for the 2020 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.1.2018 and 31.12.2019 are eligible for nomination for the award.

The deadline for submission is 1 April 2020. Submission details follow below.

Nominations can be submitted from 1 January 2020 and should be sent to the chair of the Jury, Thomas Schwentick.

The Award
The 2020 Ackermann award will be presented to the recipient(s) at CSL 2021, 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, and
• financial support to attend the conference.

The jury is entitled to give the award to more (or less) than one dissertation in a year.

The Jury
The jury consists of:

• Christel Baier (TU Dresden);
• Michael Benedikt (Oxford University);
• Mikolaj Bojanczyk (University of Warsaw);
• Jean Goubault-Larrecq (ENS Paris-Saclay);
• Simona Ronchi Della Rocca (University of Torino), the vice-president of EACSL;
• Thomas Schwentick (TU Dortmund) , the president of EACSL;
• Alexandra Silva, (University College London), ACM SigLog representative.

How to submit
The candidate or his/her supervisor should submit

1. the thesis (ps or pdf file);
2. a detailed description (not longer than 20 pages) of the thesis in ENGLISH (ps or pdf file);
3. a supporting letter by the PhD advisor and two supporting letters by other senior researchers (in English); supporting letters can also be sent directly to Thomas Schwentick;
4. a short CV of the candidate;
5. a copy of the document asserting that the thesis was accepted as a PhD thesis at a recognized University (or equivalent institution) and that the candidate has received his/her PhD within the specified period.
The submission should be sent by e-mail as attachments to the chairman of the jury, Thomas Schwentick, With the following subject line and text:
• Subject: Ackermann Award 20 Submission
• Text: Name of candidate, list of attachments
Submission can be sent via several e-mail messages. If this is the case, please indicate it in the text.

### E. W. Beth Outstanding Dissertation Prize 2020

Since 2002, the Association for Logic, Language, and Information (FoLLI) has been awarding the annual E.W. Beth Dissertation Prize to outstanding Ph.D. dissertations in Logic, Language, and Information, with financial support of the E.W. Beth Foundation. Nominations are now invited for the best dissertation in these areas resulting in a Ph.D. degree awarded in 2019.

The deadline for nominations is the 15th of April 2020.

Qualifications:

• A dissertation is eligible for the Beth Dissertation Prize 2020, if the Ph.D. degree has been awarded in Logic, Language, or Information between January 1st and December 31st, 2019.
• There are no restrictions on the nationality, ethnicity, age, gender or employment status of the author of the nominated dissertation, nor on the university, academic department or scientific institution formally conferring the Ph.D. degree, nor on the language in which the dissertation has originally been written.
• In accordance with the aim of the Beth Foundation to continue and extend the work of the Dutch logician Evert Willem Beth, nominations are invited of excellent dissertations on current topics in philosophical and mathematical logic, computer science logic, philosophy of science, philosophy of language, history of logic, history of the philosophy of science and scientific philosophy in general, as well as the current theoretical and foundational developments in information and computation, language and cognition. Dissertations with results more broadly impacting various research areas in their interdisciplinary investigations are especially solicited.
• If a nominated dissertation has originally been written in a language other than English, its dossier should still contain the required 10 page English abstract, see below. If the committee decides that a nominated dissertation in a language other than English requires translation to English for proper evaluation, the committee can transfer its nomination to the competition in 2021. The English translation must in such cases be submitted before the deadline of the call for nominations in 2021. The committee may recommend the Beth Foundation to consider supporting such nominated dissertations for English translation, upon request by the author of the dissertation.

The prize consists of:

• a certificate
• a donation of 3000 euros, provided by the E.W. Beth Foundation
• an invitation to submit the dissertation, possibly after revision, for publication in FoLLI Publications on Logic, Language and Information (Springer).

Only digital submissions are accepted, without exception. Hard copy submissions are not allowed. The following documents are to be submitted in the nomination dossier:

• The original dissertation in pdf format (ps/doc/rtf etc. not acceptable).
• A ten-page English abstract of the dissertation, presenting the main results of each chapter.
• A letter of nomination from the dissertation supervisor, which concisely describes the scope and significance of the dissertation, stating when the degree was officially awarded and the members of the Ph.D. committee. Nominations should contain the address, phone and email details of the nominator.
• Two additional letters of support, including at least one from a referee not affiliated with the academic institution that awarded the Ph.D. degree, nor otherwise related to the nominee (e.g. former teachers, supervisors, co-authors, publishers or relatives) or the dissertation.
Self-nominations are not possible.

All pdf documents must be submitted electronically, as one zip file, via EasyChair. In case of any problems with the submission one should contact the chair of the committee Mehrnoosh Sadrzadeh.

The prize will be awarded by the chair of the FoLLI board at a ceremony during the 32nd ESSLLI summer school in University of Utrecht, August 3-14, 2020.

Beth dissertation prize committee 2020:

• Maria Aloni (University of Amsterdam)
• Alexander Clark(Kings College London)
• Cleo Condoravdi (Stanford University)
• Robin Cooper (University of Gothenburg)
• Guy Emerson (University of Cambridge)
• Katrin Erk (University of Texas at Austin)
• Arash Eshghi (Hariot-Watt University)
• Sujata Ghosh (ISI, Chennai)
• Davide Grossi (University of Groningen and University of Amsterdam)
• Chris Haase (University College London)
• Aurelie Herbelot (University of Trento)
• Louise McNally (Universitat Pompeu Fabra Barcelona)
• Reinhard Muskens (University of Amsterdam)
• Laura Rimmell (Deep Mind)
• Mark Steedman (University of Edinburgh)
• Matthew Stone (Rutgers)
• Jouko Väänänen (University of Helsinki)
• Noam Zeilberger (Ecole Polytechnique)

## Conferences

### Call for bids to host TABLEAUX 2021

Jens Otten
President of, and on behalf of, the TABLEAUX Steering Committee

The TABLEAUX Steering Committee is now calling for bids to host the International Conference on Automated Reasoning with Analytic Tableaux and Related Methods ("TABLEAUX") in 2021. TABLEAUX typically merges into IJCAR (the International Joint Conference on Automated Reasoning) in even years. Previous TABLEAUX/IJCAR conferences took place in London/UK (TABLEAUX 2019), Oxford/UK (IJCAR 2018), Brasília/Brazil (TABLEAUX 2017), Coimbra/Portugal (IJCAR 2016), Wrocław/Poland (TABLEAUX 2015), Vienna/Austria (IJCAR 2014), Nancy/France (TABLEAUX 2013), Manchester/UK (IJCAR 2012), Bern/Switzerland (TABLEAUX 2011), Edinburgh/UK (IJCAR 2010), and Oslo/Norway (TABLEAUX 2009). See here for a complete list of previous conferences.

A bid should cover at least the following aspects:

• contact person: name and email address
• names of other people involved in the local organization
• experience, if any, of organizing previous similar events
• planned venue, accessibility and transportation
• suggested dates of the conference
• plans, if any, for co-location with other meetings, conferences and/or workshops
• available accommodation, e.g., hotels and/or dormitory rooms
• catering arrangements
• any relevant plans for social events, e.g., excursions
• a list of potential national and local sponsors
• expected expenses and expected registration costs

Bids that consider co-locating TABLEAUX with other conferences, such as FroCoS or ITP, are strongly encouraged. In 2013, 2015 and 2019 TABLEAUX was co-located with FroCoS (the International Symposium on Frontiers of Combining Systems) and in 2017 TABLEAUX was co-located with FroCoS and ITP (the International Conference on Interactive Theorem Proving).

The leader or leaders of the winning bid will become the Conference Chair or Co-Chairs of TABLEAUX 2021. Traditionally they will also become the PC Chair or Co-Chairs; the final decision on this will be made by the TABLEAUX Steering Committee. The PC Chair or Co-Chairs will create a PC in consultation with the TABLEAUX Steering Committee and will also be expected to edit the conference proceedings.

The bid should be limited to 10 pages and should be submitted as PDF file to Jens Otten.

The deadline for submissions is April 26th, 2020.

The TABLEAUX Steering Committee will decide which bid to accept and announce a decision as soon as possible after the deadline.

Perspective organizers are encouraged to register their intention informally and to get in touch with the TABLEAUX Steering Committee for informal discussion.

### RAMiCS 2020: 18th International Conference on Relational and Algebraic Methods in Computer Science, call for short papers and posters

April 8-11, 2020, Palaiseau, France

As a novelty this year, and additionally to the standard CfP, RAMICS is also calling for short contributions and posters. We are hence calling for presentations of original, unfinished, already published, or otherwise interesting work within the topics of the RAMICS conferences. The submission can be in the form of a poster, an abstract, a paper submitted to or published at another conference, etc. Short contributions will not be published in the conference proceedings.

Important Dates:

• Submission: 14 February 2020
Note that these dates coincide with the ones for WATA 2020, which will take place just after RAMICS, from 14 to 17 April, in Marseille. We encourage double submissions of short contributions.

### LPAR-23: 23rd International Conference on Logic for Programming, Artificial Intelligence and Reasoning, call for papers

May 22-27, 2020, Alicante, Spain

The series of International Conferences on Logic for Programming, Artificial Intelligence and Reasoning (LPAR) is a forum where, year after year, some of the most renowned researchers in the areas of logic, automated reasoning, computational logic, programming languages and their applications come to present cutting-edge results, to discuss advances in these fields, and to exchange ideas in a scientifically emerging part of the world.

List of Topics:
New results in the fields of computational logic and applications are welcome. Also welcome are more exploratory presentations, which may examine open questions and raise fundamental concerns about existing theories and practices. Topics of interest include, but are not limited to:

• Abduction and interpolation methods
• Automated reasoning
• Constraint programming
• Contextual reasoning
• Decision procedures
• Description logics
• Foundations of security
• Hardware verification
• Implementations of logic
• Inconsistency- and exception tolerant reasoning
• Interactive theorem proving
• Knowledge representation and reasoning
• Logic and computational complexity
• Logic and databases
• Logic and games
• Logic and machine learning
• Logic and the web
• Logic and types
• Logic in artificial intelligence
• Logic of distributed systems
• Logic of knowledge and belief
• Logic programming
• Logical aspects of concurrency
• Logical foundations of programming
• Modal and temporal logics
• Model checking
• Non-monotonic reasoning
• Ontologies and large knowledge bases
• Paraconsistent logics
• Probabilistic and fuzzy reasoning
• Program analysis
• Rewriting
• Satisfiability checking
• Satisfiability modulo theories
• Software verification
• Specification using logic
• Unification theory

Important Dates

• Abstract submission: February 18, 2020
• Paper submission: February 22, 2020
• Author notifications: April 8, 2020
• Conference: May 22-27, 2020

### TTCS 2020: 3rd IFIP International Conference on Topics in Theoretical Computer Science, call for papers

July 1-3, 2020, Tehran, Iran

TTCS is a bi-annual conference series, intending to serve as a forum for novel and high-quality research in all areas of Theoretical Computer Science. The conference is held in cooperation with the European Association for Theoretical Computer Science (EATCS). The proceedings will be published in the Springer LNCS series.

TTCS is organized in 2 tracks. Topics of interest include but are not limited to:

Track A: Algorithms and Complexity

• algorithms and data structures,
• algorithmic coding theory,
• algorithmic graph theory and combinatorics,
• approximation algorithms,
• computational complexity,
• computational geometry,
• computational learning theory,
• economics and algorithmic game theory,
• fixed-parameter algorithms,
• machine learning,
• optimization,
• parallel and distributed algorithms,
• quantum computing,
• randomness in computing,
• theoretical cryptography.
Track B: Logic, Semantics, and Programming Theory
• algebra and coalgebra in computer science,
• concurrency theory,
• coordination languages,
• formal verification and model-based testing,
• logic in computer science,
• methods, models of computation and reasoning for embedded, hybrid, and cyber-physical systems,
• stochastic and probabilistic specification and reasoning,
• theoretical aspects of other CS-related research areas, e.g. computational science, databases, information retrieval, and networking,
• theory of programming languages,
• type theory.

Important Dates

• Full Paper Submission: February 16, 2020
• Author notification: April 12, 2020
• Camera-ready paper: May 1, 2020
• Conference: July 1-3, 2020

### SAT 2020: 23rd International Conference on Theory and Applications of Satisfiability Testing, call for papers

July 5-9, 2020, Alghero, Italy

The International Conference on Theory and Applications of Satisfiability Testing (SAT) is the premier annual meeting for researchers focusing on the theory and applications of the propositional satisfiability problem, broadly construed. In addition to plain propositional satisfiability, it also includes Boolean optimization (such as MaxSAT and Pseudo-Boolean (PB) constraints), Quantified Boolean Formulas (QBF), Satisfiability Modulo Theories (SMT), and Constraint Programming (CP) for problems with clear connections to Boolean-level reasoning.

Scope
SAT 2020 welcomes scientific contributions addressing different aspects of the satisfiability problem, interpreted in a broad sense. Topics include, but are not restricted to:

• Practical search algorithms
• Knowledge compilation
• Implementation-level details of SAT solving tools
• Problem encodings and reformulations
• Applications
• Case studies based on rigorous experimentation

Out of Scope
Papers claiming to resolve a major long-standing open theoretical question in Mathematics or Computer Science (such as those for which a Millennium Prize is offered), are outside the scope of the conference because there is insufficient time in the schedule to referee such papers; instead, such papers should be submitted to an appropriate technical journal.

Important Dates

• Workshops July 5, 2020
• Conference July 6-9, 2020
• Abstract submission February 15, 2020
• Paper submission February 22, 2020
• Author response period March 29 – April 2, 2020
• Author notification April 18, 2020

### AiML 2020: 13th International Conference on Advances in Modal Logic, call for papers

August 17-21, 2020, Helsinki, Finland

Advances in Modal Logic is an initiative aimed at presenting the state of the art in modal logic and its various applications. The initiative consists of a conference series together with volumes based on the conferences. Information about the AiML series can be obtained here.

Topics
We invite submissions on all aspects of modal logic, including:

• history of modal logic
• philosophy of modal logic
• applications of modal logic
• automated reasoning for modal logics
• computational aspects of modal logic (complexity and decidability of modal and temporal logics, model checking, model generation)
• theoretical aspects of modal logic (topological/algebraic/categorical perspectives on modal logic, co-algebraic modal logic, completeness and canonicity, correspondence and duality theory, many-dimensional modal logics, modal fixed-point logics, model theory of modal logic, proof theory of modal logic)
• specific instances and variations of modal logic (description logics, modal logics over non-boolean bases, dynamic logics and other process logics, epistemic and deontic logics, modal logics for agent-based systems, modal logic and game theory, modal logic and grammar formalisms, provability and interpretability logics, conditional logics, spatial and temporal logics, hybrid logic, intuitionistic (modal) logics, intermediate logics, bunched implication and separation logics)
Papers on related subjects will also be considered.

Dates

• Abstracts of full papers submission deadline: 11 March 2020
• Full papers submission deadline: 18 March 2020
• Full papers acceptance notification: 18 May 2020
• Short presentations submission deadline: 25 May 2020
• Short presentations acceptance notification: 8 June 2020
• Final version of full papers and short presentations due: 11 June 2020

### CICM 2020: 13th Conference on Intelligent Computer Mathematics, call for papers

July 26-31, 2020, Bertinoro, Italy

Digital and computational solutions are becoming the prevalent means for the generation, communication, processing, storage and curation of mathematical information.

CICM brings together the many separate communities that have developed theoretical and practical solutions for mathematical applications such as computation, deduction, knowledge management, and user interfaces. It offers a venue for discussing problems and solutions in each of these areas and their integration.

CICM 2020 invites submissions in all topics relating to intelligent computer mathematics, in particular but not limited to

• theorem proving and computer algebra
• mathematical knowledge management
• digital mathematical libraries

Important Dates

• Formal submissions
• Full paper deadline: March 08
• Reviews sent to authors: April 17
• Rebuttals due: April 21
• Notification of acceptance: April 24
• Camera-ready copies due: May 03
• Conference: July 26-31
• Informal submissions and doctoral programme
Two separate submission rounds are offered so that some authors can make early travel plans while other authors submit spontaneously.
• First round submission deadline: April 15
• Notification of acceptance: May 1
• Second round submission deadline: June 15
• Notification of acceptance: July 1

### KR 2020: 17th Conference on Principles of Knowledge Representation and Reasoning, call for papers

September 12—18, 2020, Rhodes, Greece

Knowledge Representation and Reasoning (KR) is a well-established and lively field of research. In KR a fundamental assumption is that an agent's knowledge is explicitly represented in a declarative form, suitable for processing by dedicated reasoning engines. This assumption, that much of what an agent deals with is knowledge-based, is common in many modern intelligent systems. Consequently, KR has contributed to the theory and practice of various areas in AI, including automated planning and natural language understanding, and to fields beyond AI, including databases, verification, software engineering, and robotics. In recent years, KR has contributed also to new and emerging fields, including the semantic web, computational biology, cyber security, and the development of software agents.

The KR conference series is the leading forum for timely in-depth presentation of progress in the theory and principles underlying the representation and computational management of knowledge.

Scope
We solicit papers presenting novel results on the principles of KR that clearly contribute to the formal foundations of relevant problems or show the applicability of results to implemented or implementable systems. We also welcome papers from other areas that show clear use of, or contributions to, the principles or practice of KR. We also encourage "reports from the field" of applications, experiments, developments, and tests.

Topics of interest include, but are not limited to:

• Applications of KR
• Argumentation
• Belief revision and update, belief merging, information fusion
• Commonsense reasoning
• Computational aspects of knowledge representation
• Concept formation, similarity-based reasoning
• Contextual reasoning
• Decision making
• Description logics
• Explanation finding, diagnosis, causal reasoning, abduction
• Geometric, spatial, and temporal reasoning
• Inconsistency- and exception tolerant reasoning, paraconsistent logics
• KR and autonomous agents and multi-agent systems
• KR and cognitive robotics
• KR and cyber security
• KR and education
• KR and game theory
• KR and machine learning, inductive logic programming, knowledge acquisition
• KR and natural language processing and understanding
• KR and the Web, Semantic Web
• Knowledge graphs, virtual knowledge graphs, and open linked data
• Knowledge representation languages
• Logic programming, answer set programming, constraint logic programming
• Modeling and reasoning about preferences
• Multi- and order-sorted representations and reasoning
• Nonmonotonic logics, default logics, conditional logics
• Ontology formalisms and models
• Ontology-based data access, integration, and exchange
• Philosophical foundations of KR
• Qualitative reasoning, reasoning about physical systems
• Reasoning about actions and change, action languages
• Reasoning about knowledge, beliefs, and other mental attitudes
• Uncertainty, vagueness, many-valued and fuzzy logics
KR2020 will also feature Workshops and Tutorials, solicited by means of an open call, and a Doctoral Consortium.

Tracks
In addition to the main conference track, KR2020 will host the following tracks and sessions:

• Applications and Systems Track
• Recent Published Research Track
• Special Session: KR and Machine Learning
• Special Session: KR and Robotics
• Special Session: Women in KR

Important Dates

• Submission of title and abstract: 4 March 2020
• Paper submission deadline: 11 March 2020
• Author response period: 4--6 May 2020
• Camera-ready papers: 24 June 2020
• Conference dates: 12--18 September 2020
Recent Published Research Track, Workshops and Tutorials, and Doctoral Consortium will have different submission and notification dates, which will be announced separately.

### RuleML+RR 2020: 4th International Joint Conference on Rules and Reasoning, call for papers

June 29 - July 1, 2020, Oslo, Norway

RuleML+RR is part of "Declarative AI 2020: Rules, Reasoning, Decisions and Explanations" (DeclarativeAI 2020)

The 4th International Joint Conference on Rules and Reasoning (RuleML+RR 2020) is the leading international joint conference in the field of rule-based reasoning. Stemming from the synergy with the DecisionCAMP summit, which brings together leading decision management authorities, vendors, and practitioners, one of the main goals of RuleML+RR is to build bridges between academia and industry in the area of rule-based reasoning and applications.

RuleML+RR 2020 aims to bring together rigorous researchers and inventive practitioners, interested in the foundations and applications of rules and reasoning in academia, industry, engineering, business, finance, healthcare, environment, and other application areas. It provides a forum for stimulating cooperation and cross-fertilization between the many different communities focused on the research, development, and applications of rule-based systems.

Topics
RuleML+RR welcomes research from all areas of Rules and Reasoning, including topics from our 2020 theme: explainable algorithmic decision-making. The topics of the conference include:

• Machine learning approaches involving rules (e.g, extracting rules from Deep Neural Networks or rule-based classification)
• Rules for knowledge graphs and ontology learning
• Rule-based approaches to natural language processing
• Explainable AI approaches based on rules, psychological aspects of rule learning
• Rules of ethics, biases, laws, policies, and regulations
• Production & business rule systems
• Communicating rule models with Decision Model and Notation (DMN)
• Applications of rule technologies with explainable AI (xAI) elements
• Foundations of declarative AI architectures and languages
• Rule-based approaches for intelligent systems and intelligent information access
• Vocabularies, ontologies, and business rules
• Ontology-based data access
• Rule-based data integration
• Data management and data interoperability for web data
• Distributed agent-based systems for the web
• Rule-based approaches to agents
• Scalability and expressive power of logics for the semantic web
• Reasoning with incomplete, inconsistent and uncertain data
• Non-monotonic, common-sense, and closed-world reasoning for web data
• Non-classical logics and the Web
• Constraint programming
• Logic programming
• Streaming data and complex event processing
• Higher-order and modal rules
• Web reasoning and distributed rule inference and execution
• Rule markup languages and rule interchange formats
• Rule-based policies, reputation, and trust
• Rules, blockchain, and smart contracts
• Scalability and expressive power of logics for rules
• System descriptions, applications and experiences
• Rules and human language technology
• Rules in online market research and online marketing
• Applications of ontologies and rules in environmental protection
• Applications in climate change monitoring, mitigation & adaptation
• Applications in healthcare and life sciences
• Applications in peace and conflict studies
• Applications in equity and social welfare
• Applications in law, regulation, and finance
• Applications in Digital Twins
• Industrial applications of rules

Important Dates

• Title and Abstract submission: 6 March 2020
• Full papers submission: 13 March 2020
• Notification of acceptance: 30 April 2020
• Camera-ready submission: 8 May 2020
• Conference: 29 June - 1 July 2020

### ICALP 2020: 47th International Colloquium on Automata, Languages and Programming, conference relocation and deadline extension

July 8-11 2020, Saarbrücken, Germany

The ICALP and the LICS steering committee have agreed together with the conference chairs in Beijing to relocate the two conferences. ICALP and LICS 2020 will take place in Saarbrücken, Germany, July 8-11 (with satellite workshops on July 6-7).

We are very grateful to our colleagues in Beijing, for the organization so far, to the colleagues from Saarbrücken, who generously accepted this challenging task, and to all members of the TCS community who offered their help in this difficult situation.

ICALP (International Colloquium on Automata, Languages and Programming) is the main European conference in Theoretical Computer Science and annual meeting of the European Association for Theoretical Computer Science (EATCS). ICALP 2020 will be hosted on the Saarland Informatics Campus in Saarbrücken, in co-location with LICS 2020 (ACM/IEEE Symposium on Logic in Computer Science).

Topics:
ICALP 2020 will have the two traditional tracks A (Algorithms, Complexity and Games - including Algorithmic Game Theory, Distributed Algorithms and Parallel, Distributed and External Memory Computing) and B (Automata, Logic, Semantics and Theory of Programming). Papers presenting original, unpublished research on all aspects of theoretical computer science are sought.

Typical, but not exclusive topics are:
Track A

• Algorithmic Aspects of Networks and Networking
• Algorithms for Computational Biology
• Algorithmic Game Theory
• Combinatorial Optimization
• Combinatorics in Computer Science
• Computational Complexity
• Computational Geometry
• Computational Learning Theory
• Cryptography
• Data Structures
• Design and Analysis of Algorithms
• Foundations of Machine Learning
• Foundations of Privacy
• Trust and Reputation in Network
• Network Models for Distributed Computing
• Network Economics and Incentive-Based Computing Related to Networks
• Network Mining and Analysis
• Parallel
• Distributed and External Memory Computing
• Quantum Computing
• Randomness in Computation
• Theory of Security in Networks
Track B
• Algebraic and Categorical Models
• Automata
• Games and Formal Languages
• Emerging and Non-standard Models of Computation
• Databases
• Semi-Structured Data and Finite Model Theory
• Formal and Logical Aspects of Learning
• Logic in Computer Science
• Theorem Proving and Model Checking
• Models of Concurrent
• Distributed
• and Mobile Systems
• Models of Reactive
• Hybrid and Stochastic Systems
• Principles and Semantics of Programming Languages
• Program Analysis and Transformation
• Specification
• Verification and Synthesis
• Type Systems and Theory
• Typed Calculi

Important Dates

• submission: February 18, 2020, 6am GMT
• camera ready: April 28, 2020

### LICS 2020: 35th Annual ACM/IEEE Symposium on Logic in Computer Science, conference relocation

July 8-11 2020, Saarbrücken, Germany

The ICALP and the LICS steering committee have agreed together with the conference chairs in Beijing to relocate the two conferences. ICALP and LICS 2020 will take place in Saarbrücken, Germany, July 8-11 (with satellite workshops on July 6-7).

We are very grateful to our colleagues in Beijing, for the organization so far, to the colleagues from Saarbrücken, who generously accepted this challenging task, and to all members of the TCS community who offered their help in this difficult situation.

### MFPS XXXVI: 36th Conference on the Mathematical Foundations of Programming Semantics, call for papers

June 2-6, 2020, Paris Saclay, France

MFPS conferences are dedicated to the areas of mathematics, logic, and computer science that are related to models of computation in general, and to semantics of programming languages in particular. This is a forum where researchers in mathematics and computer science can meet and exchange ideas. The participation of researchers in neighbouring areas is strongly encouraged.

Topics include, but are not limited to, the following:

• bio-computation;
• concurrent qualitative and quantitative distributed systems;
• process calculi;
• probabilistic systems;
• constructive mathematics;
• domain theory and categorical models;
• formal languages;
• formal methods;
• game semantics;
• lambda calculus;
• programming-language theory;
• quantum computation;
• security;
• topological models;
• logic;
• type systems;
• type theory.
We also welcome contributions that address applications of semantics to novel areas such as complex systems, markets, and networks, for example.

Important Dates:

• March 30, 2020: Abstract Submission
• April 3, 2020: Paper Submission
• May 22, 2020: Final Papers Deadline

### SEFM 2020: 18th International Conference on Software Engineering and Formal Methods, call for papers

September 14-18, 2020, Amsterdam, The Netherlands

Overview and Scope
SEFM aims to bring together leading researchers and practitioners from academia, industry, and government, to advance the state of the art in formal methods, to facilitate their uptake in the software industry, and to encourage their integration within practical software engineering methods and tools.

Topics of interest include, but are not limited to, the following aspects of software engineering and formal methods:

• Software Development Methods
• Formal modeling, specification, and design
• Software evolution, maintenance, re-engineering, and reuse
• Design Principles
• Programming languages
• Domain-specific languages
• Type theory
• Abstraction and refinement
• Software Testing, Validation, and Verification
• Model checking, theorem proving, and decision procedures
• Testing and runtime verification
• Statistical and probabilistic analysis
• Synthesis
• Performance estimation and analysis of other non-functional properties
• Other light-weight and scalable formal methods
• Security and Safety
• Security, privacy, and trust
• Safety-critical, fault-tolerant, and secure systems
• Software certification
• Applications and Technology Transfer
• Service-oriented and cloud computing systems, Internet of Things
• Component, object, multi-agent and self-adaptive systems
• Real-time, hybrid, and cyber-physical systems
• Intelligent systems and machine learning
• HCI, interactive systems, and human error analysis
• Education
• Case studies, best practices, and experience reports

Important Dates

• Abstract submission deadline: Monday 27 April 2020 (AoE)
• Paper submission deadline: Monday 4 May 2020 (AoE)
• Paper notification: Friday 26 June 2020
• Camera ready: Tuesday 7 July 2020 (AoE)

### ICLP 2020: 36th International Conference on Logic Programming, call for papers

September 18-24, 2020, Rende, Italy

Since the first conference held in Marseille in 1982, the International Conference on Logic Programming (ICLP 2020) has been the premier international event for presenting research in logic programming.

Scope
Contributions are solicited in all areas of logic programming, including but not restricted to:

• Foundations: Semantics, Formalisms, Answer-Set Programming, Non-monotonic Reasoning, Knowledge Representation.
• Declarative Programming: Inference engines, Analysis, Type and mode inference, Partial evaluation, Abstract interpretation, Transformation, Validation, Verification, Debugging, Profiling, Testing, Logic-based domain-specific languages, constraint handling rules.
• Related Paradigms and Synergies: Inductive and Co-inductive Logic Programming, Constraint Logic Programming, Interaction with SAT, SMT and CSP solvers, Logic programming techniques for type inference and theorem proving, Argumentation, Probabilistic Logic Programming, Relations to object-oriented and Functional programming, Description logics, Neural-Symbolic Machine Learning, Hybrid Deep Learning and Symbolic Reasoning.
• Implementation: Concurrency and distribution, Objects, Coordination, Mobility, Virtual machines, Compilation, Higher Order, Type systems, Modules, Constraint handling rules, Meta-programming, Foreign interfaces, User interfaces.
• Applications: Databases, Big Data, Data Integration and Federation, Software Engineering, Natural Language Processing, Web and Semantic Web, Agents, Artificial Intelligence, Bioinformatics, Education, Computational life sciences, Education, Cybersecurity, and Robotics.

Important Dates

• Abstract registration (regular papers): May 8, 2020
• Paper submission (regular paper): May 15, 2020
• Notification to authors (regular paper): June 19, 2020
• Paper Submission (short papers): June 30, 2020
• Revision submission (TPLP papers): July 6, 2020
• Final notifications (TPLP papers): July 17, 2020
• Camera-ready copy due: July 27, 2020

### CSL 2021: Computer Science Logic, call for papers

January 25-28, 2021, Ljubljana, Slovenia

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:

• automated deduction and interactive theorem proving
• constructive mathematics and type theory
• equational logic and term rewriting
• automata and games, game semantics
• modal and temporal logic
• model checking
• decision procedures
• logical aspects of computational complexity
• finite model theory
• computational proof theory
• logic programming and constraints
• lambda calculus and combinatory logic
• domain theory
• categorical logic and topological semantics
• database theory
• specification, extraction and transformation of programs
• logical aspects of quantum computing
• logical foundations of programming paradigms
• verification and program analysis
• linear logic
• higher-order logic
• nonmonotonic reasoning

Important dates:

• paper submission: July 1, 2020 (AoE)
• conference: January 25-28, 2021

## Satellite events of IJCAR and FSCD 2020

All the following events are affiliated with either IJCAR 2020 or FSCD 2020 and are part of the Paris Nord Summer of LoVe 2020, also including Petri Nets 2020.

### IWC 2020: 9th International Workshop on Confluence, call for papers

June 30, 2020, Paris, France

The 9th International Workshop on Confluence (IWC 2020) aims at promoting further research in confluence and related properties. Confluence provides a general notion of determinism and has always been conceived as one of the central properties of rewriting. Recently there is a renewed interest in confluence research, resulting in new techniques, tool support, certification as well as new applications. The workshop aims at promoting further research in confluence and related properties.

Confluence relates to many topics of rewriting (completion, modularity, termination, commutation, etc.) and has been investigated in many formalisms of rewriting such as first-order rewriting, lambda-calculi, higher-order rewriting, constrained rewriting, conditional rewriting, etc. Recently there is a renewed interest in confluence research, resulting in new techniques, tool supports, certification as well as new applications.

Topics

• confluence and related properties (unique normal forms, commutation, ground confluence)
• completion
• critical pair criteria
• decidability issues
• complexity issues
• system descriptions
• certification
• applications of confluence

The objective of this workshop is to bring together theoreticians and practitioners to promote new techniques and results, and to facilitate feedback on the implementation and application of such techniques and results in practice. IWC 2020 also aims to be a forum for presenting and discussing work in progress, and therefore to provide feedback to authors on their preliminary research.

Important Dates

• Title and Abstract:   April 17, 2020
• Paper Submission:   April 22, 2020
• Notification to authors:   May 22, 2020
• Workshop date:   June 30, 2020

### HoTT/UF 2020: Workshop on Homotopy Type Theory and Univalent Foundations, call for contributions

July 4-5, 2020, Paris, France

Homotopy Type Theory is a young area of logic, combining ideas from several established fields: the use of dependent type theory as a foundation for mathematics, inspired by ideas and tools from abstract homotopy theory. Univalent Foundations are foundations of mathematics based on the homotopical interpretation of type theory.

The goal of this workshop is to bring together researchers interested in all aspects of Homotopy Type Theory and Univalent Foundations: from the study of syntax and semantics of type theory to practical formalization in proof assistants based on univalent type theory.

Submission Dates

• Abstract submission deadline: March 25, 2020

### WST 2020 - Call for Papers 17th International Workshop on Termination, call for papers

June 29-30, 2020, Paris, France

The Workshop on Termination (WST) traditionally brings together, in an informal setting, researchers interested in all aspects of termination, whether this interest be practical or theoretical, primary or derived. The workshop also provides a ground for cross-fertilization of ideas from the different communities interested in termination (e.g., working on computational mechanisms, programming languages, software engineering, constraint solving, etc.). The friendly atmosphere enables fruitful exchanges leading to joint research and subsequent publications.

Topics:
The 17th International Workshop on Termination welcomes contributions on all aspects of termination. In particular, papers investigating applications of termination (for example in complexity analysis, program analysis and transformation, theorem proving, program correctness, modeling computational systems, etc.) are very welcome.

Topics of interest include (but are not limited to):

• abstraction methods in termination analysis
• certification of termination and complexity proofs
• challenging termination problems
• comparison and classification of termination methods
• complexity analysis in any domain
• implementation of termination methods
• non-termination analysis and loop detection
• normalization and infinitary normalization
• operational termination of logic-based systems
• ordinal notation and subrecursive hierarchies
• SAT, SMT, and constraint solving for (non-)termination analysis
• scalability and modularity of termination methods
• termination analysis in any domain (lambda calculus, declarative programming, rewriting, transition systems, etc.)
• well-founded relations and well-quasi-orders

Competition:
Since 2003, the catalytic effect of WST to stimulate new research on termination has been enhanced by the celebration of the Termination Competition and its continuously developing problem databases containing thousands of programs as challenges for termination analysis in different categories, see here.

In 2020, the Termination Competition will run shortly before WST and the main venues (IJCAR-FSCD), and the results will be presented at IJCAR or FSCD.

Important Dates:

• submission deadline: April 12, 2020
• final version due: May 31, 2020
• workshop: July 4-5, 2020

### PAAR 2020: 7th Workshop on Practical Aspects of Automated Reasoning, call for papers

June 30th, 2020, Paris, France

The automation of logical reasoning is a challenge that has been studied intensively in fields including mathematics, philosophy, and computer science. PAAR is the workshop on turning this theory into practice: how can automated reasoning tools be built that work and are useful in applications? PAAR covers all aspects of this challenge: which theories, logics, or fragments are well-behaved in practice, and connect well to application domains? which reasoning tasks are tractable and useful? which algorithms are able to solve real-world instances? how should automated reasoning tools be designed, implemented, tested, and evaluated?

The goal of PAAR is to bring together theoreticians, tool developers, and users, to concentrate on the practical aspects of automated reasoning. The workshop welcomes high-quality contributions of any kind, including new research results, presentation of work in progress, presentation of new tools, new implementation techniques, new application domains, or case studies.

Topics include, but are not limited to:

• automated reasoning in propositional, first-order, higher-order, and non-classical logics;
• implementation of provers (SAT, SMT, resolution, superposition, tableau, instantiation-based, rewriting, logical frameworks, etc.);
• automated reasoning tools for all kinds of practical problems and applications;
• pragmatics of automated reasoning within proof assistants;
• practical experiences, usability aspects, feasibility studies;
• evaluation of implementation techniques and automated reasoning tools;
• performance aspects, benchmarking approaches; non-standard approaches to automated reasoning, non-standard forms of automated reasoning, new applications;
• implementation techniques, optimisation techniques, machine learning, strategies and heuristics, fairness;
• tools or methods that support prover development;
• system descriptions and demos.

Important dates

• Abstract registration deadline: April 8, 2020 (tentative)
• Submission deadline: April 15, 2020 (tentative)
• Workshop: June 30th, 2020

### ThEdu'20: Theorem Proving Components for Educational Software, call for extended abstracts and demonstrations

June 29 - July 5, 2020, Paris, France

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.

Topics of interest include:

• methods of automated deduction applied to checking students' input;
• methods of automated deduction applied to prove post-conditions for particular problem solutions;
• combinations of deduction and computation enabling systems to propose next steps;
• automated provers specific for dynamic geometry systems;
• proof and proving in mathematics education.

Important Dates

• Extended Abstracts: 12 April 2020
• Author Notification: 10 May 2020
• Workshop Day: 29 June 2020

### WPTE 2020: 7th International Workshop on Rewriting Techniques for Program Transformations and Evaluation, call for extended abstracts

June 29, 2020, Paris, France

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.

Important dates

• Submission of extended abstracts: May 4, 2020
• Notification of acceptance: May 25, 2020
• Final version for proceedings deadline: June 1, 2020
• Workshop: June 29, 2020
• Submission to post-proceedings: September 2020

### WiL 2020: 4th Women in Logic Workshop, call for abstracts

June 30, 2020, Paris, France

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:

• provide a platform for female researchers to share their work and achievements;
• increase the feelings of community and belonging, especially among junior faculty, post-docs and students through positive interactions with peers and more established faculty;
• establish new connections and collaborations;
• foster a welcoming culture of mutual support and growth within the logic research community.
We believe these aspects will benefit women working in logic and computer science, particularly early-career researchers.

Topics of interest include but are not limited to:

• automata theory
• automated deduction
• categorical models and logics
• concurrency and distributed computation
• constraint programming
• constructive mathematics
• database theory
• decision procedures
• description logics
• domain theory
• finite model theory
• formal aspects of program analysis
• formal methods
• foundations of computability
• games and logic
• higher-order logic
• lambda and combinatory calculi
• linear logic
• logic in artificial intelligence
• logic programming
• logical aspects of bioinformatics
• logical aspects of computational complexity
• logical aspects of quantum computation
• logical frameworks
• logics of programs
• modal and temporal logics
• model checking
• probabilistic systems
• process calculi
• programming language semantics
• proof theory
• real-time systems
• reasoning about security and privacy
• rewriting
• type systems and type theory
• and verification.

Important Dates

• Abstract submission deadline: April 22, 2020

[N.D.L.R: At the moment this newsletter is published, there seem to be no website for WiL 2020, hence I have also included the submission instructions below]

Submissions
Abstracts should be written in English (1-2 pages), and prepared using the Easychair style.

The abstracts should be uploaded to the WiL 2020 Easychair page as a PDF file before the submission deadline of April 22, 2020, anywhere on Earth.

### UNIF 2020: 34th International Workshop on Unification, call for papers

June 29, 2020, Paris, France

UNIF 2020 is the 34th event in a series of international meetings devoted to unification theory and its applications. Unification is concerned with the problem of making two terms equal, 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. Traditionally, the scope of the UNIF workshops has covered the topic of unification in a broad sense. Topics of interest to this forum include, but are not limited to:

• Unification algorithms, calculi and implementations
• Equational unification and unification modulo theories
• Unification in modal, fuzzy, temporal and description logics
• Anti-unification/generalization
• Semi-unification
• Narrowing
• Formalization of unification
• Matching Problems
• Applications
• Unification in Special Theories
• Higher-Order Unification
• Combination problems
• Constraint Solving
• Disunification
• Complexity Issues
• Type Checking and reconstruction

The International Workshop on Unification (UNIF) is a yearly forum for researchers in unification theory and related fields to meet old and new colleagues, to present recent (even unfinished) work, and to discuss new ideas and trends. It is also a good opportunity for young researchers and scientists working in related areas to get an overview of the state of the art in unification theory.

Important Dates

• Submission of titles and abstracts: April 13, 2020
• Submission of full paper: April 20, 2020
• Author notification: May 25, 2020
• Camera-ready papers: June 8, 2020
• UNIF 2020: June 29, 2020

### SC-Square 2020: 5th International Workshop on Satisfiability Checking and Symbolic Computation, call for papers

July 5, 2020, Paris, France

Symbolic Computation is concerned with the efficient algorithmic determination of exact solutions to complicated mathematical problems. Satisfiability Checking has recently started to tackle similar problems but with different algorithmic and technological solutions.

The two communities share many central interests, but researchers from these two communities rarely interact. Also, the lack of common or compatible interfaces for tools is an obstacle to their fruitful combination. Bridges between the communities in the form of common platforms and road-maps are necessary to initiate an exchange, and to support and direct their interaction. The aim of this workshop is to provide an opportunity to discuss, share knowledge and experience across both communities.

The topics of interest include but are not limited to:

• Satisfiability Checking for Symbolic Computation
• Symbolic Computation for Satisfiability Checking
• Applications relying on both Symbolic Computation and Satisfiability Checking
• Combination of Symbolic Computation and Satisfiability Checking tools
• Decision procedures and their embedding into SMT solvers and computer algebra systems

Key Dates

• Submissions: Fri. 10 April 2020
• Notification: Fri. 8 May 2020
• Final version: Fri. 29 May 2020
• Workshop: Sun. 5 July 2020

### Proof Ground 2020 Interactive Proving Contest, call for problems

June 29, 2020, Paris, France

This workshop brings together researchers of the ITP community to compete in a "proving contest".

While programming contests (e.g. ACM ICPC, International Olympiad in Informatics) challenge large numbers of participants to solve algorithmic problems within a short time, we envision proving contests to entice proof engineers to formally prove small but interesting problems from mathematics or computer science.

A [prototype contest system](https://competition.isabelle.systems/) is currently used for teaching and hosting proving contests in Coq, Isabelle, and Lean.

The workshop will be organized around an onsite contest, supplemented with informal discussions.

In order to conduct a stimulating contest we solicit interesting tasks.

A contest typically lasts for two hours and consists of around five problems with varying difficulty.

A problem:

• should contain an informal statement of the problem together with a template for the formal proof;
• should come with a reference solution (in any ITP);
• should be solvable (including formal proof) within 30 minutes;
• should be easy to state in any proof assistant, without requiring too much background library;
• could be from any part of mathematics, software verification, or your daily work with ITPs, and could also be a logic puzzle/riddle;
• could contain several subproblems which lead to partial points.

Submissions from (potential) competition participants are allowed.

Examples can be found at the current "Proving for Fun" contest system, e.g. here.

Submissions can be made via email to Simon Wimmer by the date indicated below.

Important Dates

• Submission deadline: June 1, 2020
• Workshop and Competition: June 27, 2020

### ARQNL 2020: 4th International Workshop on Automated Reasoning in Quantified Non-Classical Logics, call for papers

June 29, 2020, Paris, France

Non-classical logics – such as modal logics, conditional logics, intuitionistic logic, description logics, temporal logics, linear logic, dynamic logic, deontic logics, fuzzy logic, paraconsistent logic, relevance logic, free logic and natural logic – have many applications in AI, Computer Science, Philosophy, Linguistics and Mathematics. Hence, the automation of proof search in these logics is a crucial task.

The ARQNL workshop aims at fostering the development of proof calculi, automated theorem proving systems and model finders for all sorts of quantified, i.e. first- or higher-order, non-classical logics. The workshop will provide a forum for researchers to present and discuss recent developments in this area. These contributions may range from theory to system descriptions and implementations. Contributions may also outline relevant applications, describe problem formalizations, example problems and benchmarks. We welcome contributions from computer scientists, linguists, philosophers, and mathematicians.

Research papers (up to 15 pages), and short papers, talk abstracts, or system demonstrations (up to 8 pages) are solicited. The deadline for submitting papers is April 26th. Proceedings will be published in the CEUR Workshop Proceedings.

### Vampire20: 7th Vampire Workshop, call for papers

July 5, 2020, Paris, France

The Vampire 2020 workshop will address the newest trends in implementing first-order theorem provers, and focus on new challenges and application areas.

Important Dates

• Submission deadline: June 1, 2020
• Notification of acceptance: June 6, 2020
• Final paper submission: September 1, 2020 (tentative)
• Workshop: July 5, 2020
• Post-proceedings publication of the workshop: December 1, 2020 (tentative)

### DeMent 2020: 3rd Deduction Mentoring Workshop, call for participants

June 29, 2020, Paris, France

The DeMent 2020 workshop will provide mentoring and help on career development for young researchers working in automated reasoning, with the overall aim to attract and help them to establish themselves as researchers in automated reasoning. The workshop will address challenges of the academic life and give insight in industrial research. For doing so, the workshop will include talks from leading experts of automated reasoning in academia and industry, and will also include presentations on career-planning.

The workshop aims to reach and attract master students, PhD students and young postdocs as participants.

Important Dates

• Workshop date: June 29, 2020

### SMT 2020: 18th International Workshop on Satisfiability Modulo Theories, call for papers

July 5-6, 2020, Paris, France

The aim of the workshop is to bring together researchers and users of SMT tools and techniques. Relevant topics include but are not limited to:

• Decision procedures and theories of interest
• Combinations of decision procedures
• Novel implementation techniques
• Benchmarks and evaluation methodologies
• Applications and case studies
• Theoretical results
Papers on pragmatic aspects of implementing and using SMT tools, as well as novel applications of SMT, are especially encouraged.

Important Dates

• Abstract registration: March 29, 2020
• Paper submission: April 5, 2020
• Workshop: July 5-6, 2020

## Other Workshops

### WoLLIC 2020: 27th Workshop on Logic, Language, Information and Computation, call for papers

August 4-7, 2020, Lima, Peru

WoLLIC is an annual international forum on inter-disciplinary research involving formal logic, computing and programming theory, and natural language and reasoning. Each meeting includes invited talks and tutorials as well as contributed papers.

Contributions are invited on all pertinent subjects, with particular interest in cross-disciplinary topics. Typical but not exclusive areas of interest are:

• foundations of computing and programming
• novel computation models and paradigms
• broad notions of proof and belief
• proof mining, type theory, effective learnability
• formal methods in software and hardware development
• logical approach to natural language and reasoning
• logics of programs, actions and resources
• foundational aspects of information organization, search, flow, sharing, and protection
• foundations of mathematics
• philosophy of mathematics
• philosophical logic
• philosophy of language.

Important Dates

• April 15, 2020: Full paper deadline
• May 23, 2020: Author notification
• May 30, 2019: Final version deadline (firm)

### WADT 2020: 25th International Workshop on Algebraic Development Techniques, call for abstracts

April 25.-26. 2020, Dublin, Ireland

Collocated with ETAPS 2020.

The algebraic approach to system specification encompasses many aspects of the formal design of software systems. Originally born as a formal method for reasoning about abstract data types, it now covers new specification frameworks and programming paradigms (such as object-oriented, aspect oriented, agent-oriented, logic and higher-order functional programming) as well as a wide range of application areas (including information systems, concurrent, distributed and mobile systems). The workshop will provide an opportunity to present recent and ongoing work, to meet colleagues, and to discuss new ideas and future trends.

Important Dates

• 14.2.2020 Abstract Submission
• 25.4.2020 & 26.4.2020 Workshop
• 19.5.2020 Submission deadline for full papers
• 26.6.2020 Notification on full papers
• 17.7.2020 Camera ready final version of the papers

### GaLoP 2020: 15th Workshop on Games for Logic and Programming Languages, call for papers

April 24-25, 2020, Dublin, Ireland

Collocated with ETAPS 2020.

GaLoP is an annual international workshop on game-semantic models for logics and programming languages and their applications. This is an informal workshop that welcomes work in progress, overviews of more extensive work, programmatic or position papers and tutorials.

Areas of interest include:

• Games and other interaction-based denotational models;
• Games-based program analysis and verification;
• Logics for games and games for logics;
• Algorithmic aspects of game semantics;
• Categorical aspects of game semantics;
• Programming languages and full abstraction;
• Higher-order automata and Petri nets;
• Geometry of interaction;
• Ludics;
• Epistemic game theory;
• Logics of dependence and independence;
• Computational linguistics;
• Games and multi-valued logics.

Important Dates

• Submission: February 14, 2020
• Workshop: April 24-25, 2020

### TEASE-LP 2020: Workshop on Trends, Extensions, Applications and Semantics of Logic Programming, call for contributions

April 25, 2020, Dublin, Ireland

Collocated with ETAPS 2020.

Logic programming is a framework for expressing programs, propositions and relations as Horn clause theories, with the purpose of performing automatic inference in these theories. Horn clause theories are famous for their well-understood declarative semantics, in which models of logic programs are given inductively or coinductively. At the same time, Horn clauses give rise to efficient inference procedures, usually involving resolution. Logic programming found applications in type inference, verification, and AI. While logic programming was originally conceived for describing simple facts, it was extended to account for much more complex theories. This includes higher-order theories, inductive and coinductive data, and stochastic/probabilistic theories.

The aim of this workshop is to bring together researchers that work on extensions of logic programming and inference methods, and to foster an exchange of methods and applications that have emerged in different communities.

Topics
The central idea of this workshop is to discuss the theory of logic programming and associated topics that have as well the goal to automatically infer knowledge and proofs. Our intention is to bring together researchers that work on the numerous topics that contribute to automatic proof inference and foster an exchange that may lead to advances in the theory of logic programming.

Topics of interest include, but are not limited to, the following:

• Proof theory (e.g. focalised and uniform proofs),
• Logic programming beyond the classical Horn clause theories (e.g. coinduction, higher-order Horn clauses, probabilities, categorical logic, inductive LP),
• Extensions of logic programming (e.g. DataLog, description logic, relational programming),
• Advanced implementations (e.g. λProlog, ELPI, miniKanren),
• Type theory (e.g. polarised λ-calculus, proofs-as-programs, types for logic programming),
• Semantics (e.g. classical, categorical, algebraic, coalgebraic) , and Applications.

Important Dates

• Abstract submission Wednesday, 26 February 2020 AoE
• Notification Wednesday, 25 March 2020 AoE
• Camera-ready copy Wednesday, 1 April 2020 AoE
• Workshop Saturday, 25 April 2020

### HCVS 2020: 7th Workshop on Horn Clauses for Verification and Synthesis, call for papers

April 26, 2020, Dublin, Ireland

Collocated with ETAPS 2020.

Many Program Verification and Synthesis problems of interest can be modeled directly using Horn clauses, and many recent advances in the Constraint/Logic Programming, Verification, and Automated Deduction communities have centered around efficiently solving problems presented as Horn clauses.

This workshop aims to bring together researchers working in the communities of Constraint/Logic Programming (e.g., ICLP and CP), Program Verification (e.g., CAV, TACAS, and VMCAI), and Automated Deduction (e.g., CADE), on the topic of Horn clause based analysis, verification and synthesis.

Horn clauses have been advocated by these communities at different times and from different perspectives, and this workshop is organized to stimulate interaction and a fruitful exchange and integration of experiences.

Aims and Scope
Topics of interest include but are not limited to the use of Horn clauses, constraints, and related formalisms in the following areas:

• Analysis and verification of programs and systems of various kinds (e.g., imperative, object-oriented, functional, logic, higher-order, concurrent)
• Program synthesis
• Program testing
• Program transformation
• Constraint solving
• Type systems
• Case studies and tools
• Challenging problems

Important dates

• Paper submission: 26th February 2020
• Paper notification: 25th March 2020
• Workshop: 26th April 2020

### LSFA 2020: 15th Workshop on Logical and Semantic Frameworks, with Applications, call for papers

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.

Topics of Interest:
Topics of interest include, but are not limited to:

• Specification languages and meta-languages
• Formal semantics of languages and logical systems
• Logical frameworks
• Semantic frameworks
• Type theory
• Proof theory
• Automated deduction
• Implementation of logical or semantic frameworks
• Applications of logical or semantic frameworks
• Computational and logical properties of semantic frameworks
• Logical aspects of computational complexity
• Lambda and combinatory calculi
• Process calculi

Important Dates:

• Notification to Authors: May 12
• Proceedings version due: Jun 12
• LSFA 2020: August 26-28

### SR 2020: 8th International Workshop on Strategic Reasoning, call for papers

June 8, 2020, Santiago de Compostela, Spain

Strategic reasoning is a key topic in multi-agent systems research. The extensive literature in the field includes a variety of logics used for modeling strategic ability. Results from the field are now being used in many exciting domains such as information system security, adaptive strategies for robot teams, and automatic players capable to outperform human experts. A common feature in all these application domains is the requirement for sound theoretical foundations and tools accounting for the strategies that artificial agents may adopt in the situation of conflict and cooperation.

The SR international workshop series aims at bringing together researchers working on different aspects of strategic reasoning in computer science, both from a theoretical and a practical point of view.

SR 2020 will be held with ECAI 2020.

Topics ef Interest:
The topics covered by SR include, but are not limited to, the following:

• Logics for reasoning about strategic abilities;
• Logics for multi-agent mechanism design, verification, and synthesis;
• Logical foundations of decision theory for multi-agent systems;
• Strategic reasoning in formal verification;
• Automata theory for strategy synthesis;
• Strategic reasoning under perfect and imperfect information;
• Applications and tools for cooperative and adversarial reasoning;
• Robust planning and optimisation in multi-agent systems;
• Risk and uncertainty in multi-agent systems;
• Quantitative aspects in strategic reasoning.

Important Dates:

• Paper submission: March 13, 2020 (AoE)
• Authors notification: April 15, 2020
• Workshop: June 8, 2020

### SCSS 2020: 9th International Symposium on Symbolic Computation in Software Science, call for papers

September 10-13, 2020, Gammarth, Tunisia

Symbolic Computation is the science of computing with symbolic objects (terms, formulae, programs, representations of algebraic objects etc.). Powerful algorithms have been developed during the past decades for the major subareas of symbolic computation: computer algebra and computational logic. These algorithms and methods are successfully applied in various fields, including software science, which covers a broad range of topics about software construction and analysis.

Meanwhile, artificial intelligence methods and machine learning algorithms are widely used nowadays in various domains and, in particular, combined with symbolic computation. Several approaches mix artificial intelligence and symbolic methods and tools deployed over large corpora to create what is known as cognitive systems. Cognitive computing focuses on building systems which interact with humans naturally by reasoning, aiming at learning at scale.

The purpose of SCSS 2020 is to promote research on theoretical and practical aspects of symbolic computation in software science, combined with modern artificial intelligence techniques.

Scope
SCSS 2020 solicits submissions on all aspects of symbolic computation and their applications in software science, in combination with artificial intelligence and cognitive computing techniques. The topics of the symposium include, but are not limited to the following:

• automated reasoning, knowledge reasoning, common-sense reasoning and reasoning in science
• algorithm (program) synthesis and/or verification, alignment and joint processing of formal, semi-formal, and informal libraries.
• formal methods for the analysis of network and system security
• termination analysis and complexity analysis of algorithms (programs)
• extraction of specifications from algorithms (programs)
• theorem proving methods and techniques, collaboration between automated and interactive theorem proving
• proof carrying code
• generation of inductive assertion for algorithm (programs)
• algorithm (program) transformations
• combinations of linguistic/learning-based and semantic/reasoning methods
• formalization and computerization of knowledge (maths, medicine, economy, etc.)
• methods for large-scale computer understanding of mathematics and science
• artificial intelligence, machine learning and big-data methods in theorem proving and mathematics
• formal verification of artificial intelligence and machine learning algorithms, explainable artificial intelligence, symbolic artificial intelligence
• cognitive computing, cognitive vision, perception systems and artificial reasoners for robotics
• component-based programming
• computational origami
• query languages (in particular for XML documents)
• semantic web and cloud computing

Important Dates

• Title and abstract due: May 8, 2020
• Manuscript due: May 15, 2020
• Author notification: July 6, 2020
• Early registration: July 31, 2020
• Camera ready papers: August 10, 2020
• Conference dates: September 10-13, 2020

## Competitions

### MC 2020: 1st International Competition on Model Counting, call for benchmarks

The 1st International Competition on Model Counting (MC 2020) is a competition to deepen the relationship between latest theoretical and practical development on the various model counting problems and their practical applications. It targets the problem of counting the number of models of a Boolean formula. MC 2020 aims to identify new challenging benchmarks and to promote new solvers for the problem as well as to compare them with state-of-the-art solvers. The MC 2020 follows a direction in the community of constraint solving, where already many competitions have been organized such as on ASP (7 editions), CSP (19 editions), SAT (19 editions), SMT (14 editions), MaxSAT Evaluation (13 editions), QBF (8 editions). MC 2020 invites submission of collections of (weighted) model counting instances in the s tandard DIMACS-based submission formats as given at the competition tracks.

Submission Procedure
A benchmark submission should consist of a single zip or gzipped tar package, containing the instance files and a description of the benchmarks. Please use appropriate file naming conventions, where suited. Ideally, each instance file name should contain a short descriptive part for the problem domain as well as the parameters used for generating the instance as applicable. The benchmark description must be submitted as PDF. The description should include author information with affiliations, a description of the problem domains, a description of the parameters used for generating the instances, and the file name convention. References should be used as appropriate. The benchmark descriptions will be posted on the MC 2020 website. Furthermore, the organizers are considering publishing the collection of system and benchmark descriptions on arxiv.

Please submit benchmarks by email using the subject title "MC 2020 benchmark submission" by March 5, 2020, 23:59 AoE the latest.

## Schools and MOOCs

### MOOCs on Automated Reasoning

Hans Zantema

Two MOOCs (massive open online courses) on Automated Reasoning have been launched at the platform for online courses Coursera. After entering name and email address, they are accessible for free. Only for getting answers on quizzes and getting a certificate afterwards, payed registration is required. Both MOOCs present the material in small video lectures of around 10 minutes each, on an undergraduate level, only some basic knowledge of logic and programming is assumed. The lecturer is prof Hans Zantema from Eindhoven University of Technology.

The first one is Automated Reasoning: satisfiability. It can be accessed via coursera. After a general introduction it consists of 21 video lectures covering both several examples of SAT/SMT and underlying theory (resolution, DPLL, Tseitin transformation, simplex method). It was launched in September 2018; currently it has reached around 1200 participants.

The second one is Automated Reasoning: symbolic model checking. It can also be accessed via coursera. After a general introduction it consists of 16 video lectures on CTL model checking and the underlying BDD technology. It was launched in January 2020.

### Spring School on Theoretical Computer Science (EPIT) – Homotopy Type Theory

May 25th-29th, 2020, Ile d’Oléron, France

The EPIT is a French thematic school proposing, on an yearly basis, an intensive 5-day long training, specializing on a particular topic in theoretical computer science. It is primarily addressed to PhD students, Post-doctoral researchers and junior academics.

The 2020 edition of the EPIT will be centered around Homotopy Type Theory, a research topic at the junction of Computer Science and Mathematics. Our hope is hence to provide an introduction that is accessible to researchers in both areas.

Pre-registration is now open, please visit the registration page to know more.

As the number of places is limited, we have fixed a deadline for pre-registration to March 15, 2020

### MOVEP 2020: 14th Summer School on Modelling and Verification of Parallel Processes

June 22 - 26, 2020, Grenoble, France

MOVEP is a five-day summer school on modelling and verification of infinite state systems. It aims to bring together researchers and students working in the fields of control and verification of concurrent and reactive systems.

MOVEP 2020 will consist of ten invited tutorials. In addition, there will be special sessions that allow PhD students to present their on-going research (each talk will last around 20 minutes). Extended abstracts (2-3 pages) of these presentations will be published in informal proceedings.

Important Dates (AoE)

• Early registration: March 1st 2020
• Submission of abstracts: May 1st 2020

### Sao Paulo School of Advanced Science on Contemporary Logic, Rationality and Information

July 13th to 24th, 2020, Campinas, Brasil

The School, funded by Sao Paulo Research Foundation (FAPESP), celebrates the 90th anniversary of Newton da Costa and aims at:

• Providing an overview of the state-of-art methodology and research on contemporary logic (featuring non-classical logics), rationality and information.
• Attracting qualified candidates to work on research institutions in the State of São Paulo.

The program comprises 9 courses and 9 plenary talks delivered in English by experts in each topic, as well as oral presentations (LED Talks) and poster sessions by the students.

Topics to be covered include:

• History and Philosophy of Paraconsistent Logics
• The Australian, Belgian Brazilian,and Israeli schools on paraconsistency
• Logic and Reasoning
• Logic and Information
• Logic and Argumentation
• Methodological aspects on interpreting, translating and combining logics
• Logic, Probabiity and Artificial Intelligence.

The event will select 100 fully-funded participants (50 grantees from all states of Brazil and 50 international grantees). Funding includes airfare, medical insurance, accommodation and meals throughout the two weeks.

Undergraduate, graduate students and postdoctoral fellows (up to 5 years after completion of the Ph.D) from all countries are encouraged to apply.

## Open Positions

### 10 PhD studentships in Nottingham, UK, for UK/EU applicants

The School of Computer Science at the University of Nottingham is seeking applications for 10 fully-funded PhD studentships for Home/EU students starting on 1st October 2020.

Applicants in the area of the Functional Programming Laboratory are strongly encouraged! If you are interested in applying, please contact a potential supervisor as soon as possible:
• Thorsten Altenkirch - constructive logic, proof assistants, homotopy type theory, category theory, lambda calculus.
• Venanzio Capretta - type theory, mathematical logic, corecursive structures, proof assistants, category theory, epistemic logic.
• Graham Hutton - not taking on any new students this year, but you may find these notes useful.
• Henrik Nilsson - functional reactive programming, domain-specific languages, generalised notions of computation.
These positions are only open to Home/EU applicants.

The studentships are for three and a half years and include a stipend of £15,009 per year and tuition fees. Applicants are normally expected to have a first-class Masters or Bachelors degree in Computer Science or a related discipline, and must obtain the support of a potential supervisor in the School prior to submitting their application. Initial contact with supervisors should be made at least two weeks prior to the closing date for applications.

Eligible successful applicants are expected to apply for a EU VC Scholarship. Informal enquiries may be addressed to Kathrleen Fennemore. To apply, please submit the following items by email to Marc Williams:

1. a copy of your CV, including your actual or expected degree class(es), and results of all University examinations;
2. an example of your technical writing, such as a project report or dissertation;
3. contact details for two academic referees.
4. a research proposal – max 2 x sides A4
You may also include a covering letter but this is optional.

Closing date for applications: Friday 6 March 2020.

### Research Faculty and Postdoctoral Positions in Verification at Virginia Tech, USA

Multiple Research Faculty and Postdoctoral positions are available with the Systems Software Research Group at Virginia Tech on DARPA-funded projects on program analysis and verification. A particular focus of the positions is automated reasoning of unintended, emergent program behaviors (e.g., weird machines) and verifying their non-exploitability. Additional thrusts include verified decompilation and verified recompilation.

Computer science/engineering PhD graduates with a background and publication record in verification, security, or program analysis are sought. Background in theorem proving (e.g., Coq, HOL4, etc), program analysis techniques, low-level system software including assembly code, ISA semantics, and functional programming are highly desirable. The positions have no teaching obligations.

Interested candidates are requested to contact Prof. Binoy Ravindran with a CV or for any questions.

### Ph.D. fellowships at University of Copenhagen, Denmark

The Faculty of Science at the University of Copenhagen offers a considerable number of attractive Ph.D. fellowships with application deadline February 13, 2020.

The Programming Languages and Theory of Computation (PLTC) section at the Department of Computer Science (DIKU) welcomes proposals and applications in all aspects of programming languages and systems, computability and complexity theory. We specifically encourage applications in functional programming language theory, design and implementation technology, type theory, type systems, type-based analysis, inference and synthesis.

We research semantic, logical and algorithmic foundations of computing and programming, in particular functional programming; design and implement novel programming and domain-specific languages for emerging and future computer architectures (GPUs, reversible/quantum computing); research and develop secure, private, scalable and verifiable decentralized systems (including blockchain and distributed ledger systems) and smart contract technology; apply to and derive impetus from a number of computer science (e.g. machine learning, probabilistic programming, computational finance, database systems, and logic) and application domains in collaboration with academic and industrial collaborators.

Requirements are solid, documented programming language theory foundations, a good command of English, and willingness to live in the world's most livable city.

We encourage you to send your academic CV documenting your qualifications for programming languages and systems research to a faculty member of the PLTC section prior to applying for a Ph.D. stipend to align your and our interests.

### PhD and PostDoc positions at Aarhus University

The Department of Computer Science at Aarhus University, Denmark, offers a considerable number of PhD and PostDoc positions in the areas of Logic, Semantics and Programming Languages. Our research spans a wide spectrum of topics concerning models and logics for programming languages and type theories, language-based security, blockchains, theoretical foundations and practical tools for program analysis, formal verification and model checking.

Aarhus University admits PhD students on the basis of a bachelor's degree (for 5 year PhDs) or a master's degree (for 3 year PhDs). If admitted, all tuition is covered, and a generous stipend is provided. Postdoc positions can be for 1 or 2 years, including the possibility of renewal (depending on the individual projects and sources of funding).

Interested applicants at all levels are encouraged to contact the respective faculty for details, enclosing a CV and a short description of interests.

• Aslan Askarov (language-based security, web security, type systems, program analysis)
• Lars Birkedal (higher-order concurrent separation logic, type theory, program verification)
• Bas Spitters (computer aided proofs in cryptography, homotopy type theory, formal verification of blockchains)
• Jaco van de Pol (parallel & symbolic model checking, synthesis, graph games)
• Amin Timany (higher-order concurrent separation logic, proof assistants, type theory, program verification)

• Magnus Madsen (programming language design, functional and logic programming, type systems)
• Anders Møller (static & dynamic program analysis, program analysis and automated testing for web and mobile software)
• Andreas Pavlogiannis (algorithmic & computational foundations of model checking, quantitative verification, static & dynamic analysis, concurrency)

Aarhus University is realizing an ambitious multi-phase digitalization initiative which will help prepare researchers, students and the labour force for the digital transition of the future. The initiative aims at significant expansion of the Department of Computer Science for faculty and students.

Information about the PhD program can be found here.

### TALENT PhD positions at the University of Copenhagen, Denmark

The Faculty of Science at the University of Copenhagen announces 25 PhD openings within the TALENT programme co-funded by EU Horizon 2020, for a range of topics that includes computer science in general, and could well involve the theory and practice of SAT solving, constraint programming, and/or MIP solving in particular.

The deadline for applications is February 13, 2020, and the positions are meant to start in August 2020.

More detailed information can be found on the TALENT PhD positions web page and on the TALENT web page, but briefly, the objective of the TALENT programme is to facilitate early independence of the PhD students and fast-track their careers in academia or industry. TALENT is a unique programme by requesting, as part of the application procedure, the applicants to devise their own interdisciplinary PhD project.

In EU Horizon 2020, the University of Copenhagen is number two in Europe when it comes to attracting Marie-Sklodowska-Curie Actions, and Faculty of Science researchers have received 38 grants from the European Research Council within this program. The Faculty of Science is also host to 6 Centers of Excellence financed by the Danish National Research Foundation, and the Basic Algorithms Research Copenhagen (BARC) center at the CS department is a world-leading centre for fundamental algorithmic research. The PhD School at the Faculty of Science, in which the TALENT PhD students will be enrolled, has over 1,000 students, out of which more than half come from outside of Denmark, originating from 71 different countries.

Informal enquiries are welcome and may be sent to Jakob Nordström.

### Postdoc and PhD positions at Lund University, Denmark on SAT solving and combinatorial optimization

The Department of Computer Science at Lund University invites applications for postdoc and PhD positions focused on SAT solving and combinatorial optimization.

The postdocs and PhD students will be working in the research group of Jakob Nordström, which is currently in transition from KTH to a combined location at Lund University and the University of Copenhagen on either side of the Oresund bridge.

Much of the activities of the research group revolve around the themes of efficient algorithms for satisfiability in propositional logic (SAT solving) and lower bounds on the efficiency of methods for reasoning about SAT (proof complexity). On the practical side, one problem of interest is to gain a better understanding of, and improve, the performance of current state-of-the-art SAT solvers based on conflict-driven clause learning (CDCL). We are even more interested in exploring new algebraic or geometric techniques (such as Groebner bases or pseudo-Boolean solving) that could potentially yield exponential improvements over CDCL. We also believe that there should be ample room for technology transfer with related areas such as SMT solving, constraint programming (CP), and/or mixed integer linear programming (MIP), and so the research project will likely involve such areas.

The application deadline is February 10, 2020. See here and here for the full announcements with more information and instructions how to apply. Informal enquiries are welcome and may be sent to Jakob Nordström.

### Tenured positions at Inria and UGA

There are currently several open/competitive positions in the Tyrex research team which is a joint team between Inria and CNRS and UGA and Grenoble-INP local universities. In the Tyrex team, we investigate data-centric programming techniques to facilitate information and knowledge extraction, from database, programming languages and data analytics perspectives.

This includes, but is not limited to, a range of topics, including the design of domain specific programming languages together with their foundations (e.g., type systems, algebras, language design, synthesis of distributed programs), large scale and distributed data management (query optimization, graph management and information extraction from raw data), data science and artificial intelligence and knowledge extraction and inference (machine learning on and with property and knowledge graphs, predictive analytics, combined reasoning and learning from symbolic and numerical data).

A variety of positions are available at different levels:

• Permanent (tenured) researcher positions at Inria
• Faculty positions (tenured): assistant professor (``Maitre de conference’’) at local universities (UGA, ENSIMAG and IAE), and one professor (tenured) position at UGA
• Post-doc positions
• PhD positions
• Research engineer positions
The Tyrex research team is located at the Inria Grenoble Rhône-Alpes research center, next to Grenoble, France. Interested applicants are invited to contact Pierre Geneves by email for details.

### Senior Postdoc / Project Coordinator position in Information Security and Program Verification at ETH Zurich, Switzerland

The Institute of Information Security (the groups of Prof. Adrian Perrig and Prof. David Basin) and the Programming Methodology Group (Prof. Peter Müller) at ETH Zurich are hiring a Postdoc in a large research project in the area of digital trust. The goal of this project is to develop a comprehensive, formally verified security architecture for communication in the physical and digital world. In particular, the project will develop protocols to transfer physical trust relationships into the digital world and store, manage, and use them. The design will take into account human (mis-)behavior from the outset. A particular emphasis is on the formal verification of the architecture both at the design and implementation level to rule out any undesired behavior.

We are looking for enthusiastic and outstanding postdoctoral researchers with a strong background in some of the following topics:

• formal modeling and verification,
• program verification,
• theorem proving, model checking,
• cryptographic protocols,
• public-key infrastructure, identity management, authentication,
• networking and distributed systems, and
• design and implementation of security architectures.

In addition to research, the responsibilities of the position include project management, in particular, coordination among the involved research groups, lightweight reporting to the funding agency, and outreach to potential industrial users of the developed solutions.

All candidates matching the profile above are encouraged to apply as soon as possible. We will process applications until all positions are filled. Successful candidates are expected to start soon after acceptance, but the starting date is negotiable.

Applications should include:

• a curriculum vitae,
• a brief description of research interests, and
• letters of recommendation.
Applications and inquiries should be sent to Christoph Sprenger and Sandra Schneider by email.

Postdocs are paid employees of ETH Zurich. Salary and employment conditions are attractive. Zurich is a diverse and multicultural city which is consistently rated among the best cities in the world in which to live.

## Counting of the Ballots of the CADE Trustee Elections

Philipp Rümmer

An election was held to fill 4 positions. Maria Paola Bonacina, Pascal Fontaine, Laura Kovacs, Aart Middeldorp, Renate Schmidt, and Christoph Weidenbach were nominated. 83 valid ballots were returned. Therefore, in each iteration of the single transferrable vote algorithm described in the CADE Bylaws, a candidate is elected if she or he gets at least 42 first preference votes. Otherwise, the votes of the candidate with the least first preference votes are redistributed.

The following table reports the initial distribution of preferences among the candidates:

 Candidate 1st pref. 2nd pref. 3rd pref. 4th pref. 5th pref. 6th pref. no supp. Maria Paola Bonacina 12 12 11 10 8 13 17 Pascal Fontaine 20 21 16 9 11 2 4 Laura Kovacs 10 12 16 23 7 7 8 Aart Middeldorp 10 11 10 12 13 15 12 Renate Schmidt 6 12 15 15 13 12 10 Christoph Weidenbach 25 14 12 5 11 8 8

No candidate reaches at least 42 first preference votes.

By redistributing the votes of Renate Schmidt, one gets the following table:

 Candidate 1st pref. 2nd pref. 3rd pref. 4th pref. 5th pref. no supp. Maria Paola Bonacina 15 12 16 6 17 17 Pascal Fontaine 21 25 14 17 2 4 Laura Kovacs 10 14 24 20 7 8 Aart Middeldorp 11 13 12 13 22 12 Christoph Weidenbach 26 17 12 11 9 8

No candidate reaches at least 42 first preference votes.

By redistributing the votes of Laura Kovacs, one gets the following table:

 Candidate 1st pref. 2nd pref. 3rd pref. 4th pref. no supp. Maria Paola Bonacina 16 17 16 17 17 Pascal Fontaine 25 27 23 4 4 Aart Middeldorp 13 14 20 24 12 Christoph Weidenbach 29 23 10 13 8

No candidate reaches at least 42 first preference votes.

By redistributing the votes of Aart Middeldorp, one gets the following table:

 Candidate 1st pref. 2nd pref. 3rd pref. no supp. Maria Paola Bonacina 21 18 27 17 Pascal Fontaine 30 35 14 4 Christoph Weidenbach 32 24 19 8

No candidate reaches at least 42 first preference votes.

By redistributing the votes of Maria Paola Bonacina, one gets the following table:

 Candidate 1st pref. 2nd pref. no supp. Pascal Fontaine 43 36 4 Christoph Weidenbach 38 37 8

Now, Pascal Fontaine reaches at least 42 first preference votes, and is elected.

To find the next elected candidate, we redistribute the votes of Pascal Fontaine and get the following table:

 Candidate 1st pref. 2nd pref. 3rd pref. 4th pref. 5th pref. no supp. Maria Paola Bonacina 12 21 8 12 13 17 Laura Kovacs 13 19 25 11 7 8 Aart Middeldorp 14 11 17 14 15 12 Renate Schmidt 10 18 16 15 14 10 Christoph Weidenbach 33 13 8 13 8 8

No candidate reaches at least 42 first preference votes.

By redistributing the votes of Renate Schmidt, one gets the following table:

 Candidate 1st pref. 2nd pref. 3rd pref. 4th pref. no supp. Maria Paola Bonacina 17 21 11 17 17 Laura Kovacs 14 27 25 9 8 Aart Middeldorp 16 15 18 22 12 Christoph Weidenbach 35 16 15 9 8

No candidate reaches at least 42 first preference votes.

By redistributing the votes of Laura Kovacs, one gets the following table:

 Candidate 1st pref. 2nd pref. 3rd pref. no supp. Maria Paola Bonacina 20 28 18 17 Aart Middeldorp 19 25 27 12 Christoph Weidenbach 43 19 13 8

Now, Christoph Weidenbach reaches at least 42 first preference votes, and is elected.

To find the next elected candidate, we redistribute the votes of Christoph Weidenbach and get the following table:

 Candidate 1st pref. 2nd pref. 3rd pref. 4th pref. no supp. Maria Paola Bonacina 21 17 12 16 17 Laura Kovacs 24 24 18 9 8 Aart Middeldorp 18 22 16 15 12 Renate Schmidt 19 15 22 17 10

No candidate reaches at least 42 first preference votes.

By redistributing the votes of Aart Middeldorp, one gets the following table:

 Candidate 1st pref. 2nd pref. 3rd pref. no supp. Maria Paola Bonacina 26 19 21 17 Laura Kovacs 33 26 16 8 Renate Schmidt 22 26 25 10

No candidate reaches at least 42 first preference votes.

By redistributing the votes of Renate Schmidt, one gets the following table:

 Candidate 1st pref. 2nd pref. no supp. Maria Paola Bonacina 36 30 17 Laura Kovacs 43 32 8

Now, Laura Kovacs reaches at least 42 first preference votes, and is elected.

To find the next elected candidate, we redistribute the votes of Laura Kovacs and get the following table:

 Candidate 1st pref. 2nd pref. 3rd pref. no supp. Maria Paola Bonacina 26 21 19 17 Aart Middeldorp 27 27 17 12 Renate Schmidt 27 24 22 10

No candidate reaches at least 42 first preference votes.

By redistributing the votes of Maria Paola Bonacina, one gets the following table:

 Candidate 1st pref. 2nd pref. no supp. Aart Middeldorp 41 30 12 Renate Schmidt 39 34 10

No candidate reaches at least 42 first preference votes.

By redistributing the votes of Renate Schmidt, one gets the following table:

 Candidate 1st pref. no supp. Aart Middeldorp 71 12

Now, Aart Middeldorp reaches at least 42 first preference votes, and is elected.

To summarize, the 4 candidates elected are Pascal Fontaine, Christoph Weidenbach, Laura Kovacs, and Aart Middeldorp.