logo资料库

Mathematical logic for computer science.pdf

发布时间：2022-06-09 发布人：admin 分类：说明书 资料大小：4.38M 资料格式：pdf 举报 版权申诉
第1页 / 共363页
第2页 / 共363页
第3页 / 共363页
第4页 / 共363页
第5页 / 共363页
第6页 / 共363页
第7页 / 共363页
第8页 / 共363页
资料共363页，剩余部分请下载后查看
    Cover
    S Title
    Title: Mathematical Logic for Computer Science, Third Edition
    Copyright
    © Springer-Verlag London 2009, 2012
    ISBN 978-1-4471-4128-0
    ISBN 978-1-4471-4129-7
    DOI 10.1007/978-1-4471-4129-7
    Dedicated For Anita
    Preface
    Audience
    Organization
    Supplementary Materials
    Third Edition
    Notation
    Acknowledgments
    Contents
    Chapter 1: Introduction
    1.1 The Origins of Mathematical Logic
    1.2 Propositional Logic
    1.3 First-Order Logic
    1.4 Modal and Temporal Logics
    1.5 Program Verification
    1.6 Summary
    1.7 Further Reading
    1.8 Exercise
    References
    Chapter 2 Propositional Logic: Formulas, Models, Tableaux
    2.1 Propositional Formulas
    2.1.1 Formulas as Trees
    2.1.2 Formulas as Strings
    2.1.3 Resolving Ambiguity in the String Representation
    2.1.4 Structural Induction
    2.1.5 Notation
    2.1.6 A Formal Grammar for Formulas
    2.2 Interpretations
    2.2.1 The Definition of an Interpretation
    2.2.2 Truth Tables
    2.2.3 Understanding the Boolean Operators
    2.2.4 An Interpretation for a Set of Formulas
    2.3 Logical Equivalence
    2.3.1 The Relationship Between ↔ and ≣
    2.3.2 Substitution
    2.3.3 Logically Equivalent Formulas
    2.4 Sets of Boolean Operators
    2.4.1 Unary and Binary Boolean Operators
    2.4.2 Adequate Sets of Operators
    2.5 Satisfiability, Validity and Consequence
    2.5.1 Decision Procedures in Propositional Logic
    2.5.2 Satisfiability of a Set of Formulas
    2.5.3 Logical Consequence
    2.5.4 Theories
    2.6 Semantic Tableaux
    2.6.1 Decomposing Formulas into Sets of Literals
    2.6.2 Construction of Semantic Tableaux
    2.6.3 Termination of the Tableau Construction
    2.6.4 Improving the Efficiency of the Algorithm
    2.7 Soundness and Completeness
    2.7.1 Proof of Soundness
    2.7.2 Proof of Completeness
    2.8 Summary
    2.9 Further Reading
    2.10 Exercises
    References
    Chapter 3 Propositional Logic: Deductive Systems
    3.1 Why Deductive Proofs?
    3.2 Gentzen System G
    3.2.1 The Relationship Between G and Semantic Tableaux
    3.3 Hilbert System H
    3.3.1 Axiom Schemes and Theorem Schemes
    3.3.2 The Deduction Rule
    3.4 Derived Rules in H
    3.5 Theorems for Other Operators
    3.6 Soundness and Completeness of H
    3.7 Consistency
    3.8 Strong Completeness and Compactness
    3.9 Variant Forms of the Deductive Systems
    3.9.1 Hilbert Systems
    3.9.2 Gentzen Systems
    3.9.3 Natural Deduction
    3.9.4 Subformula Property
    3.10 Summary
    3.11 Further Reading
    3.12 Exercises
    References
    Chapter 4 Propositional Logic: Resolution
    4.1 Conjunctive Normal Form
    4.2 Clausal Form
    4.3 Resolution Rule
    4.4 Soundness and Completeness of Resolution
    4.5 Hard Examples for Resolution
    4.5.1 Tseitin Encoding
    4.6 Summary
    4.7 Further Reading
    4.8 Exercises
    References
    Chapter 5 Propositional Logic: Binary Decision Diagrams
    5.1 Motivation Through Truth Tables
    5.2 Definition of Binary Decision Diagrams
    5.3 Reduced Binary Decision Diagrams
    5.4 Ordered Binary Decision Diagrams
    5.5 Applying Operators to BDDs
    5.6 Restriction and Quantification
    5.6.1 Restriction
    5.6.2 Quantification
    5.7 Summary
    5.8 Further Reading
    5.9 Exercises
    References
    Chapter 6 Propositional Logic: SAT Solvers
    6.1 Properties of Clausal Form
    6.2 Davis-Putnam Algorithm
    6.3 DPLL Algorithm
    6.4 An Extended Example of the DPLL Algorithm
    6.4.1 Encoding the Problem in Propositional Logic
    6.4.2 Solving the Problem with the DP Algorithm?
    6.4.3 Solving the Problem with the DPLL Algorithm
    6.5 Improving the DPLL Algorithm
    6.5.1 Branching Heuristics
    6.5.2 Non-chronological Backtracking
    6.5.3 Learning Conflict Clauses
    6.6 Stochastic Algorithms
    6.6.1 Solving the 4-Queens Problem with a Stochastic Algorithm
    6.7 Complexity of SAT
    6.8 Summary
    6.9 Further Reading
    6.10 Exercises
    References
    Chapter 7 First-Order Logic: Formulas, Models, Tableaux
    7.1 Relations and Predicates
    7.2 Formulas in First-Order Logic
    7.2.1 Syntax
    7.2.2 The Scope of Variables
    7.2.3 A Formal Grammar for Formulas
    7.3 Interpretations
    7.3.1 Closed Formulas
    7.3.2 Validity and Satisfiability
    7.3.3 An Interpretation for a Set of Formulas
    7.4 Logical Equivalence
    7.4.1 Logical Equivalences in First-Order Logic
    7.5 Semantic Tableaux
    7.5.1 Examples for Semantic Tableaux
    7.5.2 The Algorithm for Semantic Tableaux
    7.6 Soundness and Completion of Semantic Tableaux
    7.6.1 Soundness
    7.6.2 Completeness
    7.7 Summary
    7.8 Further Reading
    7.9 Exercises
    References
    Chapter 8 First-Order Logic: Deductive Systems
    8.1 Gentzen System G
    8.2 Hilbert System H
    8.3 Equivalence of H and G
    8.4 Proofs of Theorems in H
    8.5 The C-Rule
    8.6 Summary
    8.7 Further Reading
    8.8 Exercises
    References
    Chapter 9 First-Order Logic: Terms and Normal Forms
    9.1 First-Order Logic with Functions
    9.1.1 Functions and Terms
    9.1.2 Formal Grammar
    9.1.3 Interpretations
    9.1.4 Semantic Tableaux
    9.2 PCNF and Clausal Form
    9.2.1 Skolem's Theorem
    9.2.2 Skolem's Algorithm
    9.2.3 Proof of Skolem's Theorem
    9.3 Herbrand Models
    9.4 Herbrand's Theorem
    9.5 Summary
    9.6 Further Reading
    9.7 Exercises
    References
    Chapter 10 First-Order Logic: Resolution
    10.1 Ground Resolution
    10.2 Substitution
    10.3 Unification
    10.3.1 The Unification Algorithm
    10.3.2 The Occurs-Check
    10.3.3 The Correctness of the Unification Algorithm
    10.3.4 Robinson's Unification Algorithm
    10.4 General Resolution
    10.5 Soundness and Completeness of General Resolution
    10.5.1 Proof of Soundness
    10.5.2 Proof of Completeness
    10.6 Summary
    10.7 Further Reading
    10.8 Exercises
    References
    Chapter 11 First-Order Logic: Logic Programming
    11.1 From Formulas in Logic to Logic Programming
    11.2 Horn Clauses and SLD-Resolution
    11.2.1 Horn Clauses
    11.2.2 Correct Answer Substitutions for Horn Clauses
    11.2.3 SLD-Resolution
    11.3 Search Rules in SLD-Resolution
    11.3.1 Possible Outcomes when Attempting a Refutation
    11.3.2 SLD-Trees
    11.4 Prolog
    11.4.1 Depth-First Search
    11.4.2 Prolog and the Theory of Logic Programming
    11.5 Summary
    11.6 Further Reading
    11.7 Exercises
    References
    Chapter 12 First-Order Logic: Undecidability and Model Theory
    12.1 Undecidability of First-Order Logic
    12.1.1 Two-Register Machines
    12.1.2 Church's Theorem
    12.2 Decidable Cases of First-Order Logic
    12.3 Finite and Infinite Models
    12.4 Complete and Incomplete Theories
    12.5 Summary
    12.6 Further Reading
    12.7 Exercises
    References
    Chapter 13 Temporal Logic: Formulas, Models, Tableaux
    13.1 Introduction
    13.2 Syntax and Semantics
    13.2.1 Syntax
    13.2.2 Semantics
    13.2.3 Satisfiability and Validity
    13.3 Models of Time
    13.3.1 Proofs of the Correspondences
    13.4 Linear Temporal Logic
    13.4.1 Equivalent Formulas in LTL
    13.5 Semantic Tableaux
    13.5.1 The Tableau Rules for LTL
    13.5.2 Construction of Semantic Tableaux
    13.5.3 From a Semantic Tableau to a Hintikka Structure
    13.5.4 Linear Fulfilling Hintikka Structures
    13.5.5 Deciding Fulfillment of Future Formulas
    13.6 Binary Temporal Operators
    13.7 Summary
    13.8 Further Reading
    13.9 Exercises
    References
    Chapter 14 Temporal Logic: A Deductive System
    14.1 Deductive System L
    14.2 Theorems of L
    14.3 Soundness and Completeness of L
    14.4 Axioms for the Binary Temporal Operators
    14.5 Summary
    14.6 Further Reading
    14.7 Exercises
    References
    Chapter 15 Verification of Sequential Programs
    15.1 Correctness Formulas
    15.2 Deductive System HL
    15.3 Program Verification
    15.3.1 Total Correctness
    15.4 Program Synthesis
    15.4.1 Solution 1
    15.4.2 Solution 2
    15.5 Formal Semantics of Programs
    15.5.1 Weakest Preconditions
    15.5.2 Semantics of a Fragment of a Programming Language
    15.5.3 Theorems on Weakest Preconditions
    15.6 Soundness and Completeness of HL
    15.7 Summary
    15.8 Further Reading
    15.9 Exercises
    References
    Chapter 16 Verification of Concurrent Programs
    16.1 Definition of Concurrent Programs
    16.2 Formalization of Correctness
    16.2.1 An Abbreviated Algorithm
    16.3 Deductive Verification of Concurrent Programs
    16.4 Programs as Automata
    16.4.1 Modeling Concurrent Programs as Automata
    16.4.2 The State Space
    16.5 Model Checking of Invariance Properties
    16.5.1 Algorithms for Searching the State Space
    16.5.2 On-the-Fly Searching
    16.6 Model Checking of Liveness Properties
    16.7 Expressing an LTL Formula as an Automaton
    16.8 Model Checking Using the Synchronous Automaton
    16.9 Branching-Time Temporal Logic
    16.9.1 The Syntax and Semantics of CTL
    16.9.2 Model Checking in CTL
    16.10 Symbolic Model Checking
    16.11 Summary
    16.12 Further Reading
    16.13 Exercises
    References
    Appendix: Set Theory
    A.1 Finite and Infinite Sets
    A.2 Set Operators
    A.3 Sequences
    A.4 Relations and Functions
    A.5 Cardinality
    A.6 Proving Properties of Sets
    References
    Index of Symbols
    Name Index
    Subject Index
    Mathematical Logic for Computer Science
    Mordechai Ben-Ari Mathematical Logic for Computer Science Third Edition
    Prof. Mordechai (Moti) Ben-Ari Department of Science Teaching Weizmann Institute of Science Rehovot, Israel ISBN 978-1-4471-4128-0 DOI 10.1007/978-1-4471-4129-7 Springer London Heidelberg New York Dordrecht ISBN 978-1-4471-4129-7 (eBook) Library of Congress Control Number: 2012941863 1st edition: © Prentice Hall International Ltd. 1993 © Springer-Verlag London 2009, 2012 This work is subject to copyright. All rights are reserved by the Publisher, whether the whole or part of the material is concerned, specifically the rights of translation, reprinting, reuse of illustrations, recitation, broadcasting, reproduction on microfilms or in any other physical way, and transmission or information storage and retrieval, electronic adaptation, computer software, or by similar or dissimilar methodology now known or hereafter developed. Exempted from this legal reservation are brief excerpts in connection with reviews or scholarly analysis or material supplied specifically for the purpose of being entered and executed on a computer system, for exclusive use by the purchaser of the work. Duplication of this publication or parts thereof is permitted only under the provisions of the Copyright Law of the Publisher’s location, in its current version, and permission for use must always be obtained from Springer. Permissions for use may be obtained through RightsLink at the Copyright Clearance Center. Violations are liable to prosecution under the respective Copyright Law. The use of general descriptive names, registered names, trademarks, service marks, etc. in this publication does not imply, even in the absence of a specific statement, that such names are exempt from the relevant protective laws and regulations and therefore free for general use. While the advice and information in this book are believed to be true and accurate at the date of pub- lication, neither the authors nor the editors nor the publisher can accept any legal responsibility for any errors or omissions that may be made. The publisher makes no warranty, express or implied, with respect to the material contained herein. Printed on acid-free paper Springer is part of Springer Science+Business Media (www.springer.com)
    For Anita
    Preface Students of science and engineering are required to study mathematics during their first years at a university. Traditionally, they concentrate on calculus, linear algebra and differential equations, but in computer science and engineering, logic, combi- natorics and discrete mathematics are more appropriate. Logic is particularly im- portant because it is the mathematical basis of software: it is used to formalize the semantics of programming languages and the specification of programs, and to ver- ify the correctness of programs. Mathematical Logic for Computer Science is a mathematics textbook, just as a first-year calculus text is a mathematics textbook. A scientist or engineer needs more than just a facility for manipulating formulas and a firm foundation in mathematics is an excellent defense against technological obsolescence. Tempering this require- ment for mathematical competence is the realization that applications use only a fraction of the theoretical results. Just as the theory of calculus can be taught to students of engineering without the full generality of measure theory, students of computer science need not be taught the full generality of uncountable structures. Fortunately (as shown by Raymond M. Smullyan), tableaux provide an elegant way to teach mathematical logic that is both theoretically sound and yet sufficiently ele- mentary for the undergraduate. Audience The book is intended for undergraduate computer science students. No specific mathematical knowledge is assumed aside from informal set theory which is sum- marized in an appendix, but elementary knowledge of concepts from computer sci- ence (graphs, languages, programs) is used. vii
    分享到：
    赞 收藏

    相关推荐

    资料库

    课程资源

    共收录17145份资料，累计13个分类，关注成员有19位，主要包括：PHP,网络管理,网页制作,Java,.Net,数据库,3G/移动开发,C/C++,游戏开发,嵌入式,讲义,软件测试,专业指导

    热门标签

    PHP 网络管理 网页制作 Java .Net 数据库 3G/移动开发 C/C++ 游戏开发 嵌入式 讲义 软件测试 专业指导

    最新资料