Logic for Programming, Artificial Intelligence, and Reasoning : 8th International Conference, LPAR 2001, Havana, Cuba, December 3-7, 2001, Proceedings / edited by Robert Nieuwenhuis, Andrei Voronkov.

Format:

Book

Contributor:

Nieuwenhuis, Robert, editor.

Voronkov, Andrei, 1959- editor.

SpringerLink (Online service)

Series:

Computer Science (Springer-11645)

Lecture notes in computer science. Lecture notes in artificial intelligence ; 2250.

Lecture Notes in Artificial Intelligence ; 2250

Language:

English

Subjects (All):

Artificial intelligence.

Software engineering.

Computer logic.

Logic, Symbolic and mathematical.

Artificial Intelligence.

Software Engineering/Programming and Operating Systems.

Logics and Meanings of Programs.

Software Engineering.

Mathematical Logic and Formal Languages.

Local Subjects:

Artificial Intelligence.

Software Engineering/Programming and Operating Systems.

Logics and Meanings of Programs.

Software Engineering.

Mathematical Logic and Formal Languages.

Physical Description:

1 online resource (XV, 741 pages).

Edition:

First edition 2001.

Contained In:

Springer eBooks

Place of Publication:

Berlin, Heidelberg : Springer Berlin Heidelberg : Imprint: Springer, 2001.

System Details:

text file PDF

Summary:

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.

Contents:

Invited Talk

Monodic Fragments of First-Order Temporal Logics: 2000-2001 A.D.

Verification

On Bounded Specifications

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

Local Temporal Logic Is Expressively Complete for Cograph Dependence Alphabets

Guarded Logics

Games and Model Checking for Guarded Logics

Computational Space Efficiency and Minimal Model Generation for Guarded Formulae

Agents

Logical Omniscience and the Cost of Deliberation

Local Conditional High-Level Robot Programs

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

Automated Theorem Proving

Proof and Model Generation with Disconnection Tableaux

Counting the Number of Equivalent Binary Resolution Proofs

Splitting through New Proposition Symbols

Complexity of Linear Standard Theories

Herbrand's Theorem for Prenex Gödel Logic and Its Consequences for Theorem Proving

Non-classical Logics

Unification in a Description Logic with Transitive Closure of Roles

Intuitionistic Multiplicative Proof Nets as Models of Directed Acyclic Graph Descriptions

Types

Coherence and Transitivity in Coercive Subtyping

A Type-Theoretic Approach to Induction with Higher-Order Encodings

Analysis of Polymorphically Typed Logic Programs Using ACI-Unification

Experimental Papers

Model Generation with Boolean Constraints

First-Order Atom Definitions Extended

Automated Proof Support for Interval Logics

Foundations of Logic

The Functions Provable by First Order Abstraction

A Local System for Classical Logic

CSP and SAT

Partial Implicit Unfolding in the Davis-Putnam Procedure for Quantified Boolean Formulae

Permutation Problems and Channelling Constraints

Simplifying Binary Propositional Theories into Connected Components Twice as Fast

Non-monotonic Reasoning

Reasoning about Evolving Nonmonotonic Knowledge Bases

Efficient Computation of the Well-Founded Model Using Update Propagation

Semantics

Indexed Categories and Bottom-Up Semantics of Logic Programs

Functional Logic Programming with Failure: A Set-Oriented View

Operational Semantics for Fixed-Point Logics on Constraint Databases

Efficient Negation Using Abstract Interpretation

Certifying Synchrony for Free

A Computer Environment for Writing Ordinary Mathematical Proofs

Termination

On Termination of Meta-programs

A Monotonic Higher-Order Semantic Path Ordering

Knowledge-Based Systems

The Elog Web Extraction Language

Census Data Repair: A Challenging Application of Disjunctive Logic Programming

Analysis of Logic Programs

Boolean Functions for Finite-Tree Dependencies

How to Transform an Analyzer into a Verifier

Andorra Model Revised: Introducing Nested Domain Variables and a Targeted Search

Databases and Knowledge Bases

Coherent Composition of Distributed Knowledge-Bases through Abduction

Tableaux for Reasoning about Atomic Updates

Inference of Termination Conditions for Numerical Loops in Prolog

Termination of Rewriting with Strategy Annotations

Inferring Termination Conditions for Logic Programs Using Backwards Analysis

Program Analysis and Proof Planning

Reachability Analysis of Term Rewriting Systems with Timbuk

Binding-Time Annotations without Binding-Time Analysis

Concept Formation via Proof Planning Failure.

Other Format:

Printed edition:

ISBN:

978-3-540-45653-7

9783540456537

Access Restriction:

Restricted for use by site license.