## Logic for Programming, Artificial Intelligence, and Reasoning: 8th International Conference, LPAR 2001, Havana, Cuba, December 3-7, 2001, ProceedingsRobert Nieuwenhuis, Andrei Voronkov This volume contains the papers presented at the Eighth International C- ference on Logic for Programming, Arti?cial Intelligence and Reasoning (LPAR 2001), held on December 3-7, 2001, at the University of Havana (Cuba), together with the Second International Workshop on Implementation of Logics. There were 112 submissions, of which 19 belonged to the special subm- sion category of experimental papers, intended to describe implementations or comparisons of systems, or experiments with systems. Each submission was - viewed by at least three program committee members and an electronic program committee meeting was held via the Internet. The high number of submissions caused a large amount of work, and we are very grateful to the other 31 PC members for their e?ciency and for the quality of their reviews and discussions. Finally, the committee decided to accept 40papers in the theoretical ca- gory, and 9 experimental papers. In addition to the refereed papers, this volume contains an extended abstract of the invited talk by Frank Wolter. Two other invited lectures were given by Matthias Baaz and Manuel Hermenegildo. Apart from the program committee, we would also like to thank the other people who made LPAR 2001 possible: the additional referees; the Local Arran- ` gements Chair Luciano Garc ́?a; Andr ́es Navarro and Oscar Guell, ̈ who ran the internet-based submission software and the program committee discussion so- ware at the LSI Department lab in Barcelona; and Bill McCune, whose program committee management software was used. |

### What people are saying - Write a review

We haven't found any reviews in the usual places.

### Contents

20002001 AD | 1 |

On Bounded Specifications | 24 |

Improving Automata Generation for Linear Temporal Logic by Considering the Automaton Hierarchy | 39 |

Local Temporal Logic Is Expressively Complete for Cograph Dependence Alphabets | 55 |

Games and Model Checking for Guarded Logics | 70 |

Computational Space Efficiency and Minimal Model Generation for Guarded Formulae | 85 |

Logical Omniscience and the Cost of Deliberation | 100 |

Local Conditional HighLevel Robot Programs | 110 |

Simplifying Binary Propositional Theories into Connected Components Twice as Fast | 392 |

Reasoning about Evolving Nonmonotonic Knowledge Bases | 407 |

Efficient Computation of the WellFounded Model Using Update Propagation | 422 |

Indexed Categories and BottomUp Semantics of Logic Programs | 438 |

A SetOriented View | 455 |

Operational Semantics for FixedPoint Logics on Constraint Databases | 470 |

Efficient Negation Using Abstract Interpretation | 485 |

Certifying Synchrony for Free | 495 |

A Refinement Theory that Supports Reasoning about Knowledge and Time for Synchronous Agents | 125 |

Proof and Model Generation with Disconnection Tableaux | 142 |

Counting the Number of Equivalent Binary Resolution Proofs | 157 |

Splitting through New Proposition Symbols | 172 |

Complexity of Linear Standard Theories | 186 |

Herbrands Theorem for Prenex Godel Logic and Its Consequences for Theorem Proving | 201 |

Unification in a Description Logic with Transitive Closure of Roles | 217 |

Intuitionistic Multiplicative Proof Nets as Models of Directed Acyclic Graph Descriptions | 233 |

Coherence and Transitivity in Coercive Subtyping | 249 |

A TypeTheoretic Approach to Induction with HigherOrder Encodings | 266 |

Analysis of Polymorphically Typed Logic Programs Using ACIUnification | 282 |

Model Generation with Boolean Constraints | 299 |

FirstOrder Atom Definitions Extended | 309 |

Automated Proof Support for Interval Logics | 320 |

The Functions Provable by First Order Abstraction | 330 |

A Local System for Classical Logic | 347 |

Partial Implicit Unfolding in the DavisPutnam Procedure for Quantified Boolean Formulae | 362 |

Permutation Problems and Channelling Constraints | 377 |

A Computer Environment for Writing Ordinary Mathematical Proofs | 507 |

On Termination of Metaprograms | 517 |

A Monotonic HigherOrder Semantic Path Ordering | 531 |

The Elog Web Extraction Language | 548 |

A Challenging Application of Disjunctive Logic Programming | 561 |

Boolean Functions for FiniteTree Dependencies | 579 |

How to Transform an Analyzer into a Verifier | 595 |

Introducing Nested Domain Variables and a Targeted Search | 610 |

Coherent Composition of Distributed KnowledgeBases through Abduction | 624 |

Tableaux for Reasoning about Atomic Updates | 639 |

Inference of Termination Conditions for Numerical Loops in Prolog | 654 |

Termination of Rewriting with Strategy Annotations | 669 |

Inferring Termination Conditions for Logic Programs Using Backwards Analysis | 685 |

Reachability Analysis of Term Rewriting Systems with Timbuk | 695 |

BindingTime Annotations without BindingTime Analysis | 707 |

Concept Formation via Proof Planning Failure | 723 |

737 | |

### Other editions - View all

Logic for Programming, Artificial Intelligence, and Reasoning: 8th ... Robert Nieuwenhuis,Andrei Voronkov No preview available - 2001 |

Logic for Programming, Artificial Intelligence, and Reasoning: 8th ... Robert Nieuwenhuis,Andrei Voronkov No preview available - 2001 |

### Common terms and phrases

abstract abstract interpretation algorithm analysis applied Artificial Intelligence atom automata automaton binary Boolean branch calculus called clause tree clopen cograph complete Computer Science condition consider constraints construction corresponding database defined definition denote derivation description logics domain encoding equation equivalent evaluation example finite first-order first-order logic fixpoint formal formula framework function given goal Herbrand higher-order implementation induction inference instantiation International interpretation language Lemma linear literals LNAI LNCS Logic Programming LPAR meta-interpreter modal modal logics model checking negation node obtained operational semantics operator parity game permutation problem predicate Proc procedure Prolog proof proof net properties propositional prove query recursive relation respect restricted rewriting rules semantics sequence sequent calculus Springer-Verlag strategy structure symbols syntactic tableau temporal logic termination termination analysis Theorem theory transition tuple update variables Voronkov