[TYPES/announce] CADE-22 last call for papers

[Carsten Schuermann]

		      LAST CALL FOR PAPERS

			     CADE-22
      22nd International Conference on Automated Deduction
	       McGill University, Montreal, Canada
			August 2-7, 2009


		Submission Deadline: 23 Feb 2009
	      http://complogic.cs.mcgill.ca/cade22/


GENERAL INFORMATION
  CADE is the major forum for the presentation of research in all
  aspects of automated deduction. The conference programme will
  include invited talks, paper presentations, system
  descriptions, workshops, tutorials, and system competitions.

SCOPE
  We invite high-quality submissions on the general topic of
  automated deduction, including foundations, applications,
  implementations and practical experiences. 

  Logics of interest include, but are not limited to

    o propositional, first-order, equational, higher-order,
      classical, description, modal, temporal, many-valued,
      intuitionistic, other non-classical, meta-logics,
      logical frameworks, type theory and set theory.

  Methods of interest include, but are not limited to

    o saturation, resolution, instance-based, tableaux, sequent
      calculi, natural deduction, term rewriting, decision
      procedures, model generation, model checking, constraint
      solving, induction, unification, proof planning, proof
      checking, proof presentation and explanation.

  Applications of interest include, but are not limited to

    o program analysis and verification, hardware verification,
      mathematics, natural language processing, computational
      linguistics, knowledge representation, ontology reasoning,
      deductive databases, functional and logic programming,
      robotics, planning, and other areas of AI.

INVITED SPEAKERS:
  Konstantin Korovin   The University of Manchester
  Martin Rinard        Massachusetts Institute of Technology
  Mark Stickel         SRI International

WORKSHOPS, TUTORIALS, SYSTEM COMPETITIONS:
  There will be a two-day programme of eight workshops and four
  tutorials before the conference. In addition, two system
  competitions will be held during the conference.

    Workshops:
      o Automated Deduction: Decidability, Complexity,
            Tractability (ADDCT)
      o Beyond SAT: What About First-Order Logic?
      o Logical Frameworks and Meta-Languages: Theory and
            Practice (LFMTP)
      o Modules and Libraries for Proof Assistants (MLPA)
      o Proof Search in Type Theories (PSTT)
      o Satisfiability Modulo Theories (SMT)
      o The International Workshop on Unification (UNIF)
      o TPTP World Workshop (TPTPWoWo)

    Tutorials:
      o Hierarchical and Modular Reasoning in Complex Theories
      o Probabilistic Analysis Using a Theorem Prover
      o Precise, Automated and Scalable Verification of Systems
            Software Using SMT solvers
      o Logics with Undefinedness

    System competitions:
      o The CADE ATP System Competition (CASC)
      o Satisfiability Modulo Theories Competition (SMT-COMP)

  Details will be published in separate calls and on the
  conference website.

STUDENT AWARDS
  Travel awards will be available to enable selected students to
  attend the conference. Details will be published on the
  conference website.

PUBLICATION DETAILS:
  The proceedings of the conference will be published in the
  Springer LNAI/LNCS series.

SUBMISSION INSTRUCTIONS:
  Submissions can be made in the categories 'regular papers' and
  'system descriptions'. The page limit in Springer LNCS style is
  15 pages for regular papers and 5 pages for system
  descriptions. Full system descriptions that provide in-depth
  presentation of original ideas in an implemented system can be
  submitted as regular papers. For the benefit of reviewers,
  additional material may be provided by a clearly marked
  appendix or a reference to a manuscript on a website. It is at
  the discretion of the reviewers whether such supplements will
  be considered. All regular papers will be evaluated according
  to the highest standards in terms of originality, significance,
  technical quality, and readability.

  Submissions must be in English and standard conforming pdf
  format. Submissions must be unpublished and not submitted for
  publication elsewhere. Authors are strongly encouraged to
  produce their papers in LaTeX.

  Formatting instructions and the LNCS style files can be
  obtained via http://www.springer.de/comp/lncs/authors.html.

  To submit your paper please use the EasyChair submission system
  at this address:
  http://www.easychair.org/conferences/?conf=cade22. 

IMPORTANT DATES:
  A paper title and a short abstract of about 100 words must be
  submitted before the paper. 

      16  Feb 2009 Abstract submission deadline
      23  Feb 2009 Paper submission deadline
      10  Apr 2009 Notification of paper decisions
      14  May 2009 Camera-ready papers due

      2-3 Aug 2009 Workshops & Tutorials
      4-7 Aug 2009 Conference, including CASC and SMT-COMP

PROGRAM COMMITTEE:
  Alessandro Armando     Università di Genova
  Franz Baader           Technische Universität Dresden
  Peter Baumgartner      NICTA, Canberra
  Maria Paola Bonacina   Università degli Studi di Verona
  Bernhard Beckert       Universität Koblenz-Landau
  Nikolaj Bjørner        Microsoft Research
  Alessandro Cimatti     Istituto per la Ricerca Scientifica e 
                             Tecnologica, Trento
  Silvio Ghilardi        Università degli Studi di Milano
  Jürgen Giesl           RWTH Aachen
  Rajeev Goré            The Australian National University
  Reiner Hähnle          Chalmers University of Technology
  John Harrison          Intel Corporation
  Miki Hermann           École Polytechnique
  Ullrich Hustadt        University of Liverpool
  Katsumi Inoue          National Institute of Informatics, Japan
  Tommi Junttila         Helsinki University of Technology
  Deepak Kapur           University of New Mexico
  Alexander Leitsch      Technische Universität Wien
  Christopher Lynch      Clarkson University
  Claude Marché          INRIA Saclay, Parc Orsay Université
  William McCune         University of New Mexico
  Aart Middeldorp        Universität Innsbruck
  Hans de Nivelle        University of Wroclaw
  Albert Oliveras        Universitat Politècnica de Catalunya
  Lawrence Paulson       University of Cambridge
  Brigitte Pientka       McGill University
  David Plaisted         University of North Carolina 
                             at Chapel Hill
  Michaël Rusinowitch    LORIA-INRIA-Lorraine
  Renate Schmidt (Chair) The University of Manchester
  Carsten Schürmann      IT-Universitetet i København
  Aaron Stump            The University of Iowa
  Geoff Sutcliffe        University of Miami
  Cesare Tinelli         The University of Iowa
  Andrei Voronkov        The University of Manchester
  Christoph Weidenbach   Max-Planck-Institut für Informatik

ORGANIZERS:
  Conference Chair:          
      Brigitte Pientka   McGill University
  Workshop & Tutorial Chair: 
      Aaron Stump        The University of Iowa
  Publicity Chair:           
      Carsten Schürmann  IT-Universitetet i København
  PC Chair:                  
      Renate Schmidt     The University of Manchester