Deduction Systems
Deduction Systems
复制标题
扣除系统
DOI：
10.1007/978-1-4612-2266-8
复制
发表时间：
1996
期刊：
影响因子：
--
通讯作者：
Patricia Johann
中科院分区：
文献类型：
--
作者：
Rolf Socher;Patricia Johann
这研究生水平的文本提供了自动演绎的基本概念和方法的理论处理。通过介绍一个涵盖一阶逻辑中归结定理证明的说明，为第一次接触这门学科的学生提供了一个完备的说明。这两个根岑式微积分和反驳方法被称为决议详细处理。各种策略修剪分辨率搜索空间，如线性，超和有序分辨率。许多例子来说明所讨论的例子。因此，学生会发现这是一个容易获得的介绍这个问题。
This graduate-level text offers a theoretical treatment of the fundamental concepts and methods of automated deduction. By presenting an account which covers resolution theorem-proving in order-sorted first-order logic it provides a self-contained account suitable for students coming to the subject for the first time. Both Gentzen-style sequent calculi and the refutation method known as resolution are treated in detail. Various strategies for pruning resolution search spaces, such as linear, hyper- and ordered resolution are covered. Numerous examples are presented to illustrate the examples discussed. As a result students will find this a readily accessible introduction to this subject.