Computational Logic ― CL 2000: First International Conference London, UK, July 24–28, 2000 Proceedings (Lecture Notes in Computer Science, 1861)

These are the proceedings of the First International Conference on Compu- tional Logic (CL 2000) which was held at Imperial College in London from 24th to 28th July, 2000. The theme of the conference covered all aspects of the theory, implementation, and application of computational logic, where computational logic is to be understood broadly as the use of logic in computer science. The conference was collocated with the following events: { 6th International Conference on Rules and Objects in Databases (DOOD 2000) { 10th International Workshop on Logic-based Program Synthesis and Tra- formation (LOPSTR 2000) { 10th International Conference on Inductive Logic Programming (ILP 2000). CL 2000 consisted of seven streams: { Program Development (LOPSTR 2000) { Logic Programming: Theory and Extensions { Constraints { Automated Deduction: Putting Theory into Practice { Knowledge Representation and Non-monotonic Reasoning { Database Systems (DOOD 2000) { Logic Programming: Implementations and Applications. The LOPSTR 2000 workshop constituted the program development stream and the DOOD 2000 conference constituted the database systems stream. Each stream had its own chair and program committee, which autonomously selected the papers in the area of the stream. Overall, 176 papers were submitted, of which 86 were selected to be presented at the conference and appear in these proceedings. The acceptance rate was uniform across the streams. In addition, LOPSTR 2000 accepted about 15 extended abstracts to be presented at the conference in the program development stream. Computational Logic - CL 2000 Preface Organisation Table of Contents Computational Logic: Memories of the Past and Challenges for the Future Introduction First Order Predicate Calculus: All the Logic We Have and All the Logic We Need Hilbert’s 1900 Address The Long Reign of the Syllogistic Logic Frege’s Thought Notation Completeness: Herbrand and Gödel Computation: Turing, Church, and von Neumann Computational Logic Heuristics and Algorithms: The Dartmouth and Cornell Meetings Combinatorial Explosions with Herbrand’s Property B Prawitz’s Independent Rediscovery of Unification Ushers in Resolution Computational Logic in Edinburgh: The A.I. Wars The Colmerauer-Kowalski Encounter Computational Logic Officially Recognized: Prolog’s Spectacular Debut The Fifth Generation Project The Aftermath: Pure Logic Programming not a Complete Panacea Realism: Side Effects, Concurrency, Software Engineering Robbins’ Conjecture Proved by Argonne’s Theorem Prover Proliferation of Computational Logic A Look at the Future: Some Challenges To Shed Further Light on the P = NP Problem To Explain the Intelligibility/Efficiency Trade-off To Explain Why Imperative Constructs are Harmful to a Program’s Intelligibility To Explain the (Informal, Intuitive) / (Formal, Rigorous) Trade-off in Proofs To Understand the Limits of Extending Constraint Logic Programming To Find New Killer Applications for LP To Enhance and Propagate the Declarative Programming Paradigm To Integrate Functional Programming with Logic Programming Hilbert Has the Last Word References ILP: Just Do It Introduction A Brief Review of Some Application Areas Five Directions for ILP Research Probabilistic Inference: ILP and Bayes Nets Stochastic Search Special-Purpose Reasoning Mechanisms Interaction with Human Experts Parallel Execution Conclusions References Databases and Higher Types Introduction A Sample Database Higher Order Modal Logic A Modal Interpretation Queries Constraints Conclusion References A Denotational Semantics for First-Order Logic Introduction Solving Equations over Algebras Semantics of Equations A Denotational Semantics for First-Order Logic Soundness Conclusions and Future Work References Logic, Knowledge Representation, and Bayesian Decision Theory Introduction Knowledge Representation Belief Networks The Independent Choice Logic The Language Semantics ICL and Belief Networks ICL, Abduction, and Logical Argumentation Reasoning in the ICL Relating Work in Other Fields Reasoning about Actions Model-Based Diagnosis Bayesian Leaning Conclusion References Logic Program Synthesis in a Higher-Order Setting Introduction Background Proof Planning Controlling the Synthesis Process Example 1: Symbolic Evaluation Example 2: Induction Example 3: Unrolling Methods Used by the System Synthesising Higher-Order Logic Programs Encoding of the Object Logic Higher-Order Program Synthesis Parameterised Synthesis Discussion Comparison with Other Systems Further Work Summary References Sample Example Synthesis Results First-Order Programs Higher-Order Horn Clause Examples Parameterised Synthesis Coverability of Reset Petri Nets and Other Well-Structured Transition Systems by Partial Deduction Introduction (Reset) Petri Nets and the Covering Problem Partial Evaluation and Partial Deduction Generic Algorithm for Partial Deduction Concrete Algorithm Encoding (Reset) Petri Nets as Logic Programs Coverability of Reset Petri Nets by Partial Deduction Other Well-Structured Transition Systems Future Work and Conclusion References Binary Speed Up for Logic Programs Introduction A Transformation to Binary Logic Programs Transformations and Binarization Binarization Can Lead to More Efficient Programs B-Stratifiable Programs Results and Comparison References A New Module System for Prolog Introduction Objectives in the Design of the Ciao Module System Discussion of the Main Issues Involved The Ciao Module System General Issues User Files and Multifile Predicates Dynamic Modules Dealing with Meta-calls Modular Syntax Enhancements Packages An Example Package: {tt argnames} Conclusions References Code for the Package texttt {argnames} Partial Models of Extended Generalized Logic Programs Introduction Preliminaries Sequents and Programs Stationary Generated Models and GWFX-Semantics Extended Normal Logic Programs and WFSX-Semantics Conclusion References Alternating Fixpoint Theory for Logic Programs with Priority Introduction Alternating Fixpoints without Priority Alternating Fixpoints with Priority Semantics for Prioritized Logic Programs Properties of Prioritized Semantics Comparison to Related Approaches Conclusion References Proving Failure in Functional Logic Programs Introduction The {it CRWL} Framework Technical Preliminaries The Proof Calculus for {it CRWL} The {it CRWLF} Framework Some Illustrative Examples Technical Preliminaries The Proof Calculus for {it CRWLF} Properties of {it CRWLF} {it CRWLF} Related to {it CRWL} Conclusions and Future Work References Semantics of Input-Consuming Logic Programs Introduction Preliminaries Basic Definitions Semantics of Input-Consuming Programs Concluding Remarks References A Denotational Semantics of Defeasible Logic Introduction The Defeasible Logic $DL$ A Denotational Semantics Correctness Full Abstraction Further Work Conclusion References Isoinitial Semantics for Logic Programs Introduction Initial and Isoinitial Models Initial and Isoinitial Semantics for Closed Theories Closed Logic Programs Termination Initial and Isoinitial Semantics for Open Theories Incomplete Information Parametricity Compositionality Open Logic Programs Incomplete Information Parametricity Compositionality Conclusion References Abstract Syntax for Variable Binders: An Overview How Abstract Is Your Syntax? Church's Use of $lambda $-Terms within Logic Equality Modulo $alpha beta eta $-Conversion A Weaker Form of $beta $-Conversion $L_lambda $-Unification Logic Programming in $L_lambda $ $lambda $-Tree Syntax Related Work Conclusions References Goal-Directed Proof Search in Multiple-Conclusioned Intuitionistic Logic Introduction Preliminaries Sequent Calculi Permutabilities Intuitionistic Logic and LJ Multiple-Conclusioned Systems for Intuitionistic Logic Goal-Directed Proofs Deriving a Logic Programming Language in LM Permutation Properties of LM Identifying a Subset of the Logic Formal Results Definite Formulae in LM Contraction-Free Fragments Conclusions and Further Work References Efficient EM Learning with Tabulation for Parameterized Logic Programs Introduction Background Constraint Approach and Distribution Approach Limitations and Problems The Idea of PRISM Problem of Computational Complexity PRISM Programs Further Definitions and Assumptions A Program Example Learning PRISM Programs Naive Approach Tabulation Approach Graphical EM Algorithm Complexity Conclusion References Model Generation Theorem Proving with Finite Interval Constraints Introduction Standard Definitions Syntax and Semantics of IV-MGTP Motivation The Language of IV-MGTP Formal Semantics of IV-MGTP The IV-MGTP Deduction Process Model Candidates Conjunctive Matching Inconsistency Subsumption Model Candidate Update IV-MGTP Procedure Soundness and Completeness Results Cryptarithmetic Channel Routing Related and Future Work Constraint Logic Programming Signed Formula Logic (Programming) IV-MGTP and CMGTP Paraconsistent Reasoning Future Work References Combining Mobile Processes and Declarative Programming Introduction Overview of Our Proposal Actions Processes Example of the Multiple Counters Example of the Dining Philosophers Operational Semantics Related Work Conclusion References Representing Trees with Constraints Introduction Motivation: Grouping Structure Using Constraints Representation Node Constraints Level Constraints Consistency Constraints Width Constraints Edge Constraints Valid Trees Using the Constraint Representation Results Conclusions References Dominance Constraints with Set Operators Introduction Dominance Constraints A Saturation Algorithm Completeness Proof Constraint Programming with Finite Sets Reduction to Finite Set Constraints Representation. Wellformedness. Problem Specific Constraints. Definition of the Concrete Solver. Proving Correctness of Implementation Conclusion References Better Communication for Tighter Cooperation Introduction Constraint Systems and Constraint Solvers Combination of Constraint Solvers The Architecture Syntax A Uniform Interface for Constraint Solvers. Operational Semantics Preliminaries. Basic Relations. Defining Strategies for Cooperating Constraint Solvers. Conclusion and Related Work References Arc Consistency Algorithms via Iterations of Subsumed Functions Introduction The Generic Iteration Algorithm with Subsumed Functions GISF for Constraint Satisfaction Problems Arc and Hyper Arc Consistency Algorithms The {A}lgorithm {tt HAC-4} for {H}yper {A}rc {C}onsistency {tt AC-4} for {B}inary {C}onstraint {S}atisfaction {P}roblems The {A}lgorithm {tt HAC-5} for {H}yper {A}rc {C}onsistency {tt AC-5} for {B}inary {C}onstraint {S}atisfaction {P}roblems Conclusions References AVAL: An Enumerative Method for SAT Introduction Literal Production The Avalanch Method (AVAL) Heuristics Pre-processing Experiments Comparison between DP and AVAL Success Rate of the Literal Production Efficiency of Our Method Threshold of Unit Clauses Production Comparison with SATZ and POSIT Challenges Beijing and DIMACS Conclusion References Constraint Logic Programming for Local and Symbolic Model-Checking Introduction Preliminaries Constraint Logic Programming Model Checking and CTL A CLP Formalization of CTL Correctness An Abstract Model of Computation A Preliminary Experimental Evaluation Conclusions References A CLP Framework for Computing Structural Test Data Introduction Motivating Example Notations and Basic Definitions Generation of the Constraint System Static Single Assignment Form Generation of the CLP Program Generation of the CLP Goal Solving the Goal Entailment Test Processing Guarded--Constraints Search Process First Experimental Results Our Prototype System Experiments Test Procedure Results Analysis Perspective References Modelling Digital Circuits Problems with Set Constraints Introduction Modelling Modelling Digital Signals with Sets and Booleans Normal Gates S-Buffers Modelling the Problems Modelling Digital Signals with Sets Modelling the Problems Cardinal Set Solver A Set Constraint Solver: Cardinal Set Variable Set Complement Set Equality Set Inclusion Set Intersection Implementation and Results Conclusions and Further Research References Promoting Constraints to First-Class Status Introduction Constraints as First-Class Values Early Failure Detection Constraint Simplification Garbage Collection of Constraints Computing Minimal Sets of Inconsistent Constraints First-Class Constraints vs. Reified Constraints Adding First-Class Constraints to an Existing Solver Related Work Conclusion and Future Work References Developing Finite Domain Constraints - A Data Model Approach Introduction Specifying a CSP by Database Integrity Constraints Compiling Data Objects into CLP Structures Data Objects and Scalar Attributes Relationships between Objects Constraint Compilation Existentially Quantified Constraint Conditional Constraints Universally Quantified Constraint Related Work Conclusions References Concurrent Constraint Programming with Process Mobility Introduction Process Migration versus Link Mobility Models of Mobile Computation Distributed Concurrent Constraint Programming Structure of the Paper The Basic Paradigm for Migration Enhancing ccp with Migration An Example Interpreter Future Work References A System for Tabled Constraint Logic Programming Introduction Extending XSB with Attributed Variables Basic Changes to the System Modifications of Tabling Engine for Attributed Variables Tabling and Constraints: Necessary Operations Projection Entailment Checking Our Solution: A General Framework A Real Example Conclusion and Future Work References Finding Tractable Formulas in NNF Introduction Our NNF Tractability Contribution Related Work CNF Tractability NNF Tractability $phi $-Formulas Syntax and Semantics Inference Rules Algorithm Description $sigma $-Formulas $omega $-Formulas Conclusions References The Taming of the (X)OR Introduction Preliminaries Simplification by Boolean Reduction Simplification by Boolean Assignments Gauss Resolution Rules Gauss-DPLL An Effective Calculus for Proof Search Correctness Conclusions References On an -Decidable Deductive Procedure for Non-Horn Sequents of a Restricted FTL Introduction Infinitary,Calculus,$G_{Lomega }^ast $,and,Induction-Free,Calculus,$G^ast $ Description of the Deductive Procedure $Sat_omega $ Conclusions, Related Works, and Future Investigations References Representing Object Code Introduction Translating Object Code into Logic Compressing the Representation Conclusions References Towards an Efficient Tableau Method for Boolean Circuit Satisfiability Checking Introduction Boolean Circuits A Tableau Method Satisfiability Preserving Simplifications An Experimental Implementation Translating Circuits into CNF Some Experiments Conclusions References Certification of Compiler Optimizations: Using Kleene Algebra with Tests Introduction Kleene Algebra and Kleene Algebra with Tests Kleene Algebra (unhbox voidb @x hbox {$@mathsf {KA}$}) Kleene Algebra with Tests (unhbox voidb @x hbox {$@mathsf {KAT}$}) $@mathsf {KAT}$ and Hoare Logic Verifying Optimizations in unhbox voidb @x hbox {$@mathsf {KAT}$} Dead Code Elimination Common Subexpression Elimination Copy Propagation Loop Hoisting Induction Variable Elimination Instruction Scheduling Algebraic Simplification Loop Unrolling Redundant Loads and Stores Array Bounds Check Elimination Introduction of Sentinels The Dead Variable Paradox References An Application of Model Building in a Resolution Decision Procedure for Guarded Formulas Introduction Preliminaries Rules Covering Literals Guarded Clauses Deciding Sets of Guarded Clauses The Model Building Procedure Flattening of Positive Body Literals Flattening of Negative Body Literals Transformation into Primitive Guarded Horn Clauses Evaluation of Guarded Clauses Integration of the Model Building Procedure into the Decision Procedure Generalization to Loosely Guarded Clauses Conclusion and Future Work References Model Checking for Timed Logic Processes Introduction Timed Logic Processes Translation of Timed Automata into TLPs Logic of Safety and Bounded Liveness (${cal L}_s$) Product Program The Trim Operation on Constraints Full Disjunction Unbounded Liveness Properties Implementation Related Work References Perfect Model Checking via Unfold/Fold Transformations Introduction Preliminaries From First-Order Formulas to Logic Programs Transformation Rules A Strategy for Unfold/Fold Proofs Decision Procedures Based on Unfold/Fold Proofs Conclusions and Related Work References Automatic Derivation and Application of Induction Schemes for Mutually Recursive Functions Introduction Deriving Multi-predicate Schemes from Definitions An Example Proof A Proof Procedure for Using Multi-predicate Schemes Implementation and Results Related Work Conclusions and Future Work References Proof Planning with Multiple Strategies Introduction Basics of Knowledge Based Proof Planning Multi-strategy Proof Planning A Motivating Example Strategies Realization in {sc Multi} Results and Experiences with {{sc Multi}} Experiments Explanation of {sc Multi}'s Success Conclusion and Related Work References The Theory of Total Unary RPO Is Decidable The Recursive Path Ordering on Words Coding Words as Trees Tree Automata RPO Theory On Normal Forms and Ordered Rewriting The Recursive Path Ordering on Terms Ordered Rewriting References On the Problem of Computing the Well-Founded Semantics Introduction Preliminaries Algorithms Procedure $Delta _w$ Conclusions References Computing Equilibrium Models Using Signed Formulas Introduction Equilibrium Logic Equilibrium Models and Equilibrium Inference Signed Logics Reduced Signed Logics Signability of $@mathbf {N}_5$ Signing $@mathbf {N}_5$ for Validity: Signing-Down and Signing-Up Signing for the Generation of Total Models Signing to Check the Equilibrium Property Complexity of Equilibrium Model Generation Conclusions References Extending Classical Logic with Inductive Definitions Introduction An Abstract Logic of Inductive Definitions ID-Logic: Classical Logic with Definitions Properties of Definitions Well-Defining Definitions Equivalence of Definitions Monotonicity or Non-monotonicity? Other Formalizations Applications of Definitions Relationship to Logic Programming Extensions References A Simple Characterization of Extended Abduction Introduction Extended Abduction Definitions Previous Characterization of Extended Abduction From Extended Abduction to Normal Abduction Translation of Explanations Translation of Anti-explanations Computing Extended Abduction Restoring Consistency Related Work Concluding Remark References A New Equational Foundation for the Fluent Calculus Introduction Unification Completeness and Its Limitations A New Equational Foundation Results An Induction Axiom Conclusion References Solving the Entailment Problem in the Fluent Calculus Using Binary Decision Diagrams Introduction Foundations Logics Planning The Fluent Calculus Binary Decision Diagrams Mapping the Fluent Calculus onto Propositional Logic Plan Extraction An Implementation Using BDDs | First Results Discussion References Decidability Results for the Propositional Fluent Calculus Introduction Specifying Systems in the Fluent Calculus Temporal Properties Fluent Calculi and Petri Nets Undecidability of $CTL_{EF}$ in $\cal{FC}_{PL}$ Decidable Properties in $\cal{FC}_{PL}$ Conclusions References A Meta-logical Semantics for Features and Fluents Based on Compositional Operators over Normal Logic Programs Introduction Motivations Backgrounds Feature and Fluents Logic Programming Event Calculus Fluent Logic Programming Non-deterministic Chronicles Meta-logical Semantics for FLP Meta-logical Representation of FLP-Chronicles Soundness and Completeness Conclusions References Default Reasoning with Specificity Introduction A General Framework Stratified Default Theories General Properties of $|mskip -thinmuskip mskip -thinmuskip sim $ Discussion and Conclusion References Planning under Incomplete Knowledge Introduction Overview of $\cal K$ Contribution of the Work Language $\cal K$ Syntax Actions, Fluents, and Types. Action/Fluent Declarations. Causation Rules. Initial State Constraints. Conditional Executability. Safety Restriction. Action Descriptions, Planning Domains, Planning Problems. Semantics Instantiation. States and Transitions. Plans The Planning System $\mathrm{DLV}^{\cal K}$ Programs in $\mathrm{DLV}^{\cal K}$ Language Enhancements Knowledge Representation in $\cal K$ A Simple Blocks World Instance Checking Correctness and Completeness of the Initial State Reasoning under Incomplete Knowledge Complexity of $\cal K$ Related Work and Conclusion References Wire Routing and Satisfiability Planning Introduction Input and Output of CCALC The Routing Domain Bus Routing Restricting the Lengths of Wires Spacing Constraints Discussion References Including Diagnostic Information in Configuration Models Introduction The Rule Language Configuring a Debian System The Diagnostic Model Missing Packages Conflicts Justifications Implementation Conclusions and Future Work References Comparing the Expressive Powers of Some Syntactically Restricted Classes of Logic Programs Introduction Logic Programs Syntactic Restrictions Semantics Translations Expressive Power Analysis Normal Logic Programs Related Work Discussion and Conclusions References On Complexity of Updates through Integrity Constraints Introduction Preliminaries Conservative Rule Based Updates Computational Complexity of Conservative Updates Complexity in Partial Interpretations Complexity in Total Interpretations The Case of Varying Signature Conclusion References Computational Complexity of Planning Based on Partial Information about the System's Present and Past States Introduction Planning Problems: Towards a More Realistic Formulation Computational Complexity of Planning problem: Why It Is Important, What Is Known, and What We Are Planning to Do Results Complexity of Plan Checking Complexity of Planning Proofs References Smallest Equivalent Sets for Finite Propositional Formula Circumscription Introduction Propositional Circumscription Equivalences between Sets of Circumscribed Formulas About the Characterization of Formula Circumscription The Smallest Sets Strongly Equivalent to a Given Set The Smallest Sets $c$-Equivalent to a Given Set A Few Examples Conclusion and Perspective References A Semantics for Persistency in Propositional Dynamic Logic Introduction Propositional Dynamic Logic Axiomatic Approaches to Persistency in Modal Action Logics A Semantic Definition of Persistency in PDL Benchmark Reasoning Examples Discussion References Applications of Annotated Predicate Calculus to Querying Inconsistent Databases Introduction Preliminaries Annotated Predicate Calculus Embedding Databases in APC Repairing Inconsistent Databases Finiteness of $unhbox voidb @x hbox {${cal T}^{bf a}({{bf DB}}xspace ,{{bf IC}}xspace )$}xspace$ Queries to Inconsistent Databases Conclusions References Querying Inconsistent Databases: Algorithms and Implementation Introduction Preliminaries Basic Notions The $textnormal {T}_omega $ Operator Integrity Constraints Query Generation for Consistent Answers Residue Calculation Query Generation ({em QUECA}) Properties of {em QUECA} Implementation Conclusions References On Verification in Logic Database Languages Introduction Datalog++: Nondeterministic, Nonmonotonic Datalog Programming with Datalog++ Euclid's Algorithm for the Greatest Common Divisor The Ford-Fulkerson Method for the Maximum-Flow Problem The Readers-Writers Problem Verification of Datalog++ Programs Properties of the {tt choice} Construct Verification of X-Predicates {em Safety} and {em Progress} Properties for Y-Predicates Application of the Methodology Conclusion and Future Work References Mining Minimal Non-redundant Association Rules Using Frequent Closed Itemsets Introduction Contribution Semantic for Association Rules Based on the Galois Connection Extracting Frequent Closed Itemsets and their Generators with the Close Algorithm Minimal Non-redundant Association Rules Generic Basis for Exact Association Rules Informative Basis for Approximate Association Rules Experimental Results Conclusion References Linearly Bounded Reformulations of Conjunctive Databases (Extended Abstract) Introduction Preliminaries and Terminology Concept of Database Reformulation Views with Bounded Definition Length Shorter Views Contained in Longer Views A Database Reformulation Algorithm Related Work Conclusions and Future Work References Some Examples and Proofs A Recursive Reformulation Example An Example of Conjunctive Reformulation Proof of Theoremnobreakspace {}ref {main-theorem} in Sectionnobreakspace {}ref {main-section} MuTACLP: A Language for Declarative GIS Analysis Introduction Temporal Annotated Constraint Logic Programming 3 Multi-theory Temporal Annotated Constraint Logic Declarative GIS Analysis in MuTACLP A Logical Representation of GIS Spatial Data Operators on Spatial Objects Creation of GIS Layers An Example Conclusions References Reasoning about Duplicate Elimination with Description Logic (Preliminary Report) Introduction Related Work Definitions Description Logics and Database Schemas Conjunctive Object Relational Queries Reasoning about Duplicate Elimination Operators A Decision Procedure for CFD Conclusion References EXP and SUBSUMES A File System Based on Concept Analysis Introduction: Querying vs. Navigation Logical Concept Analysis Logical Context and Galois Connection Logical Concepts Labelling of Concept Lattices Informal Specification of a Conceptual Shell Formal Specification of a Conceptual Shell Logical Operations Context Operations Querying and Navigation Operations Interface Operations Algorithms and Complexity Data Structures Algorithms for Operationsnobreakspace {}$tau $, $t$, andnobreakspace {}$Inc$ Algorithms for Locating and Inserting Formulas in the Diagram Discussion about Complexity Conclusion and Further Works References A Semantic Approach for Schema Evolution and Versioning in Object-Oriented Databases Introduction Related Work An Object-Oriented Data Model for Evolving Schemata Reasoning Problems Reasoning Using Description Logics Discussion Conclusions References SLDMagic - The Real Magic: (With Applications to Web Queries) Introduction Problems of Magic Set Query Evaluation Tail Recursions Nonrecursive Programs Getting Results Back into the Context of the Caller Passing Conditions on the Parameters to Called Predicates Combining Conditions for Index Access The Meta-interpreter Bottom-Up Execution of SLD-Resolution Termination Adding ``Magic Set'' Behaviour Partial Evaluation Conclusions References FLORA: Implementing an Efficient DOOD System Using a Tabling Logic Engine Introduction Preliminaries F-Logic HiLog Transaction Logic Implementation Issues Transactions in a Tabling Environment Problems with Naive Translation of HiLog and F-Logic Solutions Skeleton-Based Specialization Algorithm Putting It All Together Conclusion References Design and Implementation of the Physical Layer in WebBases: The XRover Experience Introduction Our Approach Architecture of the Virtual Physical Layer (VPL) XRover Implementation: Status and Statistics Conclusion References A Dynamic Approach to Termination Analysis for Active Database Rules Introduction Rule Execution Semantics Incremental Inference of Termination Behaviour The INFER Functions Detecting Possible Non-termination Evaluation Related Work Summary and Further Work References Constraint-Based Termination Analysis for Cyclic Active Database Rules Introduction Preliminaries Active Rules Constraint Systems Annotated Triggering Graphs Constructing Annotated Triggering Graphs Reasoning about Annotated Triggering Graphs Approximate Solution of Difference Equations Extensions Static Termination Analysis Dynamic Termination Analysis Related Work Conclusions References A Formal Model for an Expressive Fragment of XSLT Introduction XSLT by Example A Formal Model for XSLT Trees and Forests Syntax Semantics Some Remarks Expressiveness Discussion References On the Equivalence of XML Patterns Introduction Related Work Containment of Datalog Programs XML and XSLT Patterns XML Data Model Syntax of XSLT Patterns Semantics of XSLT Patterns Containment of XSLT Patterns Conclusion References Querying XML Specified WWW Sites: Links and Recursion in XML-GL (Extended Abstract) Introduction XML-GL The XML-GL Data Model Query Language Operational Semantics of XML-GL XML-GL$^{@mathit {rec}}$: Querying Web Sites XML Links in XML-GL$^{@mathit {rec}}$ Some Examples of Recursive Queries Some Basic Notions on G-Log XML-GL$^{@mathit {rec}}$ to G-Log Conclusions References A Heuristic Approach for Converting HTML Documents to XML Documents Introduction HTML/XML Documents Construction of the Data Hierarchy of an HTML Document Exclusion of HTML Elements Edge Definition Function of DAH Edge Definition Function for Table-Specific Elements DAH to XML Implementation of the Html2Xml Approach Concluding Remarks References Specification of an Active Database System Application Using Dynamic Relation Nets Introduction ECA-Rules Dynamic Relation Nets Specifying ECA-Rules with Dynamic Relation Nets Implementation Issues Conclusion References Invariance, Maintenance, and Other Declarative Objectives of Triggers - A Formal Characterization of Active Databases Introduction and Motivation The Declarative Notions The Procedural Features of an Active Database Actions, Events, and Triggers Actions and Effects Events and ECA Rules Characterizing Database Evolution Due to ECA Rules Correctness of ECA Rules Elaborating on Our Abstractions The Tables A Subset of the Triggers Interrupting Exogenous Updates Conclusion and Future Work References Fluents: A Refactoring of Prolog for Uniform Reflection and Interoperation with External Objects Introduction First Class Horn Clause Interpreters Fluents: From Reflection to Interoperation with External Objects Interpreters as Answer Sources Fluent Classes and their Operations Fluent Composers Fluent Modifiers Source Level Extensions through New Definitions Negation and {tt once/1} Reflective Meta-interpreters If-then-else All-Solution Predicates Term Copying and Instantiation State Detection Implementing Exceptions Built-Ins as a Library of Fluents Lists and Terms as Source Fluents File, URL, and Database I/O in Kernel Prolog Memoing Fluents Fluent Based Lazy Lists Related Work Future Work Conclusion References So Many WAM Variations, So Little Time Introduction The XSB Compiler and dProlog The Three Term Representations on the Heap in dProlog Comparing dProlog with Other Prolog Systems Comparing the Six Basic Modes of dProlog The Effect of Features and Optimizations in dProlog Variations in the Implementation of the Emulator Variations on the Abstract Machine Code Comparing Four Term Representation Schemas Related Work Conclusion and Future Work References A Module Based Analysis for Memory Reuse in Mercury Introduction Background Abstract Interpretation Mercury Types and Selectors Liveness Analysis Reuse Analysis Using the Analysis Results Module Based Analysis Modular Liveness Analysis Modular Reuse Analysis Conditions for Reuse. Version Control. Circular Dependencies between Modules Experimental Results Benchmarks and Results Discussion Effect on the Performance of Mercury Programs Conclusion References Mode Checking in HAL Introduction The HAL Language Type, Instantiation, and Type-Instantiation Trees Basic Mode Checking Automa This book constitutes the refereed proceedings of the First International Conference on Computational Logic, CL 2000, held in London, UK in July 2000. The 86 revised full papers presented together with five invited papers were carefully reviewed and selected from a total of 176 submissions. In accordance with the seven streams, the papers are organized in sections on program development, logic programming - theory and extensions, constraints, automated deduction - putting theory into practice, knowledge representation and nonmonotonic reasoning, database systems, and logic programming - implementations and applications.