ABE-IPSABE HOLDINGABE BOOKS
English Polski
Dostęp on-line

Książki

0.00 PLN
Schowek (0) 
Schowek jest pusty
Automated Theorem Proving: Theory and Practice

Automated Theorem Proving: Theory and Practice

Autorzy
Wydawnictwo Springer, Berlin
Data wydania
Liczba stron 231
Forma publikacji książka w twardej oprawie
Język angielski
ISBN 9780387950754
Kategorie Logika matematyczna
Zapytaj o ten produkt
E-mail
Pytanie
 
Do schowka

Opis książki

This text and software package introduces the reader to automated theorem proving and provides two approaches implemented as easy-to-use programs. The two approaches studied are semantic tree theorem proving and resolution-refutation theorem proving. The first chapters introduce the reader to first-order predicate calculus, well-formed formulae, and their transformation to clauses (implemented in a third program provided on diskette). Then the author shows how the two methods work and provides numerous examples for readers to try their hand at theorem-proving experiments. Each chapter comes with exercises intended to familiarise the readers with the ideas and with the software, and answers are provided to many of the problems.

Automated Theorem Proving: Theory and Practice

Spis treści

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.-

Polecamy również książki

Strony www Białystok Warszawa
801 777 223