自动推理Automated reasoning
点此进入淘宝搜索页搜索分類: 图书,计算机/网络,人工智能,
作者： Rajeev Gore 著
出 版 社： 湖南文艺出版社
出版时间： 2001-12-1字数：版次： 1页数： 708印刷时间： 2001/08/01开本：印次：纸张： 胶版纸I S B N ： 9783540422549包装： 平装内容简介
This book constitutes the refereed proceedings of the First International Joint Conference on Automated Reasoning, IJCAR 2001, held in Siena, Italy, in June 2001. The 37 research papers and 19 system descriptions presented together with three invited contributions were carefully reviewed and selected from a total of 112 submissions. The book offers topical sections on description, modal, and temporal logics; saturation based theorem proving, applications, and data structures; logic programming and nonmonotonic reasoning; propositional satisfiability and quantified Boolean logic; logical frameworks, higher-order logic, and interactive theorem proving; equational theorem proving and term rewriting; tableau, sequent, and natural deduction calculi and proof theory; automata, specification, verification, and logics of programs; and nonclassical logics.
目录
Invited Talks
Program Termination Analysis by Size-Change Graphs
SET Cardholder Registration: The Secrecy Proofs
Algorithms, Datastructures, and Other Issues in Efficient Automated Deduction
Description, Modal, and Temporal Logics
The Description Logic A~CA/'TiR+ Extended with Concrete Domains:
A Practically Motivated Approach
NExpTIME-Complete Description Logics with Concrete Domains
Exploiting Pseudo Models for TBox and ABox Reasoning in Expressive
Description Logics
The Hybrid #-Calculus
The Inverse Method Implements the Automata Approach for Modal
Satisfiability
Deduction-Based Decision Procedure for a Clausal Miniscoped Fragment of FTL
Tableaux for Temporal Description Logic with Constant Domains
Free-Variable Tableaux for Constant-Domain Quantified Modal Logics
with Rigid and Non-rigid Designation
Saturation Based Theorem
Proving, Applications, Instructing Equational Set-Reasoning with Otter
NP-Completeness of Refutability by Literal-Once Resolution
Ordered Resolution vs. Connection Graph Resolution
A Model-Based Completeness Proof of Extended Narrowing and Resolution
A Resolution-Based Decision Procedure for the Two-Variable Fragment with Equality
Superposition and Chaining for Totally Ordered Divisible Abelian Groups
Context Trees
On the Evaluation of Indexing Techniques for Theorem Proving 25
Logic Programming and Nonmonotonic Reasoning
Preferred Extensions of Argumentation Frameworks: Query, Answering and Computation
Bunched Logic Programming
A Top-Down Procedure for Disjunctive Well-Founded Semantics
A Second-Order Theorem Prover Applied to Circumscription
NoMoRe: A System for Non-monotonic Reasoning with Logic Programs under Answer Set Semantics 32
Propositional Satisfiabiilty and QuanfifiedBoolean Logic
Logical Franeworklss Higher-Qrder Logic Interactive Theorem proving
Semantic Guidence
Noncassical Logics
Author Index
