Book:M. Ben-Ari/Mathematical Logic for Computer Science

From ProofWiki
Jump to navigation Jump to search

M. Ben-Ari: Mathematical Logic for Computer Science

Published $\text {1993}$, Prentice Hall

ISBN 0-13-564139-X


Subject Matter


Contents

Preface
1. Introduction
1.1 The origins of mathematical logic
1.2 Propositional and predicate calculus
1.3 Theorem provers and logic programming
1.4 Non-standard logics
2. Propositional calculus
2.1 Boolean operators
2.2 Propositional formulas
2.3 Boolean interpretations
2.4 Logical equivalence and substitution
2.5 Satisfiability, validity and consequence
2.6 Semantic tableaux
2.7 Deductive proofs
2.8 Gentzen systems
2.9 Hilbert systems
2.10 Resolution
2.11 Variant forms of the deductive systems*
2.12 Complexity*
2.13 Exercises
3. Predicate calculus
3.1 Relations and predicates
3.2 predicate formulas
3.3 Interpretations
3.4 Logical equivalence and substitution
3.5 Semantic tableaux
3.6 Deductive proofs
3.7 Functions and terms
3.8 Clausal form
3.9 Herbrand models
3.10 Finite and infinite models*
3.11 Solvable cases of the decision problem*
3.12 Exercises
4. Resolution and logic programming
4.1 Ground resolution
4.2 Substitution
4.3 Unification
4.4 General resolution
4.5 Theories and theorem proving
4.6 Logic programming
4.7 Prolog
4.8 Parallel logic programming*
4.9 Complete and decidable theories*
4.10 Exercises
5. Temporal logic
5.1 Introduction
5.2 Syntax and semantics
5.3 A deductive system for linear PTL
5.4 Semantic tableaux
5.5 Soundness and completeness
5.6 Applications of temporal logic*
5.7 Extensions of temporal logic*
5.8 Exercises
6. Formalization of programs
6.1 Introduction
6.2 Axiomatisation of a language
6.3 Proving programs
6.4 Formal specification with $Z$
6.5 Exercises
7. Further reading
7.1 Mathematical logic
7.2 Complexity
7.3 Resolution and logic programming
7.4 Temporal logic
7.5 Formalization of programs
Bibliography
Appendices
A. Set theory
A.1 Finite and infinite sets
A.2 Set operators
A.3 Ordered sets
A.4 Relations and functions
A.5 Cardinality
A.6 Proving properties of sets
B. Algorithm implementation
C. Hints
Index


Next


Further Editions


Errata

Binary Logical Connective is Self-Inverse iff Exclusive Or

Chapter $2$: Propositional Calculus: $2.1$. Boolean Operations

Let $\circ$ be a binary logical connective.

Then:

$\paren {p \circ q} \circ q \dashv \vdash p$

if and only if $\circ$ is the exclusive or operator.

$\mathsf{XOR}$ is also essential since it is the only operator having an inverse, namely itself
$\paren {p \oplus q} \oplus q = p$


Source work progress

Retrieved from "https://proofwiki.org/w/index.php?title=Book:M._Ben-Ari/Mathematical_Logic_for_Computer_Science&oldid=448858"