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: |