Logic for Programming, Artificial Intelligence, and Reasoning: 8th International Conference, LPAR 2001, Havana, Cuba, December 3-7, 2001, Proceedings

Front Cover
Robert Nieuwenhuis, Andrei Voronkov
Springer Science & Business Media, Nov 21, 2001 - Computers - 741 pages
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
Author Index
737
Copyright

Other editions - View all

Common terms and phrases

Bibliographic information