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 3C0F07EE48 for ; Thu, 19 Feb 2015 19:48:45 +0100 (CET) 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 X-IronPort-Anti-Spam-Filtered: true X-IronPort-Anti-Spam-Result: A0AHAgC3L+ZUnAZZH8Bbg1hagjqJf6Z9AYVzhxeCIAaHXQEBAQEBARABAQEBAQgUCUKEMyEqBUgMJAQdWAeIFA2sCaJ9hReMTIJdZYIjDEAdgRQFhV+EZYhjhWSBUpFRgjGBfSAxAYJCAQEB X-IPAS-Result: A0AHAgC3L+ZUnAZZH8Bbg1hagjqJf6Z9AYVzhxeCIAaHXQEBAQEBARABAQEBAQgUCUKEMyEqBUgMJAQdWAeIFA2sCaJ9hReMTIJdZYIjDEAdgRQFhV+EZYhjhWSBUpFRgjGBfSAxAYJCAQEB X-IronPort-AV: E=Sophos;i="5.09,609,1418079600"; d="scan'208";a="122568605" Received: from mcclellan.cs.miami.edu ([192.31.89.6]) by mail2-smtp-roc.national.inria.fr with SMTP; 19 Feb 2015 19:48:44 +0100 Received: by mcclellan.cs.miami.edu (Postfix, from userid 501) id B85B61214A5; Thu, 19 Feb 2015 13:48:43 -0500 (EST) To: caml-list@inria.fr Message-Id: <20150219184843.B85B61214A5@mcclellan.cs.miami.edu> Date: Thu, 19 Feb 2015 13:48:43 -0500 (EST) From: geoff@cs.miami.edu (Geoff Sutcliffe) X-Validation-by: geoff@cs.miami.edu Subject: [Caml-list] TABLEAUX 2015 - Call for Papers FIRST CALL FOR PAPERS TABLEAUX 2015 23rd International Conference on Automated Reasoning with Analytic Tableaux and Related Methods Wroclaw, Poland, September 21-24, 2015 http://tableaux2015.ii.uni.wroc.pl/ GENERAL INFORMATION TABLEAUX 2015 is the 23rd in the series of international meetings on Automated Reasoning with Analytic Tableaux and Related Methods, and will be held in Wroclaw, Poland, during September 21-24, 2015. TABLEAUX 2015 will be co-located with the 10th International Symposium on Frontiers of Combining Systems (FroCoS 2015). The computer science institute of Wroclaw has a large experience in hosting international conferences. It has hosted the IEEE Symposium on Logic in Computer Science (LICS 2007), the 23rd International Conference on Automated Deduction (CADE 2011), and the 22nd European Symposium on Algorithms (ALGO 2014). TOPICS Tableaux methods offer a convenient and flexible set of tools for automated reasoning in classical logic, extensions of classical logic, and a large number of non-classical logics. For large groups of logics, tableaux methods can be generated automatically. Areas of application include verification of software and computer systems, deductive databases, knowledge representation and its required inference engines, teaching, and system diagnosis. The conference series aims to bring together researchers interested in all aspects of tableaux - theoretical foundations, applications, and implementation techniques. * tableaux methods for classical and non-classical logics (e.g. modal, temporal, description, intuitionistic, substructural, fuzzy, paraconsistent logics) and their proof theoretic foundations. * related methods (model elimination, model checking, connection methods, resolution, BDDs). * sequent calculi for classical and non-classical logics, as tools for proof search and proof representation. * flexible, easily extendable, light weight methods for theorem proving. * novel types of calculi for theorem proving and verification in classical and non-classical logics. * systems, tools, implementations and applications (provers, logical frameworks, model checkers, ... ). * implementation techniques (data structures, efficient algorithms, performance measurement, extendibility, ... ). * extensions of tableaux procedures with conflict-driven learning, generation of proofs; compact (or humanly readable) representation of proofs. * decision procedures, theoretically optimal procedures. * applications of automated deduction to mathematics, software development, protocol verification, or teaching. TABLEAUX 2015 also welcomes papers describing applications of tableaux procedures to real world examples. Such papers should be tailored to the tableaux community and should focus on the role of reasoning, and logical aspects of the solution. SUBMISSIONS Submissions are invited in two categories: A Research papers, which describe original theoretical research, original algorithms, or applications, with length up to 15 pages. B System descriptions, with length up to 10 pages. Submissions will be reviewed by the PC, possibly will help of external reviewers, taking into account readability, relevance and originality. For category A, theoretical results and algorithms must be original, and not submitted for publication elsewhere. Submissions will be reviewed taking into account correctness, theoretical prettyness, and possible implementability. For category B submissions, a working implementation must be available on the internet, which includes sources. The aim of a system description is to make the system available in such a way that users can use it, understand it, and build on it. Accepted papers in both categories will be published in the conference proceedings (within the LNAI series of Springer). For accepted papers in both of the categories, at least one author is required to attend the conference and present the paper. Further information and instructions about submissions can be found on the conference website http://tableaux2015.ii.uni.wroc.pl IMPORTANT DATES Abstract submission deadline: May 8th, 2015 Paper submission deadline: May 15th, 2015 Author Notification: July 1st, 2015 Final Version: July 17th 2015 Conference: September 21st-24th, 2015 PROGRAM COMMITTEE ----------------- Marc Bezem, University of Bergen, Norway Agata Ciabattoni, Vienna University of Technology, Austria David Delayahe, National Conservatory of Arts and Professions, Paris, France Ulrich Furbach, University of Koblenz, Germany Didier Galmiche, Universite de Lorraine, Nancy, France Silvio Ghilardi, Universita degli Studi di Milano, Italy Rajeev Gore, Australian National University, Canberra, Australia Stephane Graham-Lengrand, Ecole Polytechnique, Palaiseau, France Reiner Haehnle, Darmstadt University of Technology, Germany Konstantin Korovin, University of Manchester, UK George Metcalfe, University of Bern, Switzerland Dale Miller, INRIA Saclay-Ile-de-France, France Barbara Morawska, Technische Universitaet Dresden, Germany Boris Motik, University of Oxford, UK Claudia Nalon, University of Brasilia, Brasil Sara Negri, University of Helsinki, Finland Linh Anh Nguyen, University of Warsaw, Poland Hans de Nivelle (chair), University of Wroclaw, Poland Jens Otten, University of Potsdam, Germany Andrei Popescu, Middlesex University London, UK Renate Schmidt, University of Manchester, UK Luca Vigano, King's College, London, UK Bruno Woltzenlogel-Paleo, Vienna University of Technology, Austria WORKSHOPS AND TUTORIALS ------------------------ Workshops have been solicited in separate call, which can be found on http://tableaux2015.ii.uni.wroc.pl or http://frocos2015.ii.uni.wroc.pl Tutorials for FroCoS/TABLEAUX will be solicited in a separate call, which will be published later.