Symbolic Logic and Mechanical Theorem Proving

Inbunden, Engelska, 1973

Av Chin-Liang Chang, Richard Char-Tung Lee, CA) Chang, Chin-Liang (Lockheed Missiles & Space Company, Inc., Menlo Park, Taiwan) Lee, Richard Char-Tung (National Tsing Hua University, Hsinchu

849 kr

Beställningsvara. Skickas inom 10-15 vardagar

Fri frakt för medlemmar vid köp för minst 249 kr.

Finns i fler format (1)

Häftad

699 kr

Skickas inom 10-15 vardagar

This book contains an introduction to symbolic logic and a thorough discussion of mechanical theorem proving and its applications. The book consists of three major parts. Chapters 2 and 3 constitute an introduction to symbolic logic. Chapters 4-9 introduce several techniques in mechanical theorem proving, and Chapters 10 an 11 show how theorem proving can be applied to various areas such as question answering, problem solving, program analysis, and program synthesis.

Produktinformation

Utgivningsdatum1973-06-15
Mått152 x 229 x 29 mm
Vikt640 g
FormatInbunden
SpråkEngelska
Antal sidor331
FörlagElsevier Science
ISBN9780121703509

Tillhör följande kategorier

Matematikens grunder inom Naturvetenskap och teknik

PrefaceAcknowledgments1. Introduction1.1 Artificial Intelligence, Symbolic Logic, and Theorem Proving1.2 Mathematical BackgroundReferences2. The Propositional Logic2.1 Introduction2.2 Interpretations of Formulas in the Propositional Logic2.3 Validity and Inconsistency in the Propositional Logic2.4 Normal Forms in the Propositional Logic2.5 Logical Consequences2.6 Applications of the Propositional LogicReferencesExercises3. The First-Order Logic3.1 Introduction3.2 Interpretations of Formulas in the First-Order Logic3.3 Prenex Normal Forms in the First-Order Logic3.4 Applications of the First-Order LogicReferencesExercises4. Herbrand's Theorem4.1 Introduction4.2 Skolem Standard Forms4.3 The Herbrand Universe of a Set of Clauses4.4 Semantic Trees4.5 Herbrand's Theorem4.6 Implementation of Herbrand's TheoremReferencesExercises5. The Resolution Principle5.1 Introduction5.2 The Resolution Principle for the Propositional Logic5.3 Substitution and Unification5.4 Unification Algorithm5.5 The Resolution Principle for the First-Order Logic5.6 Completeness of the Resolution Principle5.7 Examples Using the Resolution Principle5.8 Deletion StrategyReferencesExercises6. Semantic Resolution and Lock Resolution6.1 Introduction6.2 An Informal Introduction to Semantic Resolution6.3 Formal Definitions and Examples of Semantic Resolution6.4 Completeness of Semantic Resolution6.5 Hyperresolution and the Set-of-Support Strategy: Special Cases of Semantic Resolution6.6 Semantic Resolution Using Ordered Clauses6.7 Implementation of Semantic Resolution6.8 Lock Resolution6.9 Completeness of Lock ResolutionReferencesExercises7. Linear Resolution7.1 Introduction7.2 Linear Resolution7.3 Input Resolution and Unit Resolution7.4 Linear Resolution Using Ordered Clauses and the Information of Resolved Literals7.5 Completeness of Linear Resolution7.6 Linear Deduction and Tree Searching7.7 Heuristics in Tree Searching7.8 Estimations of Evaluation FunctionsReferencesExercises8. The Equality Relation8.1 Introduction8.2 Unsatisfiability under Special Classes of Models8.3 Paramodulation—An Inference Rule for Equality8.4 Hyperparamodulation8.5 Input and Unit Paramodulations8.6 Linear ParamodulationReferencesExercises9. Some Proof Procedures Based on Herbrand's Theorem9.1 Introduction9.2 The Prawitz Procedure9.3 The V-Resolution Procedure9.4 Pseudosemantic Trees9.5 A Procedure for Generating Closed Pseudosemantic Trees9.6 A Generalization of the Splitting Rule of Davis and PutnamReferencesExercises10. Program Analysis10.1 Introduction10.2 An Informal Discussion10.3 Formal Definitions of Programs10.4 Logical Formulas Describing the Execution of a Program10.5 Program Analysis by Resolution10.6 The Termination and Response of Programs10.7 The Set-of-Support Strategy and the Deduction of the Halting Clause10.8 The Correctness and Equivalence of Programs10.9 The Specialization of ProgramsReferencesExercises11. Deductive Question Answering, Problem Solving, and Program Synthesis11.1 Introduction11.2 Class A Questions11.3 Class B Questions11.4 Class C Questions11.5 Class D Questions11.6 Completeness of Resolution for Deriving Answers11.7 The Principles of Program Synthesis11.8 Primitive Resolution and Algorithm A (A Program-Synthesizing Algorithm)11.9 The Correctness of Algorithm A11.10 The Application of Induction Axioms to Program Synthesis11.11 Algorithm A (An Improved Program-Synthesizing Algorithm)ReferencesExercises12. Concluding RemarksReferencesAppendix AA.1 A Computer Program Using Unit Binary ResolutionA.2 Brief Comments on the ProgramA.3 A Listing of the ProgramA.4 IllustrationsReferencesAppendix BBibliographyIndex