The proceedings are available in this PDF (which contains a two page extended abstract for each regular talk and short description of each invited talk).

NOTE: (c) 2017 for the individual papers by the papers’ authors. Reproduction (electronically or by other means) of all or part of this technical report is permitted for educational or research purposes only, on condition that (i) this copyright notice is included, (ii) proper attribution to the editor(s) or author(s) is made, (iii) no commercial gain is involved, and (iv) the document is reproduced without any alteration whatsoever. Re-publication of material in this report requires permission from the copyright owners.

The workshop provides an informal forum for the automated reasoning community to discuss recent work, new ideas and applications, and current trends. It aims to bring together researchers from all areas of automated reasoning in order to foster links among researchers from various disciplines; among theoreticians, implementers and users alike.

Relevant topics include but are not limited to:

• Theorem proving in classical and non-classical logics;
• Interactive theorem proving, logical frameworks, proof assistants, proof planning
• Reasoning methods:
  • Saturation-based, instantiation-based, tableau, SAT
  • Equational reasoning, unification
  • Constraint satisfaction
  • Decision procedures, SMT
  • Combining reasoning systems
  • Non-monotonic reasoning, commonsense reasoning
  • Abduction, induction, argumentation
  • Model checking, model generation, explanation
• Formal methods to specifying, deriving, transforming and verifying computer systems, requirements and software
• Logic-based knowledge representation and reasoning:
  • Ontology engineering and reasoning
  • Domain specific reasoning (spatial, temporal, epistemic,agents, etc)
• Logic and functional programming, deductive databases
• Implementation issues and empirical results, demos
• Practical experience and applications of automated reasoning

We are delighted to announce that there will be invited talks by

• Maria Paola Bonacina (Universita degli Studi di Verona) who works on semantically-guided goal-sensitive theorem proving and conflict-driven satisfiability modulo theories.


• Nello Cristianini (University of Bristol) who works on computational social science, the philosophy of artificial intelligence and statistical machine learning.

In addition to topics related to those listed above, this year one of the invited talks and the discussion that will take place straight afterwards will be centred around the topic of eXplainable Artificial Intelligence (XAI), which we believe is of great timeliness and relevance to the logic community.

XAI has become a very hot topic over the last year due to the increasing success of big data deep learning black box methods which has caused many practitioners to question the value of some logic based approaches that have traditionally been justified in terms of (implicit) notions of explainability or comprehensibility -- whose benefits were supposed to outweigh the pervieved brittleness of logical approaches in real applications. Many areas of logic-based AI are now experiencing an urgent need to scientifically justify these claims. It is worth noting that, although they have been largely neglected in recent years, such concepts were absolutely integral to the research agendas of early AI pioneers such as Donald Michie who was careful to distinguish so-called weak learning (improvement of predictive accuracy) from strong learning (exploitation of symbolic representations) and ultra-strong learning (communication of learning outcomes).

We view XAI as an attempt to restore these key values and we believe logic-based approaches are ideally placed to assist in this challenge; as exemplified by this recently started DARPA project. We are keen therefore keen to explore how the benefits of logical methods can be quantified and used to develop and delpoy practical XAI methodologies; and any submissions with a slant towards this topic are very welcome.

The workshop will be highly informal and interactive, giving all attendees an opportunity to participate. Submissions will consist of two-page abstracts that will each be given a 15-20 minute presentation slot (with an additional 5-10 minutes for questions) and the opportunity to put up a poster (up to A1) for additional discussion during the lunch and tea/coffee breaks. There will also be a moderated discussion session on each day.

We invite the submission of camera-ready, two-page extended abstracts about recent work, work in progress, or a system description. The abstract can describe work that has already been published elsewhere.

The main objective of the abstracts is to spread information about recent work in our community, and we expect to accept most on-topic submissions, but we may ask for revisions.

To prepare your submission, please use the ARW LaTeX style files available at the following LINK.

Each submission should include the names and complete addresses (including email) of all authors.

Please submit your final pdf using the EasyChair system through this LINK

Correspondence will be sent to corresponding authors indicated on EasyChair.

Registration should be made using the following Eventbrite LINK.

The registration fee for students is £90.00 and for anyone else it is £120.00.

Details of local accomodation can be found at the following University of Bristol LINK.

The workshop will take place in

Room 4.10
35 Berkeley Square
(Graduate School of Education)
University of Bristol
Bristol, BS8 1JA
MAP

There is a multistory car-park within 5 minutes walk of the venue at Trenchard Street which costs £10 per day.

If arriving by train, remember that there are two major stations in Bristol. You should aim to arrive at Bristol Temple Meads (not Bristol Parkway).

A buffet lunch together with morning and afternoon tea/coffee breaks will be provided on both days in foyer/poster area.

A confernece dinner will be provided at a local restaurant on Monday night.

• Alexander Bolotov Chair (University of Westminster)
• Jacques Fleuriot Secretary/Treasurer (University of Edinburgh)
• Simon Colton (Goldsmiths College, University of London)
• David Crocker (Escher Technologies)
• Louise Dennis (University of Liverpool)
• Ullrich Hustadt (University of Liverpool)
• Mateja Jamnik (Univerity of Cambridge)
• Florian Kammueller (Middlesex University)
• Ekaterina Komendantskaya (University of Dundee)
• Alice Miller (University of Glasgow)
• Oliver Ray (University of Bristol)
• Renate Schmidt (University of Manchester)

• Oliver Ray (csxor@bristol.ac.uk)
• Helen Cooke
• Kacper Sokol