Logic for programming, artificial intelligence, and reasoning : 12th international conference, LPAR 2005, Montego Bay, Jamaica, December 2-6, 2005 : proceedings / / Geoff Sutcliffe, Andrei Voronkov (eds.)

• Pubblicazione: Berlin ; ; New York, : Springer, c2005
• Edizione: 1st ed. 2005.
• Descrizione fisica: 1 online resource (XIV, 744 p.)
• Disciplina: 005.1/15
• Soggetto topico: Logic programming; Automatic theorem proving; Artificial intelligence
• Altri autori: SutcliffeGeoff VoronkovA <1959-> (Andrei)
• Note generali: Bibliographic Level Mode of Issuance: Monograph
• Nota di bibliografia: Includes bibliographical references and index.
• Nota di contenuto: Independently Checkable Proofs from Decision Procedures: Issues and Progress -- Zap: Automated Theorem Proving for Software Analysis -- Decision Procedures for SAT, SAT Modulo Theories and Beyond. The BarcelogicTools -- Scaling Up: Computers vs. Common Sense -- A New Constraint Solver for 3D Lattices and Its Application to the Protein Folding Problem -- Disjunctive Constraint Lambda Calculi -- Computational Issues in Exploiting Dependent And-Parallelism in Logic Programming: Leftness Detection in Dynamic Search Trees -- The nomore?+?+ Approach to Answer Set Solving -- Optimizing the Runtime Processing of Types in Polymorphic Logic Programming Languages -- The Four Sons of Penrose -- An Algorithmic Account of Ehrenfeucht Games on Labeled Successor Structures -- Second-Order Principles in Specification Languages for Object-Oriented Programs -- Strong Normalization of the Dual Classical Sequent Calculus -- Termination of Fair Computations in Term Rewriting -- On Confluence of Infinitary Combinatory Reduction Systems -- Matching with Regular Constraints -- Recursive Path Orderings Can Also Be Incremental -- Automating Coherent Logic -- The Theorema Environment for Interactive Proof Development -- A First Order Extension of Stålmarck’s Method -- Regular Derivations in Basic Superposition-Based Calculi -- On the Finite Satisfiability Problem for the Guarded Fragment with Transitivity -- Deciding Separation Logic Formulae by SAT and Incremental Negative Cycle Elimination -- Monotone AC-Tree Automata -- On the Specification of Sequent Systems -- Verifying and Reflecting Quantifier Elimination for Presburger Arithmetic -- Integration of a Software Model Checker into Isabelle -- Experimental Evaluation of Classical Automata Constructions -- Automatic Validation of Transformation Rules for Java Verification Against a Rewriting Semantics -- Reasoning About Incompletely Defined Programs -- Model Checking Abstract State Machines with Answer Set Programming -- Characterizing Provability in BI’s Pointer Logic Through Resource Graphs -- A Unified Memory Model for Pointers -- Treewidth in Verification: Local vs. Global -- Pushdown Module Checking -- Functional Correctness Proofs of Encryption Algorithms -- Towards Automated Proof Support for Probabilistic Distributed Systems -- Algebraic Intruder Deductions -- Satisfiability Checking for PC(ID) -- Pool Resolution and Its Relation to Regular Resolution and DPLL with Clause Learning -- Another Complete Local Search Method for SAT -- Inference from Controversial Arguments -- Programming Cognitive Agents in Defeasible Logic -- The Relationship Between Reasoning About Privacy and Default Logics -- Comparative Similarity, Tree Automata, and Diophantine Equations -- Analytic Tableaux for KLM Preferential and Cumulative Logics -- Bounding Resource Consumption with Gödel-Dummett Logics -- On Interpolation in Existence Logics -- Incremental Integrity Checking: Limitations and Possibilities -- Concepts of Automata Construction from LTL.
• Altri titoli varianti: LPAR 2005
• Titolo autorizzato: Logic for programming, artificial intelligence, and reasoning
• Formato: Materiale a stampa
• Livello bibliografico: Monografia
• Lingua di pubblicazione: Inglese
• Record Nr.: 9910483264503321
• Lo trovi qui: Univ. Federico II
• Serie: Lecture notes in computer science ; ; 3835.; Lecture notes in computer science. . -Lecture notes in artificial intelligence.