Logic Programming: 23rd International Conference, ICLP 2007, Porto, Portugal, September 8-13, 2007, Proceedings (Lecture Notes in Computer Science, 4670)

✍ Scribed by Verónica Dahl (editor), Ilkka Niemelä (editor)

• Publisher: Springer
• Year: 2007
• Tongue: English
• Leaves: 482
• Category: Library

✦ Synopsis

This book contains the refereed proceedings of the 23rd International Conference on Logic Programming, ICLP 2007, held in Porto, Portugal. The 22 revised full papers together with two invited talks, 15 poster presentations, and the abstracts of five doctoral consortium articles cover all issues of current research in logic programming, including theory, functional and constraint logic programming, program analysis, answer-set programming, semantics, and applications.

✦ Table of Contents

Title Page
Preface
Organization
Table of Contents
Towards Overcoming the Knowledge Acquisition Bottleneck in Answer Set Prolog Applications: Embracing Natural Language Inputs
Introduction
Processing Natural Language Using C&C Tools and Boxer
C&C Tools
CCG Parser
Boxer
Obtaining the Answer Set Programs
An Application: Solving Puzzles
Facts Extraction
Clues Extraction
Other Applications
Reasoning About Travel
RTE Examples
Conclusions
Preferences, Contexts and Answer Sets
Answer Set Programming for the Semantic Web (Tutorial)
Coinductive Logic Programming and Its Applications
Introduction
Coinduction and Logic Programming
Examples
Application to Model Checking and Verification
Verifying Liveness Properties
Verifying Properties of Timed Automata
Verification of Nested Finite and Infinite Automata
Applications to Non-monotonic Reasoning
A Top-Down Algorithm for Computing Answer Sets
Correctness of the Top-Down Algorithm
Conclusions
Multi-paradigm Declarative Languages
Introduction
Foundations of Functional Logic Programming
Basic Concepts
Narrowing
Rewriting Logic
Residuation
Aspects of Multi-paradigm Languages
External Operations
Higher-Order Operations
Constraints
Function Patterns
Encapsulating Search
Implementation
Applications
Conclusions
Logic Programming for Knowledge Representation
Introduction
Modularity
Programs with Constraints
Model Expansion and ID-Logic
Tools
Closing Comments
On Finitely Recursive Programs
Introduction
Preliminaries
Module Sequences and a Normal Form for Splitting Sequences
Properties of Finitely Recursive Programs
Compactness
The Complexity of Reasoning with Finitely Recursive Programs
Skeptical Resolution for Finitely Recursive Programs
Conclusions
Minimal Logic Programs
Introduction
Quine-McCluskey Algorithm
Equilibrium Logic
Logic Programs
Generation of Prime Implicates
Examples
Entailment
Discussion and Related Work
Generic Tableaux for Answer Set Programming
Introduction
Background
Generic Tableau Rules
Conjunctive Bodies
Cardinality Constraints
Disjunctive Heads
Proof Complexity
Discussion
Extended ASP Tableaux and Rule Redundancy in Normal Logic Programs
Introduction
Preliminaries
Normal Logic Programs and Stable Models
Propositional Satisfiability
SAT as ASP
ASP as SAT
Proof Systems for ASP and SAT
Propositional Proof Systems and Complexity
Resolution
ASP Tableaux
Extended ASP Tableaux
Proof Complexity
Relationship with Extended Resolution
Pigeonhole Principle Separates Extended ASP Tableaux from ASP Tableaux
Program Simplification and Complexity
Experiments
Conclusions
Querying and Repairing Inconsistent Databases Under Three-Valued Semantics
Introduction
Contributions
Preliminaries
Databases and Integrity Constraints
Integrity Constraints
Repairing and Querying Inconsistent Databases
Deterministic Three-Valued Semantics
Deterministic Semantics
Repairing Databases
Query Answers
Rewriting into Logic Programs
Logic Programming Approach to Automata-Based Decision Procedures
Introduction
Background and Definitions
Weak Second-Order Logic (WS1S)
Datalog for Complex Values
Automata and Datalog for Complex Values
Representation of Automata
Automata-Theoretic Operations
Experimental Evaluation
Heuristics for (Large) Conjunctions of Formulas
Related Work
Conclusions and Future Work
A Logic Programming Framework for Combinational Circuit Synthesis
Introduction
Combinatorial Objects and Combinational Circuit Synthesis
Boolean Expression Trees
Implementing Finite Functions as Logical Variable Bindings
Leaf-DAG Circuit Representations for Combinational Logic
Fast Boolean Evaluation with Bitstring Truth Table Encodings
A Comparison of Universal Boolean Function Libraries
Using Strict Boolean Inequality for Combinational Circuit Synthesis
Strict Boolean Inequality as a Universal Boolean Operator
The Symbolic Rewriting Algorithm
Minimal (<,1)-Representations for Key Boolean Functions
Synthesis from CNF and DNF Forms
Transistor Implementations for (<,1)-Circuits
Related Work
Future Work
Conclusion
Spatial-Yap: A Logic-Based Geographic Information System
Introduction
Spatial Databases
A Spatial Deductive Database System
Spatial Terms
Visualization of Spatial Data with Simple Graphics
Spatial Predicates
Real-World Applications
Study of Traffic Behavior in the City of Porto
Monitoring of Biodiversity Change
Conclusions and Future Work
The Correspondence Between the Logical Algorithms Language and CHR
Introduction
Logical Algorithms and CHR^{rp}
Logical Algorithms
CHR^{rp}: CHR with Rule Priorities
Translating Logical Algorithms to CHR^{rp}
The Translation Schema
The Correspondence Between LA and CHR^{rp} Derivations
Translating CHR^{rp} Programs into Logical Algorithms
The Implementation of LA in CHR Under $omega_r$
Overview
The Compilation of LA Programs to CHR Rules
Priority Queues
The Scheduler
A Complexity Result
Conclusions
Observable Confluence for Constraint Handling Rules
Introduction
Motivating Examples
Blocks World
Union Find
Type Class Functional Dependencies
Preliminaries
Confluence
Confluence Test
$I$-Confluence
Observable Confluence
Extensions
$I$-Confluence
$I$-Confluence Test
Examples
Reachable Confluence
Simple Confluence
Ground Confluence
Conclusion
Graph Transformation Systems in CHR
Introduction
Preliminaries
Graph Transformation System (GTS)
Constraint Handling Rules (CHR)
Representation of Graphs in CHR
On Dangling Edges
Runtime Performance
Soundness and Completeness
Confluence
Preliminaries
Critical Pair Properties
Conclusion
Multivalued Action Languages with Constraints in CLP(FD)
Introduction
An Action Language
Syntax of $\mathcal B$
Semantics of $\mathcal B$
Modeling $\mathcal B$ and Planning Problems in CLP(FD)
The Action Language \mbox{$\mathcal{B}{MV}^{FD}$}
Syntax of \mbox{$\mathcal{B}{MV}^{FD}$}
Semantics of \mbox{$\mathcal{B}{MV}^{FD}$}
Some Concrete Extensions
An Extended \mbox{$\mathcal{B}{MV}^{FD}$} Language: Looking Into the Future
Experimental Analysis
Three-Barrel Problem
2-Dimensional Protein Folding Problem
Other Examples
Conclusions and Future Work
Declarative Diagnosis of Temporal Concurrent Constraint Programs
Introduction
The Language and the Semantic Framework
Constraint Systems
Process Syntax
Operational Semantics
Denotational Semantics
Abstract Semantics
A Case Study: The Domain $Sequence(k)$
Abstract Diagnosis of $ntcc$ Programs
Our Case Study
Conclusions
Logic Programs with Abstract Constraint Atoms: The Role of Computations
Introduction and Motivation
Computations in Normal Logic Programs---Principles
Programs with Abstract Constraints---Basic Definitions
Computations for Programs with Constraints
Computations and Quasi-satisfiability Relations
Yet Another Class of Answer Sets
A Note on the Complexity
Discussion and Conclusions
Resource-Oriented Deadlock Analysis
Introduction
The Dining Philosophers Problem
Process-Oriented Deadlock Analysis
Concurrent Logic Programming
Deterministic Code
Committed Choice Nondeterminism
Finding Deadlocks
Eliminating Committed Choice Nondeterminism
Eliminating Spurious Derivations
Implementing Fair Search
Discussion
Conclusion
Static Region Analysis for Mercury
Introduction
Regions and Mercury
Region Points-to Analysis
Intraprocedural Analysis
Interprocedural Analysis
Live Region Analysis
Live Region Variables at a Program Point
Region Lifetime Across Procedure Boundary
Program Transformation
Support for Mercury Programs with Backtracking
Prototype Implementation and Experimental Results
Conclusion
Automatic Binding-Related Error Diagnosis in Logic Programs
Introduction
Related Work
Preliminaries and Notation
Assertions, Symptoms, and Errors
Traversing Abstract AND--OR Graphs
An Example
Binding Error Searching Algorithm
Conclusions and Future Work
User-Definable Resource Bounds Analysis for Logic Programs
Introduction
The Resource Assertion Language
Overview of the Approach
Size Analysis
Resource Usage Analysis
Defining the Parameters (Functions) of the Analysis
Experimental Results
Conclusions
Automatic Correctness Proofs for Logic Program Transformations
Introduction
Weighted Unfold/Fold Transformation Rules
Proving Correctness Via Weighted Programs
Weighted Goal Replacement
The Weighted Unfold/Fold Proof Method
Conclusions
Core TuLiP Logic Programming for Trust Management
Introduction
Preliminaries on Logic Programs
Core TuLiP
The Lookup and Inference AlgoRithm (LIAR)
CoreTuLiP vs. RT_0
Translating RT_0 into CoreTuLiP
A Flexible Syntax
Related Work
Conclusions
Demand-Driven Indexing of Prolog Clauses
Introduction
State of the Art and Related Work
Indexing in the WAM
Demand-Driven Indexing of Static Predicates
A Simple WAM Extension for Any Argument Indexing
From Any Argument Indexing to Multi-argument Indexing
Beyond Datalog and Other Implementation Issues
Demand-Driven Index Construction and Its Properties
More Implementation Choices
Demand-Driven Indexing of Dynamic Predicates
Implementation in XXX and in YAP
Performance Evaluation
Performance of Demand-Driven Indexing When Ineffective
Performance of Demand-Driven Indexing When Effective
Performance of Demand-Driven Indexing on ILP Applications
Concluding Remarks
Design, Implementation, and Evaluation of a Dynamic Compilation Framework for the YAP System
Introduction
Related Work
Dynamic Optimization Systems
System Architecture
Mixed Mode Interpreter
Compilation Control
Type-Feedback-Based Profiler
The Compiler
Exception Handling
The Compiler
Partial Compilation
Region-Based Compilation
Multiple Version Code Management
Evaluation
Benchmarking Methodology
Dynamic Compilation
Code Quality
Conclusions
Declarative Debugging of Missing Answers in Constraint Functional-Logic Programming
Tightly Integrated Probabilistic Description Logic Programs for the Semantic Web
Overview
View Updating Through Active Integrity Constraints
Prosper: A Framework for Extending Prolog Applications with a Web Interface
Web Sites Verification: An Abductive Logic Programming Tool
Web Checking Rules
Mapping Rules to Abductive Logic Programs
Conclusions
Visual Logic Programming Method Based on Structural Analysis and Design Technique
Approximating Horn Knowledge Bases in Regular Description Logics to Have PTIME Data Complexity
A Linear Transformation from Prioritized wCircumscription to Disjunctive Logic Programming
Representation and Execution of a Graph Grammar in Prolog
On Applying Program Transformation to Implement Suspension-Based Tabling in Prolog
Aggregates in Constraint Handling Rules
Computing Fuzzy Answer Sets Using DLVHEX
The Use of a Logic Programming Language in the Animation of Z Specifications
Extended Abstract
A Stronger Notion of Equivalence for Logic Programs
A Register-Free Abstract Prolog Machine with Jumbo Instructions
Introduction
The TOAM Jr. Instruction Set
Experimental Results
Advanced Techniques for Answer Set Programming
A Games Semantics of ASP
Introduction
Preliminary Results
Future Work
Modular Answer Set Programming
Universal Timed Concurrent Constraint Programming
Introduction
An Universal Binder (Abstractions)
Extension and Implementation of CHR
Author Index