HOME > 상세정보


Automated Theorem Proving : theory and practice

Automated Theorem Proving : theory and practice

Newborn, Monty
서명 / 저자사항
Automated Theorem Proving theory and practice / Monty Newborn.
New York :   Springer-Verlag,   2001.  
xiii, 231p. : ill. ; 24cm + 1 CD-ROM.
Includes bibliographical references and index Includes index
000 00624namuu2200193 a 4500
001 000001072190
005 20020523144857
008 020507s2001 nyua 01 0aeng d
020 ▼a 0387950753
040 ▼d 244002
049 ▼l 151125165
082 0 4 ▼a 004.01/5113 ▼2 21
090 ▼a 004.015113 ▼b N534a
100 1 ▼a Newborn, Monty
245 1 0 ▼a Automated Theorem Proving ▼b theory and practice / ▼c Monty Newborn.
260 ▼a New York : ▼b Springer-Verlag, ▼c 2001.
300 ▼a xiii, 231p. : ▼b ill. ; ▼c 24cm + ▼e 1 CD-ROM.
504 ▼a Includes bibliographical references and index ▼a Includes index


No. 소장처 청구기호 등록번호 도서상태 반납예정일 예약 서비스
No. 1 소장처 세종학술정보원/과학기술실/ 청구기호 004.015113 N534a 등록번호 151125165 도서상태 대출가능 반납예정일 예약 서비스 C M



1 A Brief Introduction to COMPILE, HERBY, and THEO.- 1.1 COMPILE.- 1.1.1 Creating an executable version of COMPILE.- 1.1.2 Running COMPILE.- 1.2 HERBY.- 1.2.1 Creating an executable version of HERBY.- 1.2.2 Running HERBY.- 1.3 THEO.- 1.3.1 Creating an executable version of THEO.- 1.3.2 Running THEO.- 1.4 The Accompanying Software.- Exercises for Chapter 1.- 2 Predicate Calculus, Well-Formed Formulas and Theorems.- 2.1 The Syntax of Well-Formed Formulas.- 2.2 Examples of Well-Formed Formulas.- 2.3 Creating Well-Formed Formulas from Statements in English.- 2.4 Interpretations of Well-Formed Formulas.- 2.5 A Set of Axioms to Prove Theorems in Group Theory.- 2.6 An Axiom System for Euclidean Geometry.- Exercises for Chapter 2.- 3 COMPILE: Transforming Well-Formed Formulas to Clauses.- 3.1 The Transformation Procedure of COMPILE.- 3.2 Using COMPILE.- 3.3 Examples of the Transformation of Wffs to Clauses.- Exercises for Chapter 3.- 4 Inference Procedures.- 4.1 An Informal Introduction to Binary Resolution and Binary Factoring.- 4.2 The Processes of Substitution and Unification.- 4.3 Subsumption.- 4.4 The Most General Unifier.- 4.5 Determining All Binary Resolvents of Two Clauses.- 4.6 Merge Clauses.- 4.7 Determining All Binary Factors of a Clause.- 4.8 A Special Case of Binary Resolution: Modus Ponens.- 4.9 Clauses and Subsumption.- 4.10 Logical Soundness.- 4.11 Base Clauses and Inferred Clauses.- Exercises for Chapter 4.- 5 Proving Theorems by Contracting Closed Semantic Trees.- 5.1 The Herbrand Universe of a Set of Clauses.- 5.2 The Herbrand Base of a Set of Clauses.- 5.3 An Interpretation on the Herbrand Base.- 5.4 Establishing the Unsatisfiability of a Set of Clauses.- 5.5 Semantic Trees.- 5.6 Noncanonical Semantic Trees.- Exercises for Chapter 5.- 6 Resolution-Refutation Proofs.- 6.1 Examples of Resolution-Refutation Proofs.- 6.2 The Depth and Length of Resolution-Refutation Proofs.- 6.3 Obtaining a Resolution-Refutation Proof from a Semantic Tree.- 6.4 Linear Proofs.- 6.5 Restrictions on the Form of Linear Proofs.- 6.6 The Lifting Lemma.- 6.7 Linear Proofs and Factoring.- Exercises for Chapter 6.- 7 HERBY: A Semantic-Tree Theorem Prover.- 7.1 Heuristics for Selecting Atoms.- 7.2 Additional Heuristics.- 7.2.1 List ordering heuristics.- 7.2.2 Preliminary phase (Phase 0): Base clause resolution heuristic (BCRH).- 7.2.3 Heuristic limiting the number of literals in a clause.- 7.2.4 Heuristic limiting the number of terms in a literal.- 7.2.5 Tree pruning heuristic.- 7.3 Assigning a Hash Code to a Literal and to a Clause.- 7.4 The Overall Algorithm.- 7.5 Obtaining a Resolution-Refutation Proof.- Exercises for Chapter 7.- 8 Using HERBY.- 8.1 Proving Theorems with HERBY: The Input File.- 8.2 HERBY's Convention on Naming the Output File.- 8.3 The Options Available to the User.- 8.3.1 Option to prove a set of theorems.- 8.3.2 Obtaining help by typing"?".- 8.4 User Interaction During the Construction.- 8.5 Option Examples.- 8.6 The Printout Produced by HERBY.- 8.7 A Second Example, the Printout Produced Using the r1 Option.- Exercises for Chapter 8.- 9 THEO: A Resolution-Refutation Theorem Prover.- 9.1 Iteratively Deepening Depth-First Search and Linear Proofs.- 9.2 Searching for a Linear-Merge Proof.- 9.3 Searching for a Linear-nc Proof.- 9.4 Searching for a Linear-Merge-nc Proof.- 9.5 The Extended Search Strategy.- 9.6 Bounding the Number of Literals in a Clause.- 9.7 Bounding the Number of Terms in a Literal.- 9.8 Bounding the Number of Different Variables in an Inference.- 9.9 Ordering Clauses at Each Node.- 9.10 A Hash Table that Stores Information About Clauses.- 9.10.1 Assigning a hash code to a literal.- 9.10.2 Assigning a hash code to a clause.- 9.10.3 Entering clauses in clause_hash_table.- 9.11 Using Entries in clause_hash_table.- 9.12 Unit Clauses.- 9.12.1 Obtaining a contradiction.- 9.12.2 Unit hash table resolutions.- 9.13 Assigning Hash Codes to Instances and Variants of Unit Clauses.- 9.14 Other Hash Codes Generated.-

정보제공 : Aladin

관련분야 신착자료

김효곤 (2022)