LEADER 04956nam 2200637 a 450 001 9910484466603321 005 20200520144314.0 010 $a3-540-48282-2 024 7 $a10.1007/11916277 035 $a(CKB)1000000000283913 035 $a(SSID)ssj0000318695 035 $a(PQKBManifestationID)11249851 035 $a(PQKBTitleCode)TC0000318695 035 $a(PQKBWorkID)10336055 035 $a(PQKB)11028466 035 $a(DE-He213)978-3-540-48282-6 035 $a(MiAaPQ)EBC3068545 035 $a(PPN)123139430 035 $a(EXLCZ)991000000000283913 100 $a20060919d2006 uy 0 101 0 $aeng 135 $aurnn#008mamaa 181 $ctxt 182 $cc 183 $acr 200 10$aLogic for programming, artificial intelligence, and reasoning $e13th international conference, LPAR 2006, Phnom Penh, Cambodia, November 13-17, 2006 : proceedings /$fMiki Hermann, Andrei Voronkov (eds.) 205 $a1st ed. 2006. 210 $aBerlin ;$aNew York $cSpringer$dc2006 215 $a1 online resource (XIV, 592 p.) 225 1 $aLNCS sublibrary. SL 7, Artificial intelligence 225 1 $aLecture notes in computer science,$x0302-9743 ;$v4246.$aLecture notes in artificial intelligence 300 $aBibliographic Level Mode of Issuance: Monograph 311 $a3-540-48281-4 320 $aIncludes bibliographical references and index. 327 $aHigher-Order Termination: From Kruskal to Computability -- Deciding Satisfiability of Positive Second Order Joinability Formulae -- SAT Solving for Argument Filterings -- Inductive Decidability Using Implicit Induction -- Matching Modulo Superdevelopments Application to Second-Order Matching -- Derivational Complexity of Knuth-Bendix Orders Revisited -- A Characterization of Alternating Log Time by First Order Functional Programs -- Combining Typing and Size Constraints for Checking the Termination of Higher-Order Conditional Rewrite Systems -- On a Local-Step Cut-Elimination Procedure for the Intuitionistic Sequent Calculus -- Modular Cut-Elimination: Finding Proofs or Counterexamples -- An Executable Formalization of the HOL/Nuprl Connection in the Metalogical Framework Twelf -- A Semantic Completeness Proof for TaMeD -- Saturation Up to Redundancy for Tableau and Sequent Calculi -- Branching-Time Temporal Logic Extended with Qualitative Presburger Constraints -- Combining Supervaluation and Degree Based Reasoning Under Vagueness -- A Comparison of Reasoning Techniques for Querying Large Description Logic ABoxes -- A Local System for Intuitionistic Logic -- CIC : Type-Based Termination of Recursive Definitions in the Calculus of Inductive Constructions -- Reducing Nondeterminism in the Calculus of Structures -- A Relaxed Approach to Integrity and Inconsistency in Databases -- On Locally Checkable Properties -- Deciding Key Cycles for Security Protocols -- Automating Verification of Loops by Parallelization -- On Computing Fixpoints in Well-Structured Regular Model Checking, with Applications to Lossy Channel Systems -- Verification Condition Generation Via Theorem Proving -- An Incremental Approach to Abstraction-Carrying Code -- Context-Sensitive Multivariant Assertion Checking in Modular Programs -- Representation of Partial Knowledge and Query Answering in Locally Complete Databases -- Sequential, Parallel, and Quantified Updates of First-Order Structures -- Representing Defaults and Negative Information Without Negation-as-Failure -- Constructing Camin-Sokal Phylogenies Via Answer Set Programming -- Automata for Positive Core XPath Queries on Compressed Documents -- Boolean Rings for Intersection-Based Satisfiability -- Theory Instantiation -- Splitting on Demand in SAT Modulo Theories -- Delayed Theory Combination vs. Nelson-Oppen for Satisfiability Modulo Theories: A Comparative Analysis -- Automatic Combinability of Rewriting-Based Satisfiability Procedures -- To Ackermann-ize or Not to Ackermann-ize? On Efficiently Handling Uninterpreted Function Symbols in -- Lemma Learning in the Model Evolution Calculus. 410 0$aLecture notes in computer science ;$v4246. 410 0$aLecture notes in computer science.$pLecture notes in artificial intelligence. 410 0$aLNCS sublibrary.$nSL 7,$pArtificial intelligence. 517 3 $aLPAR 2006 606 $aLogic programming$vCongresses 606 $aAutomatic theorem proving$vCongresses 606 $aArtificial intelligence$vCongresses 615 0$aLogic programming 615 0$aAutomatic theorem proving 615 0$aArtificial intelligence 676 $a006.3 701 $aHermann$b Miki$f1958-$01760417 701 $aVoronkov$b A$g(Andrei),$f1959-$01752961 712 12$aLPAR (Conference) 801 0$bMiAaPQ 801 1$bMiAaPQ 801 2$bMiAaPQ 906 $aBOOK 912 $a9910484466603321 996 $aLogic for programming, artificial intelligence, and reasoning$94199379 997 $aUNINA