From mboxrd@z Thu Jan 1 00:00:00 1970 Return-Path: Received: from mail2-relais-roc.national.inria.fr (mail2-relais-roc.national.inria.fr [192.134.164.83]) by c5ff346549e7 (Postfix) with ESMTP id 283DB5D5 for ; Mon, 18 Feb 2019 13:59:47 +0000 (UTC) X-IronPort-AV: E=Sophos;i="5.58,384,1544482800"; d="scan'208";a="369870723" Received: from sympa.inria.fr ([193.51.193.213]) by mail2-relais-roc.national.inria.fr with ESMTP; 18 Feb 2019 14:59:43 +0100 Received: by sympa.inria.fr (Postfix, from userid 20132) id 296EB825CB; Mon, 18 Feb 2019 14:59:43 +0100 (CET) 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 82AC87F61F for ; Mon, 18 Feb 2019 14:52:19 +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@mail-qk1-f227.google.com IronPort-PHdr: =?us-ascii?q?9a23=3A6xrZ6BW0D5B5i8k7Xk4NED0Z+IvV8LGtZVwlr6E/?= =?us-ascii?q?grcLSJyIuqrYbB2Dt8tkgFKBZ4jH8fUM07OQ7/iwHzRYqb+681k6OKRWUBEEjc?= =?us-ascii?q?hE1ycBO+WiTXPBEfjxciYhF95DXlI2t1uyMExSBdqsLwaK+i764jEdAAjwOhRo?= =?us-ascii?q?LerpBIHSk9631+ev8JHPfglEnjWwba9xIRmssQndqtQdjJd/JKo21hbHuGZDdf?= =?us-ascii?q?5MxWNvK1KTnhL86dm18ZV+7SleuO8v+tBZX6nicKs2UbJXDDI9M2Ao/8LrrgXM?= =?us-ascii?q?TRGO5nQHTGoblAdDDhXf4xH7WpfxtTb6tvZ41SKHM8D6Uaw4VDK/5KhsVRHolT?= =?us-ascii?q?wHNyYn/27Llsx+gqVboBe7qBx+xY7ffYWZOfV6c6/Ye94RWGhPUdtLVyFZH42y?= =?us-ascii?q?cYwBAekPM+hYtITxu0cCoQeiCQS2GO/j1jlFjWL2060g1OQhFBnL3AM+ENIJvn?= =?us-ascii?q?TUos74O7sJUeyvyanIzC/Mb/ZX2Tvn9ofHbw0hrPeRVrx+dsrRzFMgFwLDjliI?= =?us-ascii?q?tYzlJy+V1vwXv2ic9epgWvqji3M7pA1rujiv2t8giobOhoISxVDE8Tt2zJwpKt?= =?us-ascii?q?2/TU53ed+kEJ1KtyGbLYR6WM0iQ3twtCkk0LIGop66czQKyJs9xh7fceaLc4+S?= =?us-ascii?q?4hLsTOqePS13i297d76mmRq/81Ksyuz6Vsm611ZGtjdFktjXuXAOzRDc8NSIRu?= =?us-ascii?q?Fn8Ue9wTqPzBjT6vtFIUAymqrUNYQhzqQtmZUNt0nIAyz4mF3ugaOIakkp/vKk?= =?us-ascii?q?5ufnb7n8uJOQKZF4hhvgPqgwmMGzGfk0PwwQU2SB9+mwyafv8E79TblQk/E6jK?= =?us-ascii?q?/Uu43AK8sBvK62GQpV354j6xmhCzem18wVnXwdI1JEfBKLlpHpO1LTLPzhA/ez?= =?us-ascii?q?nUqgnTVxy/DJOb3hBZrNLnzdn7v7Ybl97EtcxBIyzdBZ+Z1UFqkMLOzvVkL1rt?= =?us-ascii?q?DVDR80Pxaqz+r5FtlxzJ0SVXyND6OBNaPdq16I5uYhI+mWY48VvS7wK/c76P7p?= =?us-ascii?q?g385l0QQcrWy3ZcNbXC4H+5pI0CYYXb2nNgODHoKshIkTOP2kF2CTSJTZ3GqUq?= =?us-ascii?q?0g/D47DYamAZ7HRoCsm7yBwDy2HoZWZ2BDElCDC23kd4SCW/cWaSKdONVtkjIe?= =?us-ascii?q?Vevpd4h0gRqnsQu/z7t8MsLV/DcZvNTtzo4myffUkEQ9+Dt6AeyWyCeITmhxny?= =?us-ascii?q?UFSyJlj+hEvUVhxwLbguBDiPtCGIkPtqoYADd/DobVyqlBM/63XwvAetmTT1P/?= =?us-ascii?q?HoetGnc0T9s0wpkDb1svQoz+3CCG5DKjBvour5LOHIY9q/6O1GO3Isd0zneA2a?= =?us-ascii?q?U83QF/H5l/cFa+j6s6zDD9Qo7El0LDyfSvfKUYmTfOrSKNlzDR+k5fVwF0XOPO?= =?us-ascii?q?WnVNPkY=3D?= X-IronPort-Anti-Spam-Filtered: true X-IronPort-Anti-Spam-Result: =?us-ascii?q?A0BCAADQt2pch+PeVdFjgheCa1FZjH+LB?= =?us-ascii?q?YoGkCGBJANUAQwjgVSGZxoHAQQwCQ0BAwEBAgEBAQEBEwEBAQgNCQgpIwyCOgy?= =?us-ascii?q?DKCMBASYSOzQdCAEFASIcEoMFAYFyD59oPIoqgiCCeAEBBYEwAU8FQYMRBx+BJ?= =?us-ascii?q?AgJAQiHcYF9PIIIF4F/gRGGFw4LAQEBARiBIQqDVoImiWophz2EOI0+CYc9g2+?= =?us-ascii?q?HHyWCRogHiDOQDYxJDyGBJW2BIXKDBgEzCQmCJIILgUkzgQuBG4I7TYUQITMBj?= =?us-ascii?q?RiCTAEB?= X-IPAS-Result: =?us-ascii?q?A0BCAADQt2pch+PeVdFjgheCa1FZjH+LBYoGkCGBJANUAQw?= =?us-ascii?q?jgVSGZxoHAQQwCQ0BAwEBAgEBAQEBEwEBAQgNCQgpIwyCOgyDKCMBASYSOzQdC?= =?us-ascii?q?AEFASIcEoMFAYFyD59oPIoqgiCCeAEBBYEwAU8FQYMRBx+BJAgJAQiHcYF9PII?= =?us-ascii?q?IF4F/gRGGFw4LAQEBARiBIQqDVoImiWophz2EOI0+CYc9g2+HHyWCRogHiDOQD?= =?us-ascii?q?YxJDyGBJW2BIXKDBgEzCQmCJIILgUkzgQuBG4I7TYUQITMBjRiCTAEB?= X-IronPort-AV: E=Sophos;i="5.58,384,1544482800"; d="scan'208";a="369868319" Received: from mail-qk1-f227.google.com ([209.85.222.227]) by mail2-smtp-roc.national.inria.fr with ESMTP/TLS/AES128-GCM-SHA256; 18 Feb 2019 14:52:17 +0100 Received: by mail-qk1-f227.google.com with SMTP id f196so9956580qke.10 for ; Mon, 18 Feb 2019 05:52:18 -0800 (PST) DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=cs-miami-edu.20150623.gappssmtp.com; s=20150623; h=subject:to:message-id:date:from; bh=hlZEVt6upSjt9Q0nJOnClHrzSSmD0X+PvlW4aIqYhYs=; b=xVCfJHE62WUpAI9r0mkKququJ3zATyhQ9RQlYHdPLX0jJj4BHPfu+E8AcdYWMlWWNm j912NSclED5olf5bFymsMESr4moPL+bysU9pzQZSwS53zpXP4jdhQpw1GjDIuJPXb8cQ Q3ADTTKIor1W+RVus6Qsbp83v0lxaekVEi75ucnAs1/TfTKF/UNaDzy1TC5kLI0uUM0o UZD0eC4DtCTMUr0woedT1iyouBmEIJKtThoMEDlgXBcpvUKHCy9ify6ORWZXhD+gK1uV Iezpu1NkgU4Uixu9dB9LVawh/uY6xOngfloNzZ7ti5Rwvq6Ha1XCNT8a/eB6qccITwwF FA4w== X-Google-DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=1e100.net; s=20161025; h=x-gm-message-state:subject:to:message-id:date:from; bh=hlZEVt6upSjt9Q0nJOnClHrzSSmD0X+PvlW4aIqYhYs=; b=kVqLSjJDQu7GSjQuc+lEV5vcrMJTw7WULSO/WKOPW/wXEmjwXSrPZhM5gQIdQWdXuI krO0DHBCcjeTaMPehmTL5qGHdMWu/EYrfOWIJjUn2XJzMg56NYr3tBbZoEUKhqGkza/N qgPxGfkMIL6CTIRa0iNA5NNk6ZbW3avoPRQWJkA4d/Rae0KF3M7Mu4+L/Ee16amzEPZt o70J2MLrIILExGbSadSykLH/+w36X/KOdBJdFcOJQMijsYzV3GMicnkGx4yh1RpFdzhG 9RNYZ8gt8+Oq/OhQE3IULePaPyW5jFUNzIzu2izd0aVZPBHn1IbVs9koXCVmLFmkfMIP gsfA== X-Gm-Message-State: AHQUAuZZQrkRYZUYSfdiY62DQcP3ZqHpd2XFU1KrCeTQ7jh78uJOybAB E3DqpRArgsFO8b8OEWIWkAfHsCGHih7628oJD+gqvztzCQ4PDg== X-Google-Smtp-Source: AHgI3IaBBtLxRnm3+jAEYHUAKJJ9EFkQXwe4g/XBXih58IRHjDsdLN+O0Imi2i5Ty8RtSohx9A8Y9ju3uOn/ X-Received: by 2002:a37:6a44:: with SMTP id f65mr17180959qkc.244.1550497936984; Mon, 18 Feb 2019 05:52:16 -0800 (PST) Received: from cs.miami.edu (ewell.cs.miami.edu. [192.31.89.12]) by smtp-relay.gmail.com with ESMTP id v2sm1535315qkl.1.2019.02.18.05.52.16 for ; Mon, 18 Feb 2019 05:52:16 -0800 (PST) X-Relaying-Domain: cs.miami.edu Received: by cs.miami.edu (Postfix, from userid 3640) id 790A11700E13; Mon, 18 Feb 2019 08:51:52 -0500 (EST) To: X-Mailer: mail (GNU Mailutils 2.99.98) Message-Id: <20190218135152.790A11700E13@cs.miami.edu> Date: Mon, 18 Feb 2019 08:51:52 -0500 (EST) From: geoff@cs.miami.edu X-Validation-by: geoff@cs.miami.edu Subject: [Caml-list] CADE-27: Second Call for Papers Reply-To: geoff@cs.miami.edu X-Loop: caml-list@inria.fr X-Sequence: 17351 Errors-to: caml-list-owner@inria.fr Precedence: list Precedence: bulk Sender: caml-list-request@inria.fr X-no-archive: yes List-Id: List-Archive: List-Help: List-Owner: List-Post: List-Subscribe: List-Unsubscribe: The 27th International Conference on Automated Deduction (CADE-27) Natal, Brazil 25-30 August 2019 http://www.cade-27.info CALL FOR PAPERS CADE is the major international forum for presenting research on all aspects of automated deduction. 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 (extended): 20 February 2019 Submission deadline (extended): 27 February 2019 * 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 chair 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: 20 February 2019 Submission deadline: 27 February 2019 Rebuttal phase: 2 April 2019 Notification: 15 April 2019 Final version: 27 May 2019 SUBMISSION INSTRUCTIONS Papers should be submitted via https://easychair.org/conferences/?conf=cade27 CADE-27 ASSOCIATED EVENTS Automated Reasoning: Challenges, Applications, Directions, Exemplary Achievements (ARCADE), http://cl-informatik.uibk.ac.at/users/swinkler/arcade/ The CADE ATP System Competition, http://www.tptp.org/CASC/27/ Deduction Mentoring Workshop Logical and Semantic Frameworks, with Applications (LSFA), https://sites.google.com/view/lsfa2019 Proof eXchange for Theorem Proving (PxTP), http://pxtp.gforge.inria.fr/2019/ Theorem Prover Components for Educational Software (ThEdu'19), http://www.uc.pt/en/congressos/thedu/thedu19 The 6th Vampire Workshop CADE-27 ORGANIZERS Conference Chair: Elaine Pimentel Federal University of Rio Grande do Norte, Brazil Organizers: Carlos Olarte Federal University of Rio Grande do Norte, Brazil Joao Marcos Federal University of Rio Grande do Norte, Brazil Claudia Nalon University of Brasilia, Brazil Giselle Reis CMU, Qatar Program Committee Chair: Pascal Fontaine Universite de Lorraine, CNRS, Inria, LORIA, France Workshop, Tutorial, and Competition Chair: Giles Reger University of Manchester, UK Publicity Chair: Geoff Sutcliffe University of Miami, USA Program Committee: Carlos Areces, FaMAF - Universidad Nacional de Cordoba, Argentina Franz Baader, TU Dresden, Germany Clark Barrett, Stanford University, USA Jasmin Christian Blanchette, Vrije Universiteit Amsterdam, The Netherlands Maria Paola Bonacina, Universita degli Studi di Verona, Italy Leonardo Mendonca de Moura, Microsoft Research, USA Hans de Nivelle, Nazarbayev University, Astana, Kazakhstan Clare Dixon, University of Liverpool, UK Mnacho Echenim, Universite de Grenoble, France Marcelo Finger, University of Sao Paulo, Brazil Pascal Fontaine, Universite de Lorraine, CNRS, Inria, LORIA, France Silvio Ghilardi, Universita degli Studi di Milano, Italy Juergen Giesl, RWTH Aachen University, Germany Rajeev Gore, The Australian National University, Australia Stefan Hetzl, Technische Universitaet Wien, Austria Marijn J. H. Heule, The University of Texas at Austin, USA Nao Hirokawa, JAIST, Japan Moa Johansson, Chalmers University of Technology, Sweden Cezary Kaliszyk, University of Innsbruck, Austria Deepak Kapur, University of New Mexico, USA Benjamin Kiesl, Technische Universitaet Wien, Austria Konstantin Korovin, The University of Manchester, UK Laura Kovacs, Technische Universitaet Wien, Austria Ramana Kumar, DeepMind, UK Claudia Nalon, University of Brasilia, Brazil Vivek Nigam, Federal University of Paraiba & Fortiss, Brazil & Germany Carlos Olarte, Federal University of Rio Grande do Norte, Brazil Jens Otten, University of Oslo, Norway Andre Platzer, Carnegie Mellon University, USA Andrew Reynolds, The University of Iowa, USA Philipp Ruemmer, Uppsala University, Sweden Renate A. Schmidt, The University of Manchester, UK Stephan Schulz, DHBW Stuttgart, Germany Roberto Sebastiani, University of Trento, Italy Natarajan Shankar, SRI International, USA Viorica Sofronie-Stokkermans, Universitaet Koblenz-Landau, Germany Martin Suda, Czech Technical University, Czech Republic Geoff Sutcliffe, University of Miami, USA Rene Thiemann, University of Innsbruck, Austria Uwe Waldmann, Max Planck Institute for Informatics, Germany Christoph Weidenbach, Max Planck Institute for Informatics, Germany Sarah Winkler, University of Innsbruck, Austria