| Invited Talk | |
| Monodic Fragments of First-Order Temporal Logics: 2000-2001 A.D | p. 1 |
| Verification | |
| On Bounded Specifications | p. 24 |
| Improving Automata Generation for Linear Temporal Logic by Considering the Automaton Hierarchy | p. 39 |
| Local Temporal Logic Is Expressively Complete for Cograph Dependence Alphabets | p. 55 |
| Guarded Logics | |
| Games and Model Checking for Guarded Logics | p. 70 |
| Computational Space Efficiency and Minimal Model Generation for Guarded Formulae | p. 85 |
| Agents | |
| p. 100 |
| Local Conditional High-Level Robot Programs | p. 110 |
| A Refinement Theory That Supports Reasoning about Knowledge and Time for Synchronous Agents | p. 125 |
| Automated Theorem Proving | |
| Proof and Model Generation with Disconnection Tableaux | p. 142 |
| Counting the Number of Equivalent Binary Resolution Proofs | p. 157 |
| Automated Theorem Proving | |
| Splitting through New Proposition Symbols | p. 172 |
| Complexity of Linear Standard Theories | p. 186 |
| Herbrand's Theorem for Prenex Gödel Logic and Its Consequences for Theorem Proving | p. 201 |
| Non-classical Logics | |
| Unification in a Description Logic with Transitive Closure of Roles | p. 217 |
| Intuitionistic Multiplicative Proof Nets as Models of Directed Acyclic Graph Descriptions | p. 233 |
| Types | |
| Coherence and Transitivity in Coercive Subtyping | p. 249 |
| A Type-Theoretic Approach to Induction with Higher-Order Encodings | p. 266 |
| Analysis of Polymorphically Typed Logic Programs Using ACI-Unification | p. 282 |
| Experimental Papers | |
| p. 299 |
| First-Order Atom Definitions Extended | p. 309 |
| Automated Proof Support for Interval Logics | p. 320 |
| Foundations of Logic | |
| The Functions Provable by First Order Abstraction | p. 330 |
| A Local System for Classical Logic | p. 347 |
| CSP and SAT | |
| Partial Implicit Unfolding in the Davis-Putnam Procedure for Quantified Boolean Formulae | p. 362 |
| Permutation Problems and Channelling Constraints | p. 377 |
| Simplifying Binary Propositional Theories into Connected Components Twice as Fast | p. 392 |
| Non-monotonic Reasoning | |
| Reasoning about Evolving Nonmonotonic Knowledge Bases | p. 407 |
| Efficient Computation of the Well-Founded Model Using Update Propagation | p. 422 |
| Semantics | |
| Indexed Categories and Bottom-Up Semantics of Logic Programs | p. 438 |
| Functional Logic Programming with Failure: A Set-Oriented View | p. 455 |
| Operational Semantics for Fixed-Point Logics on Constraint Databases | p. 470 |
| Experimental Papers | |
| Efficient Negation Using Abstract Interpretation | p. 485 |
| Certifying Synchrony for Free | p. 495 |
| A Computer Environment for Writing Ordinary Mathematical Proofs | p. 507 |
| Termination | |
| On Termination of Meta-programs | p. 517 |
| A Monotonic Higher-Order Semantic Path Ordering | p. 531 |
| Knowledge-Based Systems | |
| The Elog Web Extraction Language | p. 548 |
| Census Data Repair: A Challenging Application of Disjunctive Logic Programming | p. 561 |
| Analysis of Logic Programs | |
| Boolean Functions for Finite-Tree Dependencies | p. 579 |
| How to Transform an Analyzer into a Verifier | p. 595 |
| Andorra Model Revised: Introducing Nested Domain Variables and a Targeted Search | p. 610 |
| Databases and Knowledge Bases | |
| Coherent Composition of Distributed Knowledge-Bases through Abduction | p. 624 |
| Tableaux for Reasoning about Atomic Updates | p. 639 |
| Termination | |
| Inference of Termination Conditions for Numerical Loops in Prolog | p. 654 |
| Termination of Rewriting with Strategy Annotations | p. 669 |
| Inferring Termination Conditions for Logic Programs Using Backwards Analysis | p. 685 |
| Program Analysis and Proof Planning | |
| Reachability Analysis of Term Rewriting Systems with Timbuk | p. 695 |
| Binding-Time Annotations without Binding-Time Analysis | p. 707 |
| Concept Formation via Proof Planning Failure | p. 723 |
| Author Index | p. 737 |
| Table of Contents provided by Publisher. All Rights Reserved. |