編程、人工智能與推理用邏輯Logic for programming, artificial intelligence, and reasoning

內(nèi)容概要

This book constitutes the refereed proceedings of the 13th International Conference on Logic for Programming, Artificial Intelligence, and Reasoning, LPAR 2006, held in Phnom Penh, Cambodia in November 2006.　　The 38 revised full papers presented together with 1 invited talk were carefully reviewed and selected from 96 submissions. The papers address all current issues in logic programming, logic-based program manipulation, formal method, automated reasoning, and various kinds of AI logics.

書籍目錄

Higher-Order Termination: From Kruskal to ComputabilityDeciding Satisfiability of Positive Second Order Joinability　FormulaeSAT Solving for Argument FilteringsInductive Decidability Using Implicit InductionMatching Modulo Superdevelopments Application to Second-Order MatchingDerivational Complexity of Knuth-Bendix Orders RevisitedA Characterization of Alternating Log Time by First Order Functional ProgramsCombining Typing and Size Constraints for Checking the Termination of Higher-Order Conditional Rewrite SystemsOn a Local-Step Cut-Elimination Procedure for the Intuitionistic Sequent CalculusModular Cut-Elimination: Finding Proofs or CounterexamplesAn Executable Formalization of the HOL/Nuprl Connection in the Metalogical Framework TwelfA Semantic Completeness Proof for TaMeDSaturation Up to Redundancy for Tableau and Sequent CalculiBranching-Time Temporal Logic Extended with Qualitative Presburger ConstraintsCombining Supervaluation and Degree Based Reasoning Under Vagueness.A Comparison of Reasoning Techniques for Querying Large Description Logic ABoxesA Local System for Intuitionistic LogicCIC": Type-Based Termination of Recursive Definitions in the Calculus of Inductive ConstructionsReducing Nondeterminism in the Calculus of Structures ..A Relaxed Approach to Integrity and Inconsistency in DatabasesOn Locally Checkable PropertiesDeciding Key Cycles for Security ProtocolsAutomating Verification of Loops by ParallelizationOn Computing Fixpoints in Well-Structured Regular Model Checking with Applications to Lossy Channel SystemsVerification Condition Generation Via Theorem ProvingAn Incremental Approach to Abstraction-Carrying CodeContext-Sensitive Multivariant Assertion Checking in Modular Programs……Author Index

圖書封面

評論、評分、閱讀與下載

---

    編程、人工智能與推理用邏輯Logic for programming, artificial intelligence, and reasoning PDF格式下載

---