書誌事項

Deduction systems

Rolf Socher-Ambrosius, Patricia Johann

(Graduate texts in computer science)

Springer, c1997

大学図書館所蔵 件 / 20

この図書・雑誌をさがす

注記

Includes bibliographical references (p. [199]-200) and index

内容説明・目次

内容説明

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.

目次

  • Contents: Mathematical Preliminaries
  • Syntax of first-order languages
  • Semantics of first-order languages
  • The Gentzen calculus G. Normal Forms and Herbrand's Theorem
  • Resolution and unification
  • Improved Deduction efficiency
  • Resolution in sorted logic.

「Nielsen BookData」 より

関連文献: 1件中  1-1を表示

詳細情報

ページトップへ