ARW 2018

Proceedings

Proceedings are available in PDF format here.

Group Photo

General Information

The 25th Automated Reasoning Workshop (ARW 2018) will take place at the University of Cambridge on 12-13 April 2018.

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.

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
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
Machine learning and automated reasoning systems
Practical experience and applications of automated reasoning

The workshop will be highly interactive, giving all attendees an opportunity to participate. There will be sessions for displaying posters and open discussion sessions organised around specific topics such as “Automated Reasoning and Artificial Intelligence”.

Submissions

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.

The call for papers is available in plain text format.

To prepare your submission, please use the ARW LaTeX style file provided from the workshop website. Each submission should include the names and complete addresses (including email) of all authors. For the final versions we require all sources (TeX file and any input files). Please send your submissions via EasyChair here.

Programme

Each workshop participant will be asked to give a short talk (around 10 minutes depending on time constraints) to introduce their research. Each participant will also be allocated space in a poster session (please make your posters A1 size), where they can further present and discuss their work. Please prepare posters for the event.

Invited Talks

Ekaterina Komendantskaya (Heriot-Watt University) - Machine learning for mining, understanding and automating computer proofs

April 12th 10:00

As software for mechanised proofs flourishes, we are about to enter the age of "Big Proof" (i.e. a Big Data stage of mechanised proof development). Large corpora of computer proofs, written in a range of programming languages, is already available on the Web. The question is: How much of Big Data technology is applicable in "Big Proof" domain?

In this talk, I will give a comparative overview of several machine learning methods used to mine, analyse and understand the existing corpora of mechanised proofs, and to automate new proofs. I will use the Machine Learning for Proof General (ML4PG) tool for Demos.

Lawrence Paulson (University of Cambridge) - A Career in Research: Mike Gordon and Hardware Verification

April 13th 14:00

The story of Mike Gordon's scientific career is instructive. Mike conceived the radical idea of hardware verification in the late 70s, a surprising choice given the number of other new fields he could have joined. Mike talked to researchers in the systems side of his Department (at Edinburgh). With impressive method, he learned about hardware and designed a small microcoded computer. Then he investigated the problem of how to verify this computer.

First he wanted to model behaviours using recursive domain equations. Then he opted for a CCS-like process calculus and implemented it on top of LCF. Finally he opted for higher-order logic, again a radical choice compared with the favoured alternatives of first-order logic and dependent type theory. Ultimately he realised his ambitions on a grand scale, with the verification of the ARM6 processor and landmark work on verifying assembly language code and proof-producing compilation. His foresight and boldness allowed him to transform the practices of verification and hardware design.

Discussion Panel: Natural language processing and information retrieval for automated reasoning

April 13th 12:00 - 13:00

Ekaterina Komendantskaya, Lawrence Paulson and Yiannos Stathopoulos

The focus of the discussion will be on large-scale mathematical knowledge available in formalised libraries; In particular, on how these libraries can support sophisticated searches using natural language processing and information retrieval technologies. Amongst others, an important aim of developing sophisticated search tools is to provide automated support for construction of formal proofs, for example, by mining libraries for proof patterns and clustering lemmas based on the similarity of the proofs they are used in.

Schedule

This is a preliminary schedule subject to change.

April Thursday 12th
9:00	Registration
10:00	Invited Talk (Ekaterina Komendantskaya)
11:00	Coffee Break
11:30	Short Talks: 9: Juan Casanova and Alan Bundy Meta-unification: An algorithm for finding solutions to constraint systems over unifiers with meta-variables 11: Cláudia Nalon, Ullrich Hustadt and Clare Dixon Separated Normal Form Transformation Revisited 12: Yue Li Models of Coinductive First-order Horn Clauses 20: Kemas Wiharja, Jeff Z. Pan, Martin Kollingbaum and Yu Deng Pattern-Based Reasoning to Investigate the Correctness of Knowledge Graphs 22: Alexander Bolotov, Montserrat Hermo and Paqui Lucio A tree-style one-pass tableau for an extension of ECTL+
12:30	Poster Session
13:00	Group Photo and Lunch
14:00	Short Talks: 1: Alexander Steen Leo-III: A Theorem Prover for Classical and Non-Classical Logics 2: Maximilian Doré The Elfe Prover; Verifying mathematical proofs of undergraduate students 23: Kyndylan Nienhuis, Alexandre Joannou and Peter Sewell Proving security properties of CHERI-MIPS 7: Ahmed Bhayat and Giles Reger Higher-order Reasoning Vampire Style 15: Fabio Papacchini, Cláudia Nalon, Ullrich Hustadt and Clare Dixon Extending the KSP Prover to More Expressive Modal Logics 19: Alasdair Armstrong, Thomas Bauereiss, Kathryn E. Gray, Prashanth Mundkur, Alastair Reid, Peter Sewell, Brian Campbell, Shaked Flur, Robert M. Norton, Christopher Pulte, Ian Stark and Mark Wassell Detailed Models of Instruction Set Architectures: From Pseudocode to Formal Semantics 18: Victor B. F. Gomes, Martin Kleppmann, Dominic P. Mulligan and Alastair R. Beresford Verifying Strong Eventual Consistency for Conflict-free Replicated Data Types 16: Alasdair Armstrong, Neel Krishnaswami, Peter Sewell and Mark Wassell Formalisation of MiniSail in the Isabelle Theorem Prover
15:30	Poster Session and Coffee
16:30	Screening of a documentary about Bletchley Park. Finishing at 17:30.
19:00	Dinner (Clare College Old Court). Dinner is served at 19:00 so please arrive before 18:50.
April Friday 13th
9:00	Short Talks: 8: Thomas Tuerk Real-world formal documentation 14: Alexander Bolotov and Alexander Gorchakov Tuning Natural Deduction Proof Search by Analytic Methods. 6: Giles Reger and Martin Riener Instantiation for Theory Reasoning in Vampire 24: Sen Zheng and Renate A.Schmidt Towards Polynomial Time Forgetting and Instance Query; Rewriting in Ontology Languages 25: Warren Del-Pinto and Renate Schmidt Iterative Abduction using Forgetting
10:00	Coffee and Poster Session
10:30	Short Talks: 10: Murdoch J. Gabbay Equivariant ZFA with Choice: a position paper 17: Peter Backeman BREU with Connections 21: Michael Rawson and Giles Reger Designing a proof calculus for the application of learned search heuristics 26: Yang XU, Jun LIU, Shuwei CHEN, Xiaomei ZHONG and Xingxing HE Contradiction Separation Based Dynamic Multi-Clause Synergized Automated Deduction 27: Julio Cesar Lopez Hernandez and Konstantin Korovin Reasoning with Large Theories Using Over-Approximation Abstraction-Refinement
11:30	Coffee and Poster Session
12:00	Discussion Panel
13:00	Lunch
14:00	Invited Talk (Larry Paulson)
15:00	Coffee and Business meeting

Student Grants

There is a small number of grants available for PhD students. Applications must include:

an abstract of at most 2 pages following the formatting details on the submissions page.
a recommendation letter from their supervisor
a covering letter from the student

Recipients of grants are expected to present their work in the poster sessions. The abstracts will be published in the workshop notes.

The ARW committee will review the applications. Preference will be given to those who would not otherwise have resources to attend the workshop, and whose attendance would benefit both the applicant and the workshop.

Applicants who receive grants will be allowed to register at a reduced student registration rate.

All applications should be sent to arw2018@easychair.org using ARW2018 Student Grant as the subject of the email. The deadline for applying for these grants is 1 March 2018.

Organisers

ARW Committee

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

Local Organisers

Mateja Jamnik (Mateja dot Jamnik at cl dot cam dot ac dot uk)
Edward Ayers
Angeliki Koutsoukou-Argyraki
Wenda Li
Chaitanya Mangla
Lawrence Paulson
Zohreh Shams

Local Arrangements

Venue Location

The workshop will take place in the Computer Laboratory (CL) at the Department of Computer Science and Technology (CST) on the West Cambridge site. Directions are available here.

View on Google Maps.

Dinner Location

The dinner at Clare College will take place at 19:00 on the 12th of April. Please try to arrive before 18:50. The dining hall is in Old Court which is near Kings College Chapel.