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 mail3-relais-sop.national.inria.fr (mail3-relais-sop.national.inria.fr [192.134.164.104]) by sympa.inria.fr (Postfix) with ESMTPS id CEB8B80035 for ; Wed, 12 Oct 2016 15:31:21 +0200 (CEST) Authentication-Results: mail3-smtp-sop.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 (mail3-smtp-sop.national.inria.fr: no sender authenticity information available from domain of geoff@cs.miami.edu) identity=pra; client-ip=192.31.89.6; receiver=mail3-smtp-sop.national.inria.fr; envelope-from="geoff@cs.miami.edu"; x-sender="geoff@cs.miami.edu"; x-conformance=sidf_compatible Received-SPF: Pass (mail3-smtp-sop.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=mail3-smtp-sop.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 (mail3-smtp-sop.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=mail3-smtp-sop.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=3A/79NGRBCuK1ooJQ33upxUyQJP3N1i/DPJgcQr6Af?= =?us-ascii?q?oPdwSP74pcbcNUDSrc9gkEXOFd2CrakV0ayK6eu+AiQp2tWoiDg6aptCVhsI24?= =?us-ascii?q?09vjcLJ4q7M3D9N+PgdCcgHc5PBxdP9nC/NlVJSo6lPwWB6kO74TNaIBjjLw09?= =?us-ascii?q?fr2zQd+IyZjtnL7ps7ToICxwzAKnZr1zKBjk5S7wjeIxxbVYF6Aq1xHSqWFJce?= =?us-ascii?q?kFjUlhJFaUggqurpzopM0roGxsvKcq/stEFKH7ZLgQTLpCDT1gPXpmytfssEzM?= =?us-ascii?q?QAyB6FMXSSMTkxNNAk7I4AyyHrj8tSX0/tFgxCKePMP4QPFnCnyZ8653RUqw22?= =?us-ascii?q?88PDkj/TSPhw=3D=3D?= X-IronPort-Anti-Spam-Filtered: true X-IronPort-Anti-Spam-Result: =?us-ascii?q?A0AoAwD7Of5X/wZZH8BCGh0BBQELARgBF?= =?us-ascii?q?wEGAYMEAQEBAQF0fAGCeIo6mVkBiVeICIIMASWIVRQBAQEBAQEBAQEBAV0nQQ6?= =?us-ascii?q?BYxiCOyEqBUgwBB2JFA4tph+ZRwaDIjKSJQtZgi8FiDyRRoYngwSGR4JHjTmIf?= =?us-ascii?q?4N6g38eNoVMIjSEDIRYAQEB?= X-IPAS-Result: =?us-ascii?q?A0AoAwD7Of5X/wZZH8BCGh0BBQELARgBFwEGAYMEAQEBAQF?= =?us-ascii?q?0fAGCeIo6mVkBiVeICIIMASWIVRQBAQEBAQEBAQEBAV0nQQ6BYxiCOyEqBUgwB?= =?us-ascii?q?B2JFA4tph+ZRwaDIjKSJQtZgi8FiDyRRoYngwSGR4JHjTmIf4N6g38eNoVMIjS?= =?us-ascii?q?EDIRYAQEB?= X-IronPort-AV: E=Sophos;i="5.31,482,1473112800"; d="scan'208";a="196527453" Received: from mcclellan.cs.miami.edu ([192.31.89.6]) by mail3-smtp-sop.national.inria.fr with SMTP; 12 Oct 2016 15:31:20 +0200 Received: by mcclellan.cs.miami.edu (Postfix, from userid 501) id E89C212149D; Wed, 12 Oct 2016 09:31:19 -0400 (EDT) To: caml-list@inria.fr Message-Id: <20161012133119.E89C212149D@mcclellan.cs.miami.edu> Date: Wed, 12 Oct 2016 09:31:19 -0400 (EDT) From: geoff@cs.miami.edu (Geoff Sutcliffe) X-Validation-by: geoff@cs.miami.edu Subject: [Caml-list] AI Communications: Special Issue on Automated Reasoning CALL FOR PAPERS --------------------------------- Special issue of the AI Communications on Automated Reasoning --------------------------------- IMPORTANT DATES --------------- Abstract submission: January 8, 2017 Paper submission: January 15, 2017 Notification of acceptance: April 15, 2017 Final versions: June 15, 2017 BACKGROUND ---------- This special issue follows two successful 2016 events in Automated Reasoning: Artificial Intelligence and Theorem Proving (AITP 2016) (http://aitp-conference.org/) Practical Aspects of Automated Reasoning (PAAR 2016) (http://cs.ru.nl/paar16/). About PAAR: 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. PAAR brings together different groups to concentrate on practical aspects of the implementation and application of automated reasoning tools. About AITP: Large-scale semantic processing and strong computer assistance of mathematics and science is our inevitable future. New combinations of AI and reasoning methods and tools deployed over large mathematical and scientific corpora will be instrumental to this task. AITP is the forum for discussing how to get there as soon as possible, and the force driving the progress towards that. SCOPE AND TOPICS ---------------- The focus of the special issue will be on new combination of AI and Automated Reasoning, and on practical applications of Automated Reasoning. The topics of interest include: * Automated reasoning in propositional, first-order, higher-order and non-classical logics * AI and big-data methods in theorem proving and mathematics * Collaboration between automated and interactive theorem proving * Alignment and joint processing of formal, semi-formal, and informal libraries * Implementation of provers (SAT, SMT, resolution, tableau, instantiation- based, rewriting, logical frameworks, etc) * Automated reasoning tools for all kinds of practical problems and applications * Methods for large-scale computer understanding of mathematics and science * Common-sense reasoning and reasoning in science * Combinations of linguistic/learning-based and semantic/reasoning methods * 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, optimizations techniques, strategies and heuristics, fairness Participants of AITP 2016 and PAAR 2016, as well as other authors are invited to submit contributions. SUBMISSION GUIDELINES --------------------- This special issue welcomes original high-quality contributions that have been neither published in nor simultaneously submitted to other venues. Submissions will be peer-reviewed using the standard refereeing procedure of the AI Communications. Full papers of a maximum extension of 15 pages should be prepared according to the AIComm style guidelines described at the following link: http://www.iospress.nl/journal/ai-communications/ Papers should be submitted through the AIComm mstracker: http://mstracker.com/submit1.php?jc=aic GUEST EDITORS ------------- Pascal Fontaine Cezary Kaliszyk Stephan Schulz Josef Urban