8. LPAR 2001: Havana, Cuba

Invited Talk

• Ian M. Hodkinson, Frank Wolter, Michael Zakharyaschev:
  Monodic fragments of first-order temporal logics: 2000-2001 A.D. 1-23
  

Verification

• Orna Kupferman, Moshe Y. Vardi:
  On Bounded Specifications. 24-38
  
• Klaus Schneider:
  Improving Automata Generation for Linear Temporal Logic by Considering the Automaton Hierarchy. 39-54
  
• Volker Diekert, Paul Gastin:
  Local Temporal Logic is Expressively Complete for Cograph Dependence Alphabets. 55-69
  

Guarded Logics

• Dietmar Berwanger, Erich Grädel:
  Games and Model Checking for Guarded Logics. 70-84
  
• Lilia Georgieva, Ullrich Hustadt, Renate A. Schmidt:
  Computational Space Efficiency and Minimal Model Generation for Guarded Formulae. 85-99
  

Agents

• Natasha Alechina, Brian Logan:
  Logical Omniscience and the Cost of Deliberation. 100-109
  
• Sebastian Sardiña:
  Local Conditional High-Level Robot Programs. 110-124
  
• Kai Engelhardt, Ron van der Meyden, Yoram Moses:
  A Refinement Theory that Supports Reasoning About Knowledge and Time. 125-141
  

Automated Theorem Proving

• Reinhold Letz, Gernot Stenz:
  Automated Theorem Proving Proof and Model Generation with Disconnection Tableaux. 142-156
  
• Joseph D. Horton:
  Counting the Number of Equivalent Binary Resolution Proofs. 157-171
  

Automated Theorem Proving

• Hans de Nivelle:
  Splitting Through New Proposition Symbols. 172-185
  
• Christopher Lynch, Barbara Morawska:
  Complexity of Linear Standard Theories. 186-200
  
• Matthias Baaz, Agata Ciabattoni, Christian G. Fermüller:
  Herbrand's Theorem for Prenex Gödel Logic and its Consequences for Theorem Proving. 201-215
  

Non-Classical logics

• Franz Baader, Ralf Küsters:
  Unification in a Description Logic with Transitive Closure of Roles. 217-232
  
• Guy Perrier:
  Intuitionistic Multiplicative Proof Nets as Models of Directed Acyclic Graph Descriptions. 233-248
  

Types

• Yong Luo, Zhaohui Luo:
  Coherence and Transitivity in Coercive Subtyping. 249-265
  
• Carsten Schürmann:
  A Type-Theoretic Approach to Induction with Higher-Order Encodings. 266-281
  
• Jan-Georg Smaus:
  Analysis of Polymorphically Typed Logic Programs Using ACI-Unification. 282-298
  

Experimental Papers

• Miyuki Koshimura, Hiroshi Fujita, Ryuzo Hasegawa:
  Model Generation with Boolean Constraints. 299-308
  
• Bijan Afshordel, Thomas Hillenbrand, Christoph Weidenbach:
  First-Order Atom Definitions Extended. 309-319
  
• Thomas Marthedal Rasmussen:
  Automated Proof Support for Interval Logics. 320-329
  

Foundations of Logic

• Daniel Leivant:
  The Functions Provable by First Order Abstraction. 330-346
  
• Kai Brünnler, Alwen Fernanto Tiu:
  A Local System for Classical Logic. 347-361
  

CSP and SAT

• Jussi Rintanen:
  Partial Implicit Unfolding in the Davis-Putnam Procedure for Quantified Boolean Formulae. 362-376
  
• Toby Walsh:
  Permutation Problems and Channelling Constraints. 377-391
  
• Alvaro del Val:
  Simplifying Binary Propositional Theories into Connected Components Twice as Fast. 392-406
  

Non-monotonic Reasoning

• Thomas Eiter, Michael Fink, Giuliana Sabbatini, Hans Tompits:
  Reasoning about Evolving Nonmonotonic Knowledge Bases. 407-421
  
• Andreas Behrend:
  Efficient Computation of the Well-Founded Model Using Update Propagation. 422-437
  

Semantics

• Gianluca Amato, James Lipton:
  Indexed Categories and Bottom-Up Semantics of Logic Programs. 438-454
  
• Francisco Javier López-Fraguas, Jaime Sánchez-Hernández:
  Functional Logic Programming with Failure: A Set-Oriented View. 455-469
  
• Stephan Kreutzer:
  Operational Semantics for Fixed-Point Logics on Constraint Databases. 470-484
  

Experimental Papers

• Susana Muñoz-Hernández, Juan José Moreno-Navarro, Manuel V. Hermenegildo:
  Efficient Negation Using Abstract Interpretation. 485-494
  
• Sylvain Boulmé, Grégoire Hamon:
  Certifying Synchrony for Free. 495-506
  
• David McMath, Marianna Rozenfeld, Richard Sommer:
  A Computer Environment for Writing Ordinary Mathematical Proofs. 507-516
  

Termination

• Alexander Serebrenik, Danny De Schreye:
  On Termination of Meta-Programs. 517-530
  
• Cristina Borralleras, Albert Rubio:
  A Monotonic Higher-Order Semantic Path Ordering. 531-547
  

Knowledge-Based Systems

• Robert Baumgartner, Sergio Flesca, Georg Gottlob:
  The Elog Web Extraction Language. 548-560
  
• Enrico Franconi, Antonio Laureti Palma, Nicola Leone, Simona Perri, Francesco Scarcello:
  Census Data Repair: a Challenging Application of Disjunctive Logic Programming. 561-578
  

Analysis of Logic Programs

• Roberto Bagnara, Enea Zaffanella, Roberta Gori, Patricia M. Hill:
  Boolean Functions for Finite-Tree Dependencies. 579-594
  
• Marco Comini, Roberta Gori, Giorgio Levi:
  How to Transform an Analyzer into a Verifier. 595-609
  
• Rong Yang, Steve Gregory:
  Andorra Model Revised: Introducing Nested Domain Variables and a Targeted Search. 610-623
  

Databases and Knowledge Bases

• Ofer Arieli, Bert Van Nuffelen, Marc Denecker, Maurice Bruynooghe:
  Coherent Composition of Distributed Knowledge-Bases Through Abduction. 624-638
  
• Christian G. Fermüller, Georg Moser, Richard Zach:
  Tableaux for Reasoning About Atomic Updates. 639-653
  

Termination

• Alexander Serebrenik, Danny De Schreye:
  Inference of Termination Conditions for Numerical Loops in Prolog. 654-668
  
• Salvador Lucas:
  Termination of Rewriting With Strategy Annotations. 669-684
  
• Samir Genaim, Michael Codish:
  Inferring Termination Conditions for Logic Programs Using Backwards Analysis. 685-694
  

Program Analysis and Proof Planning

• Thomas Genet, Valérie Viet Triem Tong:
  Reachability Analysis of Term Rewriting Systems with Timbuk. 695-706
  
• Wim Vanhoof, Maurice Bruynooghe:
  Binding-Time Annotations Without Binding-Time Analysis. 707-722
  
• Raul Monroy:
  Concept Formation via Proof Planning Failure. 723-736