20. CADE 2005: Tallinn, Estonia

• Gilles Dowek:
  What Do We Know When We Know That a Theory Is Consistent?. 1-6
  
• Evelyne Contejean, Pierre Corbineau:
  Reflecting Proofs in First-Order Logic with Equality. 7-22
  
• Chad E. Brown:
  Reasoning in Extensional Type Theory with Equality. 23-37
  
• Christian Urban, Christine Tasson:
  Nominal Techniques in Isabelle/HOL. 38-53
  
• Brigitte Pientka:
  Tabling for Higher-Order Logic Programming. 54-68
  
• Kaustuv Chaudhuri, Frank Pfenning:
  A Focusing Inverse Method Theorem Prover for First-Order Linear Logic. 69-83
  
• Serge Autexier:
  The CoRe Calculus. 84-98
  
• Tal Lev-Ami, Neil Immerman, Thomas W. Reps, Shmuel Sagiv, S. Srivastava, Greta Yorsh:
  Simulating Reachability Using First-Order Logic with Applications to Verification of Linked Data Structures. 99-115
  
• Guillaume Dufay, Amy P. Felty, Stan Matwin:
  Privacy-Sensitive Information Flow with JML. 116-130
  
• Ting Zhang, Henny B. Sipma, Zohar Manna:
  The Decidability of the First-Order Theory of Knuth-Bendix Order. 131-148
  
• Jordi Levy, Joachim Niehren, Mateu Villaret:
  Well-Nested Context Unification. 149-163
  
• Guillem Godoy, Ashish Tiwari:
  Termination of Rewrite Systems with Shallow Right-Linear, Collapsing, and Right-Ground Rules. 164-176
  
• Sean Bechhofer, Ian Horrocks, Daniele Turi:
  The OWL Instance Store: System Description. 177-181
  
• Boris Konev, Frank Wolter, Michael Zakharyaschev:
  Temporal Logics over Transitive States. 182-203
  
• Ullrich Hustadt, Boris Konev, Renate A. Schmidt:
  Deciding Monodic Fragments by Temporal Resolution. 204-218
  
• Viorica Sofronie-Stokkermans:
  Hierarchic Reasoning in Local Theory Extensions. 219-234
  
• Claudio Castellini, Alan Smaill:
  Proof Planning for First-Order Temporal Logic. 235-249
  
• Andreas Meier, Erica Melis:
  System Description: Multi A Multi-strategy Proof Planner. 250-254
  
• Randal E. Bryant, Sanjit A. Seshia:
  Decision Procedures Customized for Formal Verification. 255-259
  
• Viktor Kuncak, Huu Hai Nguyen, Martin C. Rinard:
  An Algorithm for Deciding BAPA: Boolean Algebra with Presburger Arithmetic. 260-277
  
• Franz Baader, Silvio Ghilardi:
  Connecting Many-Sorted Theories. 278-294
  
• Sean McLaughlin, John Harrison:
  A Proof-Producing Decision Procedure for Real Arithmetic. 295-314
  
• Marco Bozzano, Roberto Bruttomesso, Alessandro Cimatti, Tommi A. Junttila, Peter van Rossum, Stephan Schulz, Roberto Sebastiani:
  The MathSAT 3 System. 315-321
  
• Graham Steel:
  Deduction with XOR Constraints in Security API Modelling. 322-336
  
• Kumar Neeraj Verma, Helmut Seidl, Thomas Schwentick:
  On the Complexity of Equational Horn Clauses. 337-352
  
• Greta Yorsh, Madanlal Musuvathi:
  A Combination Method for Generating Interpolants. 353-368
  
• Marco Benedetti:
  sKizzo: A Suite to Evaluate and Certify QBFs. 369-376
  
• Tomasz Truderung:
  Regular Protocols and Attacks with Regular Knowledge. 377-391
  
• Peter Baumgartner, Cesare Tinelli:
  The Model Evolution Calculus with Equality. 392-408
  
• Christian G. Fermüller, Reinhard Pichler:
  Model Representation via Contexts and Implicit Generalizations. 409-423
  
• Mizuhito Ogawa, Eiichi Horita, Satoshi Ono:
  Proving Properties of Incremental Merkle Trees. 424-440
  
• Jian Zhang:
  Computer Search for Counterexamples to Wilkie's Identity. 441-451
  
• Alex Sinner, Thomas Kleemann:
  KRHyper - In Your Pocket. 452-457