Logic for Programming, Artificial Intelligence, and Reasoning: 12th International Conference, LPAR 2005, Montego Bay, Jamaica, December 2-6, 2005. Proceedings

Front Matter....Pages -
Independently Checkable Proofs from Decision Procedures: Issues and Progress....Pages 1-1
Zap: Automated Theorem Proving for Software Analysis....Pages 2-22
Decision Procedures for SAT, SAT Modulo Theories and Beyond. The BarcelogicTools....Pages 23-46
Scaling Up: Computers vs. Common Sense....Pages 47-47
A New Constraint Solver for 3D Lattices and Its Application to the Protein Folding Problem....Pages 48-63
Disjunctive Constraint Lambda Calculi....Pages 64-78
Computational Issues in Exploiting Dependent And-Parallelism in Logic Programming: Leftness Detection in Dynamic Search Trees....Pages 79-94
The nomore  + + Approach to Answer Set Solving....Pages 95-109
Optimizing the Runtime Processing of Types in Polymorphic Logic Programming Languages....Pages 110-124
The Four Sons of Penrose....Pages 125-138
An Algorithmic Account of Ehrenfeucht Games on Labeled Successor Structures....Pages 139-153
Second-Order Principles in Specification Languages for Object-Oriented Programs....Pages 154-168
Strong Normalization of the Dual Classical Sequent Calculus....Pages 169-183
Termination of Fair Computations in Term Rewriting....Pages 184-198
On Confluence of Infinitary Combinatory Reduction Systems....Pages 199-214
Matching with Regular Constraints....Pages 215-229
Recursive Path Orderings Can Also Be Incremental....Pages 230-245
Automating Coherent Logic....Pages 246-260
The Theorema Environment for Interactive Proof Development....Pages 261-275
A First Order Extension of Stålmarck’s Method....Pages 276-291
Regular Derivations in Basic Superposition-Based Calculi....Pages 292-306
On the Finite Satisfiability Problem for the Guarded Fragment with Transitivity....Pages 307-321
Deciding Separation Logic Formulae by SAT and Incremental Negative Cycle Elimination....Pages 322-336
Monotone AC-Tree Automata....Pages 337-351
On the Specification of Sequent Systems....Pages 352-366
Verifying and Reflecting Quantifier Elimination for Presburger Arithmetic....Pages 367-380
Integration of a Software Model Checker into Isabelle....Pages 381-395
Experimental Evaluation of Classical Automata Constructions....Pages 396-411
Automatic Validation of Transformation Rules for Java Verification Against a Rewriting Semantics....Pages 412-426
Reasoning About Incompletely Defined Programs....Pages 427-442
Model Checking Abstract State Machines with Answer Set Programming....Pages 443-458
Characterizing Provability in BI ’s Pointer Logic Through Resource Graphs....Pages 459-473
A Unified Memory Model for Pointers....Pages 474-488
Treewidth in Verification: Local vs. Global....Pages 489-503
Pushdown Module Checking....Pages 504-518
Functional Correctness Proofs of Encryption Algorithms....Pages 519-533
Towards Automated Proof Support for Probabilistic Distributed Systems....Pages 534-548
Algebraic Intruder Deductions....Pages 549-564
Satisfiability Checking for PC(ID)....Pages 565-579
Pool Resolution and Its Relation to Regular Resolution and DPLL with Clause Learning....Pages 580-594
Another Complete Local Search Method for SAT....Pages 595-605
Inference from Controversial Arguments....Pages 606-620
Programming Cognitive Agents in Defeasible Logic....Pages 621-636
The Relationship Between Reasoning About Privacy and Default Logics....Pages 637-650
Comparative Similarity, Tree Automata, and Diophantine Equations....Pages 651-665
Analytic Tableaux for KLM Preferential and Cumulative Logics....Pages 666-681
Bounding Resource Consumption with Gödel-Dummett Logics....Pages 682-696
On Interpolation in Existence Logics....Pages 697-711
Incremental Integrity Checking: Limitations and Possibilities....Pages 712-727
Concepts of Automata Construction from LTL....Pages 728-742
Back Matter....Pages -