================================================================ 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@logic.at)