Vol-556 Copyright © 2009 for the individual papers by the papers' authors. Copying permitted for private and academic purposes. Re-publication of material from this volume requires permission by the copyright owners. This volume is published by its editors.

---

FTP 2009
First-Order Theorem Proving

Proceedings of the 7th International Workshop on First-Order Theorem Proving ( FTP'09 )

Oslo, Norway, July 6-7, 2009.

Nicolas Peltier *
Viorica Sofronie-Stokkermans **

Table of Contents

Foreword

1. Preface
   Nicolas Peltier, Viorica Sofronie-Stokkermans , pages i-i

   Invited papers

2. Model-Checking of Array-Based Systems: from Foundations to Implementation
   Silvio Ghilardi , pages 1-2
3. Presenting Constraints
   Peter Jeavons , pages 3-3

   Contributed Papers

4. Constraint Modelling: A Challenge for First Order Automated Reasoning
   Peter Baumgartner, John Slaney , pages 4-18
5. Toward an Efficient Equality Computation in Connection Tableaux: A Modification Method without Symmetry Transformation
   Koji Iwanuma, Hidetomo Nabeshima, Katsumi Inoue , pages 19-33
6. Redundancy Elimination in Monodic Temporal Reasoning
   Michel Ludwig, Ullrich Hustadt , pages 34-48
7. Minimal Model Generation with Respect to an Atom Set
   Miyuki Koshimura, Hidetomo Nabeshima, Hiroshi Fujita, Ryuzo Hasegawa , pages 49-59
8. Literal Projection and Circumscription
   Christoph Wernhard , pages 60-74
9. Inductive Reasoning for Shape Invariants
   Lilia Georgieva, Patrick Maier , pages 75-89
10. Analysis of Authorizations in SAP R/3
    Manuel Lamotte-Schubert, Christoph Weidenbach , pages 90-104
11. Towards the Verification of Security-Aware Transaction E-services
    Silvio Ranise , pages 105-119

    Position papers

12. A Fixed Point Representation of References
    Susumu Yamasaki , pages 120-129
13. Static Types As Search Heuristics
    Hao Xu , pages 130-139