24th Automated Reasoning Workshop (ARW'17)

3-4 April, 2017

University of Bristol


The proceedings are available in this PDF


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.

Monday, 3rd April
09:00-09:55 Registration
10:00-10:55 Invited Talk: Conflict-Driven Reasoning by Maria Paola Bonacina
11:00-11:25 Coffee
11:30-12:55 Session 1 (Natural Deduction and Abstract Argumentation)
  • On the Complexity of the Natural Deduction Proof Search Algorithm
    by Alexander Bolotov, Vasilyi Shangin, Daniil Kozhemiachenko
  • ABAplus: Implementing Attack Reversal in Structured Argumentation with Preferences
    by Ziyi Bao, Kristijonas Cyras, Francesca Toni
  • AA-CBR: Explaining Case-Based Reasoning via Argumentation
    by Kristijonas Cyras, Francesca Toni
13:00-13:55 Lunch
14:00-15:25 Session 2 (Logic-based Machine Learning)
  • Automatically Discovering Human-readable Rules to Predict Effective Compiler Settings for Embedded Software
    by Craig Blackmore, Oliver Ray, Kerstin Eder
  • The role of textualisation and argumentation in understanding the machine learning process: a position paper
    by Kacper Sokol, Peter Flach
  • TBA
15:30-15:55 Coffee
16:00-16:55 Business Meeting
17:00-18:55 Free Time: Relax or vist one of the following:
19:00-21:00 Dinner: Zero Degrees - Restaurant and Micro-Brewery

Tuesday, 4th April
09:30-10:55 Session 3 (Description Logics and Knowledge Bases)
  • Forgetting Role Symbols in ALCOQH(top role)-Ontologies
    by Yizheng Zhao, Renate Schmidt
  • Forgetting for Abduction in ALC-Ontologies
    by Warren Del-Pinto, Renate Schmidt
  • A Framework for Axiom Selection in Large Theories
    by Julio Cesar Lopez Hernandez, Konstantin Korovin
11:00-11:25 Coffee
11:30-12:55 Session 4 (Temporal Logics and Diagrammatic Inference)
  • Mind the Gap: Metric Temporal Logic Translations
    by Ana Ozaki, Ullrich Hustadt, Clare Dixon
  • Verifying A Security Protocol for Secure Service Migration in Commercial Cloud Environments with AVISPA
    by Gayathri Karthick, Florian Kammueller, Glenford Mapp, Mahdi Aiash
  • Diagrammatic Reasoning for Ontology Debugging
    by Zohreh Shams, Mateja Jamnik, Gem Stapleton, Yuri Sato
13:00-13:55 Lunch
14:00-14:55 Invited Talk: Why did the chicken cross the Road? by Nello Cristianini
15:00-15:55 Coffee + Discussion (eXplainable AI)
16:00-18:00 Drinks: Avon Groge Hotel White Lion Bar and Terrace

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.

Mar 22submission open*
Mar 29submission close*
Apr 03-04workshop

* Notification of acceptance will be given within 2 days of submission.
* We expect to accept most on-topic submissions without revisions.

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

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).

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

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

The workshop participants will be invited to attend dinner at a local restaurant on Monday night (if finances allow, we will cover at least part of the cost, but this is still to be confirmed).