| Invited Talk / Session 1： |
| Monodic Fragments of First-Order Temporal Logics: 2000-2001 A.D / Ian Hodkinson ; Frank Wolter ; Michael Zakharyaschev |
| Verification / Session 2： |
| On Bounded Specifications / Orna Kupferman ; Moshe Y. Vardi |
| Improving Automata Generation for Linear Temporal Logic by Considering the Automaton Hierarchy / Klaus Schneider |
| Local Temporal Logic Is Expressively Complete for Cograph Dependence Alphabets / Volker Diekert ; Paul Gastin |
| Guarded Logics / Session 3： |
| Games and Model Checking for Guarded Logics / Dietmar Berwanger ; Erich Grädel |
| Computational Space Efficiency and Minimal Model Generation for Guarded Formulae / Lilia Georgieva ; Ullrich Hustadt ; Renate A. Schmidt |
| Agents / Session 4： |
| Local Conditional High-Level Robot Programs / Natasha Alechina ; Brian Logan ; Sebastian SardiñaLogical Omniscience and the Cost of Deliberation： |
| A Refinement Theory That Supports Reasoning about Knowledge and Time for Synchronous Agents / Kai Engelhardt ; Ron van der Meyden ; Yoram Moses |
| Automated Theorem Proving / Session 5： |
| Proof and Model Generation with Disconnection Tableaux / Reinhold Letz ; Gernot Stenz |
| Counting the Number of Equivalent Binary Resolution Proofs / Joseph D. Horton |
| Splitting through New Proposition Symbols / Hans de NivelleSession 6： |
| Complexity of Linear Standard Theories / Christopher Lynch ; Barbara Morawska |
| Herbrand's Theorem for Prenex Gödel Logic and Its Consequences for Theorem Proving / Matthias Baaz ; Agata Ciabattoni ; Christian G. Fermüller |
| Non-classical Logics / Session 7： |
| Unification in a Description Logic with Transitive Closure of Roles / Franz Baader ; Ralf Küsters |
| Intuitionistic Multiplicative Proof Nets as Models of Directed Acyclic Graph Descriptions / Guy Perrier |
| Types / Session 8： |
| Coherence and Transitivity in Coercive Subtyping / Yong Luo ; Zhaohui Luo |
| A Type-Theoretic Approach to Induction with Higher-Order Encodings / Carsten Schürmann |
| Analysis of Polymorphically Typed Logic Programs Using ACI-Unification / Jan-Georg Smaus |
| Experimental Papers / Session 9： |
| First-Order Atom Definitions Extended / Miyuki Koshimura ; Hiroshi Fujita ; Ryuzo Hasegawa ; Bijan Afshordel ; Thomas Hillenbrand ; Christoph WeidenbachModel Generation with Boolean Constraints： |
| Automated Proof Support for Interval Logics / Thomas Marthedal Rasmussen |
| Foundations of Logic / Session 10： |
| The Functions Provable by First Order Abstraction / Daniel Leivant |
| A Local System for Classical Logic / Kai Brunnler ; Alwen Fernanto Tiu |
| CSP and SAT / Session 11： |
| Partial Implicit Unfolding in the Davis-Putnam Procedure for Quantified Boolean Formulae / Jussi Rintanen |
| Permutation Problems and Channelling Constraints / Toby Walsh |
| Simplifying Binary Propositional Theories into Connected Components Twice as Fast / Alvaro del Val |
| Non-monotonic Reasoning / Session 12： |
| Reasoning about Evolving Nonmonotonic Knowledge Bases / Thomas Eiter ; Michael Fink ; Giuliana Sabbatini ; Hans Tompits |
| Efficient Computation of the Well-Founded Model Using Update Propagation / Andreas Behrend |
| Semantics / Session 13： |
| Indexed Categories and Bottom-Up Semantics of Logic Programs / Gianluca Amato ; James Lipton |
| Functional Logic Programming with Failure: A Set-Oriented View / F.J. Lopez-Fraguas ; J. Sanchez-Hernandez |
| Operational Semantics for Fixed-Point Logics on Constraint Databases / Stephan Kreutzer |
| Efficient Negation Using Abstract Interpretation / Susana Muñoz ; Juan José Moreno ; Manuel HermenegildoSession 14： |
| Certifying Synchrony for Free / Sylvain Boulmé ; Grégoire Hamon |
| A Computer Environment for Writing Ordinary Mathematical Proofs / David McMath ; Marianna Rozenfeld ; Richard Sommer |
| Termination / Session 15： |
| On Termination of Meta-programs / Alexander Serebrenik ; Danny De Schreye |
| A Monotonic Higher-Order Semantic Path Ordering / Cristina Borralleras ; Albert Rubio |
| Knowledge-Based Systems / Session 16： |
| The Elog Web Extraction Language / Robert Baumgartner ; Sergio Flesca ; Georg Gottlob |
| Census Data Repair: A Challenging Application of Disjunctive Logic Programming / Enrico Franconi ; Antonio Laureti Palma ; Nicola Leone ; Simona Perri ; Francesco Scarcello |
| Analysis of Logic Programs / Session 17： |
| Boolean Functions for Finite-Tree Dependencies / Roberto Bagnara ; Enea Zaffanella ; Roberta Gori ; Patricia M. Hill |
| How to Transform an Analyzer into a Verifier / Marco Comini ; Giorgio Levi |
| Andorra Model Revised: Introducing Nested Domain Variables and a Targeted Search / Rong Yang ; Steve Gregory |
| Databases and Knowledge Bases / Session 18： |
| Coherent Composition of Distributed Knowledge-Bases through Abduction / Ofer Arieli ; Bert Van Nuffelen ; Marc Denecker ; Maurice Bruynooghe |
| Tableaux for Reasoning about Atomic Updates / Georg Moser ; Richard Zach |
| Inference of Termination Conditions for Numerical Loops in Prolog / Session 19： |
| Termination of Rewriting with Strategy Annotations / Salvador Lucas |
| Inferring Termination Conditions for Logic Programs Using Backwards Analysis / Samir Genaim ; Michael Codish |
| Program Analysis and Proof Planning / Session 20： |
| Reachability Analysis of Term Rewriting Systems with Timbuk / Thomas Genet ; Valerie Viet Triem Tong |
| Binding-Time Annotations without Binding-Time Analysis / Wim Vanhoof |
| Concept Formation via Proof Planning Failure / Raúl Monroy |
| Author Index |
| Invited Talk / Session 1： |
| Monodic Fragments of First-Order Temporal Logics: 2000-2001 A.D / Ian Hodkinson ; Frank Wolter ; Michael Zakharyaschev |
| Verification / Session 2： |
図書
