| Description Logics and Semantic Web / Session 1： |
| Reasoning with Expressive Description Logics: Theory and Practice / Ian Horrocks |
| BDD-Based Decision Procedures for <$>{\cal K}<$> / Guoqiang Pan ; Ulrike Sattler ; Moshe Y. Vardi |
| Proof-Carrying Code and Compiler Verification / Session 2： |
| Temporal Logic for Proof-Carrying Code / Andrew Bernard ; Peter Lee |
| A Gradual Approach to a More Trustworthy, Yet Scalable, Proof-Carrying Code / Robert R. Schneck ; George C. Necula |
| Formal Verification of a Java Compiler in Isabelle / Martin Strecker |
| Non-classical Logics / Session 3： |
| Embedding Lax Logic into Intuitionistic Logic / Uwe Egly |
| Combining Proof-Search and Counter-Model Construction for Deciding Gödel-Dummett Logic / Dominique Larchey-Wendling |
| Connection-Based Proof Search in Propositional BI Logic / Didier Galmiche ; Daniel Méry |
| System Descriptions / Session 4： |
| DDDLIB: A Library for Solving Quantified Difference Inequalities / Jesper B. Møller |
| An LCF-Style Interface between HOL and First-Order Logic / Joe Hurd |
| System Description: The MathWeb Software Bus for Distributed Mathematical Reasoning / Jürgen Zimmer ; Michael Kohlhase |
| Proof Development with ΩMEGA / Jörg Siekmann ; Christoph Benzmüller ; Vladimir Brezhnev ; Lassaad Cheikhrouhou ; Armin Fiedler ; Andreas Franke ; Helmut Horacek ; Andreas Meier ; Erica Melis ; Markus Moschner ; Immanuel Normann ; Martin Pollet ; Volker Sorge ; Carsten Ullrich ; Claus-Peter Wirth ; Juörgen Zimmer |
| LearnΩmatic: System Description / Mateja Jamnik ; Manfred Kerber |
| HyLoRes 1.0: Direct Resolution for Hybrid Logics / Carlos Areces ; Juan Heguiabehere |
| SAT / Session 5： |
| Testing Satisfiability of CNF Formulas by Computing a Stable Set of Points / Eugene Goldberg |
| A Note on Symmetry Heuristics in SEM / Thierry Boy de la Tour |
| A SAT Based Approach for Solving Formulas over Boolean and Linear Mathematical Propositions / Gilles Audemard ; Piergiorgio Bertoli ; Alessandro Cimatti ; Artur Kornilowicz ; Roberto Sebastiani |
| Model Generation / Session 6： |
| Deductive Search for Errors in Free Data Type Specifications Using Model Generation / Wolfgang Ahrendt |
| Reasoning by Symmetry and Function Ordering in Finite Model Generation / Belaid Benhamou |
| Algorithmic Aspects of Herbrand Models Represented by Ground Atoms with Ground Equations / Bernhard Gramlich ; Reinhard Pichler |
| A New Clausal Class Decidable by Hyperresolution / Lilia Georgieva ; Ullrich Hustadt ; Renate A. SchmidtSession 7： |
| CASC / Session 8： |
| Spass Version 2.0 / Christoph Weidenbach ; Uwe Brahm ; Thomas Hillenbrand ; Enno Keen ; Christian Theobald ; Dalibor Topić |
| System Description: GrAnDe 1.0 / Stephan Schulz ; Geoff Sutcliffe |
| The HR Program for Theorem Generation / Simon Colton |
| AutoBayes/CC - Combining Program Synthesis with Automatic Code Certification - System Description - / Michael Whalen ; Johann Schumann ; Bernd Fischer |
| CADE-CAV Invited Talk |
| The Quest for Efficient Boolean Satisfiability Solvers / Lintao Zhang ; Sharad Malik |
| Recursive Path Orderings Can Be Context-Sensitive / Cristina Borralleras ; Salvador Lucas ; Albert RubioSession 9： |
| Combination of Decision Procedures / Session 10： |
| Shostak Light / Harald Ganzinger |
| Formal Verification of a Combination Decision Procedure / Jonathan Ford ; Natarajan Shankar |
| Combining Multisets with Integers / Calogero G. Zarba |
| Logical Frameworks / Session 11： |
| The Reflection Theorem: A Study in Meta-theoretic Reasoning / Lawrence C. Paulson |
| Faster Proof Checking in the Edinburgh Logical Framework / Aaron Stump ; David L. Dill |
| Solving for Set Variables in Higher-Order Theorem Proving / Chad E. Brown |
| Model Checking / Session 12： |
| The Complexity of the Graded μ-Calculus / Orna Kupferman |
| Lazy Theorem Proving for Bounded Model Checking over Infinite Domains / Leonardo de Moura ; Harald Rueß ; Maria Sorea |
| Equational Reasoning / Session 13： |
| Well-Foundedness Is Sufficient for Completeness of Ordered Paramodulation / Miquel Bofill |
| Basic Syntactic Mutation / Christopher Lynch ; Barbara Morawska |
| The Next Waldmeister Loop / Bernd Lochner |
| Proof Theory / Session 14： |
| Focussing Proof-Net Construction as a Middleware Paradigm / Jean Marc Andreoli |
| Proof Analysis by Resolution / Matthias Baaz |
| Author Index |
| Description Logics and Semantic Web / Session 1： |
| Reasoning with Expressive Description Logics: Theory and Practice / Ian Horrocks |
| BDD-Based Decision Procedures for <$>{\cal K}<$> / Guoqiang Pan ; Ulrike Sattler ; Moshe Y. Vardi |
図書
