编程、人工智能与推理用逻辑Logic for programming, artificial intelligence, and reasoning

出版时间：2006-12  出版社：Springer-Verlag New York Inc  作者：Hermann, Miki (EDT)/ Voronkov, Andrei (EDT)  页数：588  

内容概要

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