# Association for Automated Reasoning

December 2017

## From the AAR President, Larry Wos

In a recent conversation with my colleague Ross Overbeek, author of the inference rule UR-resolution and the weighting strategy, a question arose whose answer is crucial to certain users of some automated reasoning programs. Specifically, has something vital been lost in the recent design and implementation of such programs? Arguably, the newer programs offer far more power today if measured in terms of the number of conclusions drawn per CPU-second. But, does that tell the whole story? Can such programs prove deep theorems and solve hard problems?

To begin to answer this question, I offer a set of three clauses that form an unsatisfiable set, meaning that the deduction of appropriate conclusions leads to a proof by contradiction.

P(e(x,e(e(e(x,y),e(z,y)),z))).
-P(e(x,y)) | -P(x) | P(y).
-P(e(e(a,b),e(b,a))) | -P(e(e(a,b),e(e(b,c),e(a,c)))).

The set of clauses is not merely a syntactic example; rather, the set corresponds to a deep theorem from logic.

Of course, you might prefer a problem relying on equality exclusively. To this end, I offer a second unsatisfiable set of three clauses corresponding to a deep theorem of mathematics.

(((y ∨ x) ∧ x) ∨ (((z ∧ (x ∨ x)) ∨ (u ∧ x)) ∧ x1)) ∧ (w ∨ ((x2 ∨ x) ∧ (x ∨ x3)))=x.
x = x.
b ∨ (a ∧ (b ∧ c))!=b | b ∧ (a ∨ (b ∨ c))!=b | ((a ∧ b) ∨ (b ∧ c)) ∨ b!=b | ((a ∨ b)∧ (b ∨ c))∧ b!=b.

Which, if any, of the newer programs, given this set that relies on equality, finds a proof of unsatisfiability? I would enjoy hearing about any results, positive or negative; e-mail: wos@mcs.anl.gov.

## Guest Column: The Power of Failed Proofs

Wolfgang Ahrendt
Chalmers University of Technology

In his guest column for the AAR Newsletter No. 120, June 2017, Christoph Weidenbach makes a quest for automated reasoning procedures that can at the same time prove and disprove a conjecture. I could not agree more with that. While reasoning procedures for decidable (fragments of) logics are naturally strong in this respect, the community has generally a hard time to find effective methods that search for proofs AND disproofs in undecidable logics. This does not mean that we neglect the advances that have been made. There is a variety of work on showing non-consequence, in particular via model finding, but also via mapping non-consequence back to consequence, like in monomorphic (algebraic) logics. From 2004 to 2007, Peter Baumgartner, Hans de Nivelle, and myself gathered people interested in these topics in a series of DISPROVING workshops. Much has happened since then, but there is still not much of an understanding that this forms a field within automated reasoning. And certainly, there is too little co-construction of proof and disproof, which is really Christoph's point.

The point I want to make in this column is related, yet different. It is about the power of failed proofs. As we all know, much of the course of mathematical discovery was attributed to failed attempts of proving conjectures, which then led to refinements in the assumptions, and often to revised definitions of central concepts. (As a side note, this is sometimes overdone in computer science papers. Often, some result cannot be established for a class of problems the authors were aiming at originally. The subclass of problems where the approach still works gives rise to a definition, together with a nice name, of that subclass. That definition is then sold as a contribution to the field, which is justified in some cases, but less so in others.)

Failed proof attempts result in artefacts we may call, a bit sloppy, ‘partial proofs’. What that means precisely depends entirely on the proof format and procedure. Either way, partial proofs can be subjected to analysis, to retrieve useful information from them. And of course, in the context of automated reasoning, we like the analysis to be automated. It could not be otherwise.

Some of the earlier applications of failed proof analysis are the works on patching conjectures by Monroy, Bundy, Ireland and by Protzen, in the mid 90s. There, conjectures which are either untrue or just not provable with a given technique are patched, to obtain provable conjectures. Since then, many techniques involving failed proof analysis were invented and used, in application areas like the search for sufficiently strong induction hypotheses, or theory exploration, among others. In particular, we lately see a growing number of applications of partial proof analysis in verification and bug finding. For instance, several variants of verification based test case generation rely on unfinished proof construction, and the analysis of the resulting partial proofs, to extract the (pre)conditions under which the various program paths are executed. Other application areas may re-iterate failed proof attempts of refined variants of a conjecture, for instance to generate loop invariants.

For a more concrete illustration of how useful failed proofs can be in the context of verification, let me briefly mention the work Mauricio Chimento, Gordon Pace, Gerardo Schneider, and myself did lately on combined static and runtime verification of Java programs. The goal was to optimise, with results from static verification, runtime monitors which check compliance of observed runs with a specification. In that work, we do not limit ourselves to using the results of complete (static) proofs. Instead, we aggressively analyse partial proofs resulting from failed proof attempts. This is especially relevant as we aim, in that work, at fully automated, from the user perspective ‘low effort’ static verification, without any user interaction, and with no code annotations! Naturally, most attempts to prove method contracts fail in such a setting. But the automated analysis of the resulting partial proofs allows us to generate (pre)conditions under which the execution is ‘covered’ by the closed parts of the proof. Such conditions are later used in the generation of an optimised monitor, to not trigger runtime checks of cases which are already covered statically. This limits the runtime overhead of monitoring, in some cases dramatically. [Ahrendt,Chimento,Pace,Schneider; Verifying data- and control-oriented properties combining static and runtime verification: theory and tools; Formal Methods in System Design]

There are several parallel developments in the exploitation of failed proofs, and I am sure we will see more. But they are so far mostly seen as a particular ‘trick’ in their respective context. It would be great if we could conceive these developments as contributions to a common theme, and have cross-application discussions about this. Also, I would like to encourage everyone to consider whether and how one's own proof technology does — or could — allow for partial proof analysis.

## Results of CADE Trustee Elections

Martin Giese

An election was held from 28 September to 26 October 2017 to fill three positions on the board of trustees of CADE, Inc.

Four candidates were nominated (in alphabetic order): Jürgen Giesl, Marijn Heule, Andrew Reynolds, Bruno Woltzenlogel Paleo.

Ballots were sent by electronic mail to all members of AAR on 28 September, for a total of 1172 ballots. 107 valid ballots were returned, which translates to a participation level of 9.1% (as compared to 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 counting of the votes according to the single transferable vote algorithm described in the CADE Bylaws is detailed near the end of this newsletter.

The three candidates elected are Jürgen Giesl, Marijn Heule, and Andrew Reynolds.

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 thank Pascal Fontaine and Geoff Sutcliffe for their service on the board of trustees for the last three, resp. six years.

Geoff continues to take care of the AAR and CADE web presence even after his term of service, and we are very grateful for this service!

We also thank Leonardo de Moura for his service as ex-officio trustee for CADE-26.

I would also like to thank Bruno Woltzenlogel Paleo for running in the election.

Congratulations to Jürgen Giesl, Marijn Heule, and Andrew Reynolds on being elected!

## Call for volunteers for AAR and CADE Secretary

Christoph Weidenbach

After seven years of excellent service, AAR and CADE Secretary Martin Giese has informed the CADE Board of Trustees and the AAR Board of Directors that he wishes to step down. Martin deserves heartfelt thanks from all our field! Thus, the two corporations are seeking a new Secretary.

The role of Secretary is an important one, and most precious to our organizations. Former secretaries include Bill McCune, Bob Veroff, Maria Paola Bonacina, Amy Felty, and Wolfgang Ahrendt. The two roles of Secretary of AAR and Secretary of CADE have been filled by the same person since 1999, because AAR and CADE are strongly interconnected: CADE is a subcorporation of AAR, and the members of AAR elect the board of trustees of CADE. Thus, this call is for candidates to be the Secretary of both AAR and CADE.

The Secretary is a full-right member of both the AAR Board of Directors and the CADE Board of Trustees. The Secretary shares with the other members of these boards the responsibility, and opportunity, to influence and shape the core community work and decisions. In addition, the Secretary has the following distinguished duties:

• Organize the nomination and election process of Trustees; collect candidate statements; send e-mail ballots to all members; collect votes and apply the STV algorithm; prepare the document with the results for the AAR Newsletter;
• Within the Board of Trustees, organize the elections for CADE President;
• In cooperation with the CADE President and the AAR Newsletter Editor, publish CADE and AAR related announcements;
• In cooperation with the CADE Board of Trustees and IJCAR Steering Committee, organize the bidding process for CADE/IJCAR venues;
• In cooperation with the CADE President and the AAR Newsletter Editor, publish the call for Herbrand Award nominations;

Clearly, this is a very important job, which may give a lot of reward: the new Secretary will inherit all necessary documents and historical records from the outgoing Secretary and will be welcomed by the two boards. As CADE President I'll be happy to welcome the new Secretary and help towards a smooth transition.

Interested applicants should send an e-mail message with a brief statement, highlighting motivation and previous organizational experience, if any, and the url of their web page, to

no later than January 31st, 2018. The Secretary will be appointed by the two boards as soon as possible and all applicants will be informed of the outcome.

## Proposals Solicited for Sites for IJCAR 2020

IJCAR Steering Committee Chair

We invite proposals for sites around the world to host the 10th International Joint Conference on Automated Reasoning (IJCAR) to be held in summer 2020. Previous IJCAR meetings include IJCAR 2001 in Siena, Italy; IJCAR 2004 in Cork, Ireland; IJCAR 2006 as part of FLoC in Seattle, Washington; IJCAR 2008 in Sydney, Australia; IJCAR 2010 as part of FLoC in Edinburgh, Scotland; IJCAR 2012 in Manchester, UK; IJCAR 2014 as part of the Vienna Summer of Logic in Vienna, Austria; IJCAR 2016 in Coimbra, Portugal; and IJCAR 2018 as part of FLoC in Oxford, UK.

IJCAR is a merger of CADE (Conference on Automated Deduction), TABLEAUX (Conference on Analytic Tableaux and Related Methods), and FroCoS (Symposium on Frontiers of Combining Systems) and possibly other meetings. Usually a considerable number of Workshops are also affiliated with the conference.

The deadline for proposals is February 15, 2018. Proposals should be sent to the IJCAR Steering Committee Chair. We encourage proposers to register their intention informally as soon as possible. The final selection of the site will be made within one month after the proposal due date.

Proposals should address the following points that also represent criteria for evaluation:

• National, regional, and local AR community support: IJCAR Conference Chair and host institution, IJCAR Local Arrangements Committee, availability of (and reward for) student-volunteers.
• National, regional, and local government and industry support, both organizational and financial
• Accessibility (i.e., transportation), attractiveness, and desirability of proposed site.
• Appropriateness of proposed dates (including consideration of holidays/other events during the period), hotel prices, and access to dormitory facilities (a.k.a. residence halls).
• An estimate on registration for the conference and workshops, both for regular participants and students.
• Conference and exhibit facilities for the anticipated number of registrants (typically up to 200), for example, number, capacity and audiovisual equipment of meeting rooms; a large plenary session room that can hold all the registrants; enough rooms for parallel sessions/workshops/tutorials; Internet connectivity and workstations for demos/competitions; catering services; and presence of professional staff.
• Residence accommodations and food services in a range of price categories and close to the conference facilities, for example, number and cost range of hotels, and availability and cost of dormitory rooms (e.g., at local universities) and kind of services they offer.
• Rough budget projections for the various budget categories, e.g., cost of renting/cleaning the meeting rooms, if applicable; cost of professional conference secretariat, if hired; and financial model for satellite workshops and/or co-located events.
• Balance with regard to the geographical distribution of previous IJCAR conferences and its constituent meetings.

Perspective organizers are encouraged to get in touch with the IJCAR Steering Committee Chair for informal discussion. If the host institution is not actually located at the proposed site, then one or more visits to the site by the proposers is strongly encouraged.

## Conferences: Calls for Participation

### From the Fundamental Lemma to Discrete Geometry, to Formal Verification (60th birthday of Thomas Hales)

June, 18-22d, 2018, Pittsburgh PA, U.S.A.

The conference is held in honor of Thomas C. Hales on the occasion of his 60th birthday.

The conference will feature talks on representation theory, discrete geometry, and formal verification, with 1.5 days dedicated to each of these topics and with broadly accessible public lectures at the interfaces.

## Conferences: Calls for Papers

### AITP 2018: Artificial Intelligence and Theorem Proving

March 25-30, 2018, Aussois, France

Large-scale semantic processing and strong computer assistance of mathematics and science is our inevitable future. New combinations of AI and reasoning methods and tools deployed over large mathematical and scientific corpora will be instrumental to this task. The AITP conference is the forum for discussing how to get there as soon as possible, and the force driving the progress towards that.

Topics:

• AI, machine learning and big-data methods in theorem proving and mathematics.
• Collaboration between automated and interactive theorem proving.
• Common-sense reasoning and reasoning in science.
• Alignment and joint processing of formal, semi-formal, and informal libraries.
• Methods for large-scale computer understanding of mathematics and science.
• Combinations of linguistic/learning-based and semantic/reasoning methods.
• Formal verification of AI and machine learning algorithms, explainable AI.

Dates:

• Submission deadline: December 3, 2017
• Author notification: January 10, 2018
• Conference registration: January 24, 2018
• Camera-ready versions: January 31, 2018
• Conference: March 25-30, 2018

### CiE 2018: Sailing Routes in the World of Computation

July 30 - August 3, 2018, Kiel, Germany

CiE 2018 is the fourteenth conference organized by CiE (Computability in Europe), a European association of mathematicians, logicians, computer scientists, philosophers, physicists and others interested in new developments in computability and their underlying significance for the real world.

Special Sessions:

• Approximation and Optimization
• Bioinformatics and Bio-inspired Computing
• Computing with Imperfect Information
• Continuous Computation
• History and Philosophy of Computing
• SAT-Solving

Important Dates (tentative):

• Deadline for article registration (abstract submission): January 17, 2018
• Deadline for article submission: February 1, 2018
• Notification of acceptance: April 6, 2018
• Final versions due: April 20, 2018
• Deadline for informal presentations submission: April 20, 2018 (the notifications of acceptance for informal presentations will be sent few days after submission)
• Early registration before: May 30, 2018

### FLoC 2018: 7th Federated Logic Conference

July 6-19, 2018, Oxford, England, UK

In 1996, as part of its Special Year on Logic and Algorithms, DIMACS hosted the first Federated Logic Conference (FLoC). It was modeled after the successful Federated Computer Research Conference (FCRC), and synergetically brought together conferences that apply logic to computer science.

The seventh Federated Logic Conference (FLoC'18) will be held in Oxford, UK, in July 2018, at the Mathematical Institute and the Blavatnik School of Government at the University of Oxford. FLoC 2018 brings together nine major international conferences related to mathematical logic and computer science:

Please refer to the individual websites for conference-specific Calls for Papers, deadlines and information on how to submit.

In addition to conferences, FLoC 2018 will also feature 79 workshops (7-8 July, 13 July, and 18-19 July) and the School on Foundations of Programming and Software Systems (FoPSS, 30 June - 6 July).

The list of workshops can be found on the FLoC workshops web page.

Important Dates:

• Conference papers due: see individual conference web pages
• Conference papers notification: 31st March 2018
• Workshop papers due: 15th April 2018
• Workshop papers notification: 15th May 2018
• Camera-ready versions: 31st May 2018

### IJCAR 2018: 9th International Joint Conference on Automated Reasoning

July 14-17, 2018, Oxford, UK, affiliated with FLoC 2018

IJCAR is the premier international joint conference on all topics in automated reasoning. The IJCAR technical program will consist of presentations of high-quality original research papers, system descriptions, and invited talks.

IJCAR 2018 takes place as part of FLoC 2018 and is the merger of leading events in automated reasoning:

• CADE (Conference on Automated Deduction),
• FroCoS (Symposium on Frontiers of Combining Systems) and
• TABLEAUX (Conference on Analytic Tableaux and Related Methods).

Topics include:

• Logics of interest include: propositional, first-order, classical, equational, higher-order, non-classical, constructive, modal, temporal, many-valued, substructural, description, type theory, etc.
• Methods of interest include: tableaux, sequent calculi, resolution, model- elimination, inverse method, paramodulation, term rewriting, induction, unification, constraint solving, decision procedures, model generation, model checking, semantic guidance, interactive theorem proving, logical frameworks, AI-related methods for deductive systems, proof presentation, automated theorem provers, combination of decision procedures, SAT and SMT solving, etc.
• Applications of interest include: verification, formal methods, program analysis and synthesis, computer mathematics, declarative programming, deductive databases, knowledge representation, etc.

Important Dates:

• Abstract submission: January 22nd 2018
• Paper submission: January 29th 2018
• Camera-ready paper versions due: April 23rd, 2018
• IJCAR Conference: July 14nd-17th 2018
• FLoC: July 6th-19th 2018
Important Notice: due to very strict FLoC constraints, deadlines are Sharp!

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

### ITP 2018: 9th International Conference on Interactive Theorem Proving

July 9-12, 2018, Oxford, UK, affiliated with FLoC 2018

The ITP conference series is concerned with all topics related to interactive theorem proving, ranging from theoretical foundations to implementation aspects and applications in program verification, security, and formalization of mathematics. ITP is the evolution of the TPHOLs conference series to the broad field of interactive theorem proving. TPHOLs meetings took place every year from 1988 until 2009. The ninth ITP conference, ITP 2018, will be held in Oxford, July 9-12, 2018.

Scope of Conference:
ITP welcomes submissions describing original research on all aspects of interactive theorem proving and its applications. Suggested topics include but are not limited to the following:

• formal aspects of hardware and software
• formalizations of mathematics
• improvements in theorem prover technology
• user interfaces for interactive theorem provers
• formalizations of computational models
• verification of security algorithms
• use of theorem provers in education
• industrial applications of interactive theorem provers
• concise and elegant worked examples of formalizations (proof pearls)

Important Dates:

• Abstract submission deadline: January 25, 2018
• Full paper submission deadline: January 31, 2018
• Author notification: March 31, 2018
• Camera-ready papers: May 2, 2018
• Conference: July 9-10, 2018

### SAT 2018: 21st International Conference on Theory and Applications of Satisfiability Testing

July 9-12, 2018, Oxford, UK, affiliated with FLoC 2018

SAT 2018 welcomes scientific contributions addressing different aspects of the satisfiability problem, interpreted in a broad sense. Domains include MaxSAT and Pseudo-Boolean (PB) constraints, Quantified Boolean Formulae (QBF), Satisfiability Modulo Theories (SMT), as well as Constraint Satisfaction Problems (CSP). Topics include, but are not restricted to:

• Theoretical advances (including algorithms, proof complexity, parameterized complexity, and other complexity issues);
• Practical search algorithms;
• Knowledge compilation;
• Implementation-level details of SAT solving tools and SAT-based systems;
• Problem encodings and reformulations;
• Applications (including both novel applications domains and improvements to existing approaches);
• Case studies and reports on insightful findings based on rigorous experimentation.

Important Dates:
All deadlines are 23.59 AoE (anywhere on earth)

• 31 Jan 2018: Abstract submission
• 7 Feb 2018: Paper submission
• 12-14 Mar 2018: Author response period
• 9-12 Jul 2018: Conference

The full CfP and more information are available on the conference website.

### TAP 2018: 12th International Conference on Tests And Proofs

June 27-29, 2018, Toulouse, France

TAP's scope encompasses many aspects of verification technology, including foundational work, tool development, and empirical research. Its topics of interest center around the connection between proofs (and other static techniques) and testing (and other dynamic techniques). Papers are solicited on, but not limited to, the following topics:

• Verification and analysis techniques combining proofs and tests
• Program proving with the aid of testing techniques
• Deductive techniques supporting the automated generation of test vectors and oracles (theorem proving, model checking, symbolic execution, SAT/SMT solving, constraint logic programming, etc.)
• Deductive techniques supporting novel definitions of coverage criteria,
• Program analysis techniques combining static and dynamic analysis
• Specification inference by deductive and dynamic methods
• Testing and run-time analysis of formal specifications
• Search-based techniques for proving and testing
• Verification of verification tools and environments
• Applications of test and proof techniques in new domains, such as security, configuration management, learning
• Combined approaches of test and proof in the context of formal certifications (Common Criteria, CENELEC, ...)
• Case studies, tool and framework descriptions, and experience reports about combining tests and proofs

Important Dates:

• Abstract: 23 February 2018
• Paper: 2 March 2018
• Camera-Ready Version: 23 April 2018
• Conference: 27-29 June 2018

### RAMiCS 2018: 17th International Conference on Relational and Algebraic Methods in Computer Science

October 29 - November 2, 2018, Groningen, The Netherlands

Since 1994, the RAMiCS conference series has been the main venue for research on relation algebras, Kleene algebras and similar algebraic formalisms, and their applications as conceptual and methodological tools in computer science and beyond.

Topics:
We invite submissions in the general fields of algebras relevant to computer science and applications of such algebras. Topics include but are not limited to:

• Theory
• algebras such as semigroups, residuated lattices, semirings, Kleene algebras, relation algebras and quantales
• their connections with program logics and other logics
• their use in the theories of automata, concurrency, formal languages, games, networks and programming languages
• the development of algebraic, algorithmic, category-theoretic, coalgebraic and proof-theoretic methods for these theories
• their formalization with theorem provers
• Applications
• tools and techniques for program correctness, specification and verification
• quantitative and qualitative models and semantics of computing systems and processes
• algorithm design, automated reasoning, network protocol analysis, social choice, optimization and control
• industrial applications

Important Dates:

• Abstract Submission: 6 April 2018
• Paper Submission: 13 April 2018
• Author Notification: 29 June 2018
• Final Version: 27 July 2018
• RAMiCS 2018: 29 October - 2 November 2018

### RuleML+RR 2018: International Joint Conference on Rules and Reasoning

September 18-21, 2018, Luxembourg, part of LuxLogAI

The International Joint Conference on Rules and Reasoning (RuleML+RR), the leading international joint conference in the field of rule-based reasoning, calls for high-quality papers related to theoretical advances, novel technologies, and innovative applications concerning knowledge representation and reasoning with rules. Stemming from the synergy between the well-known RuleML and RR events, one of the main goals of this conference is to build bridges between academia and industry.

RuleML+RR 2018 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 and other application areas. It will provide a forum for stimulating cooperation and cross-fertilization between the many different communities focused on the research, development and applications of rule-based systems.

RuleML+RR welcomes original research from all areas of Rules and Reasoning. Topics of particular interest include:

• Rule-based languages for intelligent information access and for the semantic web
• Vocabularies, ontologies, and business rules
• Ontology-based data access
• Data management, and data interoperability for web data
• Distributed agent-based systems for the web
• 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
• Production & business rules systems
• Streaming data and complex event processing
• Rules for machine learning, knowledge extraction and information retrieval
• Rule-based approaches to natural language processing
• Rule discovery, extraction and transformation
• Rules and ontology learning
• Deep Learning for rules and ontologies
• Neural Networks and logic rules
• Neural Networks and ontologies
• Rule-based approaches to agents
• Higher-order and modal rules
• Rules for knowledge graphs
• Pragmatic web reasoning and distributed rule inference / rule execution
• Big data reasoning with rules
• Rule markup languages and rule interchange formats
• Rule-based policies, reputation, and trust
• 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 rule technologies in healthcare and life sciences
• Applications of rule technologies in law, regulation and finance
• Industrial applications of rules
• Rules and social media
• Rules of ethics, laws, policies, and regulations

Important Dates:

• Title and Abstract submission: 20 Apr 2018
• Full papers submission: 27 Apr 2018
• Notification of acceptance: 1 June 2018
• Camera-ready submission: 15 June 2018
• Conference: 18-21 Sept 2018

### KR 2018: 16th International Conference on Principles of Knowledge Representation and Reasoning

October 30th - November 2d, 2018, Tempe AZ, U.S.A.

KR 2018 is co-located with DL 2018 and NMR 2018.

Knowledge Representation and Reasoning (KRR) is an exciting, well-established field of research. In KRR 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, KRR has contributed to the theory and practice of various areas in AI, such as automated planning, natural language understanding, among others, as well as to fields beyond AI, including databases, verification, and software engineering. In recent years KRR has contributed to new and emerging fields including the semantic web, computational biology, and the development of software agents.

We solicit papers presenting novel results on the principles of KRR 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 KRR. We also encourage “reports from the field” of applications, experiments, developments, and tests.

Topics of interest include, but are not limited to:

• Argumentation
• Belief revision and update, belief merging, information fusion
• Computational aspects of knowledge representation
• Concept formation, similarity-based reasoning
• Contextual reasoning
• Description logics
• Decision making
• Explanation finding, diagnosis, causal reasoning, abduction
• Inconsistency- and exception tolerant reasoning, paraconsistent logics
• KR and autonomous agents: intelligent agents, cognitive robotics, multi-agent systems
• KR and game theory
• KR and machine learning, inductive logic programming, knowledge discovery and acquisition
• KR and natural language processing
• KR and the Web, Semantic Web
• Logic programming, answer set programming, constraint logic programming
• Multi- and order-sorted representations and reasoning
• Nonmonotonic logics, default logics, conditional logics
• Philosophical foundations of KR
• Ontology formalisms and models
• Preference modeling and representation, reasoning about preferences,
• preference-based reasoning
• Qualitative reasoning, reasoning about physical systems
• Reasoning about actions and change, action languages, situation calculus, dynamic logic
• Reasoning about knowledge and belief, epistemic and doxastic logics
• Spatial reasoning and temporal reasoning
• Uncertainty, representations of vagueness, many-valued and fuzzy logics

Important Dates:

• Submission of title and abstract: 13 May 2018
• Paper submission deadline: 20 May 2018
• Author response period: 25-27 June 2018
• Camera-ready papers due: 3-10 August 2018
• Conference date: 30 October-2 November 2018

## Workshops

### ETAPS 2018 Workshops

April 14-21, 2018, Thessaloniki, Greece

The European Joint Conferences on Theory and Practice of Software (ETAPS) is the primary European forum for academic and industrial researchers working on topics relating to Software Science.

ETAPS, established in 1998, is a confederation of five main annual conferences (ESOP, FASE, FOSSACS, POST and TACAS) accompanied this year by 14 satellite workshops and other events.

The complete list of workshops affiliated with ETAPS 2018 can be found on this web page. Submission deadlines range from mid-January to February.

### SYSMICS 2018: 2d Substructural logics

February, 26-28th, 2018, Vienna, Austria

Substructural logics are non-classical logics lacking some of the structural rules of classical logic, and are motivated by philosophical, linguistic and computational considerations. Traditionally, substructural logics have been investigated using proof theoretic and algebraic methods. In recent years, combined approaches have started to emerge. The program of this SYSMICS workshop will be focused on the interactions between syntactic and semantic methods in substructural and related logics, as well as their applications.

Important Dates:

• 15th December 2017: abstract submission deadline
• 22nd December 2017: author notification
• 26-28th February 2018: workshop

### SetVR 2018: International Workshop on Set Visualization and Reasoning 2018

June 18-22, 2018, Edinburgh, UK

SetVR 2018 will be the 6th meeting, with the first one held in 2004, previously called the Euler Diagrams Workshop. It aims to promote theoretical, empirical, applied research on visualization and diagrammatic reasoning, especially, about sets (set-theoretical and grouped data). SetVR 2018 welcomes submissions of types: full papers (16 pages) and short papers (8 pages; at least 5 pages). Accepted papers are expected to be published on-line by CEUR Workshop Proceedings (CEUR-WS.org). SetVR 2018 will run as part of the Diagrams 2018 conference, which will be held from June 18th to 22nd in 2018, and is expected to occupy one day during this period.

Topics include:

• Information Visualization: diagram/graph drawing and layout, data visualization, ontology visualization, human-computer interaction
• Diagrammatic Logic: formalization, inference system, expressiveness, decidability, computational complexity, automated reasoning, history of notation
• Cognitive Science: efficacy evaluation, cognitive process, cognitive model, educational outcome
• Application of Diagrams: visual modeling, real world reasoning, ontology engineering, data exploration

Important Dates:

• Paper Submission Due: 5th February, 2018

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

### Matryoshka 2018: 1st European Workshop on Higher-Order Automated Reasoning

June 25-27, 2018, Amsterdam, The Netherlands

Matryoshka 2018 is co-located with WAIT 2018.

This workshop brings together researchers working on automated deductive techniques for higher-order logics (especially simple type theory and dependent type theory). There has been much progress in recent years with the higher-order automatic theorem provers Leo-III and Satallax, the Lean proof assistant, and metaprovers such as HOLyHammer and Sledgehammer.

With the Matryoshka project, we aim at designing a new generation of higher-order automatic theorem provers based on state-of-the-art first-order provers, including E, VeriT, and CVC4, and to integrate them in popular proof assistants. We believe that first-order automatic provers are the best tools available to perform most of the tedious logical work inside proof assistants. We encourage researchers motivated by the same goals to get in touch with us, subscribe to the matryoshka-devel mailing list, and join forces.

The workshop succeeds to the LPAR-05 workshop on Empirically Successful Automated Reasoning in Higher-Order Logic (ESHOL), held in Montego Bay, Jamaica. The Matryoshka workshop series is conceived to be a meeting point for the Matryoshka team and colleagues working on the same challenge. It is an informal event. We expect to hold it at least once a year until the project's completion in 2023.

Please send an email to the organizers (Alexander Bentkamp and Jasmin Christian Blanchette) if you would like to give a talk, demonstrate a tool, or otherwise participate.

### 4th International Workshop on Automated (Co)inductive Theorem Proving

June 28-29, 2018, Amsterdam, The Netherlands

WAIT 2018 is co-located with Matryoshka 2018.

Inductive and coinductive theorem proving is a topic of growing interest in the automated reasoning community. The Fourth International Workshop on Automated (Co)inductive Theorem Proving (WAIT 2018) focuses on all relevant aspects of (co)inductive reasoning.

The workshop is an informal event and aims to give researchers interested in the topic a chance to meet, exchange ideas, and have a platform for discussions.

We invite talks featuring demonstrations and tutorials of (co)inductive theorem provers, challenge problems, new directions of research, or anything else of interest to the (co)inductive theorem proving community.

The previous events in the series were hosted in London, Gothenburg, and Vienna. This fourth installment explicitly generalizes the scope to include coinductive methods.

Please send an email to the organizers (Johannes Hölzl and Jasmin Christian Blanchette) if you would like to give a talk, demonstrate a tool, or otherwise participate.

### PhDs in Logic X

May, 1-4th, 2018, Prague, Czech Republic

“PhDs in Logic” is an annual graduate conference organized by local graduate students. This interdisciplinary conference welcomes contributions to various topics in mathematical logic, philosophical logic, and logic in computer science. It involves tutorials by established researchers as well as short (20 minute) presentations by PhD students, master students and first-year postdocs on their research.

PhD students, master students, and first-year postdocs in logic from disciplines that include but are not limited to philosophy, mathematics, and computer science are invited to submit an extended abstract on their research. Submitted abstracts should be about 2 pages long (not including references). Each abstract will be anonymously reviewed by the scientific committee. The accepted abstracts will be presented by their authors in a 20 minute presentation during the conference. The deadline for abstract submission is 19th January 2018.

### FLoC 2018: The 2018 Federated Logic Conference - Workshops Announcement

July 6-19, 2018, Oxford, UK

The seventh Federated Logic Conference (FLoC'18) will be held in Oxford, UK, in July 2018, at the Mathematical Institute and the Blavatnik School of Government at the University of Oxford.

In addition to nine major international conferences related to mathematical logic and computer science (CAV, CSF, FM, FSCD, ICLP, IJCAR, ITP, LICS and SAT), FLoC 2018 will feature as many as 79 workshops and the School on Foundations of Programming and Software Systems (FoPSS, 30 June - 6 July).

The selection process for workshops is now over and the complete list can be found on the FLoC workshops web page.

Individual CfPs of the workshops related to automated reasoning are or will be also included in this or the following newsletter.

### CL&C 2018: 7th Classical Logic and Computation 2018

July 7, 2018, Oxford, UK

This year, CL&C will be held as satellite workshop of FSCD 2018 (former TLCA + rRTA). CL&C is focused on the interplay between, on one side, the exploration of the computational content of classical mathematical proofs, and on the other side, the languages and the semantic models proposed in computer science for this task: continuations, game models, denotational models, learning models and so forth. the scientific aim of this workshop is to bring together researchers from both proof theory and computer science and to exchange ideas.

The following paper categories are welcome:

• version of lambda calculi adapted to represent classical logic;
• design of programming languages inspired by classical logic;
• cut-elimination for classical systems;
• proof representation for classical logic;
• translations of classical to intuitionistic proofs;
• constructive interpretation of non-constructive principles;
• witness extraction from classical proofs;
• constructive semantics for classical logic (e.g. game semantics, classical realization);
• case studies (for any of the previous points).

Important Dates:

• Abstract registration deadline march 12, 2018
• Submission deadline march 19, 2018
• Author notification may, 17 2018.
• Final version june, 17, 2018.

### WiL 2018: Second Women in Logic Workshop

July 8, 2018, Oxford, UK

Affiliated with the Thirty-Third Annual ACM/IEEE Symposium on Logic in Computer Science (LICS), 9-12 July 2018 and held as part of the Federated Logic Conference 2018 (FLoC), 6-19 July 2018.

Women are chronically underrepresented in the LICS community; consequently they sometimes feel both conspicuous and isolated, and hence there is a risk that the under-representation is self-perpetuating.

The workshop will provide an opportunity for women in the field to increase awareness of one another and one another's work, to combat the feeling of isolation. It will also provide an environment where women can present to an audience comprised of mostly women, replicating the experience that most men have at most LICS meetings, and lowering the stress of the occasion; we hope that this will be particularly attractive to early-career women.

Topics of interest of this workshop include but are not limited to the usual Logic in Computer Science (LICS) topics. These are:

• 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, 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:

• Paper submission deadline: 31 March 2018
• Author notification: 8 May 2018
• Contribution for Informal Proceedings: 31 May 2018

### DCM 2018: 12th International Workshop on Developments in Computational Models

July 8, 2018, Oxford, UK

Several new models of computation have emerged in the last years, and many developments of traditional computation models have been proposed with the aim of taking into account the new demands of users of computer systems and the new capabilities of computation engines.

The aim of this workshop is to bring together researchers who are currently developing new computation models or new features for traditional computation models, in order to foster their interaction, to provide a forum for presenting new ideas and work in progress, and to enable newcomers to learn about current activities in this area. The proceedings are produced after the meeting, so that authors can incorporate the workshop feedback in the published papers.

DCM 2018 will take place in Oxford on July 8, as a one-day satellite event of FLoC 2018, associated to LICS'18.

Topics of interest include all abstract models of computation and their applications to the development of programming languages and systems. This includes (but is not limited to):

• Functional calculi: lambda-calculus, pattern-calculi, combinatory logic, term and graph rewriting;
• Object calculi;
• Interaction-based systems: interaction nets, games, agent and multi-agent systems;
• Concurrent models: process calculi, action graphs, distributed systems;
• Calculi expressing locality, mobility, and active data;
• Quantum computational models;
• Biological or chemical models of computation;

Important Dates:

• Submission deadline: 8 April 2018
• Pre-proceedings version: 27 May 2018
• Workshop: 8 July 2018
• Full version of paper: 1 October 2018
• Final versions due: 15 December 2018

### LFMTP 2018: Logical Frameworks and Meta-Languages: Theory and Practice

July 7 2018, Oxford, UK

LFMTP is affiliated with FSCD 2018 (part of FLoC)

Logical frameworks and meta-languages form a common substrate for representing, implementing and reasoning about a wide variety of deductive systems of interest in logic and computer science. Their design, implementation and their use in reasoning tasks, ranging from the correctness of software to the properties of formal systems, have been the focus of considerable research over the last two decades. This workshop will bring together designers, implementors and practitioners to discuss various aspects impinging on the structure and utility of logical frameworks, including the treatment of variable binding, inductive and co-inductive reasoning techniques and the expressiveness and lucidity of the reasoning process.

LFMTP 2018 will provide researchers a forum to present state-of-the-art techniques and discuss progress in areas such as the following:

• Encoding and reasoning about the meta-theory of programming languages, logical systems and related formally specified systems.
• Theoretical and practical issues concerning the treatment of variable binding, especially the representation of, and reasoning about, datatypes defined from binding signatures.
• Logical treatments of inductive and co-inductive definitions and associated reasoning techniques, including inductive types of higher dimension in homotopy type theory.
• Graphical languages for building proofs, applications in geometry, equational reasoning and category theory.
• New theory contributions: canonical and substructural frameworks, contextual frameworks, proof-theoretic foundations supporting binders, functional programming over logical frameworks, homotopy and cubical type theory.
• Applications of logical frameworks: proof-carrying architectures, proof exchange and transformation, program refactoring, etc.
• Techniques for programming with binders in functional programming languages such as Haskell, OCaml or Agda, and logic programming languages such as lambda Prolog or Alpha-Prolog.

Important Dates:

• Abstract submission deadline: Monday April 9th
• Submission deadline: Monday April 16th
• Notification to authors: Monday May 14th
• Final version due: Monday June 4th
• Workshop date: Saturday July 7th

### ADSL 2018: 1st Workshop on Automated Deduction for Separation Logics

July 13, 2018, Oxford, UK

In recent times, program verification, and particularly deductive program verification, has made significant progress. This progress is in part due to the incorporation of logical back ends such as SMT solvers and other automated theorem-proving technologies. In parallel to these developments, the verification of heap manipulating programs, and static analyses in particular, has met with substantial successes, largely due to the development of Separation Logics.

The goal of this workshop is to bring together academic researchers and industrial practitioners focused on improving the state of the art of automated deduction methods for Separation Logics. We will consider technical submissions presenting work on the following topics (the list is not exclusive):

• the integration of Separation Logics with SMT,
• proof search and automata-based decision procedures for Separation Logics and sister logics such as Bunched Implication Logic;
• computational complexity of logical problems such as satisfiability, entailment and abduction;
• alternative semantics and computation models based on the notion of resource;
• application of separation and resource logics to different fields, such as sociology and biology.

The workshop is affiliated with the 33rd Annual ACM/IEEE Symposium on Logic in Computer Science (LICS 2018) and part of the Federated Logic Conference 2018 (FLOC 2018).

Important dates:

• Papers due: 20th of April 2018
• Author notification: 18th of May 2018
• Workshop: 13 July 2018

### LC 2018: Logic Colloquium

July 23-28, Udine, Italy

The Logic Colloquium 2018 is the annual European summer meeting of the Association of Symbolic Logic (ASL).

The Association for Symbolic Logic (ASL) is an international organization supporting research and critical studies in logic. Its primary function is to provide an effective forum for the presentation, publication, and discussion of scholarly work in this area of inquiry. The Association holds two major annual meetings to present current research in all aspects of logic in a way that is accessible to all logicians.

Important Dates:

• Deadline for abstract submission: April 27, 2018
• Deadline for travel grant applications: May 4, 2018
• Deadline for early registration: May 23, 2018

## Summer schools

### SAT/SMT/AR Summer School 2018

The next edition of the SAT/SMT/AR Summer School will take place in Manchester, UK on 3-6th July 2018. Satisfiability (SAT), Satisfiability Modulo Theories (SMT), and Automated Reasoning (AR) continue to make rapid advances and find novel uses in a wide variety of applications, both in computer science and beyond. The SAT/SMT/AR Summer School aims to bring a select group of students up to speed quickly in this exciting research area. The school continues the successful line of Summer Schools that ran from 2011 to 2015 as SAT/SMT Summer Schools and added AR in 2016. We will also include a special session on computer algebra to continue the activity of the SC2 summer school in 2017.

Further details (including a list of talks, application details, and grants for students) will be circulated and added to the website in January. The early application deadline is currently planned for May 1st.

## Books

### Applied Logic for Computer Scientists

As described on its Springer web page, this book, written by Mauricio Ayala-Rincon and Flavio de Moura,

• provides readers with the fundamental tools needed to develop mathematical certificates of correctness and robustness of software and hardware systems;
• explains how logical deductive rules are related with proof commands available in deductive frameworks such as PVS;
• clarifies the differences between constructive and classical deduction.

### Temporal Type Theory: A topos-theoretic approach to systems and behavior

This book, written by Patrick Schultz and David I. Spivak, is available on arXiv. The abstract follows.

This book introduces a temporal type theory, the first of its kind as far as we know. It is based on a standard core, and as such it can be formalized in a proof assistant such as Coq or Lean by adding a number of axioms. Well-known temporal logics—such as Linear and Metric Temporal Logic (LTL and MTL)—embed within the logic of temporal type theory. The types in this theory represent “behavior types”. The language is rich enough to allow one to define arbitrary hybrid dynamical systems, which are mixtures of continuous dynamics—e.g. as described by a differential equation—and discrete jumps. In particular, the derivative of a continuous real-valued function is internally defined. We construct a semantics for the temporal type theory in the topos of sheaves on a translation-invariant quotient of the standard interval domain. In fact, domain theory plays a recurring role in both the semantics and the type theory.

### Computer Arithmetic and Formal Proofs: Verifying Floating-point Algorithms with the COQ System

Floating-point arithmetic is ubiquitous in modern computing, as it is the tool of choice to approximate real numbers. Due to its limited range and precision, its use can become quite involved and potentially lead to numerous failures. One way to greatly increase confidence in floating-point software is by computer-assisted verification of its correctness proofs.

This book provides a comprehensive view of how to formally specify and verify tricky floating-point algorithms with the Coq proof assistant. It describes the flocq formalization of floating-point arithmetic and some methods to automate theorem proofs. It then presents the specification and verification of various algorithms, from error-free transformations to a numerical scheme for a partial differential equation. The examples cover not only mathematical algorithms but also C programs as well as issues related to compilation.

The authors of this book are Sylvie Boldo and Guillaume Melquiond. Full references are available on the publisher web page.

## Open Positions

### Multiple Ph.D. positions at TU Darmstadt, Germany

Software Factory 4.0 project, coordinated by Prof. Dr. Heiko Mantel

The Project:
You will be working on the LOEWE project “Software-Factory 4.0” (SF4.0), funded by the German State of Hesse.

The goal of “Software-Factory 4.0” is to enable legacy software systems (as used for high performance computing and cyber-physical production systems) to keep up with the rapid technological advances made in the development of new hardware and middleware platforms. Existing software must be retrofitted to fully exploit the potential provided by technological progress. Complete re-development of the existing stock of production software is unfeasible. At the same time, superficially adapted legacy software prevents optimal hardware usage. This is known as the “software gap”.

SF4.0 aims to create methods and tools that enable continuous and largely automated re-engineering of software to meet changed requirements and technological constraints. Re-engineering keeps software development costs manageable and allows one to preserve expert domain knowledge inherent to legacy software. In SF4.0, special emphasis will be put on the reliability of the resulting software. Formal methods and semantics will be applied for this purpose.

The two main application areas to be explored in SF4.0 are “High Performance Computing” (HPC) and “Industrie 4.0”. In the former, parallelization of existing software is the main driving force, while the latter focuses on the variability aspects of cyber-physical production systems and the development of digital twins.

SF4.0 consists of eight part projects, each of which offers 1-2 Ph.D. positions in the areas of computer science and mechanical engineering. A selection of the specific areas includes: concurrency semantics, cyber-physical production systems, formal methods, parallel and distributed computing, software-aided construction, software engineering, and static program analysis.

You are enthusiastic about applied and/or theoretical research and you have a strong background and demonstrable interest in one or more of the areas mentioned above.

We are looking for researchers with an independent mind who are willing to cooperate in our international team. We expect good communicative and social skills. Candidates should be prepared to prove their English language skills.

As a research outcome we expect publications, software tools, and a Ph.D. thesis.

What We Offer:

• starting date of the position: from January 2018
• a highly stimulating, dynamic, international scientific environment
• the chance to participate in a highly visible, economically relevant research project
• full status as an employee at TU Darmstadt, including pension and health care benefits
• excellent facilities for professional and personal development

Further Information and How to Apply:
Applications should arrive before December 6, 2017. The application process will be available until all positions are filled.

An electronic application form and a description of the different part projects is available at the SF4.0 application portal

Further information on the project, open positions and the application process can be found at the coordinator web page and project web page.

### 2 Studentships in Swansea, UK

Formal Modelling, Analysing and Testing of Real Time Systems

The Swansea Railway Verification Group has two studentship available on Formal Modelling, Analysing and Testing of Real Time Systems:

• For a PhD (4 years)
• For an MSci (1 year)

• Closing date for both studentships: 15 December 2017
• Start date for both studentships: January 2018 (or later)

### 3-year postdoc and 3-year PhD-student position at the University of Innsbruck, Austria

Formalizing Complexity and Termination Techniques

The Computational Logic research group at the University of Innsbruck has two open positions funded by the FWF (Austrian science fund) via the START project “Certifying Termination and Complexity Proofs of Programs”.

The project aims at increasing the reliability in current complexity and termination provers by independently checking the generated proofs. To this end, several analysis techniques will be formalized in the theorem prover Isabelle/HOL, with a focus on LLVM and integer transition systems.

For this project, we are looking for two enthusiastic researchers with a background in computational logic. Knowledge of automated termination analysis, complexity analysis, or theorem proving would be an asset. Candidates with a strong theoretical background in related areas are also encouraged to apply. The PhD-student candidate must have a Master's or equivalent degree. Knowledge of German is not essential.

The salary is determined by the FWF-funding scheme (3,627 EUR monthly gross salary for postdocs, and 2,071 EUR for PhD-students, cf. this web page).

Applications (including a CV, a publication list (only for postdocs), and a letter of recommendation) may be emailed to the project leader René Thiemann no later than December 18, 2017.

We plan to make decisions on these positions in December 2017. The preferred starting date is within the first three months of 2018. Informal inquiries are also welcome via email.

The city of Innsbruck 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.

Further information is available from the following links:

### PhD Program at Carnegie Mellon, USA

Pure and Applied Logic

The Homotopy Type Theory research group at CMU Philosophy has positions open in the coming academic year 2018-19 for incoming PhD students interested in doing research in type theory, homotopy theory, (higher) category theory, and related areas. For more information about our very active research group, see the info page.

The department also has a research group focused on interactive theorem proving, formal verification, and formalization of mathematics, centered on the Lean Theorem Prover.

For information about the Pure and Applied Logic PhD program at CMU, see the info page.

Admitted students receive full tuition, a generous living stipend, health insurance, and other benefits. Students are typically assigned limited teaching duties as graders or teaching assistants, or, when available, are supported by a research grant. Upon completion of the program, students receive the degree of PhD in Pure and Applied Logic. For further information, please contact Steve Awodey or Jeremy Avigad.

## Counting of the Ballots of the CADE Trustee Elections

Martin Giese

An election was held to fill 3 positions. Juergen Giesl, Marijn Heule, Andrew Reynolds, and Bruno Woltzenlogel Paleo were nominated. 107 valid ballots were returned. Therefore, in each iteration of the single transferable vote algorithm described in the CADE Bylaws, a candidate is elected if she or he gets at least 54 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. no supp. Juergen Giesl 42 16 26 13 10 Marijn Heule 20 28 25 19 15 Andrew Reynolds 20 32 19 19 17 Bruno Woltzenlogel Paleo 25 20 21 21 20

No candidate reaches at least 54 first preference votes.

By redistributing the votes of Marijn Heule, one gets the following table:

 Candidate 1st pref. 2nd pref. 3rd pref. no supp. Juergen Giesl 46 29 22 10 Andrew Reynolds 34 29 27 17 Bruno Woltzenlogel Paleo 27 35 25 20

No candidate reaches at least 54 first preference votes.

By redistributing the votes of Bruno Woltzenlogel Paleo, one gets the following table:

 Candidate 1st pref. 2nd pref. no supp. Juergen Giesl 56 41 10 Andrew Reynolds 43 47 17

Now, Juergen Giesl reaches at least 54 first preference votes, and is elected.

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

 Candidate 1st pref. 2nd pref. 3rd pref. no supp. Marijn Heule 37 30 25 15 Andrew Reynolds 31 38 21 17 Bruno Woltzenlogel Paleo 35 24 28 20

No candidate reaches at least 54 first preference votes.

By redistributing the votes of Andrew Reynolds, one gets the following table:

 Candidate 1st pref. 2nd pref. no supp. Marijn Heule 55 37 15 Bruno Woltzenlogel Paleo 47 40 20

Now, Marijn Heule reaches at least 54 first preference votes, and is elected.

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

 Candidate 1st pref. 2nd pref. no supp. Andrew Reynolds 54 36 17 Bruno Woltzenlogel Paleo 47 40 20

Now, Andrew Reynolds reaches at least 54 first preference votes, and is elected.

To summarize, the 3 candidates elected are Juergen Giesl, Marijn Heule, and Andrew Reynolds.

## The Editor's Corner

Philipp Rümmer and Sophie Tourret

Obituaries

• The mathematician Vladimir Voevodsky, Fields medalist and strong advocate of computer-verified mathematics, has passed away. His eulogy can be found here.
• The logician Kosta Dosen, known for his works in proof theory, also passed away recently.
• We should also remember Corrado Böhm who was, among other things, a pioneer in lambda-calculus and functional programming.

* * *

An OCaml library for first-order logic worth knowing

Less than a year before officially completing my PhD (Sophie writing), I was faced with a dilemma: either implement my most recent results or pursue the theoretical work without the backing of experiments. Given the short amount of time I had left, I was tempted to just forget the implementation, even knowing that this would degrade the worth of my results. Indeed, on top of my own calculus and data-structures, I also needed to implement from scratch well-founded orderings and congruence closure on ground first-order terms, among other things. Fortunately, at that time I became aware of LogTK, an OCaml library for first-order logic. LogTK is not too hard to handle when you have prior experience in OCaml, especially thanks to this tutorial, that really helped me a lot to get started. Thanks to it, I had experimental results in time for the following CADE deadline.

What I really want to say with this story is that LogTK is a cool piece of software that allowed me to go further than I expected during my PhD. If you have experience in OCaml and need to implement something in first-order logic that can't just be hacked from an existing solver, you may want to give it a try!

By the way, if you know of some other cool and not well-known library related to automated reasoning, feel free to write something about it and send it to us.

* * *

We wish happy end-of-the-year festivities and holidays to all the members of the AAR.