Newsletter No. 111

June 2015

June 2015

- From the AAR President, Larry Wos
- Announcement of the 2015 Herbrand Award
- Skolem Awards at CADE-25
- IJCAR 2016 PC Co-Chair Appointment
- Call for Nominations: CADE Trustees Election
- New Conference Replacing RTA-TLCA
- Conferences
- CADE-25: International Conference on Automated Deduction
- LNK 2015: Non-Classical Logic. Theory and Applications
- RAMiCS 2015: Relational and Algebraic Methods in Computer Science
- MICAI-2015: Mexican International Conference on Artificial Intelligence
- KEOD 2015: Knowledge Engineering and Ontology Development
- LPAR-20: Logic for Programming, Artificial Intelligence and Reasoning
- FLOPS 2016: Functional and Logic Programming
- iFM 2016: Integrated Formal Methods

- Workshops
- Proving in Mathematics Education at University and at School
- BLC 2015: British Logic Colloquium
- SR-2015: Strategic Reasoning
- DIFTS '15: Design and Implementation of Formal Tools and Systems
- LNMR 2015: Learning and NonMonotonic Reasoning
- ACL2 2015: ACL2 Theorem Prover and Its Applications
- DCM 2015: Developments in Computational Models

- Tutorials
- 25th Anniversary of Superposition: Status and Future
- Isabelle Tutorial 1
- Reasoning about Computational Systems using Abella
- Beluga: Programming Proofs about Formal Systems
- From Programs to Logic: The CPROVER Verification Tools
- The Sequent Calculus of the KeY Tool
- Lean Theorem Prover: A Tutorial
- Isabelle Tutorial 2
- Coq Tutorial

- Open Positions
- The Editor's Corner

Do you have in hand a program that proves theorems? Would you like to have access to a set of problems, focusing on geometry, that are graduated in difficulty and that might, if considered, lead you to the formulation of a new strategy? This column offers just such a set of problems.

Yes, the problems you find here focus on plane geometry, an area of mathematics
you most likely first studied in high school. But plane geometry is hardly
“simple”. I note, for example, that the eminent logician Alfred
Tarski took an interest in geometry and worked on it for many years. Among his
accomplishments in the area was a 13-axiom system that enables a person, or a
program if sufficiently powerful, to prove a large number of theorems. Points
were all he needed: just the notions of betweenness, denoted by `T`, and
equidistant, denoted by `E`.

For Tarski, betweenness does not mean for points `x`, `y`, and `z` that `y` is
necessarily strictly between `x` and `z`; in fact, for him, `T(x,y,z)` admits that `x`
and `y` and `z` are all the same point. When I encountered this axiom system, I
found it most surprising that just betweenness and equidistance sufficed.

The following axioms provide the basis of any study you might undertake.

identity axiom for betweenness:

-T(x,y,x) | (x = y).

transitivity axiom of betweenness:

-T(x,y,u) | -T(y,z,u) | T(x,y,z).

connectivity axiom for betweenness:

-T(x,y,z) | -T(x,y,u) | (x = y) | T(x,z,u) | T(x,u,z).

reflexivity axiom for equidistance:

E(x,y,y,x).

identity axiom for equidistance:

-E(x,y,z,z) | (x = y).

transitivity axiom for equidistance:

-E(x,y,z,u) | -E(x,y,v,w) | E(z,u,v,w).

Outer Pasch's axiom (2 clauses):

-T(x,v,u) | -T(y,u,z) | T(x,f1(v,x,y,z,u),y). -T(x,v,u) | -T(y,u,z) | T(z,v,f1(v,x,y,z,u)).

Euclid's axiom (three clauses):

-T(x,u,v) | -T(y,u,z) | (x = u) | T(x,z,f2(v,x,y,z,u)). -T(x,u,v) | -T(y,u,z) | (x = u) | T(x,y,f3(v,x,y,z,u)). -T(x,u,v) | -T(y,u,z) | (x = u) | T(f2(v6,x,y,z,u),v6,f3(v6,x,y,z,u)).

five-segment axiom:

-E(x1,y1,x2,y2) | -E(y1,z1,y2,z2) | -E(x1,u1,x2,u2) | -E(y1,u1,y2,u2) | -T(x1,y1,z1) | -T(x2,y2,z2) | (x1 = y1) | E(z1,u1,z2,u2).

axiom of segment construction (two clauses):

T(x,y,f4(x,y,u,v)). E(y,f4(x,y,u,v),u,v).

lower dimension axiom (three clauses):

-T(c1,c2,c3). -T(c2,c3,c1). -T(c3,c1,c2).

upper dimension axiom:

-E(x,u,x,v) | -E(y,u,y,v) | -E(z,u,z,v) | (u = v) | T(x,y,z) | T(y,z,x) | T(z,x,y).

weakened continuity axiom (two clauses):

-E(u1,x1,u1,x2) | -E(u1,z1,u1,z2) | -T(u1,x1,z1) | -T(x1,y1,z1) | E(u1,y1,u1,f5(x1,y1,z1,x2,z2,u1)). -E(u1,x1,u1,x2) | -E(u1,z1,u1,z2) | -T(u1,x1,z1) | -T(x1,y1,z1) | T(x2,f5(x1,y1,z1,x2,z2,u1),z2).

I strongly conjecture that, in the following set of theorems, your program will find the first few perhaps easy to prove. I believe, however, that the set will tax your program after the first few successes.

E(x,y,x,y). % Satz 2.1, CHZ1 -E(xa,xb,xc,xd) | E(xc,xd,xa,xb). % Satz 2.2, CHZ2 -E(xa,xb,xc,xd) | -E(xc,xd,xe,xf) | E(xa,xb,xe,xf). % Satz 2.3, CHZ3 -E(xa,xb,xc,xd) | E(xb,xa,xc,xd). % Satz 2.4, CHZ4 -E(xa,xb,xc,xd) | E(xa,xb,xd,xc). % Satz 2.5, CHZ5 E(x,x,y,y). % Satz 2.8, CHZ8 -T(xa,xb,xc) | -T(xa1,xb1,xc1) | -E(xa,xb,xa1,xb1) | -E(xb,xc,xb1,xc1) | E(xa,xc,xa1,xc1). % Satz 2.11, CHZ11 xq = xa | -T(xq,xa,u) | -E(xa,u,xc,xd) | f4(xq,xa,xc,xd) = u. % Satz 2.12, CHZ12 -E(u,v,x,x) | u=v. % Not one of Szmielew's theorems but we proved it, CHZZ -T(xa,xb,xc) | T(xc,xb,xa). % Satz 3.2., CH4 T(x,y,y). % Satz 3.1, CH3 T(xa,xa,xb). % Satz 3.3, CH2 -T(xa,xb,xc) | -T(xb,xa,xc) | xa = xb. % Satz 3.4, CHZ34 -T(xa,xb,xd) | -T(xb,xc,xd) | T(xa,xb,xc). % Satz 3.51, CHZ351 -T(xa,xb,xd) | -T(xb,xc,xd) | T(xa,xc,xd). % Satz 3.52, CHZ352 -T(xa,xb,xc) | -T(xa,xc,xd) | T(xb,xc,xd). % Satz 3.61, CHZ361 -T(xa,xb,xc) | -T(xa,xc,xd) | T(xa,xb,xd). % Satz 3.61a, CHZ361a -T(xa,xb,xc) | -T(xb,xc,xd) | xb = xc | T(xa,xc,xd). % Satz 3.71, CHZ71 -T(xa,xb,xc) | -T(xa,xc,xd) | T(xa,xb,xd). % Satz 3.62, CHZ362 -T(xa,xb,xc) | -T(xb,xc,xd) | xb = xc | T(xa,xb,xd). % Satz 3.72, CH72

The goal is to prove all 20 theorems. A systematic approach that merits study and that offers an interesting challenge consists of proving a theorem, adjoining that theorem for the next experiment, and then seeking another proof. The results of this iterative approach might shed light on the power of your program.

As you probably have surmised, I have used OTTER to prove all 20 theorems; but I relied on a wide variety of approaches, only one of which was the cited iterative approach. If your program is able to prove all the theorems with this approach or any approach, I would enjoy hearing from you about your success.

I am happy to announce that **Andrei Voronkov** will be awarded the Herbrand Award
at CADE 2015, in recognition of his numerous theoretical and practical
contributions to automated deduction, and the development of the award-winning
Vampire theorem prover.

The Skolem Award was instituted to reward a CADE paper that has passed the test of time by being most influential in the field.

The Skolem award committee for CADE-25 consisted of Alessandro Armando, Gilles Barthe, Claude Kirchner (chair), Christopher Lynch, Leonardo de Moura, Ulrike Sattler, Geoff Sutcliffe, Toby Walsh, and Christoph Weidenbach.

According to this committee's recommendation, the following papers receive Skolem Awards in 2015:

- CADE-20 (2005):
**Christian Urban**and**Christine Tasson**.*Nominal Techniques in Isabelle/HOL.* - CADE-14 (1997):
**Hantao Zhang**.*SATO: An Efficient Propositional Prover.* - CADE-8 (1986):
**Leo Bachmair and Nachum Dershowitz**.*Commutation, Transformation, and Termination.* - CADE-0 (1968) and CADE-1 (1975) considered jointly:
**N. G. de Bruijn**.*The Mathematical Language AUTOMATH, its Usage, and Some of its Extensions*(presented at CADE-0).

It is a pleasure to report that the IJCAR Steering Committee appointed Nicola Olivetti and Ashish Tiwari as PC Co-Chairs of IJCAR 2016. Both join the IJCAR Steering Committee, and Ashish also joins the CADE Board as ex officio trustee.

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

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

- Peter Baumgartner (elected 2013)
- Maria Paola Bonacina (president, elected 2013)
- Amy Felty (CADE-25 program co-chair)
- Pascal Fontaine (elected 2014)
- Martin Giese (secretary)
- Jürgen Giesl (elected 2014)
- Neil Murray (treasurer)
- Larry Paulson (elected 2010, reelected 2013)
- Brigitte Pientka (elected 2010, reelected 2013)
- Renate Schmidt (vice-president, elected 2010, reelected 2012)
- Geoff Sutcliffe (elected 2011, reelected 2014)
- Ashish Tiwari (IJCAR 2016 program co-chair)
- Christoph Weidenbach (elected 2009, reelected 2012)

The terms of Renate Schmidt and Christoph Weidenbach expire. Both have served for two terms, and therefore cannot be nominated for a third term.

The term of office of Amy Felty as CADE-25 program co-chair also ends. As outgoing ex-officio trustee, she is eligible to be nominated as elected trustee.

In summary, we are seeking to elect two trustees.

Nominations can be made by any AAR member, either by e-mail or in person at the CADE business meeting at CADE-25 in Berlin. 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 Maria Paola Bonacina, CADE President
(`mariapaola (dot) bonacina (at) univr (dot) it`), and Martin Giese,
CADE Secretary (`martingi (at) ifi (dot) uio (dot) de`), up to the
upcoming CADE business meeting.

As requested by the participants of the RTA-TLCA conference in Vienna 2014, the united Steering Committees of Rewriting Techniques and Applications (RTA) and Typed Lambda Calculi and Applications (TLCA) have prepared a proposal to replace our existing two conferences by a new one of a broader scope.

As we embark on this exciting journey, we invite all members of the computer science community to provide comments, remarks, and suggestions for the new conference. All input will be passed on to the steering committee of the new conference after its constitutional general meeting on 1 July 2015.

It is our thesis that formal elegance is a prerequisite to efficient implementation. -- Gérard Huet[4] We, the communities behind the RTA[1] and TLCA[2] conferences, believe that our field has evolved and developed richer connections with many both practical and theoretical aspects of computer science and logic research since the inception of RTA in 1983 and TLCA in 1993. In particular, the scope of the two original conferences widened to include a significant overlap, and in fact the conferences have already collaborated by having most of our meetings since 2003 as the joint RDP[3] conference. We have therefore decided to propose a new conference,Formal Structures for Computation and Deduction (FSCD)which not only combines our scope but further extends it to cover all the inter-related formal areas that researchers in formal structures for computation and deduction engage in. The name of the new conference comes from an unpublished but important book by Gérard Huet[4] that was a strong influence on many researchers in our area. We are grateful to Gérard for allowing us to reuse the name. The extended scope of the conference will include all research related to formal structures for computation and deduction, in particular all areas/categories included in the attached non-exhaustive list of topics. We look very much forward to serve the scientific community with this new conference, which inherits as well as updates and modernizes the scope of the conferences it replaces. References. [1]http://rewriting.loria.fr/rta/ [2]http://www.mimuw.edu.pl/tlca/ [3]http://users.dsic.upv.es/~rdp03/ [4]http://pauillac.inria.fr/~huet/PUBLIC/Formal_Structures.ps.gz FSCD initial non-exhaustive list of topics (intended to extend the current RTA and TLCA scope, and expected to evolve over time): 1. Calculi a. Lambda-calculus b. Rewriting formats (string, term, higher-order, graph, conditional, ...) c. Proof theory (natural deduction, sequent calculi, proof nets, ...) d. Strategies in computation and deduction 2. Type Theory and Logical Frameworks a. Type systems (recursive, intersection types, polymorphism, ...) b. Dependent types and homotopy type theory c. Linear logic and other constructive logics d. Implicit complexity 3. Fundamentals of Functional and Declarative Programming a. Unification and narrowing b. Tree automata c. Continuations and control operators d. Coinduction and infinitary systems 4. Semantics a. Abstract machines b. Categorical semantics c. Denotational and game semantics d. Quantitative models (timing, probabilities) 5. Algorithmic Analysis of Formal Systems a. Type inference and type checking b. Complexity analysis c. Checking termination, confluence, and related properties d. Formalisation and certification 6. Tools and Applications a. Proof assistants and interactive theorem proving b. Automated deduction (completion, constraints, equational logic...) c. Symbolic computation d. Implementation techniques for formal systems e. Case studies and applications based on formal systems

1 to 7 August 2015, Berlin, Germany

Registration, accommodation, and travel information for CADE-25 and all the affiliated events can be found at the conference website. The call for the Woody Bledsoe Student Travel Award is included below.

1-3 August 2015: Workshops, Tutorials, Special Session, Competitions

4-7 August 2015: CADE main conference, Competitions

CADE is the major forum for the presentation of research in all aspects of automated deduction. The CADE-25 conference programme will include invited talks, paper presentations, system descriptions, workshops, tutorials, system competitions, a poster session, and a special jubilee session on the past, present, and future of automated deduction.

Invited speakers (CADE-25 jubilee session)

- Ursula Martin, University of Oxford
- Frank Pfenning, Carnegie Mellon University
- David Plaisted, University of North Carolina at Chapel Hill
- Andrei Voronkov, University of Manchester

Invited speakers (CADE-25 main conference)

- Ulrich Furbach, University of Koblenz, ECCAI invited talk
- Edward Zalta, Stanford University
- Michael Genesereth, Stanford University (joint with RuleML Symposium)

Numerous further invited presentations will be part of the CADE-25 workshop program. Reception and dinner speeches will be given by Wolfgang Bibel and Jörg Siekmann.

- 7 invited presentations (see above)
- 24 regular research papers
- 12 system descriptions
- 9 workshops and 1 poster event
- 6 tutorials
- 3 system competitions
- presentation of Herbrand Award to Andrei Voronkov
- presentation of Skolem Awards (for most influential CADE papers from CADE-20, CADE-14, CADE-8, and CADE-0-1)
- presentation of best paper award to Vijay D'Silva and Caterina Urban

- Bridging: Bridging the gap between human and automated reasoning
- DT: 29. Jahrestreffen der GI-Fachgruppe Deduktionssysteme
- HOL4: HOL4 Workshop
- IWC: The 4th International Workshop on Confluence
- LFMTP: International Workshop on Logical Frameworks and Meta-Languages: Theory and Practice
- LOCAS: Low-level Code Analysis for Security
- PxTP: Workshop on Proof eXchange for Theorem Proving
- QUANTIFY: 2nd International Workshop on Quantification
- Vampire: The Vampire Workshop

- Abella: Reasoning about Computational Systems using Abella
- Beluga: Programming proofs about formal systems
- CPROVER: From Programs to Logic: The CPROVER verification tools
- Isabelle: Isabelle Tutorial
- Lean: Lean Theorem Prover: a Tutorial
- Superposition: 25th Anniversary of Superposition: Status and Future

- CASC: The CADE ATP System Competition
- CoCo: The 4th Confluence Competition
- termCOMP: Termination Competition

- EPS: The CADE-25 Taskforce towards an Encyclopedia of Proof Systems

The Woody Bledsoe Student Travel Award was created to honor the memory of Woody Bledsoe, for his contributions to mathematics, artificial intelligence, and automated theorem proving, and for his dedication to students. The award is intended to enable selected students to attend the International Conference on Automated Deduction (CADE) or the International Joint Conference on Automated Reasoning (IJCAR), whichever is scheduled for the year, by covering part of their expenses.

The winners of the CADE-25 Woody Bledsoe Student Award will be partially reimbursed (e.g., between Euro 200 and Euro 750) for their conference registration, transportation, and accommodation expenses. Preference will be given to students who will play an active role in the conference (including satellite workshops, competitions, tutorials and poster events) and do not have alternative funding. However, also students in other situations are very much encouraged to apply.

A nomination consists of a recommendation letter of up to 300 words from the student's advisor. Nominations for CADE-25 should be sent by e-mail to the chairs and conference organizers.

Nominations must arrive no later than 21 June 2015. The winners will be notified by 28 June 2015.

The awards will be presented at CADE-25; in case a winner does not attend, the chairs may transfer the award to another nominee or give no award.

24 to 26 September 2015, Toruń, Poland

This is the seventh conference on this topic. The first, second, fourth and sixth editions of conference were organized by Department of Logic and Methodology at Łódź University. The third and fifth edition was organized by Department of Logic at NCU in Toruń. The thematic range of the conference remains the same: theories of nonclassical logics (modal, many-valued, temporal, paraconsistent, epistemic, deontic, substructural, and nonmonotonic logic) and their applications in computer science, artificial intelligence, formal linguistics, cognitive studies, as well as to the deeper analysis of traditional philosophical problems.

The deadline for abstracts is **15 July 2015**.
See the conference web
site for details.

28 September to 1 October 2015, Braga, Portugal

Since 1994, the RelMiCS meetings on Relational Methods in Computer Science have been a main forum for researchers who use the calculus of relations and similar algebraic formalisms as methodological and conceptual tools. The AKA workshop series on Applications of Kleene algebra started with a Dagstuhl seminar in 2001 and was co-organised with the RelMiCS conference until 2009. Since 2011, joint RAMiCS conferences continue to encompass the scope of both RelMiCS and AKA.

If you are doing a PhD or an MSc in the research areas of the RAMiCS
conference, please consider submitting an extended abstract of your
ongoing work for presentation at the conference.
The deadline for extended abstracts is **3 July 2015**. See the
conference web site
for details.

25 to 31 October 2015, Cuernavaca, Mexico

MICAI is an international conference covering all areas of Artificial Intelligence, traditionally held in Mexico. The conference is organized by the Mexican Society for Artificial Intelligence (SMIA) and hosted by the Instituto de Investigaciones Eléctricas, Cuernavaca, Mexico, near Mexico City. The scientific program includes keynote lectures, paper presentations, tutorials, panels, and workshops.

The deadline for abstracts is **23 June 2015**. See the
conference web site
for details.

12 to 14 November 2015, Lisbon, Portugal

Knowledge engineering refers to all technical, scientific and social aspects involved in building, maintaining and using knowledge-based systems. Knowledge engineering is a multidisciplinary field, bringing in concepts and methods from several computer science domains such as artificial intelligence, databases, expert systems, decision support systems and geographic information systems. The KEOD conference aims at becoming a major meeting point for researchers and practitioners interested in the study and development of methodologies and technologies for knowledge engineering and ontology development.

The deadline for regular papers is **2 July 2015**.
See the conference web site
for details.

24 to 28 November 2015, Suva, Fiji

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

Prospective authors are required to register a title and an abstract by **30
June 2015**. See the conference web
site for details.

3 to 6 March 2016, Kochi, Japan

FLOPS aims to bring together practitioners, researchers and implementors of the declarative programming, to discuss mutually interesting results and common problems: theoretical advances, their implementations in language systems and tools, and applications of these systems in practice. The scope includes all aspects of the design, semantics, theory, applications, implementations, and teaching of declarative programming. FLOPS specifically aims to promote cross-fertilization between theory and practice and among different styles of declarative programming.

The paper submission deadline is **14 September 2015**.
See the conference web site for details.

1 to 5 June 2016, Reykjavík, Iceland

iFM 2016 is concerned with how the application of formal methods may involve modelling different aspects of a system which are best expressed using different formalisms. Correspondingly, different analysis techniques may be used to examine different system views, different kinds of properties, or simply in order to cope with the sheer complexity of the system. The iFM conference series seeks to further research into hybrid approaches to formal modelling and analysis; i.e., the combination of methods for system development, regarding modelling and analysis, and covering all aspects from language design through verification and analysis techniques to tools and their integration into software engineering practice.

**Prospective workshop organizers** are invited to submit proposals for
workshops to be affiliated to iFM 2016, on topics related to the
conferences main subjects. The deadline is **20 July 2015**.
Contact the workshop chair, Marcel
Kyas, for details.

25 to 27 August 2015, Győr, Hungary

The minisymposium intends to discuss usability of technology applications in education in relation to proving and primarily focuses on a specific technology, Computer Theorem Proving (TP), for education in academia and beyond. The proposal is backed by increasing interest in technology integration in education to support proofs as well as the applications of TP.

For preparing discussions we invite submission of abstracts (at most 3 pages)
on topics including, but not limited to: demonstration of tools supporting
proofs and using TP technology; experiences from academic courses of various
kinds using TP-based software; applications of mathematics and mathematical
activities which might specifically take advantage from support by TP-based
software; mathematical concepts and TP technology specifically
relevant for software support in teaching and learning to prove; and
experiences from initiatives and activities filling the gap between school and
university. The submission deadline is **15 June 2015**. See the
minisymposium's web site
for details.

2 to 4 September 2015, Cambridge, UK

The British Logic Colloquium is a general logic meeting covering a variety
of topics within mathematical, philosophical and computer science logic. The
meeting will include ten invited talks and a number of contributed talks.
Anyone wishing to contribute a talk should send an abstract (of about 250
words) to blc-2015@cl.cam.ac.uk by
**15 July 2015**.

Moreover, the **BLC PhD** day (on 1 and 2 September) provides an opportunity for postgraduates to meet and
discuss their research or area of interest with fellow young
logicians. If you wish to attend the PhD day, please email
blc-2015-phd@maths.cam.ac.uk, including your name, affiliation, and
whether you would like to present a talk or a poster.

There is a limited number of bursaries available for students who wish
to attend. A bursary will provide a subsidy for travel and
accommodation costs. Applications for bursaries should be accompanied
by a short paragraph stating your affiliation, the name of your
supervisor and a brief description of your research; priority will be
given to those contributing a talk in either the PhD day or the main
BLC meeting. Deadline: **15 July 2015**.

21 and 22 September 2015, Oxford, UK

Strategic reasoning is one of the most active research areas in the multi-agent system domain. The literature in this field is extensive and provides a plethora of logics for modelling strategic ability. Theoretical results are now being used in many exciting domains, including software tools for information system security, robot teams with sophisticated adaptive strategies, and automatic players capable of beating expert human adversary, just to cite a few. All these examples share the challenge of developing novel theories and tools for agent strategies that take into account the likely behaviour of adversaries. The SR international workshop aims to bring together researchers working on different aspects of strategic reasoning in computer science, artificial intelligence and multi-agent systems research, both from a theoretical and a practical viewpoint.

Submissions should be an abstract of at most 5 pages. The submission deadline
is **1 July 2015** (strict). See the workshop web site for details.

26 and 27 September 2015, Austin, Texas

The Design and Implementation of Formal Tools and Systems (DIFTS) workshop emphasizes insightful experiences in formal tools and systems design. The workshop provides an opportunity for discussing engineering aspects and various design decisions required to put formal tools and systems into practical use.

The workshop is co-located with FMCAD 2015 and SAT 2015. The regular talks of DIFTS workshop will be on September 26, 2015. The full-day tutorial (joint with FMCAD 2015, SAT 2015, and MEMOCODE 2015) will be on September 27, 2015.

The workshop specifically solicits contributions with substantial engineering details that often do not get published but have significant practical impact. Papers in the following two categories are solicited: (a) system category (10 pages, double column, 11pt), and (b) tool category (8 pages, double column, 11pt). The abstract submission deadline is 7 July 2015. See the workshop web site for details.

27 to 30 September 2015, Lexington, Kentucky, USA

The 2nd International Workshop on Learning and NonMonotonic Reasoning (LNMR 2015) is co-located with the 13th International Conference on Logic Programming and Nonmonotonic Reasoning (LPNMR 2015).

This workshop follows from its first edition in 2013 in an attempt to provide an open forum for the identification of problems and discussion of possible collaborations among researchers with complementary expertise. To facilitate interactions between researchers in the areas of (machine) learning and nonmonotonic reasoning, we welcome contributions focusing on problems and perspectives concerning both learning and nonmonotonic reasoning.

Papers must be registered by **22 June 2015**. See the workshop web site for details.

1 and 2 October 2015, Austin, Texas, USA

The 2015 ACL2 Workshop will be held in Austin, Texas, in conjunction with (and immediately following) FMCAD 2015. We invite users of ACL2, users of other theorem provers, and persons interested in the applications of theorem proving technology to attend. Keynote talks will be given by J Strother Moore and John O'Leary.

See the workshop web site for further information including paper submission, organization, venue, lodging, and eventually, registration and program information.

28 October 2015, Cali, Colombia

The 11th International Workshop on Developments in Computational Models will be a satellite event of ICTAC 2015 (International Colloquium on Theoretical Aspects of Computing). The aim of this workshop is to bring together researchers who are currently developing new computational models or new features for traditional computational 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.

Submissions should be an abstract of at most 5 pages. The submission deadline
is **3 August 2015**. See the workshop web site for details.

1 August 2015, Berlin, Germany

A full-day tutorial on superposition, organized by Stephan Schulz and Christoph Weidenbach, is scheduled as associated event of CADE-25. Superposition is the calculus behind successful automatic theorem provers such as E, SPASS, and Vampire. See the CADE web site for details.

1 August 2015, Berlin, Germany

A full-day tutorial on Isabelle is scheduled as associated event of CADE-25. Isabelle is a popular proof assistant based on higher-order logic.

2 August 2015, Berlin, Germany

A half-day tutorial on the Abella proof assistant is scheduled as associated event of CADE-25. Abella is based on lambda-tree syntax and is well-suited for reasoning about the meta-theory of programming languages and other logical systems which manipulate objects with binding.

2 August 2015, Berlin, Germany

A half-day tutorial on the Beluga language is scheduled as associated event of CADE-25. Beluga allows specification of formal systems (such as lambda-calculi and type systems) using a foundation of contextual modal logic.

3 August 2015, Berlin, Germany

A half-day tutorial on the CPROVER program verification system is scheduled as associated event of CADE-25. CPROVER is one of the largest, most established and powerful automatic verification systems for C and C++.

3 August 2015, Berlin, Germany

A half-day tutorial on the KeY system's sequent calculus is scheduled as associated event of CADE-25. is a formal software development tool that aims to integrate design, implementation, formal specification, and formal verification of object-oriented (e.g., Java) software as seamlessly as possible.

3 August 2015, Berlin, Germany

A half-day tutorial on the Lean prover is scheduled as associated event of CADE-25. Lean is a new theorem prover that aims to bridge the gap between interactive and automated theorem proving, by situating automated tools and methods in a framework that supports user interaction and the construction of fully specified axiomatic proofs.

21 to 23 August 2015, Nanjing, China

A three-day tutorial on the Isabelle proof assistant will precede the ITP 2015 conference.

27 to 29 August 2015, Nanjing, China

A three-day tutorial on the Coq proof assistant will follow the ITP 2015 conference.

The University of Innsbruck invites applications for a 6 year postdoctoral position in the Computational Logic research group. Candidates must hold a PhD degree in computer science. A strong background in computational logic (in particular term rewriting) is desired. The ideal candidate enjoys working with students at all levels. Candidates are expected to conduct research leading to a habilitation and contribute to teaching and administration. Knowledge of German is not essential.

The position is a full-time "B1/3 position" with teaching obligations of
4 hours per semester. The annual gross salary is approximately EUR 50,000.
See also the official job advert (reference MIP-8628).
Applications (including CV, publication list, and two letters of
recommendation) must be submitted electronically
no later than **30 June 2015**. The starting date for the position is
1 October 2015. Informal inquiries may be addressed to
`aart.middeldorp at uibk.ac.at`.

TU Wien, TU Graz, and JKU Linz are seeking exceptionally talented and motivated students for their joint doctoral program LogiCS. The LogiCS doctoral college focuses on interdisciplinary research topics covering (i) computational logic, and applications of logic to (ii) databases and artificial intelligence as well as to (iii) computer-aided verification.

Successful applicants will work with and be
supervised by leading researchers in the fields of computational
logic, databases and knowledge representation, and computer-aided
verification.
The LogiCS faculty comprises 15 renowned researchers with strong
records in research, teaching and advising, complemented by 12
associated members who further strengthen the research and teaching
activities of the college.
Detailed information about the application process is available on the
LogiCS web-page.
Next application deadline: **1 July 2015**.

The Inria Nancy – Grand-Est research center, colocated with LORIA, is
looking for a confirmed (or an outstanding junior) software engineer for the
development of a new counterexample generator for higher-order logic. The
targeted hiring date is **1 October 2015**. The contract is for two years.
The montly salary is expected to be
between 2600 to 3200 EUR gross, depending on experience. This position can be
interesting for an outgoing Ph.D. student or a strong programmer with a
master's degree. Neither knowledge of French nor European citizenship are required.

This project aims at developing a generic counterexample generator for higher-order logic, targeted at the hundreds of users of Coq, Isabelle, and similar systems, to help them debug their specifications. This generator will be based on an SMT solver. Solid bases in functional programming and experience with logic are prerequisites.

See the official job advert or contact the newsletter editor for more information.

The **Skolem award** was established to
reward a CADE
paper that has passed the test of time. Starting this year, at every CADE the Skolem Award
Committee selects a paper presented at the CADE held 10 years earlier to
receive the Skolem award. Until 2025, additional awards will be given to cover
CADE since its beginnings in 1968.
The CADE board of trustees appointed Claude Kirchner to chair the first
Skolem Award Committee, responsible for selecting the first round of
awards at CADE-25. The first
year's results are presented above. Congratulations to
the winners!

I am also pleased to see the **Herbrand award** go to
Andrei Voronkov. My students and I use Vampire (and countless other automatic
theorem provers) on a daily basis to discharge interactive proof obligations.
Congratulations, Andrei!

* * *

Back in March, I attended the **second workshop on automating induction** in
Gothenburg, Sweden. It is exciting to see that many problems that looked very
difficult are perhaps not as difficult as we thought. I went there as an
observer, hoping to benefit from this research as an end user. I am
particularly excited about combinations such as “superposition +
induction” and “SMT + induction”. So far, the workshop
series has been a mostly European affair, despite the pioneering work on
automating induction in the ACL2 prover. The third workshop is expected to be
held next spring in Vienna, Austria, hopefully with a wider geographical
reach. A wiki and
mailing list have been set up to discuss shared issues, such as benchmark
problems and formats for problems and solutions. You are welcome to join!

* * *

This brings me to my last point. Increasingly, we see **software reuse**
in the world of reasoners. The
higher-order automatic prover LEO-II relies on a first-order prover
to detect inconsistent clause sets early. Its rival Satallax is
built around a SAT solver, and recent versions (starting with CASC 2013) also
invoke a first-order prover. SMT solvers are built on SAT solvers in a nice
modular fashion (at least in principle). And there are dozens more examples of
the kind, sometimes with many layers of nesting.
Basing your work on other people's work means that your software will get
better even if you stop working on it actively. *It is a great recipe for
academic success!*

However, for such a cooperative architecture to work well, each reasoner must
be a good “team player”. Often, we put a lot of work into
processing the input and forget about the output. When connecting formal tools
together, it is crucial that the output is detailed enough and at the same
level of abstraction as the input. This I call the **Russian doll
principle**, and I like to see it as the practical materialization of
institution theory.
The TPTP/TSTP languages are well designed in that respect,
since they closely reflect each other. Parallel efforts for SMT-LIB should be
encouraged. As developers, we often forget that our software might be embedded
in other tools. This belief that we stand at the top of the food (or tool)
chain is usually either wrong or self-fulfilling.

Another related lesson, from Bjarne Stroustrup, is what he calls the
**zero-overhead principle**. Consider a reasoner (prover, solver, model
finder, etc.) B based on a reasoner A for a less rich logic. In an ideal
world, B should be as efficient as A on problems within A's fragment. Such
problems should just “slide through”. And problems *mostly*
within A's fragment should still *mostly* slide through, with most of
the work performed by A. I attribute much of the success of SMT solvers to
this observation and find it unsurprising that Vampire's new SAT-based AVATAR
architecture is giving that venerable prover such a boost.
(Un)fortunately, it takes much more than a blind
observance of the Russian doll and zero-overhead principles to get one's
hands on an Herbrand award!