Logic for Programming, Artificial Intelligence, and Reasoning: 11th International Conference, LPAR 2004, Montevideo, Uruguay, March 14-18, 2005. Proceedings

Front Matter....Pages -
CERES in Many-Valued Logics....Pages 1-20
A Decomposition Rule for Decision Procedures by Resolution-Based Calculi....Pages 21-35
Abstract DPLL and Abstract DPLL Modulo Theories....Pages 36-50
Combining Lists with Non-stably Infinite Theories....Pages 51-66
Abstract Model Generation for Preprocessing Clause Sets....Pages 67-78
Flat and One-Variable Clauses: Complexity of Verifying Cryptographic Protocols with Single Blind Copying....Pages 79-94
Applications of General Exact Satisfiability in Propositional Logic Modelling....Pages 95-109
BCiC: A System for Code Authentication and Verification....Pages 110-124
Ordered Resolution with Selection for $\mathcal{H}(@)$ ....Pages 125-141
On a Semantic Subsumption Test....Pages 142-153
Suitable Graphs for Answer Set Programming....Pages 154-168
Weighted Answer Sets and Applications in Intelligence Analysis....Pages 169-183
How to Fix It: Using Fixpoints in Different Contexts....Pages 184-193
Reasoning About Systems with Transition Fairness....Pages 194-208
Entanglement – A Measure for the Complexity of Directed Graphs with Applications to Logic and Games....Pages 209-223
How the Location of * Influences Complexity in Kleene Algebra with Tests....Pages 224-239
The Equational Theory of 〈ℕ, 0, 1, + , ×, ↑〉 Is Decidable, but Not Finitely Axiomatisable....Pages 240-256
A Trichotomy in the Complexity of Propositional Circumscription....Pages 257-269
Exploiting Fixable, Removable, and Implied Values in Constraint Satisfaction Problems....Pages 270-284
Evaluating QBFs via Symbolic Skolemization....Pages 285-300
The Dependency Pair Framework: Combining Techniques for Automated Termination Proofs....Pages 301-331
Automated Termination Analysis for Incompletely Defined Programs....Pages 332-346
Automatic Certification of Heap Consumption....Pages 347-362
A Formalization of Off-Line Guessing for Security Protocol Analysis....Pages 363-379
Abstraction-Carrying Code....Pages 380-397
A Verification Environment for Sequential Imperative Programs in Isabelle/HOL....Pages 398-414
Can a Higher-Order and a First-Order Theorem Prover Cooperate?....Pages 415-431
A Generic Framework for Interprocedural Analyses of Numerical Properties....Pages 432-432
Second-Order Matching via Explicit Substitutions....Pages 433-448
Knowledge-Based Synthesis of Distributed Systems Using Event Structures....Pages 449-465
The Inverse Method for the Logic of Bunched Implications....Pages 466-480
Cut-Elimination: Experiments with CERES....Pages 481-495
Uniform Rules and Dialogue Games for Fuzzy Logics....Pages 496-510
Nonmonotonic Description Logic Programs: Implementation and Experiments....Pages 511-527
Implementing Efficient Resource Management for Linear Logic Programming....Pages 528-543
Layered Clausal Resolution in the Multi-modal Logic of Beliefs and Goals....Pages 544-559
Back Matter....Pages -