LEADER 01328nem0-2200397---450- 001 990009611820403321 005 20120801132823.0 035 $a000961182 035 $aFED01000961182 035 $a(Aleph)000961182FED01 035 $a000961182 100 $a20120730d1959----km-y0itay50------ba 101 0 $aita 102 $aIT 120 $ab--------bl-- 121 $aaa-aabb-a$b-------- 123 1 $aa$b1:25000$de0021500$ee0022230$fn0374000$gn0373500 124 $aa$bd$c--$db$e-$f--$g-- 200 1 $aCenturipe$bDocumento cartografico$fIGM 205 $a3. ed 206 $a1:25000 ; proiezione conforme universale trasversa di Mercatore (E2°15-E2°22'30''/N37°40'-N37°35') 210 $aFirenze$cIGM$d1959 215 $a1 carta$ccolor.$d37 x 42 cm su foglio 51 x 62 cm 225 1 $aCarta d'Italia$v269, quadrante 1, tavoletta NO 300 $aIl meridiano di riferimento è Monte Mario, Roma 300 $aRicognizioni generali del 1927, parziali del 1943 540 1 $aFoglio 269, quadrante 1, tavoletta N. O. 610 0 $aSicilia$aCarte 710 02$aIstituto geografico militare$05005 801 0$aIT$bUNINA$gRICA$2UNIMARC 901 $aMP 912 $a990009611820403321 952 $aMP Cass.2 269, 1(4)$bIst. s. i.$fILFGE 959 $aILFGE 996 $aCenturipe$9849340 997 $aUNINA LEADER 07315nam 22007695 450 001 9910483264503321 005 20251226204321.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(BIP)13210730 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 $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,$x2945-9141 ;$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 JavaVerification 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. 330 $aThis volume containsthe full papers presentedat the 12th InternationalConf- ence on Logic for Programming, Arti'cial Intelligence, and Reasoning (LPAR), held 2-6 December 2006,in MontegoBay,Jamaica.The callfor papersattracted 108 full paper submissions, each of which were reviewed by at least three - viewers. The Program Committee accepted the 46 papers that appear in these proceedings. The conference program also included 4 invited talks, by Tom Ball of Microsoft Research, Doug Lenat of Cycorp, Roberto Nieuwenhuis of the U- versidad Polit´ ecnica de Cataluna ~ , and Allen Van Gelder of the University of California at Santa Cruz. Papers or abstracts for the invited talks are in these proceedings. In addition to the main program, the conference o'ered a short paper track, which attracted 13 submissions, of which 12 were accepted, and the Workshop on Emperically Successful Higher Order Logic (ESHOL). Thanks go to: the authors (of both accepted and rejected papers); the P- gramCommitteeandtheirreviewers;theinvitedspeakers;ChristophBenzmuller ¨ , John Harrison, and Carsten Schur ¨ mann for organizing ESHOL; Celia Alleyne- Ebanks for administering the conference in Jamaica; the Honorable Minister Phillip Paulwell of the Ministry of Commerce, Science and Technology for op- ing the conference (and Daphne Simmonds for introducing us to the minister); the Mona Institute of Applied Sciences at the University of the West Indies for their support; Microsoft Research for sponsorship of student regsitrations; the Kurt Godel ¨ Society for taking registrations; and EasyChair for hosting the review process. 410 0$aLecture Notes in Artificial Intelligence,$x2945-9141 ;$v3835 606 $aSoftware engineering 606 $aArtificial intelligence 606 $aComputer programming 606 $aComputer science 606 $aMachine theory 606 $aSoftware Engineering 606 $aArtificial Intelligence 606 $aProgramming Techniques 606 $aComputer Science Logic and Foundations of Programming 606 $aFormal Languages and Automata Theory 615 0$aSoftware engineering. 615 0$aArtificial intelligence. 615 0$aComputer programming. 615 0$aComputer science. 615 0$aMachine theory. 615 14$aSoftware Engineering. 615 24$aArtificial Intelligence. 615 24$aProgramming Techniques. 615 24$aComputer Science Logic and Foundations of Programming. 615 24$aFormal Languages and Automata Theory. 676 $a005.1/15 701 $aSutcliffe$b Geoff$01235917 701 $aVoronkov$b A$g(Andrei),$f1959-$01752961 712 12$aLPAR (Conference) 801 0$bMiAaPQ 801 1$bMiAaPQ 801 2$bMiAaPQ 906 $aBOOK 912 $a9910483264503321 996 $aLogic for programming, artificial intelligence, and reasoning$94198193 997 $aUNINA