CADE-25 Workshops- Calls for Papers

[Geoff Sutcliffe]

================================================================

     Joint Call for Papers of Associated Workshops at the
 25th International Conference of Automated Deduction (CADE-25)
                     1-7 August 2015, Berlin
                       http://cade-25.info

================================================================

Workshops
- Bridging the Gap between Human and Automated Reasoning (Bridging)
- Automated Theorem Proving meets Interactive Theorem Proving (AMI)
- International Workshop on Confluence (IWC)
- Deduktionstreffen 2015 (DT)
- The Fourth International Workshop on Proof eXchange for Theorem 
  Proving (PxTP)
- International Workshop on Quantification (QUANTIFY 2015)
- The 2nd Vampire Workshop (Vampire)
- International Workshop on Logical Frameworks and Meta-Languages: Theory 
  and Practice (LFMTP)
- CADE-25 Poster Session and Task-Force towards an Encyclopedia of Proof 
  Systems (EPS)

******************************************************************************
Bridging the Gap between Human and Automated Reasoning (Bridging)
=================================================================
http://ratiolog.uni-koblenz.de/bridging.html

Human reasoning or the psychology of deduction is well researched in
cognitive psychology and in cognitive science. There are a lot of
findings which are based on experimental data about reasoning tasks,
among others models for the Wason selection task or the suppression
task discussed by Byrne and others. This research is supported also by
brain researchers, who aim at localizing reasoning processes within
the brain. Automated deduction, on the other hand, is mainly focusing
on the automated proof search in logical calculi. And indeed there
is tremendous success during the last decades. Recently a coupling of
the areas of cognitive science and automated reasoning is addressed
in several approaches. For example there is increasing interest in
modeling human reasoning within automated reasoning systems including
modeling with answer set programming, deontic logic or abductive logic
programming. There are also various approaches within AI research.

This workshop is intended to get an overview of existing approaches and
make a step towards a cooperation between computational logic and
cognitive science. Topics of interest include, but are not limited to
the following:
- limits and differences between automated and human reasoning
- psychology of deduction
- common sense reasoning
- logics modeling human cognition
- modeling human reasoning using automated reasoning systems
- non-monotonic, defeasible, and classical reasoning and possible explanations 
  for human reasoning
- application fields of automated reasoning in the interaction with human 
  reasoners

IMPORTANT DATES
===============
Submission deadline: May 1, 2015
Notification: May 22, 2015
Final Submission: June 5, 2015
Workshop: Aug 1, 2015

For more details see: http://ratiolog.uni-koblenz.de/bridging.html

******************************************************************************
Automated Theorem Proving meets Interactive Theorem Proving (AMI)
=================================================================
http://ami2015.it.uu.se/

AIMS AND SCOPE
==============
The AMI workshop provides an informal platform for researchers
interested in automated theorem proving (ATP) and interactive
theorem proving (ITP), for instance, developers and users of ATP,
SMT and similar systems, and developers and users of ITP systems
such as Coq, HOL, Isabelle or Mizar. Its aim is the exchange of
experiences and ideas for pushing these technologies further into the
mainstream: to explore methods or tools from ATP that could be
benefit ITP and vice versa; to advance the integration and
convergence of these technologies, e.g. by considering tools and
techniques from mathematics, programming languages or AI; to bring
ATP and ITP work flows closer to mathematical and engineering
practice.

WORKSHOP TOPICS include
=======================
- proof automation for ITP: from tactics and decision procedures via
  FOL to fragments of CoC and HOL; ATP with types and data types;
- ATP with large data sets (as generated by ITP systems): machine
  learning and other AI approaches, proof management;
- theory hierarchies in ITP/ATP systems: their design and management;
- ideas and techniques from mathematics and programming;
- use and user experience: ATP/ITP uses and integrations in fields
  like formalised mathematics or hardware/software verification.

SUBMISSIONS
===========
To foster discussions, we ask for submissions of extended abstracts of
2 to 4 pages as well as for full papers of at most 15 pages. If
submissions are based on previously published material that should be
stated clearly. Presentations will be selected based on the quality of
their contribution and their relevance to the workshop. All accepted
submissions will be published online at the workshop web site. Quality
of submissions permitting, we are planning their considation for a
journal special issue after the workshop. Papers must be submitted
via EasyChair.

IMPORTANT DATES
===============
Abstract submission: May 7 2015
Paper submission: May 14 2015
Notification: June 16 2015
Final Version: June 25 2015
Workshop: August 2 2015

PROGRAMME COMMITTEE
===================
Christoph Benzmueller (FU Berlin, Germany)
Nicolai Bjorner (Microsoft Research)
Simon Foster (University of York, UK)
Mike Gordon (University of Cambridge, UK)
Tim Griffin (University of Cambridge, UK)
Sebastiaan Joosten (TU Eindhoven/RU Nijmegen, Netherlands)
Chantal Keller (Microsoft Research/MSR-Inria)
Gerwin Klein (NICTA/UNSW, Australia)
Assia Mahboubi (Inria/MSR-Inria, France)
Andrei Paskevich (LRI/Universite Paris Sud, France)
Stephan Schulz (DHBW, Germany)

INVITED SPEAKERS (joint with the PxTP workshop)
===============================================
Bart Jacobs (KU Leuven, Belgium)
Georges Gonthier (Microsoft Research - Inria)

ORGANISERS
==========
Damien Pous (ENS Lyon, France)
Georg Struth (University of Sheffield, UK)
Tjark Weber (Uppsala University, Sweden)

******************************************************************************
International Workshop on Confluence (IWC)
==========================================
http://www.csl.sri.com/users/tiwari/iwc2015/

Confluence provides a general notion of determinism and has been
conceived as one of the central properties of rewriting systems.
Confluence relates to many topics of rewriting (completion, modularity,
termination, commutation, etc.) and had been investigated in many
formalisms of rewriting such as first-order rewriting, lambda-calculi,
higher-order rewriting, constraint rewriting, conditional rewriting, etc.
Recently there is a renewed interest in confluence research, resulting
in new techniques, tool support, confluence competition, and
certification as well as in new applications. The scope of the workshop
is all these aspects of confluence and related topics.

The goal of the workshop is to provide a forum for researchers
interested in the topic of confluence to exchange and share new
developments in the field. The workshop will enable discussion on
theoretical results, new problems, applications, implementations and
benchmarks, and share the current state-of-the-art on the
development of confluence tools.

Specific topics of interest include:
- confluence and related properties (unique normal forms,
  commutation, ground confluence)
- completion
- critical pair criteria
- decidability issues
- complexity issues
- system descriptions
- certification
- applications of confluence

Submission May 15, 2015
Notification June 12, 2015
Final version July 3, 2015
Workshop August 2, 2015

******************************************************************************
Deduktionstreffen 2015 (DT)
===========================
http://conference.mi.fu-berlin.de/cade-25/DT

The 'Deduktionstreffen' is the annual meeting of the section
'Deduction Systems' of the German Informatics Society (Gesellschaft
fuer Informatik e.V. (GI)). It is a friendly and informal meeting with
a familiar atmosphere. All members and friends of the German Deduction
Community are invited to present, discuss and share their latest
research results and ideas at the event.

A particular focus of the 'Deduktionstreffen' is on young researchers
and students, which are particularly encouraged to present their
ongoing research projects to a wider audience. Another goal of the
meeting is stimulate networking effects and to foster collaborative
research projects.

The format of the event is as follows: Accepted abstracts are
presented as 5min teaser talks followed by a poster presentation.
The 'Deduktionstreffen 2015' is associated with the 25th Conference of
Automated Deduction (CADE-25; http://cade-25.info).

Submission of Presentation Abstracts
====================================
Please submit your presentation abstract (max. 1 page) via Easychair:
https://easychair.org/conferences/?conf=deduktionstreffen201. The
(preliminary) submission deadline is May 1, 2015. Notification is
planned for mid May.

Invited Speakers
================
Renate Schmidt, University of Manchester
tba

Program Committee
=================
Serge Autexier, DFKI Bremen
Bernhard Beckert, KIT
Christoph Benzmueller, FU Berlin (co-chair)
Christian Blanchette, TU Muenchen
Ulrich Furbach, Universitaet Koblenz
Juergen Giesl, RWTH Aachen
Matthias Horbach, Universitaet Koblenz/MPII (co-chair)
Dieter Hutter, DFKI Bremen 
Manfred Kerber, University of Birmingham
Christoph Kreitz, Universitaet Potsdam
Jens Otten, Universitaet Potsdam
Florian Rabe, Jacobs University Bremen
Stephan Schulz, DHBW Stuttgart 
Viorica Sofronie-Stokkermans, Universitaet Koblenz/MPII
Volker Sorge, University of Birmingham
Christoph Weidenbach, MPII Saarbruecken

Local Organisation
==================
Christoph Benzmueller, FU Berlin 
Alexander Steen, FU Berlin
Max Wisniewski, FU Berlin

******************************************************************************
The Fourth International Workshop on Proof eXchange for Theorem Proving (PxTP)
==============================================================================
http://pxtp15.lri.fr

Background
==========
The PxTP workshop brings together researchers working on various aspects
of communication, integration, and cooperation between reasoning systems
and formalisms.

The progress in computer-aided reasoning, both automated and interactive,
during the past decades, made it possible to build deduction tools that
are increasingly more applicable to a wider range of problems and are
able to tackle larger problems progressively faster. In recent years,
cooperation of such tools in larger verification environments has
demonstrated the potential to reduce the amount of manual intervention.
Examples include the Sledgehammer tool providing an interface between
Isabelle and (untrusted) automated provers, and also collaboration of
the HOL Light and Isabelle systems in the formal proof of the Kepler
conjecture.

Cooperation between reasoning systems relies on availability of
theoretical formalisms and practical tools to exchange problems,
proofs, and models. The PxTP workshop strives to encourage such
cooperation by inviting contributions on suitable integration,
translation and communication methods, standards, protocols,
and programming interfaces. The workshop welcomes the interested
developers of automated and interactive theorem proving tools,
developers of combined systems, developers and users of translation
tools and interfaces, and producers of standards and protocols.
We are interested both in success stories and in descriptions
of the current bottlenecks and proposals for improvement.

Topics
======
Topics of interest for this workshop include all aspects of
cooperation between reasoning tools, whether automatic or
interactive. More specifically, some suggested topics are:
- applications that integrate reasoning tools (ideally
  with certification of the result);
- translations between logics, proof systems, models;
- distribution of proof obligations among heterogeneous
  reasoning tools;
- algorithms and tools for checking and importing (replaying,
  reconstructing) proofs;
- proposed formats for expressing problems and solutions for
  different classes of logic solvers (SAT, SMT, QBF, first-order
  logic, higher-order logic, typed logic, rewriting, etc.);
- meta-languages, logical frameworks, communication methods,
  standards, protocols, and APIs connected to problems, proofs,
  and models;
- comparison, refactoring, and optimization of proofs;
- practical experiences, case studies, feasibility studies;
- applications relying on importing proofs from automatic theorem
  provers, such as certified static analysis, proof-carrying code,
  or certified compilation;
- data structures and algorithms for improved proof production in
  solvers (e.g., efficient proof representations).

Submissions
===========
Researchers interested in participating are invited to submit either
an extended abstract (up to 8 pages) or a regular paper (up to 15
pages). 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. We expect that one author of every accepted
paper will present their work at the workshop.

Submitted papers should describe previously unpublished work, and must
be prepared using the LaTeX EPTCS class (http://style.eptcs.org/).
Papers will be submitted via EasyChair, at the PxTP'2015 workshop page
(http://www.easychair.org/conferences/?conf=pxtp2015). Accepted full
papers will appear in an EPTCS volume.

Important dates
===============
- Abstract submission: Thu, May 7, 2015
- Paper submission: Thu, May 14, 2015
- Notification: Tue, June 16, 2015
- Camera ready versions due: Thu, June 25, 2015
- Workshop: August 2-3, 2015

Invited speakers (joint with the AMI 2015 workshop)
===================================================
- Georges Gonthier (Microsoft Research)
- Bart Jacobs (KU Leuven)

Program committee
=================
- Jesse Alama (Vienna University of Technology)
- Peter Baumgartner (NICTA)
- Jasmin Blanchette (TU Muenchen)
- Guillaume Burel (CEDRIC, ENSIIE)
- Evelyne Contejean (LRI, CNRS, Universite Paris Sud)
- Cezary Kaliszyk (University of Innsbruck), co-chair
- Ramana Kumar (University of Cambridge)
- Dale Miller (Inria / LIX, Ecole polytechnique)
- Bruno Woltzenlogel Paleo (Vienna University of Technology)
- Andrei Paskevich (LRI, Universite Paris Sud), co-chair
- Damien Pous (LIP, CNRS, ENS Lyon)
- Geoff Sutcliffe (University of Miami)
- Laurent Thery (Inria)
- Cesare Tinelli (University of Iowa)
- Josef Urban (Radboud University Nijmegen)

Previous PxTP editions
======================
- PxTP 2011 (http://pxtp2011.loria.fr/), affiliated with CADE-23
- PxTP 2012 (http://pxtp2012.inria.fr/), affiliated with IJCAR 2012
- PxTP 2013 (http://www.cs.ru.nl/pxtp13/), affiliated with CADE-24

******************************************************************************
International Workshop on Quantification (QUANTIFY 2015)
========================================================
http://fmv.jku.at/quantify15/

Quantifiers play an important role in language extensions of many logics. 
The use of quantifiers often allows for a more succinct encoding as it 
would be possible without quantifiers. However, the introduction of 
quantifiers affects the complexity of the extended formalism in general. 
Consequently, theoretical results established for the quantifier-free 
formalism may not directly be transferred to the quantified case. Further, 
techniques successfully implemented in reasoning tools for quantifier-free 
formulas cannot directly be lifted to a quantified version.

The goal of the 2nd International Workshop on Quantification (QUANTIFY 2015) 
is to bring together researchers who investigate the impact of quantification 
from a theoretical as well as from a practical point of view. Quantification 
is a topic in different research areas such as in SAT in terms of QBF, in CSP 
in terms of QCSP, in SMT, etc. This workshop has the aim to provide an 
interdisciplinary forum where researchers of various fields may exchange 
their experiences.

IMPORTANT DATES
===============
Please follow http://fmv.jku.at/quantify15/ for any updates.

May    8 2015: paper submission
May   29 2015: notification of acceptance
June  23 2015: camera-ready version of papers
August 1 2015: workshop 

TOPICS OF INTEREST
==================
The workshop is concerned with all theoretical and practical 
aspects of quantification in logics such as QBF, QCSP, SMT, 
and theorem proving. The topics of interest include 
(but are not limited to):

- Complexity results 
- Encodings with and without quantification and comparisons thereof
- Applications of quantification 
- Implementations of reasoning tools
- Case studies and experimental results
- Intersections between the different research communities 
  working on quantification
- Surveys of state-of-the-art approaches to handling quantification

SUBMISSION OF EXTENDED ABSTRACTS
================================
Submissions of extended abstracts are solicited and will be managed via
Easychair:
https://easychair.org/conferences/?conf=quantify15

Submitted papers should be formatted in either LNCS format or a 
standard LaTeX article format (paper size A4, font size 11pt).

We solicit two types of submissions:
1. Talk abstracts (maximum two pages, excluding references) 
describing already published results.
2. Full papers (maximum 14 pages, excluding references) on novel, 
unpublished work.

The talk abstracts of category 1 should include a relevant 
bibliography of related work and an outline of the planned talk. 
For this category, we explicitly advocate talks which survey results 
already published, maybe in multiple articles or presentations 
capturing the commonalities and differences
of various quantification approaches (perhaps even interdisciplinary).

Each submission will be assessed by the program committee and the 
workshop organizers with respect to novelty, originality, and scope.

Submissions related to completed work as well as work in progress are
welcome. Authors are encouraged to provide additional material such as
source code of tools, experimental data, benchmarks and related 
publications in an appendix or a related webpage. The additional
material will be considered at the discretion of the reviewers.

Previously published work or extensions thereof may be submitted to the
workshop but that case has to be explicitly stated in the submitted
paper. This regulation also applies to work which is currently under 
review elsewhere.

Since the workshop does not have official proceedings, work related to
accepted submissions can be resubmitted to other venues without 
restrictions.

Authors of accepted abstracts and papers are expected to give a talk at
the workshop.

PROGRAM CHAIRS
==============
Hubie Chen, Universidad del Pais Vasco and Ikerbasque
Florian Lonsing, Vienna University of Technology, Austria
Martina Seidl, Johannes Kepler University Linz, Austria

******************************************************************************
The 2nd Vampire Workshop (Vampire)
==================================
http://easychair.org/smart-program/Vampire2015/index.html

IMPORTANT DATES
===============
Submission deadline: June 15, 2015
Notification of acceptance: June 20, 2015
Final paper submission: June 30, 2015
Workshop day: August 2, 2015

WORKSHOP AIM
============
The workshop aims at discussing the development and use of the
first-order theorem prover Vampire. The workshop will address the
newest trends in implementing first-order theorem provers, and focus
on new challenges and application areas.
Workshop participants will include both Vampire developers and users
and provides a convenient opportunity for interesting discussions
between tool developers and users. The users can learn more about
Vampire and its recent developments. The developers can learn more
about the use of Vampire, its efficiency in various application areas
and needs of the users.
The workshop is going to to shed the light on on problems such as
- what is essential for substantial progress in theorem proving tools;
- what are the best implementation principles to be used;
- what are the best heuristics and strategies, depending on application
  areas;
- both successful and unsuccessful case studies;
- missing features in modern theorem provers.
The workshop will also overview the most recent advances made in
Vampire.

PAPER SUBMISSION
================
We seek submissions reporting on theory, application, case studies,
experiments and work-in-progress using Vampire and other theorem
provers in various applications. Submissions can be in any form,
ranging from work in progress to completed work. For example, the
users can submit:
- extended abstracts or full papers;
- theoretical papers;
- experimental papers and case studies
- or in general any papers that can benefit tool developers and users.
Papers can be of any length, ranging from 2-page abstracts to full
papers up to 20 pages in length. The papers should use the
EasyChair LaTeX, Microsoft Word, or ODT templates, which can be
found at:
http://www.easychair.org/publications/epic-templates.
Submissions should be made using EasyChair, via the link:
https://easychair.org/conferences/?conf=vampire2015
The workshop proceedings will be published in the EasyChair EPiC
series.

PROGRAM COMMITEE
================
Laura Kovacs (Chalmers University of Technology) - chair
Andrei Voronkov (University of Manchester) - chair

******************************************************************************
International Workshop on Logical Frameworks and Meta-Languages: 
Theory and Practice (LFMTP)
================================================================
http://lfmtp.org/workshops/2015/

Logical frameworks and meta-languages form a common substrate for
representing, implementing, and reasoning about a wide variety of
deductive systems of interest in logic and computer science. Their
design and implementation and their use in reasoning tasks ranging
from the correctness of software to the properties of formal
computational systems have been the focus of considerable research
over the last two decades. This workshop will bring together
designers, implementors, and practitioners to discuss various aspects
impinging on the structure and utility of logical frameworks, including
the treatment of variable binding, inductive and co-inductive reasoning
techniques and the expressivity and lucidity of the reasoning process.

LFMTP 2015 will provide researchers a forum to present state-of-the art
techniques and discuss progress in areas such as the following:
- Encoding and reasoning about the meta-theory of programming
  languages and related formally specified systems.
- Theoretical and practical issues concerning the treatment of
  variable binding, especially the representation of, and reasoning
  about, datatypes defined from binding signatures.
- Logical treatments of inductive and co-inductive definitions and
  associated reasoning techniques.
- New theory contributions: canonical and substructural
  frameworks, contextual frameworks, proof-theoretic foundations
  supporting binders, functional programming over logical
  frameworks, homotopy type theory.
- Applications of logical frameworks, e.g., in proof-carrying
  architectures such as proof-carrying authorization.
- Techniques for programming with binders in functional
  programming languages such as Haskell, OCaml, or Agda and
  logic programming languages such as lambda Prolog or Alpha-
  Prolog.

Program / Invited Speakers
==========================
TBA

Registration
============
Registration for LFMTP is open and early registration ends on TBA.
Please see the CADE-25 registration page for more details.
Important Dates
- Friday, April 30th: Abstract submission deadline
- Friday, May 7th: Submission deadline
- Friday June, 12th: Notification to authors
- Friday July, 3rd: Final version due
- Saturday August, 1st: Workshop date

Submission
==========
In addition to regular papers, we also solicit "work in progress" reports,
in a broad sense. Those do not need to report fully polished research
results, but should be interesting for the community at large.
Submitted papers should be in PDF, formatted using the ACM
SIGPLAN style guidelines. The length is restricted to 8 pages for
regular papers and 4 pages for "Work in Progress" papers.
Submission is via EasyChair. Submit to LFMTP15 now!

Proceedings
===========
TBA

Program Committee
=================
- Iliano Cervesato (Carnegie Mellon University, co-chair)
- Kaustuv Chaudhuri (Inria & LIX/Ecole polytechnique, co-chair)
The rest of the program committee will be finalized shortly.

******************************************************************************
CADE-25 Poster Session and Task-Force towards an Encyclopedia of Proof 
Systems (EPS)
======================================================================
http://proofsystem.github.io/Encyclopedia

Aims and Scope
==============
In this jubilee edition of CADE, we shall commemorate the multitude of
proof systems that form the theoretical foundations for automated
deduction. To achieve this goal, this alternative workshop proposes to
bring the whole community together in a task-force to produce a concise
encyclopedia of proof systems. Every entry in this encyclopedia will
follow a given template and will preferably be exactly one page long,
displaying the inference rules of the proof system and possibly a few
clarifying remarks. The one-page encyclopedia entries will be
displayed as posters during CADE (the Conference on Automated
Deduction).

Submission Instructions
=======================
Please visit the task-force's website for instructions:
http://proofsystem.github.io/Encyclopedia

Participation in CADE is not required for submission,
but is strongly encouraged.

Important Dates
===============
- Submission Deadline: 19th of April 2015
- Notification: 15th of May 2015
(Submit early!!)

Publication Plans
=================
When the encyclopedia reaches a broad coverage of various proof systems, 
its publication as a book will be sought. However, this is not yet
guaranteed and details are still undefined.

Organization
============
Bruno Woltzenlogel Paleo (bruno at logic.at)

******************************************************************************