Promotional Information

Springer Book Archives

Table of 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.- Automated Theorem Proving.- 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 ChannellingConstraints.- 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.- Experimental Papers.- 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.- Termination.- 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.