Workshop Description

General Information

The Fifth Workshop on Practical Aspects of Automated Reasoning will take place on July 2nd, 2016 in Coimbra, Portugal. PAAR is associated with the 8th International Joint Conference on Automated Reasoning (IJCAR-2016).

Scope

PAAR provides a forum for developers of automated reasoning tools to discuss and compare different implementation techniques, and for users to discuss and communicate their applications and requirements. The workshop brings together different groups to concentrate on practical aspects of the implementation and application of automated reasoning tools. It allows researchers to present their work in progress, and to discuss new implementation techniques and applications.

Topics include but are not limited to:

  • automated reasoning in propositional, first-order, higher-order and non-classical logics;
  • implementation of provers (SAT, SMT, resolution, tableau, instantiation-based, rewriting, logical frameworks, etc);
  • automated reasoning tools for all kinds of practical problems and applications;
  • pragmatics of automated reasoning within proof assistants;
  • practical experiences, usability aspects, feasibility studies;
  • evaluation of implementation techniques and automated reasoning tools;
  • performance aspects, benchmarking approaches;
  • non-standard approaches to automated reasoning, non-standard forms of automated reasoning, new applications;
  • implementation techniques, optimisation techniques, strategies and heuristics, fairness;
  • support tools for prover development;
  • system descriptions and demos.

We are particularly interested in contributions that help the community to understand how to build useful reasoning systems in practice, and how to apply existing systems to real problems.

Proceedings

Special Issue of AICom

Submissions are now open to a Special Issue of AI Communications on Automated Reasoning.
Abstract submission January 8, 2017
Paper submission January 15, 2017
Notification of acceptance April 15, 2017
Final versions June 15, 2017

Submission

Researchers interested in participating are invited to submit either an extended abstract (up to 8 pages) or a regular paper (up to 15 pages) via EasyChair. Submissions will be refereed by the program committee, which will select a balanced program of high-quality contributions. Short submissions that could stimulate fruitful discussion at the workshop are particularly welcome.

Submissions should be in PDF. Final versions should be prepared in LaTeX using the "easychair.cls" class file. Paper should be submitted through the EasyChair page. PAAR proceedings will be published electronically in the EasyChair Proceedings in Computing (EPiC) series or in the CEUR workshop proceedings.

Important Dates

Abstract submission deadline: May 2nd, 2016
Paper submission deadline: May 9th, 2016
Author notification: June 6th, 2016
Camera-ready paper versions due: June 18th, 2016
Workshop: July 2nd, 2016

Registration

Registration to PAAR is part of the IJCAR registration process.

Program

July 2

9:00 - 10:30 PROOFS, MODELS, CERTIFICATES

Chair: Renate A. Schmidt 		Organizers (9:00 - 9:10)
Introduction

Jean Marie Lagniez, Daniel Le Berre, Tiago de Lima and Valentin Montmirail (9:10 - 9:40)
On Checking Kripke Models for Modal Logic K

Michael Färber and Cezary Kaliszyk (9:40 - 10:10)
No Choice: Reconstruction of First-order ATP Proofs without Skolem Functions

Benoit Razet and Bodhayan Roy (10:10 - 10:30)
Computing Certificates of Regular Expression Equivalence (presentation only)
10:30 - 11:00 coffee break
11:00 - 12:30 SYSTEMS AND TOOLS FOR ATP

Chair: Pascal Fontaine 		Christoph Wernhard (11:00 - 11:30)
The PIE Environment for First-Order-Based Proving, Interpolating and Eliminating - Extended Abstract

Mohamed Hassona and Stephan Schulz (11:30 -12:00)
Deduction as a Service

Cezary Kaliszyk, Geoff Sutcliffe and Florian Rabe (12:00 - 12:30)
TH1: The TPTP Typed Higher-Order Form with Rank-1 Polymorphism
12:30 - 14:00 lunch break
14:00 - 15:30 FOL ATP

Chair: Josef Urban 		Koen Claessen and Ann Lillieström (14:00 - 14:30)
Handling Common Transitive Relations in First-Order Automated Reasoning

Haniel Barbosa (14:30 - 15:00)
Efficient Instantiation Techniques in SMT (Work In Progress)

Eugen Kuksa and Till Mossakowski (15:00 - 15:30 )
Prover-independent Axiom Selection for Automated Theorem Proving in Ontohub
15:30 - 16:00 coffee break
16:00 - 17:30 SATURATION AND RESOLUTION

Chair: Stephan Schulz 		Andreas Teucke and Christoph Weidenbach (16:00 - 16:30)
Ordered Resolution with Straight Dismatching Constraints

Tomer Libal and Alexander Steen (16:30 - 17:00 )
Towards a Substitution Tree Based Index for Higher-order Resolution Theorem Provers

Jelena Vlasenko, Maryam Daryalal, Volker Haarslev and Brigitte Jaumard (17:00 - 17:30)
A Saturation-based Algebraic Reasoner for ELQ
19:30 - 22:00 Drinks and dinner
The workshop dinner will take place at O Cantinho dos Reis (Google map)
The place is not easy to find: we meet at 19:10 at the Astoria hotel for those who want.

Call For Papers

[.txt]

Program Committee

Previous Workshops