[DL] CADE'05:Call for participation

[Brigitte Pientka]

----------------------------------------------------------
                         CADE-20
       20th International Conference on Automated Deduction
            Tallinn, Estonia, July 22 - July 27, 2005
                http://deepthought.ttu.ee/it/cade/

                   CALL FOR PARTICIPATION

-----------------------------------------------------------
    IMPORTANT DATES:

   Deadline for early registration: 20. June, 2005.
   Deadline for non-cash payments: 12. July, 2005.
   Workshops: July 22-23, 2005
   Conference: July 24-27, 2005
-----------------------------------------------------------

CADE is the major forum for the presentation of research
in all aspects of automated deduction.

  -Logics of interest include propositional, first-order, equational,
higher-order, classical, intuitionistic, constructive, modal,
temporal, many-valued, substructural, description, and meta-logics,
logical frameworks, type theory and set theory.

  -Methods of interest include saturation, resolution, tableaux,
sequent calculi, term rewriting, induction, unification, constraint
solving, decision procedures, model generation, model checking,
natural deduction, proof planning, proof presentation, proof checking,
and explanation.

  -Applications of interest include hardware and software development,
systems analysis and verification, deductive databases, functional and
logic programming, computer mathematics, natural language processing,
computational linguistics, robotics, planning, knowledge
representation, and other areas of AI.

     INVITED TALKS:

Invited talks will be given at CADE-20 by Randal Bryant (CMU), Gilles
Dowek (Ecole Polytechnique) and by Frank Wolter (U. Liverpool).

     INVITED TUTORIALS:

- Bruno Blanchet
  An Automatic Security Protocol Verifier based on
  Resolution Theorem Proving

- Enrico Giunchiglia
  Beyond SAT: QSAT, and SAT-based Decision Procedures

      ACCEPTED PAPERS:

- Tomasz Truderung:
  Regular Protocols and Attacks with Regular Knowledge

- Greta Yorsh and Madan Musuvathi:
  A Combination Method for Generating Interpolants

- Ullrich Hustadt, Boris Konev and Renate A. Schmidt.
  Deciding monodic fragments by temporal resolution

- Guillaume Dufay, Amy Felty and Stan Matwin.
  Privacy-Sensitive Information Flow with JML

- Viktor Kuncak, Hai, Huu Nguyen and Martin Rinard.
  An Algorithm for Deciding BAPA: Boolean Algebra with Presburger
Arithmetic

- Franz Baader and Silvio Ghilardi.
  Connecting many-sorted theories

- Claudio Castellini and Alan Smaill.
  Proof Planning for First-Order Temporal Logic

- Graham Steel.
  Deduction with XOR Constraints in Security API Modelling

- Tal Lev-Ami, Neil Immerman, Siddharth Srivastava, Greta Yorsh, Mooly
  Sagiv and Thomas W. Reps.
  Simulating Reachability using First-Order Logic with Applications to
  Verification of Linked Data Structures

- Viorica Sofronie-Stokkermans.
  Hierarchic reasoning in local theory extensions

- Kaustuv Chaudhuri and Frank Pfenning.
  A Focusing Inverse Method Prover for First-Order Linear Logic

- Mizuhito Ogawa, Eiichi Horita and Satoshi Ono.
  Proving Properties of Incremental Merkel Trees

- Evelyne Contejean and Pierre Corbineau.
  Reflecting Proofs in First-Order Logic with Equality

- Chad Brown.
  Reasoning in Extensional Type Theory with Equality

- Christian Fermueller and Reinhard Pichler.
  Model Representation via Contexts and Implicit Generalizations

- Peter Baumgartner and Cesare Tinelli.
  ME-E -- The Model Evolution Calculus with Equality

- Brigitte Pientka.
  Tabling for higher-order logic programming

- Christian Urban and Christine Tasson.
  Nominal Techniques in Isabelle/HOL

- Kumar Neeraj Verma, Helmut Seidl and Thomas Schwentick.
  On the Complexity of Equational Horn Clauses

- Jordi Levy, Mateu Villaret and Joachim Niehren.
  Well-Nested Context Unification

- Serge R. Autexier.
  The CORE Calculus

- Guillem Godoy and Ashish Tiwari.
  Termination of Rewrite Systems with Shallow Right-Linear,
  Collapsing, and Right-Ground Rules

- Jian Zhang.
  Computer Search for Counterexamples to Wilkie's Identity

- John Harrison and Sean McLaughlin.
  A Proof Producing Decision Procedure for Real Arithmetic

- Ting Zhang, Henny Sipma and Zohar Manna.
  The Decidability of the First-order theory of Knuth-Bendix Order

     SYSTEM DESCRIPTIONS

- Sean Bechhofer, Ian Horrocks and Daniele Turi.
  The OWL Instance Store (System Description)

- Andreas Meier and Erica Melis.
  MULTI: A Multi-Strategy Proof Planner (System Description)

- Marco Bozzano, Roberto Bruttomesso, Alessandro Cimatti, Tommi
  Junttila, Peter van Rossum, Stephan Schulz and Roberto Sebastiani.
  MathSAT 3 (System Description)

- Marco Benedetti.
  sKizzo: A Suite to Evaluate and Certify QBFs (System Description)

- Alex Sinner and Thomas Kleemann.
  KRHyper - In Your Pocket (System Description)

     WORKSHOPS AND TUTORIALS:

- Empirically Successful Classical Automated Reasoning (ESCAR)
  Geoff Sutcliffe, Stephan Schulz, and Bernd Fischer

- Workshop on Disproving: Non-Theorems, Non-Validity, Non-Provability
  Wolfgang Ahrendt, Peter Baumgartner and Hans de Nivelle

-  Empirically Successful Classical Automated Reasoning (ESCAR)
   Geoff Sutcliffe, Stephan Schulz, and Bernd Fischer

- Constraints in Formal Verification 2005 (CFV'05).
  Joao Marques-Silva, Miroslav Velev

- Tutorial: Integrating Object-Oriented Design and
             Deductive Verification of Software
  Wolfgang Ahrendt, Bernhard Beckert, Reiner Haehnle, Peter Schmitt

---------------------------------------------------------------------

   Organizing Chair:                 Tanel Tammet (Tallinn TU)
   Workshop and Tutorial Chair:      Frank Pfenning (CMU)
   Program Chair:                    Robert Nieuwenhuis (UPC Barcelona)
   Publicity Chair:                  Brigitte Pientka (McGill)

--------------------------------------------------------------------