编程、人工智能与推理用逻辑Logic for programming, artificial intelligence, and reasoning
点此进入淘宝搜索页搜索分类: 图书,计算机/网络,人工智能,
作者： Miki Hermann著
出 版 社： 湖南文艺出版社
出版时间： 2006-12-1字数：版次： 1页数： 588印刷时间： 2006/12/01开本：印次：纸张： 胶版纸I S B N ： 9783540482819包装： 平装编辑推荐
The LNCS series reports state-of-the-art results in computer science research, development, and education, at a high level and in both printed and electronic form. Enjoying tight cooperation with the R&D community, with numerous individuals, as well as with prestigious organizations and societies, LNCS has grown into the most comprehensive computer science resarch forum available.
The scope of LNCS, including its subseries LNAI, spans the whole range of computer science and information technology including interdisciplinary topics in a variety of application fields. The type of material publised traditionally includes.
-proceedings(published in time for the respective conference)
-post-proceedings(consisting of thoroughly revised final full papers)
-research monographs(which may be basde on outstanding PhD work, research projects, technical reports, etc.)
内容简介
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 Computability
Deciding Satisfiability of Positive Second Order JoinabilityFormulae
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
……
Author Index
