LEADER 06209nam 22007335 450 001 996465724003316 005 20200701063135.0 024 7 $a10.1007/11591191 035 $a(CKB)1000000000213540 035 $a(SSID)ssj0000318699 035 $a(PQKBManifestationID)11279925 035 $a(PQKBTitleCode)TC0000318699 035 $a(PQKBWorkID)10311624 035 $a(PQKB)10006854 035 $a(DE-He213)978-3-540-31650-3 035 $a(MiAaPQ)EBC3068299 035 $a(PPN)123098769 035 $a(EXLCZ)991000000000213540 100 $a20100409d2005 u| 0 101 0 $aeng 135 $aurnn#008mamaa 181 $ctxt 182 $cc 183 $acr 200 10$aLogic for Programming, Artificial Intelligence, and Reasoning$b[electronic resource] $e12th International Conference, LPAR 2005, Montego Bay, Jamaica, December 2-6, 2005, Proceedings /$fedited by Geoff Sutcliffe, Andrei Voronkov 205 $a1st ed. 2005. 210 1$aBerlin, Heidelberg :$cSpringer Berlin Heidelberg :$cImprint: Springer,$d2005. 215 $a1 online resource (XIV, 744 p.) 225 1 $aLecture Notes in Artificial Intelligence ;$v3835 300 $aBibliographic Level Mode of Issuance: Monograph 311 08$aPrinted edition: 9783540305538 320 $aIncludes bibliographical references and index. 327 $aIndependently 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. 410 0$aLecture Notes in Artificial Intelligence ;$v3835 606 $aSoftware engineering 606 $aArtificial intelligence 606 $aComputer programming 606 $aComputer logic 606 $aMathematical logic 606 $aSoftware Engineering/Programming and Operating Systems$3https://scigraph.springernature.com/ontologies/product-market-codes/I14002 606 $aArtificial Intelligence$3https://scigraph.springernature.com/ontologies/product-market-codes/I21000 606 $aProgramming Techniques$3https://scigraph.springernature.com/ontologies/product-market-codes/I14010 606 $aSoftware Engineering$3https://scigraph.springernature.com/ontologies/product-market-codes/I14029 606 $aLogics and Meanings of Programs$3https://scigraph.springernature.com/ontologies/product-market-codes/I1603X 606 $aMathematical Logic and Formal Languages$3https://scigraph.springernature.com/ontologies/product-market-codes/I16048 615 0$aSoftware engineering. 615 0$aArtificial intelligence. 615 0$aComputer programming. 615 0$aComputer logic. 615 0$aMathematical logic. 615 14$aSoftware Engineering/Programming and Operating Systems. 615 24$aArtificial Intelligence. 615 24$aProgramming Techniques. 615 24$aSoftware Engineering. 615 24$aLogics and Meanings of Programs. 615 24$aMathematical Logic and Formal Languages. 676 $a005.1/15 702 $aSutcliffe$b Geoff$4edt$4http://id.loc.gov/vocabulary/relators/edt 702 $aVoronkov$b Andrei$4edt$4http://id.loc.gov/vocabulary/relators/edt 712 12$aLPAR (Conference) 906 $aBOOK 912 $a996465724003316 996 $aLogic for Programming, Artificial Intelligence, and Reasoning$9772423 997 $aUNISA