From mboxrd@z Thu Jan 1 00:00:00 1970 Return-Path: X-Original-To: caml-list@sympa.inria.fr Delivered-To: caml-list@sympa.inria.fr Received: from mail2-relais-roc.national.inria.fr (mail2-relais-roc.national.inria.fr [192.134.164.83]) by sympa.inria.fr (Postfix) with ESMTPS id DD0917FD90 for ; Fri, 13 Jan 2017 14:34:36 +0100 (CET) Authentication-Results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=geoff@cs.miami.edu; spf=Pass smtp.mailfrom=geoff@cs.miami.edu; spf=None smtp.helo=postmaster@mcclellan.cs.miami.edu Received-SPF: None (mail2-smtp-roc.national.inria.fr: no sender authenticity information available from domain of geoff@cs.miami.edu) identity=pra; client-ip=192.31.89.6; receiver=mail2-smtp-roc.national.inria.fr; envelope-from="geoff@cs.miami.edu"; x-sender="geoff@cs.miami.edu"; x-conformance=sidf_compatible Received-SPF: Pass (mail2-smtp-roc.national.inria.fr: domain of geoff@cs.miami.edu designates 192.31.89.6 as permitted sender) identity=mailfrom; client-ip=192.31.89.6; receiver=mail2-smtp-roc.national.inria.fr; envelope-from="geoff@cs.miami.edu"; x-sender="geoff@cs.miami.edu"; x-conformance=sidf_compatible; x-record-type="v=spf1" Received-SPF: None (mail2-smtp-roc.national.inria.fr: no sender authenticity information available from domain of postmaster@mcclellan.cs.miami.edu) identity=helo; client-ip=192.31.89.6; receiver=mail2-smtp-roc.national.inria.fr; envelope-from="geoff@cs.miami.edu"; x-sender="postmaster@mcclellan.cs.miami.edu"; x-conformance=sidf_compatible IronPort-PHdr: =?us-ascii?q?9a23=3ACf5n9RVW3c0p8f6PmZTptlehgNHV8LGtZVwlr6E/?= =?us-ascii?q?grcLSJyIuqrYZROEt8tkgFKBZ4jH8fUM07OQ6PG8HzdaqsrQ+DBaKdoXCE9D0Z?= =?us-ascii?q?1X1yUbQ+e7SmTDZMbwaCI7GMkQHHRExFqcdXZvJcDlelfJqWez5zNBUj/2NA5y?= =?us-ascii?q?O/inUtWK15f/hKiO/MjYagBMwT68eq9aLROsrAyXuNNFr5FlL/M+xxzHrFNDYK?= =?us-ascii?q?JTxGptJBSekwu0pui9+5Btux9Np/kl9sBOXOSpLOwDUbVEAWF+YCgO78rxuEyb?= =?us-ascii?q?QA=3D=3D?= X-IronPort-Anti-Spam-Filtered: true X-IronPort-Anti-Spam-Result: =?us-ascii?q?A0DBEgDY1nhY/wZZH8BdHAEBBAEBCgEBF?= =?us-ascii?q?wEBBAEBCgEBgwUPAQEBAQF+gQmDA4p1lFMBkD2CD4INASmCQoYJEgEBAQEBAQE?= =?us-ascii?q?BAQEBYiiCMxmCQSEqTTAEHV+IaA6gRJImiAgHgi+ODyCBGgmCZgxbgjEFkB2LF?= =?us-ascii?q?YZcgxWHW4Umi1SSZSYCL4FGhxsgNQGGKYI8AQEB?= X-IPAS-Result: =?us-ascii?q?A0DBEgDY1nhY/wZZH8BdHAEBBAEBCgEBFwEBBAEBCgEBgwU?= =?us-ascii?q?PAQEBAQF+gQmDA4p1lFMBkD2CD4INASmCQoYJEgEBAQEBAQEBAQEBYiiCMxmCQ?= =?us-ascii?q?SEqTTAEHV+IaA6gRJImiAgHgi+ODyCBGgmCZgxbgjEFkB2LFYZcgxWHW4Umi1S?= =?us-ascii?q?SZSYCL4FGhxsgNQGGKYI8AQEB?= X-IronPort-AV: E=Sophos;i="5.33,221,1477954800"; d="scan'208";a="255196799" Received: from mcclellan.cs.miami.edu ([192.31.89.6]) by mail2-smtp-roc.national.inria.fr with SMTP; 13 Jan 2017 14:34:35 +0100 Received: by mcclellan.cs.miami.edu (Postfix, from userid 501) id 0D3071214EF; Fri, 13 Jan 2017 08:34:35 -0500 (EST) To: caml-list@inria.fr Message-Id: <20170113133435.0D3071214EF@mcclellan.cs.miami.edu> Date: Fri, 13 Jan 2017 08:34:35 -0500 (EST) From: geoff@cs.miami.edu (Geoff Sutcliffe) X-Validation-by: geoff@cs.miami.edu Subject: [Caml-list] CADE-26 Call for Papers The 26th International Conference on Automated Deduction (CADE-26) Gothenburg, Sweden 6-11 August 2017 http://www.cade-26.info CALL FOR PAPERS CADE is the major international forum at which research on all aspects of automated deduction is presented. High-quality submissions on the general topic of automated deduction, including foundations, applications, implementations, theoretical results, practical experiences and user studies are solicited. Key dates: Abstract deadline: 11 February 2017 Submission deadline: 18 February 2017 * Logics of interest include propositional, first-order, equational, higher-order, classical, description, modal, temporal, many-valued, constructive, other non-classical, meta-logics, logical frameworks, type theory, set theory, as well as any combination thereof. * Paradigms of interest include theorem proving, model building, constraint solving, computer algebra, model checking, proof checking, and their integration. * Methods of interest include resolution, superposition, completion, saturation, term rewriting, decision procedures, model elimination, connection methods, tableaux, sequent calculi, natural deduction, as well as their supporting algorithms and data structures, including matching, unification, orderings, induction, indexing techniques, proof presentation and explanation, proof planning. * Applications of interest include program analysis, verification and synthesis of software and hardware, formal methods, computational logic, computer mathematics, natural language processing, computational linguistics, knowledge representation, ontology reasoning, deductive databases, declarative programming, robotics, planning, and other areas of artificial intelligence. Submissions can be made in two categories: regular papers and system descriptions. The page limit in Springer LNCS style is 15 pages excluding references for regular papers and 10 pages excluding references for system descriptions. Submissions must be unpublished and not submitted for publication elsewhere. They will be judged on relevance, originality, significance, correctness, and readability. System descriptions must contain a link to a working system and will also be judged on usefulness and design. Proofs of theoretical results that do not fit in the page limit, executables of systems, and input data of experiments should be made available, via a reference to a website or in an appendix of the paper. For papers containing experimental evaluations, all data needed to rerun the experiments must be available. Reviewers will be encouraged to consider this additional material, but submissions must be self-contained within the respective page limit; considering the additional material should not be necessary to assess the merits of a submission. The review process will include a feedback/rebuttal period where authors will have the option to respond to reviewer comments. The PC chairs may solicit further reviews after the rebuttal period. The proceedings of the conference will be published in the Springer LNCS/LNAI series. Formatting instructions and the LNCS style files can be obtained at http://www.springer.de/comp/lncs/authors.html At every CADE conference the Program Committee selects one of the accepted papers to receive the CADE Best Paper Award. The award recognizes a paper that the Program Committee collegially evaluates as the best in terms of originality and significance, having substantial confidence in its correctness. Overall technical quality, completeness, scholarly accuracy, and readability are also considered. Characteristics associated with a best paper include, for instance, introduction of a strong new technique or approach, solution of a long-standing open problem, introduction and solution of an interesting and important new problem, highly innovative application of known ideas or existing techniques, and presentation of a new system of outstanding power. Under exceptional circumstances, the Program Committee may give two awards (ex aequo) or give no award. IMPORTANT DATES Abstract deadline: 11 February 2017 Submission deadline: 18 February 2017 Rebuttal phase: 8 April 2017 Notification: 22 April 2017 Final version: 27 May 2017 SUBMISSION INSTRUCTIONS Papers should be submitted via https://easychair.org/conferences/?conf=cade26 CADE-26 ORGANIZERS Conference Chairs: Wolfgang Ahrendt Chalmers University of Technology Moa Johansson Chalmers University of Technology Program Committee Chair: Leonardo de Moura Microsoft Research Workshop, Tutorial, and Competition Chair: Philipp Ruemmer Uppsala University Publicity Chair: Magnus Myreen Chalmers University of Technology Program Committee: Clark Barrett Stanford University Christoph Benzmueller Freie Universitaet Berlin Jasmin Christian Blanchette Inria Nancy & LORIA Nikolaj Bjorner Microsoft Research Maria Paola Bonacina Universita degli Studi di Verona Leonardo de Moura Microsoft Research Hans de Nivelle University of Wroclaw Stephanie Delaune CNRS, IRISA Gilles Dowek Inria & ENS Paris-Saclay Amy Felty University of Ottawa Silvio Ghilardi Universita degli Studi di Milano Reiner Haehnle Technical University of Darmstadt Marijn Heule The University of Texas at Austin Moa Johansson Chalmers University of Technology Dejan Jovanovic SRI International Deepak Kapur University of New Mexico Konstantin Korovin The Manchester University Laura Kovacs Vienna University of Technology Christopher Lynch Clarkson University Assia Mahboubi INRIA Aart Middeldorp University of Innsbruck Dale Miller INRIA and LIX/Ecole Polytechnique Albert Oliveras Technical University of Catalonia Lawrence Paulson University of Cambridge Ruzica Piskac Yale University Philipp Ruemmer Uppsala University Renate Schmidt The University of Manchester Stephan Schulz DHBW Stuttgart Roberto Sebastiani University of Trento Viorica Sofronie-Stokkermans University Koblenz-Landau Geoff Sutcliffe University of Miami Cesare Tinelli The University of Iowa Ashish Tiwari SRI International Andrei Voronkov The University of Manchester Christoph Weidenbach Max Planck Institute for Informatics Freek Wiedijk Radboud University Nijmegen