Association for Automated Reasoning

Newsletter No. 120
June 2017

From the AAR President, Larry Wos

As I sit at the computer, I imagine that at least some of you who read this column spend some research time wondering about what might be termed theoretical problems in automated reasoning. Indeed, some may be wondering about challenges that do not focus on a specific theorem, puzzle, or problem but, instead, focus on a general problem -- a problem that, if solved, would add to the power of various reasoning programs. Well, late though it may be, I offer you such a challenge.

Although the power offered by today's computer is indeed impressive compared with that offered thirty years ago, twenty years ago, and even ten years ago, far more is needed. I am not speaking of computational power, however. Rather, I am referring to the need for strategies.

When the set of support strategy was formulated around 1963, its use brought into range proofs that had been out of our reach at Argonne National Laboratory. Decades later, the introduction of the hot list strategy -- the focus in this column -- played a key role in enabling our group to obtain new proofs, some of which were surprisingly elegant.

Briefly, the hot list strategy enables the researcher to include in a so-called hot list clauses that are conjectured to merit repeated and immediate visiting to complete the application of an inference rule (rather than initiate it) when the program has decided to retain a new clause.

Definition: initial and extended hot list. The initial hot list is a (possibly empty) set of clauses (or their equivalent) selected by the researcher and included in the input. The initial hot list can be extended by adjoining new members to it during a run. Each member of the hot list (initial and extended) is eligible for automatic and immediate consideration to complete applications of the inference rules in use, with the requirement that the application of one of those inference rules be initiated by focusing on a clause (or its equivalent) that the program has decided to retain. In particular, no inference rule is permitted to apply to a set of clauses all of which are members of the hot list. An example is in order.

Consider the theorem in ring theory that asserts the provability of commutativity (of multiplication) when the ring satisfies the property that the cube of x, for every x, is x itself. If I had a program that offered the hot list strategy and I was seeking a proof of this theorem, I would place in the hot list xxx = x. I would assign the heat parameter the value 1. When the program decided to retain a new conclusion, before anything else (intuitively), the program would consider applying to the new conclusion and xxx = x whatever inference rule was in use (typically paramodulation). If the value 2 was assigned to the heat parameter, then any conclusions drawn via the preceding comment would immediately be considered, again, with xxx = x.

Bill McCune made two significant contributions to the hot list strategy. The first was his development of the dynamic hot list strategy, which allows the program to adjoin new items to the hot list during the run. McCune also programmed the strategy to apply to any inference rule in use, not just to paramodulation, which was my original formulation.

Now, especially for those interested in general questions, I offer the following challenge. Given a formulation of some specific theorem or assignment, which elements (clauses, for example) are wisely placed in the initial hot list? For one possibility, should items placed in the initial hot list always be unit clauses? For another, should such items always be free of variables? Should items that correspond to the denial of the theorem be the only elements in the initial hot list, or should they be kept off this list? I leave to you other possibilities. I note from recent experiments that placing unwise choices in the initial hot list can use CPU time unprofitably.

For a second challenge, what criteria should be used to enable the program to rely on the dynamic hot list strategy? The way OTTER applies the dynamic version is for the user to assign a weight, or threshold, in the input such that any newly retained conclusion whose weight is less than or equal to this assignment is automatically adjoined to the hot list.

If you glance at the literature in abstract algebra, you might indeed see what amounts to a manifestation of the use of the hot list strategy by mathematicians. For example, various proofs of the cited theorem from ring theory repeatedly rely, for deduced steps, on the use of the so-called special hypothesis, xxx = x. For a radically different bit of evidence of the possible value of the hot list strategy, I note that in some of my rather recent research focusing on the Meredith single axiom for classical propositional calculus -- an axiom that played a prominent role in a recent column -- a glance at some of the resulting proofs show that sometimes one-fourth of the deduced steps relied on the same formula, namely, the Meredith single axiom. Therefore, placing the Meredith single axiom in the initial hot list with, say, an assignment of the value 1 to heat would indeed merit experimentation. For a third bit of evidence, in Tarskian geometry, I tried two experiments that differed only in that the first relied on the hot list strategy while the second did not. The first found a proof; the second did not.

One more illustration will prove beneficial. Assume that you are using hyperresolution as the only inference rule. Further, assume you are interested in an area of logic that relies solely on condensed detachment, the following in clause form. (The symbol " | " denotes logical or, and the symbol "-" denoted logical not.) 

-P(i(x,y)) | -P(x) | P(y).
Assume that you conjecture that the hot list is to be used and that you plan to place in that list the three axioms of the area under study. Given these assumptions, you had best also include the given clause for condensed detachment. When a new formula is accepted for retaining, before anything else occurs, that new formula will be considered with a member of the hot list and, because of condensed detachment, will be considered with hyperresolution and the given clause. Without the inclusion in the hot list of the given clause, the hot list will not come into play because the study is based on the sole use of condensed detachment.

I welcome your ideas regarding possibly powerful choices for members of the initial hot list or for criteria for adjoining dynamically (in the context of the dynamic hot list strategy) to this list.

Guest Column: An Automatic Reasoning Challenge

Christoph Weidenbach, President of CADE Inc.

In 1996 Bill McCune proved the Robbins Conjecture, the equivalence between a Boolean algebra and a Robbins algebra. The formalization of the Robbins Conjecture is a problem in first-order logic with equality. Bill designed a specific version of Otter, called EQP, to fit exactly this problem. He worked several years on it. He put together all available theorem proving technology of this time, including AC theory unification, basic superposition, knowing that the resulting calculus and implementation was highly incomplete. Him eventually finding a proof for the Robbins Conjecture is attributed to his genius in designing automatic theorem provers, his insistence, his devotion to high risk research, and, of course, luck. Had the Robbins conjecture been wrong, he would have failed because there is no way that EQP would have found a counter-example to the conjecture.

In 2016 Marijn Heule, Oliver Kullmann, and Victor W. Marek solved the Pythagorean Triples Problem by providing a counter-example. The problem asks whether it is possible to color the natural numbers by two colors red and blue, such that all natural numbers x, y, z satisfying x2 + y2 = z2 do not have assigned the same color. By educated guessing, they assumed that the interval between 1 and 7825 is sufficiently large to find a counter-example. Then they did a careful encoding of all potential solutions in this interval in propositional logic. The problem was far to large to be solvable by a single SAT solver instance. So they found a genius way of breaking it into not too many pieces, where each piece is solvable by a single SAT solver instance in a reasonable amount of time. Knowing the average solution time for each piece and the number of pieces, they were able to safely estimate the overall time to establish the counter-example, or finding that the Pythagorean Triples Problem has a solution in the interval. Had the Pythagorean Triples Problem been solvable in general, there is no way that their disproving attempt could have actually proven it.

The challenge is to develop automated reasoning procedures that can at the same time prove and disprove a conjecture. Proving a conjecture amounts to finding a proof for the conjecture. Disproving a conjecture amounts to finding a counter-model to the conjecture. For first-order logic, the representation of models during proof search is still in a very early stage. A general proof of solvability of the Pythagorean Triples Problem would require automatic reasoning in second-order logic modulo the theory of non-linear arithmetic over the naturals. Very little is known as to how this logic can be automatized.

Logics, where the people from our community have developed automatic reasoning procedures to simultaneously search for a counter-example, represented by a model, and a proof are typically decidable, such as propositional logic (SAT) or propositional logic modulo theories (SMT). It has proven that the simultaneous search for finding both proofs and models is beneficial to the automation of both. A future challenge is to improve the existing procedures and to extend the ideas to more expressive logic fragments. A natural next candidate logic could be a first-order fragment modulo theories, where the first-order part includes arbitrarily quantified variables restricted to a finite domain. Automatic reasoning advances on such a fragment would have a great impact on many areas in automated reasoning and also support future attacks to open problems such as the above solutions to the Robbins Conjecture and Pythagorean Triples Problem.

Announcement of the 2017 Herbrand Award

Christoph Weidenbach, President of CADE Inc.

The 2017 Herbrand Award for distinguished contributions to automated reasoning will be presented to Lawrence C. Paulson for his pioneering contributions to the automation in proof assistants and the foundations of formal security protocol verification as well as his impressive formalizations of deep mathematical theories.

Call for Nominations: CADE Trustees Election

Martin Giese, Secretary of AAR and CADE

The affairs of CADE are managed by its Board of Trustees. This includes the selection of CADE (IJCAR) co-chairs, the selection of CADE venues, electing Herbrand award winners, instituting new awards, etc.

Nominations for three CADE trustee positions are being sought, in preparation for the elections to be held after CADE-26.

The current members of the board of trustees are (in alphabetical order):

The terms of Pascal Fontaine, Jürgen Giesl, and Geoff Sutcliffe end. Geoff Sutcliffe has served for two consecutive terms, and therefore cannot be nominated for a third term. Pascal Fontaine and Jürgen Giesl can be nominated for a second term.

The term of office of Leonardo de Moura as CADE-26 program chair also ends; he is replaced by IJCAR 2018 program co-chair Stephan Schulz. As outgoing ex-officio trustee, Leonardo de Moura is eligible to be nominated as elected trustee.

In summary, we are seeking to elect three trustees.

Nominations can be made by any AAR member, either by e-mail or in person at the CADE business meeting at CADE-26 in Gothenburg. Two members, a principal nominator and a second, are required to make a nomination, and it is their responsibility to ask people's permission before nominating them. A member may nominate or second only one candidate. Nominees must be AAR members. For further details please see the CADE Inc. bylaws at the CADE web site.

E-mail nominations are to be sent to Christoph Weidenbach, CADE President, and Martin Giese, CADE Secretary, up to the upcoming CADE business meeting.

First Call for Proposals for Sites for CADE-27 in 2019

Christoph Weidenbach, President of CADE Inc. and Martin Giese, Secretary of AAR and CADE

We invite proposals for sites around the world to host the international Conference on Automated Deduction (CADE) to be held in summer 2019. CADE typically merges into IJCAR (the International Joint Conference in Automated Reasoning) in even years, and meets as an independent conference in odd years. For odd years, both proposals to host CADE alone or CADE co-located with other conferences are welcome. CADE's/IJCAR's recent location history is as follows:

The upcoming CADE/IJCAR events will be:

The final deadline for proposals will be 30 October 2017 and final selection of the site will be made within two months after the proposal due date. A detailed call for proposals will be published after CADE-26. If you are interested in hosting CADE-27, preferably outside Europe, please get in touch with Martin Giese, CADE Secretary or Christoph Weidenbach, CADE President, for further information.

Special Issues

Special Issue of Mathematical Structures in Computer Science in Celebration of the Sixtieth Birthday of Dale Miller, call for Papers

Papers are invited to a special issue of Mathematical Structures in Computer Science, a journal published by Cambridge University Press. This special issue is being collated in celebration of the sixtieth birthday of Professor Dale Miller. To be appropriate for this collection, papers must be broadly related to one or more of the areas that have been spanned by the work of Professor Miller to-date. These areas include structural proof theory, proof search and computation, foundations of logic programming, higher-order unification, reasoning about relational specifications and certification of proofs. This list is meant to be illustrative and is not exhaustive; if you are interested in submitting a paper and would like to ascertain its relevance to the theme of the special issue, please feel free to contact the editors of the issue.

Papers that are submitted for consideration of publication must be prepared in LaTeX and should use the MSCS style file that can be downloaded from ftp.cup.cam.ac.uk. Please also follow the layout and other manuscript format related instructions with the exception of double spacing that you will find here. Manuscripts should also be limited to about 25 pages. While this is not a hard constraint, the reason why a paper exceeds this limit must be apparent to the editors from an inspection of its content, else it may be declined without review.

To submit a manuscript to the special issue, please use the ScholarOne site for MSCS. Once you are at this site, you will need to create an account if you do not have one already. Once you are logged in, select the "Author" tab and follow the instructions. At the end of the page, under the "Special Issue" heading, select "Miller Festschrift" prior to submission. Please note that at this stage we will need only a PDF file prepared as indicated above. The LaTeX source will be required after the manuscript has been accepted.

Conferences: Calls for Workshops

FLoC 2018: The 2018 Federated Logic Conference, call for workshops

6-19 July 2018, Oxford, UK

The Seventh Federated Logic Conference (FLoC 2018) will host the following nine conferences and affiliated workshops. Researchers and practitioners are invited to submit proposals for workshops on topics in the field of computer science, related to logic in the broad sense. Each workshop proposal must indicate one affiliated conference of FLoC 2018.

Important Dates:

For more information, see the Workshop Guidelines page.

Conferences: Calls for Papers

LOPSTR 2017: 27th International Symposium on Logic-Based Program Synthesis and Transformation, call for papers

October 10 - 12, 2017, University of Namur, Namur, Belgium

Important dates:

The aim of the LOPSTR series is to stimulate and promote international research and collaboration on logic-based program development. LOPSTR is open to contributions in logic-based program development in any language paradigm. LOPSTR has a reputation for being a lively, friendly forum for presenting and discussing work in progress. Formal proceedings are produced only after the symposium so that authors can incorporate this feedback in the published papers.

Topics of interest cover all aspects of logic-based program development, all stages programming-in-the-small and programming-in-the-large. Both full papers and extended abstracts describing applications in these areas are especially welcome. Contributions are welcome on all aspects of logic-based program development, including, but not limited to:

For more information see the conference website.

GCAI 2017: Global Conference on Artificial Intelligence, call for papers

18-22 October 2017, Miami, USA

The 3rd Global Conference on Artificial Intelligence (GCAI 2017) will be held in Miami, USA, at the Courtyard Marriott hotel in Coconut Grove, 18-22 October 2017. The conference, which addresses all aspects of artificial intelligence, is being organized by LRG and the University of Miami. The program chairs are Christoph Benzmueller, Christine Lisetti and Martin Theobald. The conference chair is Geoff Sutcliffe.

Topics include:

Important Dates:

For information about the submission process, see the conference website.

MACIS 2017: 7th International Conference on Mathematical Aspects of Computer and Information Sciences, call for papers

November 15-17, 2017 Vienna, Austria

MACIS is a series of biennial conferences focusing on research in mathematical and computational aspects of computing and information science. MACIS 2017 will feature invited presentations and a selective four-track program of contributed papers describing original and unpublished research.

Tracks of the conference are:

Important Dates:

For information about the submission process, see the conference website.

SBMF 2017: 20th Brazilian Symposium on Formal Methods, call for papers

27th of November to 1st of December 2017, Recife, Pernambuco, Brazil

SBMF 2017 is the twentieth of a series of events devoted to the development, dissemination and use of formal methods for the construction of high-quality computational systems. It is now a well-established event, with an international reputation. In 2017, SBMF will take place in Recife, the capital of the state Pernambuco, which is located in the northeast Brazil. It is the 9th city by population in Brazil, with over 1.5 million inhabitants, and it receives more than 5 million tourists from Brazil and abroad per year.

Topics include:

Important Dates:

For information about the submission process, see the conference website.

NCMPL 2017: Non-classical Modal and Predicate Logics, call for papers

December 4-7 2017, Guangzhou, China

The international conference on Logic and Cognition is held once every year since 2001. It is sponsored and organized by Institute of Logic and Cognition, which is one of the key research institutes of humanities and social sciences in Universities affiliated to the Chinese Ministry of Education. The 8th conference will be held in Guangzhou in December 2017. The topic of the conference is Non-classical Modal and Predicate Logics.

Topics include:

Important Dates:

For information about the submission process, see the conference website.

CPP 2018: 7th ACM SIGPLAN International Conference on Certified Programs and Proofs, call for papers

8-9 January 2018, Los Angeles, USA

Certified Programs and Proofs (CPP) is an international forum on theoretical and practical topics in all areas, including computer science, mathematics, and education, that consider certification as an essential paradigm for their work. Certification here means formal, mechanized verification of some sort, preferably with production of independently checkable certificates.

Topics
Submissions in research areas related to formal certification of programs and proofs are welcome:

Important Dates:

For information about the submission process, see the conference website.

Conferences: Calls for Participation

TFP 2017: 18th Symposium on Trends in Functional Programming, call for participation

19-21 June, 2017, Canterbury, UK

The symposium on Trends in Functional Programming (TFP) is an international forum for researchers with interests in all aspects of functional programming, taking a broad view of current and future trends in the area. It aspires to be a lively environment for presenting the latest research results, and other contributions (see below). Authors of draft papers will be invited to submit revised papers based on the feedback receive at the symposium. A post-symposium refereeing process will then select a subset of these articles for formal publication.

TFP 2017 will be the main event of a pair of functional programming events. TFP 2017 will be accompanied by the International Workshop on Trends in Functional Programming in Education (TFPIE), which will take place on 22 June.

For information about registration, see the registration page.

LPNMR 2017: 14th International Conference on Logic Programming and Nonmonotonic Reasoning, call for participation

July 3-6, 2017, Hanasaari, Espoo, Finland

LPNMR 2017 is the fourteenth in the series of international meetings on logic programming and non-monotonic reasoning. LPNMR is a forum for exchanging ideas on declarative logic programming, non-monotonic reasoning, and knowledge representation. The aim of the conference is to facilitate interactions between researchers and practitioners interested in the design and implementation of logic-based programming languages and database systems, and those working in knowledge representation and nonmonotonic reasoning. LPNMR strives to encompass theoretical and experimental studies that have led or will lead to advances in declarative programming and knowledge representation, as well as their use in practical applications. This edition of LPNMR will feature several workshops and a special session dedicated to the 7th ASP Competition. A Doctoral Consortium will also be a part of the program.

For information about registration, see the registration webpage.

CAV 2017: 29th International Conference on Computer-Aided Verification, call for participation

22-28 July 2017, Heidelberg, Germany

CAV 2017 is the 29th in a series dedicated to the advancement of the theory and practice of computer-aided formal analysis methods for hardware and software systems. The conference covers the spectrum from theoretical results to concrete applications, with an emphasis on practical verification tools and the algorithms and techniques that are needed for their implementation. Along with the main conference, CAV will feature eight workshops (including a special workshop in honor of David Dill) and tutorials.

Important Dates:

For information about registration, see the registration website.

VSTTE 2017: 9th Working Conference on Verified Software: Theories, Tools, and Experiments, call for participation

July 22-23, 2017, Heidelberg, Germany

The goal of the VSTTE conference series is to advance the state of the art in the science and technology of software verification, through the interaction of theory development, tool evolution, and experimental validation. VSTTE 2017 is co-located with CAV.

Important Dates:

For information about registration, see the conference website.

CADE 2017: 26th International Conference on Automated Deduction, call for participation

6-11 August 2017, Gothenburg, Sweden

The conference on Automated Deduction (CADE) is the major international forum at which research on all aspects of automated deduction is presented. The first conference was held in 1974, with this year's conference being the 26th CADE. Early CADEs were mostly biennial, and annual conferences started in 1996. The CADE conference series is managed by CADE Inc. which is a subcorporation of the Association for Automated Reasoning (AAR).

Important Dates:

For information about registration, see the registration website.

Logic in Stockholm 2017, call for participation

August 7-25 2017, Stockholm, Sweden

There will be a series of logic-related events in Stockholm in August 2017, including in particular:

For information about registration, see the website.

FSCD 2017: Second International Conference on Formal Structures for Computation and Deduction, call for participation

4-7 September 2017, Oxford, UK

FSCD covers all aspects of formal structures for computation and deduction from theoretical foundations to applications. Building on two communities, RTA (Rewriting Techniques and Applications) and TLCA (Typed Lambda Calculi and Applications), FSCD embraces their core topics and broadens their scope to closely related areas in logics, proof theory and new emerging models of computation such as quantum computing or homotopy type theory. FSCD 2017 is organised in cooperation with the ACM SIGLOG and SIGPLAN and co-located with ICFP 2017.

For information about registration, see the registration page.

Workshops

DL 2017: 30th International Workshop on Description Logics, call for participation

July 18-21 2017, Montpellier, France

The DL workshop is the major annual event of the Description Logic research community. It is the forum at which those interested in description logics, both from academia and industry, meet to discuss ideas, share information and compare experiences. In 2017, the DL workshop will be held in Montpellier from July 18th to July 21st. As 2017 marks the 30th anniversary of the event, we look forward to a strong turnout, with established researchers, students, and newcomers to the area coming together to reflect on the advances and successes of DL research and the challenges for the future.

For the programme and information about registration, see the workshop website.

CICLOPS 2017: 15th International Colloquium on Implementation of Constraint and LOgic Programming Systems, call for papers

28th August 2017 Melbourne, Australia

Co-located with ICLP'17, CP'17, and SAT'17.

This workshop aims at discussing and exchanging experience on the design, implementation, and optimization of logic, constraint (logic) programming systems, and other systems based on logic as a means to express computations. Experience backed up by real implementations and their evaluation will be given preference, as well as descriptions of work in progress in that direction.

Topics include:

Important Dates:

For information about the submission process, see the workshop website.

WFLP 2017: 25th International Workshop on Functional and Logic Programming and 31st Workshop on (Constraint) Logic Programming, call for papers

September 19-22, 2017, Wuerzburg, Germany

Part of Declare 2017 - Conference on Declarative Programming

WFLP 2017 is the combination of two workshops of a successful series of annual workshops on declarative programming. The international workshops on functional and logic programming aim at bringing together researchers interested in functional programming, logic programming, as well as their integration. The workshops on (constraint) logic programming serve as the scientific forum of the annual meeting of the Society of Logic Programming (GLP e.V.) and bring together researchers interested in logic programming, constraint programming, and related areas like databases, artificial intelligence, and operations research.

In this year both workshops will be jointly organized and collocated with the 21st International Conference on Applications of Declarative Programming and Knowledge Management (INAP 2017) and the Summer School on Advanced Concepts for Databases and Logic Programming under the umbrella of the conference on Declarative Programming (Declare 2017) in order to promote the cross-fertilizing exchange of ideas and experiences among researchers and students from the different communities interested in the foundations, applications, and combinations of high-level, declarative programming languages and related areas. The technical program of the workshop will include invited talks, presentations of refereed papers and demo presentations.

Topics include:

Important Dates:

For information about the submission process, see the workshop website.

EPS: Encyclopedia of Proof Systems, call for contributions

September 24-25, 2017, Brasilia, Brazil

Affiliated to Tableaux, FroCoS and ITP 2017.

Aims and Scope
The Encyclopedia of Proof Systems was created in 2014 with the goal of being a quick reference for the various proof systems used by logicians. Since then, it has collected 64 entries on various logics and calculi. This was only possible due to the collaboration of many members of the logic community.

This event aims to promote the encyclopedia and attract more contributions and collaborators. It consists of:

The activities planned for this meeting will be announced closer to the event.

Submission Instructions
Please visit the encyclopaedia's website for instructions.

Participation in TABLEAUX, FroCoS or ITP is not required for submission, but is strongly encouraged.

Important Dates

Workshop DaLí - Dynamic Logic: new trends and applications, call for papers

24 September, 2017, Brasília, Brazil

Co-located with FroCoS, Tableaux and ITP 2017.

Topics
We invite submissions on the general field of Dynamic Logic, its variants and applications, including, but not restricted to:

Informations about submissions and publications can be found on the workshop's website.

Important Dates:

LSFA'17: 12th Workshop on Logical and Semantic Frameworks, with Applications, call for papers

23-24 September 2017, Brasília, Brazil

Satellite event of Tableaux, FroCoS and ITP 2017.

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.

LSFA 2017 aims to be a forum for presenting and discussing work in progress, and therefore to provide feedback to authors on their preliminary research. The proceedings are produced after the meeting, so that authors can incorporate this feedback in the published papers.

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

Submission And Publication:

informations about the submission requirements and publication process can be found on the workshop's website.

WPTE 2017: Fourth International Workshop on Rewriting Techniques for Program Transformations and Evaluation, call for papers

8 September, 2017, Oxford, UK

affiliated with FSCD 2017

Aims and Scope:
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.

Topics of interest in the scope of this workshop include:

The programming languages of interest include pure, deterministic, impure, nondeterministic, concurrent, parallel languages, and may employ programming paradigms such as functional, logical, typed, imperative, object-oriented, and higher-order.

Important Dates:

For more information such as paper submission process and program committee, see the workshop's website.

Workshop on Formal Verification of Autonomous Vehicles, call for papers

19th September 2017, Turin, Italy

co-located with iFM 2017

Important Dates:

Objectives and Scope:
Incorporating formal methods into the design of autonomous vehicles presents significant new challenges, particularly due to the complex integration of discrete and continuous controllers. The main challenges associated with the formal design of autonomous vehicles includes modelling, specification, verification and synthesis.

The aim of this workshop is to bring together researchers from the formal verification community that are developing formal methods for autonomous vehicles and industrial researchers working, e.g., in the area of control theory or robotics, interested in applying verification techniques for designing and developing of autonomous vehicles.

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

for more information such as submission guidelines, see the workshop's website.

PxTP 2017: The Fifth International Workshop on Proof eXchange for Theorem Proving, call for papers

23-24 September 2017, Brasilia, Brazil

associated with the Tableaux, FroCoS and ITP conferences

Background:
The PxTP workshop brings together researchers working on various aspects of communication, integration, and cooperation between reasoning systems and formalisms.

Topics:
Topics of interest for this workshop include all aspects of cooperation between reasoning tools, whether automatic or interactive. More specifically, some suggested topics are:

Important Dates:

For information about the submission process, see the workshop's website.

3rd Workshop on Connexive Logics, call for papers

September 7th, 2017, Kyoto, Japan

Description:
Modern connexive logic started in the 1960s with seminal papers by Richard B. Angell and Storrs McCall. Connexive logics are orthogonal to classical logic insofar as they validate certain non-theorems of classical logic, namely

Aristotle's Theses: 

~(~A=3D>A), ~(A=3D>~A)
Boethius' Theses: 
(A=3D>B)=3D>~(A=3D>~B), (A=3D>~B)=3D>~(A=3D>B)

Systems of connexive logic have been motivated by considerations on a content connection between the antecedent and succedent of valid implications and by applications that range from Aristotle's syllogistic to Categorial Grammar and the study of causal implications. Surveys of connexive logic can be found in:

S. McCall, "A History of Connexivity", in D.M. Gabbay et al. (eds.), Handbook of the History of Logic. Volume 11. Logic: A History of its Central Concepts, Amsterdam, Elsevier, 2012, pp. 415-449. H. Wansing, "Connexive Logic", in Edward N. Zalta (ed.), The Stanford Encyclopedia of Philosophy (Fall 2014 Edition). (see here)

There is also a special issue on connexive logics in the IfCoLog Journal of Logics and their Applications. The entire issue is available here.

This workshop is meant to present current work on connexive logic and to stimulate future research.

Keynote speakers:

Call for abstracts:
Any papers related to connexive logics are welcome. Topics of interest include (but are not limited to) the following:

Submissions of extended abstracts (up to five pages) should be sent to both organizers (Hitoshi Omori and Heinrich Wansing) as a pdf file.

Deadline for submission: June 30th 2017.
Notification of acceptance: July 7th 2017.

9th International Workshop on Logic and Cognition: Non-classical Modal and Predicate Logics, call for papers

4-8 December 2017, Guangzhou (Canton), China

The aim of the conference is to bring together researchers in both pure and applied aspects of various branches of non-classical logics, not only to present recent advances in their particular fields, but mainly foster the exchange of ideas between researchers focusing on (1) separate branches of non-classical logic and (2) foundational and applied issues.

We invite submissions on both (a) theoretical topics from all branches of mathematical logic (e.g., proof-theory, model theory, game theory, computational complexity, etc.), as well as (b) their applications in various areas (including computer science, linguistics, mathematics, philosophy, etc.).

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

Strong papers on propositional logics can also be accepted, provided they relate to the themes in the main scope of the conference (e.g., the study of completions in algebraic semantics, propositional quantification, etc.).

Full versions of selected papers will be published in a special issue of an international peer-reviewed journal (to be specified).

Submissions
Extended abstracts of 1-2 pages (including references) should be submitted via the EasyChair web interface

Important dates
Deadline for abstracts: 1 September 2017
Notification of acceptance: 20 September 2017
Conference: 4-8 December 2017

More details are available on the workshop's website.

Summer and Autumn Schools

LogiCS/RiSE Summer School on Logic, AI and Verification

July 3-5, 2017, Vienna, Austria

The doctoral college Logical Methods in Computer Science (LogiCS) and the Austrian Society for Rigorous Systems Engineering (RiSE) will host a summer school on Logic, Artificial Intelligence and Verification at TU Wien, Vienna, Austria from July 3 to July 5, 2017. The summer school targets master and doctoral students in Computer Science and Mathematics with a strong interest in Logic, Artificial Intelligence and Automated Verification. The event is open to all interested students.

Speakers and courses:

For information about registration, see the registration webpage.

ISR 2017: 9th International School on Rewriting

July 3-7, 2017, Eindhoven, The Netherlands

The 9th International School on Rewriting (ISR 2017) is aimed at master and PhD students, researchers, and practitioners interested in the study of rewriting concepts and their applications. The school features lectures by renowned researchers in rewriting, and is organized in two parallel tracks: the Basic Track and the Advanced Track.

Speakers and courses:

You can register for ISR 2017 by sending an email to h.zantema@tue.nl. Please mention your full name, institution, and the track you wish to attend. It is appreciated if you mention the subjects you are particularly interested in.

ESSLLI 2017: 29th European Summer School in Logic, Language, and Information

17-28 July, 2017, University of Toulouse, France

The European Summer School in Logic, Language and Information (ESSLLI) is an event organized every year in a different European country under the auspices of the Association for Logic, Language and Information (FoLLI). It brings together logicians, linguists, computer scientists, and philosophers to study logic, language, information and their interconnections. ESSLLI attracts about 400 participants from all over the world, both senior and junior and is a great place to learn and network-and have a lot of fun in the process.

ESSLLI 2017 features 44 courses at foundational, introductory, and advanced levels, as well as 4 workshops, 4 invited lectures, and a student session to foster interdisciplinary discussion of current research. Courses and workshops are one week long and cover a wide variety of topics within the combined areas of interest: Language and Logic, Language and Computation, and Logic and Computation.

Important Dates:

For information about the programme and registration, see the school webpage.

NLS 2017: The Third Nordic Logic Summer School

August 7-11, Stockholm, Sweden

The third Nordic Logic Summer School is arranged under the auspices of the Scandinavian Logic Society. The two previous schools were organized in Nordfjordeid, Norway (2013) and Helsinki (2015). The intended audience is advanced master students, PhD-students, postdocs and experienced researchers wishing to learn the state of the art in a particular subject.

Speakers and courses:

Important Dates:

For information about application and registration, see the registration webpage.

ESSLLI 2018: 30th European Summer School in Logic, Language and Information, Call for Course and Workshop Proposals

6-17 August, 2018, Sofia, Bulgaria

Proposals for courses and workshops at ESSLLI 2018 are invited in all areas of Logic, Linguistics and Computing Sciences. Cross-disciplinary and innovative topics are particularly encouraged. Each course and workshop will consist of five 90 minute sessions, offered daily (Monday-Friday) in a single week. Proposals for two-week courses should be structured and submitted as two independent one-week courses, e.g. as an introductory course followed by an advanced one. In such cases, the ESSLLI programme committee reserves the right to accept just one of the two proposals.

Important Dates:

For more information about submission, see the detailed call.

Open Positions

PhD and Postdoc Position in Monad-Based Programming and Verification at FAU, Germany

In the Theoretical Computer Science group (Chair Computer Science 8) at the Friedrich-Alexander-Universität Erlangen-Nürnberg, we have a PhD and a postdoc position available in the DFG-Project "A High Level Language for Programming and Specifying Multi-Effect Algorithms", which is concerned with monad-based semantics and program logics for side-effecting iteration and recursion. The technical part of the project proposal can be made available on request.

The project is supervised by Sergey Goncharov and Lutz Schröder. The positions are in the TV-L E13 or E14 pay scale depending on qualification of the applicant; the project duration is three years.

Please contact and Sergey Goncharov to enquire or apply by e-mail.

3 year postdoc position in Innsbruck, Austria

The Computational Logic research group is looking for a postdoctoral researcher in connection with the FWF (Austrian Science Fund) project "FORTissimo: Automating the First-Order Theory of Rewriting". The project runs for 3 years starting from 1 September 2017. Salary is paid according to the FWF funding scheme for postdocs (40 hours) and amounts to approximately EUR 50K per year (gross).

Candidates must hold a PhD degree in computer science or mathematics. Knowledge of automata theory and rewriting is helpful, experience with and a liking of working with proof assistants (preferably Isabelle/HOL) is desirable. Candidates close to obtaining a PhD degree are also invited to apply. Knowledge of German is not required.

The main task of a successful applicant will be to collaborate with other project members in order to extend the Isabelle Formalization of Rewriting with the decision procedure for the first-order theory of rewriting for left-linear and right-ground rewrite systems.

Applications (including CV and names and contact details of two references) must be send by email to Aart Middeldorp no later than 1 August 2017. Informal inquiries are welcome.

The city of Innsbruck, which hosted the Olympic Winter Games in 1964, 1976 and 2012 (YOG), is superbly located in the beautiful surroundings of the Tyrolean Alps. The combination of the Alpine environment and urban life in this historic town provides a high quality of living. The Computational Logic in Innsbruck is one of the leading research groups in the area of rewriting and formalization in the world.

Further information is available from the following links:

PostDoc Position at INRIA, Sophia Antipolis, France

A postdoctoral position is available within the Marelle Inria Team in Sophia Antipolis (south of France). The position is funded by the ANR Fastrelax research project on "Fast and reliable approximation" for numerical computation.

We are looking for a candidate who is interested in applying theorem proving techniques to effective numerical computation.

One of our interests is to formalise bounds on polynomial approximations of functions (Berstein polynomials and Taylor models).

Another interest is to formalize in Coq some results in real and complex analysis (differential equations, Padé approximants, generalized Fourier series or Lyapunov certificates).

Funding starts in 2017 and is available for 12 months. The net salary is around 2100 euros/month, (health insurance and social coverage are included).

The candidate must have a PhD, and a strong knowledge in theorem proving and/or mathematics.

Potential candidates can contact Laurent Théry or Laurence Rideau.

Short-term PhD Student or Postdoc Position in Innsbruck, Austria

We invite candidates for a PhD student or Postdoc researcher position to start as soon as possible in the ongoing Certification Redux project of the CL group at the University of Innsbruck.

Since the project officially ends on January 31, 2018, any initial contract will also have to end on this date. However, it is highly likely that the project can be extended for at least another year after January 2018.

PhD student positions like Postdoc positions are formal employment in Austria, with a regular salary and benefits. Applications before June 30 will receive a full consideration.

A background in proof assistants (preferably Isabelle/HOL) or term rewriting will be of advantage. Knowledge of German is not required, the group is international and the language of communication is English.

Candidates for the PhD position must hold a master's degree in computer science or mathematics and candidates for the Postdoc position hold a doctoral degree in computer science or mathematics.

The main task of a successful applicant will be to collaborate with other project members in order to formalize (first-order) AC-unification (that is, unification in the presence of associative and commutative function symbols) as part of the Isabelle Formalization of Rewriting and further extend this formalization to cover AC-critical pairs and normalized completion.

Applications and informal inquiries are welcome, please contact Christian Sternagel. Applications should include a CV as well as names and contact details of two references.

The city of Innsbruck, which hosted the Olympic Winter Games in 1964, 1976 and 2012 (YOG), is superbly located in the beautiful surroundings of the Tyrolean Alps. The combination of the Alpine environment and urban life in this historic town provides a high quality of living. The CL group is one of the leading groups in the area of rewriting, formalization and certification in the world.

Postdoctoral openings at the Università degli Studi di Verona, Italy

We invite applications for one postdoctoral researcher position at the Dipartimento di Informatica of the Università degli Studi di Verona, in beautiful Verona, Italy, EU. The researchers will be supervised by Maria Paola Bonacina.

The position is funded for one year, possibly renewable, in the context of a two-year project running from April 2017 to March 2019. The main aim of the project is to implement the first SGGS theorem prover. SGGS, which stands for Semantically-Guided Goal-Sensitive reasoning, is a theorem-proving method that generalizes Conflict-Driven Clause Learning (CDCL) to first-order logic. It was designed by Maria Paola Bonacina and David A. Plaisted: more information about it can be found here.

The ideal candidate should have background in theorem proving and enthusiasm for building a new theorem prover and playing with it, with the possibility of contributing extensions or improvements to the method as suggested by implementation and experiments. The position is full-time on research (no teaching assignments). Interested candidates can email their CV and short description of relevant research background to Maria Paola Bonacina. The position must be filled by March 2018 at the very latest. Applications will be considered as soon as received.

Open Postdoc and Ph.D. Positions in Concurrency and Software Security at TU Darmstadt, Germany

The Chair Modeling and Analysis of Information Systems at TU Darmstadt, led by Heiko Mantel, is offering multiple positions. We are looking for researchers who are interested in addressing foundational problems that are or will be of practical relevance. The research focus shall be on concurrency, software security, or their combination.

The spectrum of possible research topics includes

Your research shall be based on solid formal foundations and could result, e.g., in foundational insights, in program analysis and transformation techniques, in tools that are reliable and efficient, or in verified critical software systems.

For more information about the open positions and how to apply, see http://www.mais.informatik.tu-darmstadt.de/Positions.html

Researcher positions (postdoc) in "Verification of Quantum Cryptography" in Tartu, Estonia

At the Quantum Cryptography Group, University of Tartu, we have two open postdoc positions on Verification of Quantum Cryptography.

We are starting a project in which we will develop methods for the verification of proofs in quantum cryptography. Similar to what the EasyCrypt tool does in classical cryptography. The scope of the project covers everything from the logical foundations, through the development of tools, to the verification of real quantum protocols.

The ideal candidate would have experience in:

Of course, expertise in all those areas is very rare, so candidates who are strong in some of those areas and are interested in the others are encouraged to apply!

Please contact Dominique Unruh if you have more questions about the project, the required background, Estonia, the position itself, or the application process.

The salary range is 30000-36000 Euro per year (depending on experience), which is highly competitive in Estonia due to low costs of living and low income tax rate (20%), pension contributions and health insurance are covered by the employer.

The position is for three years, September 1, 2017 till August 31, 2020. The starting date and duration can be negotiated (in both directions).

To apply, please send the following documents to Dominique Unruh:

The deadline for applications is June 1, 2017, but later applications can be considered.

The original jop offer is here.

PhD and Postdoc positions in Innsbruck, Austria

We invite candidates for multiple PhD student and Postdoc researcher positions to start in 2017 or 2018 in the 5-year project "Strong Modular Proof Assistance: Reasoning across Theories" in the CL group at the University of Innsbruck.

The starting date can be negotiated. PhD student positions like Postdoc positions are formal employment in Austria, with a regular salary and benefits. Applications before June 15 will receive a full consideration.

A background in proof assistants or machine learning is an advantage. Knowledge of German is not required, the group is international and the language of communication is English.

Candidates for a PhD position must hold a MSc in computer science or mathematics and candidates for the postdoctoral position hold a PhD degree in computer science or mathematics.

Applications and informal inquiries are welcome, please contact Cezary Kaliszyk. Applications should include a CV and names and contact details of two references. For the Postdoc positions please include a brief research statement.

The city of Innsbruck, which hosted the Olympic Winter Games in 1964, 1976 and 2012 (YOG), is superbly located in the beautiful surroundings of the Tyrolean Alps. The combination of the Alpine environment and urban life in this historic town provides a high quality of living. The CL group is one of the leading groups concerned with formalization and certification in the world.

More information and links about the project, the group, and the university can be found here.

Open position at Kernkonzept in Dresden, Germany

Kernkonzept seeks outstanding formal-methods experts to join their team in Dresden, Germany. Applicants should have a background in formal methods and software verification. Please visit this page for the concrete job descriptions.

Kernkonzept is a small and friendly operating-systems engineering company that leverages the microkernel-based L4Re operating system for industrial use. The formal-methods engineers at Kernkonzept will have the task to prepare the safety and security certification of the L4Re system according to different international standards. If you are interested or have questions, please contact us.

Interactive theorem proving: 3 Postdoctoral positions at Cambridge, United Kingdom

ALEXANDRIA is a five-year ERC-funded project aimed at making interactive theorem proving useful in mathematical research. The workplan includes pilot studies to identify critical issues, library development and the implementation of advanced search, perhaps using machine learning. Two mathematicians and an Isabelle architect will be hired. Official descriptions of the vacancies are online:

We can look forward to some exciting developments! And while this project will be based on Isabelle, I also hope for fruitful cooperation with users of other systems.

The Editor's Corner: Survey Results for the AAR Newsletter

Dear readers,

as you may recall, in the last newsletter we provided a link to a survey, with questions about the background of our readers, changes people would like to see in the newsletter, and the possibility to give general suggestions for improvements. We are happy that 31 of our readers completed the survey, and that we received a number of quite insightful comments; the following paragraphs summarise the survey results.

Use of the newsletter. Of the 31 people who answered, 29 are reading the newsletter each time it is published, while one particularly faithful reader is returning to the newsletter repeatedly to check deadlines, and one slightly less attentive reader only takes a look at the newsletter once in a while.

Similarly, the question about the relative value of the different newsletter sections yielded only moderately interesting answers. Each of the considered sections (calls of conferences, workshops, or special issues; lists of summer/winter schools; job announcements; and editor's corner) were described as very useful by more than 20 participants and in each case less than 10 participants were either undecided or found the section not so useful.

We felt that the most insightful outcome of the question was the free-text comment that

... With the current crop of scam conferences, it's useful to have a community-vetted source of conference announcements for real conferences ...
We will do our best to keep this standard in the upcoming editions of the newsletter!

Guest column. Our question about the possibility of including a guest column in the newsletter was received positively, with 19 Yes answers and 10 people being Undecided. As a direct consequence of these answers, we welcome the contribution by Christoph Weidenbach that is included in the present newsletter. As reference for the future contributors of this column, the free-text answers revealed that our readers like discussions, logic puzzles, and prefer to keep the column short and conceptual:

Good idea, if you can fill the slot with interesting contributions.
I'd read it if it's short and not overly technical (i.e., accessible to a general ITP audience).
I totally agree with this idea, another idea could be some 'logical puzzle' to solve. Could be a lot of fun :)
We definitely need some kind of discussion about the area.

Readers. The maybe most interesting answer concerned the question about the scientific background of the newsletter audience:

Scientific background
Other areas were specified as: We believe the AAR newsletter reflects this diversity and plan for it to continue doing so.

Employment of the newsletter audience is mainly academic, with answers including 16x Faculty/Academic, 7x Student/PhD student, and 4x Post-doc. Only one reader answered that she/he is working at a company.

Free-text suggestions, as expected, included the most insightful feedbacks we received.

I hope this survey is not meant to prepare some sort of scaling down of the AAR Newsletter. Quite to the contrary, I hope it will prepare further growth. The importance of the AAR Newsletter cannot be overestimated. It is an authentic treasure for our field, a trove of current and past data. Other web pages (e.g., workshops, schools, conferences) routinely disappear after a certain number of years. The stability over time that the Newsletter provides is unmatched.
We confirm that no scaling down of the newsletter is planned, and congratulate all the past newsletter editors on their great work! (for this positive feedback is certainly not due to us as newly employed editors)
it might be good to have short contributions from a variety of people, to give an impression of current activity without overwhelming detail.
This is what we hope to achieve with the guest column.
A kind of forum would be great; readers could comment articles or to invited notes.
The options of having a discussion forum associated with the newsletter, or a comment section for each newsletter both seem very interesting. They have been transmitted to the AAR board that will be the one to decide whether it can and should be done.

Although the poll is now over, you are welcome to send us your suggestions and contributions anytime. Especially, do not hesitate to manifest yourself if you would like to contribute to the guest column.

Thanks to all the participants for their useful feedbacks!