計算世界中的迷人國度

《計算世界中的迷人國度》是1999年出版的圖書，作者是Wos，Larry;Pieper，GailW.;。

基本介紹

• 中文名：計算世界中的迷人國度
• 作者：Wos，Larry、Pieper，GailW.
• 出版時間：1999年12月
• 出版社：WorldScie
• 頁數：587 頁
• ISBN：9789810239107
• 定價：747 元

內容簡介

This text demonstrates - through examples and puzzles and intriguing questions - how to make your computer reason logically. To help you, the book includes a CD-ROM with OTTER, the world's most powerful general-purpose reasoning program. The automation of reasoning has advanced markedly in the last few decades of the 20th century, and this book discusses some of the remarkable successes that automated reasoning programs have had in tackling challenging problems in mathematics, logic, program verification and circuit design. Because the intended audience includes students and teachers, the book provides many exercises (with hints and answers), as well as tutorial chapters that gently introduce readers to the field of logic and to automated reasoning in general. For more advanced researchers, the book presents challenging questions, many of which are still unsolved.

目錄

Frewrd

Preface

Chaper 1 he Meu, he Map, ad he Magic

1.1 he Meu fr he Grad Feas

1.2 he Bk's Audiece

1.3 he Map

1.4 Reasig i Review

1.5 Reasig by Cmpuer versus Reasig by a Pers . .

1.6 bsacles he Effecive Aumai f Reasig . . .

1.6.1 Laguage

1.6.2 Iferece Rules

1.6.3 Assigme Cmplei

1.6.4 Sraeg

1.6.5 Redudacy

1.6.6 Specific versus Geeral Ifrmai

1.6.7 Cclusi Reei

1.6.8 Cclusi Geerai

1.6.9 Iadequae Fcus

1.6.10 Cclusi Repeii

1.6.11 Redudacy-Crl rasfrmais

1.6.12 Size f Deduci Sep

1.6.13 Mearules fr Prgram Use

1.6.14 Idexig

1.7 Paradigms fr Reasig ad fr Research

1.8 he Fuure f Aumaed Reasig

Chaper 2 Learig Lgic by Example

2.1 ad, r, , if-he (implies)

2.2 A Laguage fr Aumaed Reasig Prgrams

2.2.1 Predicaes ad Csas

2.2.2 Variables

2.2.3 Fucis

2.3 Cmbiais f r wih ad, Cmplex if-he, ad

DeMrga's Laws

2.4 Assumpis ad Axims, ypes f Reasig, ad Prf

2.4.1 Assumpis ad Axims

2.4.2 ypes f Reasig, Iferece Rules

2.4.3 Prf

2.5 Summary

Chaper 3 Aumaed Reasig i Full

3.1 Lgic

3.1.1 ad

3.1.2 r

3.1.3

3.1.4 if-he ad implies

3.1.5 is-equivale-

3.1.6 Relaiships ad Laws i Lgic

3.2 A Laguage Udersd by a Aumaed Reasig Prgram .

3.2.1 Variables

3.3 Submiig a Prblem a Reasig Prgram

3.3.1 Assumpis ad Axims

3.3.2 Special Facs ad he Special Hyphesis

3.3.3 Deial f he Gal r herem

3.4 Iferece Rules

3.4.1 Uificai

3.4.2 Biary Reslui

3.4.3 UR-Reslui

3.4.4 Hyperreslui

3.4.5 Paramdulai

3.4.6 her Iferece Rules

3.5 he Empy Clause

3.6 Prf by Cradici

3.7 Demdulai

3.8 Subsumpi

3.9 Sraegy

3.9.1 he Se f Suppr Sraegy

3.9.2 Weighig

3.9.3 Ui Preferece Sraegy

3.9.4 her Sraegies

……

Chaper 4 Lgic Circui Desig

Chaper 5 Lgic Circui Validai

Chaper 6 Research i Mahemaics

Chaper 7 Research i Frmal Lgic

Chaper 8 he Frmal reame f Aumaed Reasig

Chaper 9 Ws's Biased Guide fr he Effecive Use f ER

Chaper 10 A Auhr's Appraisal f His Papers

Chaper 11 pe Quesis, Hard Prblems, Iriguig Challeges

Chaper 12 Epilgue ad Afer-Dier Liqueur

Appedix A Feaurig Ipu Files, Prfs, ad upu File Fragmes

Refereces

Idex