Skip to main content
Disciplines
Automotive Business IT + Informatics Construction + Real Estate Electrical Engineering + Electronics Energy + Sustainability Insurance + Risk Finance + Banking Management + Leadership Marketing + Sales Mechanical Engineering + Materials
Events
DE
EN
Books
Journals
Topic Page
Marketing
Start single access now
Access for companies
EXTENDED SEARCH
Log in
Top

2012 | Book

Introduction Read chapter Read first chapter

Mathematical Logic for Computer Science

Author: Mordechai Ben-Ari

Publisher: Springer London

Part of: Springer Professional "Wirtschaft+Technik" , Springer Professional "Technik" , Springer Professional "Wirtschaft"

Login to get access
insite
SEARCH

About this book

Mathematical Logic for Computer Science is a mathematics textbook with theorems and proofs, but the choice of topics has been guided by the needs of students of computer science. The method of semantic tableaux provides an elegant way to teach logic that is both theoretically sound and easy to understand. The uniform use of tableaux-based techniques facilitates learning advanced logical systems based on what the student has learned from elementary systems.

The logical systems presented are: propositional logic, first-order logic, resolution and its application to logic programming, Hoare logic for the verification of sequential programs, and linear temporal logic
for the verification of concurrent programs.

The third edition has been entirely rewritten and includes new chapters on central topics of modern computer science: SAT solvers and model checking.

Table of Contents

Frontmatter
Chapter 1. Introduction
Abstract
Logic formalizes valid methods of reasoning. The study of logic was begun by the ancient Greeks whose educational system stressed competence in reasoning and in the use of language. Along with rhetoric and grammar, logic formed part of the trivium, the first subjects taught to young people. Rules of logic were classified and named. The most widely known set of rules are the syllogisms; here is an example of one form of syllogism:
Premise All rabbits have fur.
Premise Some pets are rabbits.
Conclusion Some pets have fur.
If both premises are true, the rules ensure that the conclusion is true.
Mordechai Ben-Ari
Chapter 2. Propositional Logic: Formulas, Models, Tableaux
Abstract
Propositional logic is a simple logical system that is the basis for all others. Propositions are claims like ‘one plus one equals two’ and ‘one plus two equals two’ that cannot be further decomposed and that can be assigned a truth value of true or false. From these atomic propositions, we will build complex formulas using Boolean operators:
‘one plus one equals two’ and ‘Earth is farther from the sun than Venus’.
Mordechai Ben-Ari
Chapter 3. Propositional Logic: Deductive Systems
Abstract
The concept of deducing theorems from a set of axioms and rules of inference is very old and is familiar to every high-school student who has studied Euclidean geometry. Modern mathematics is expressed in a style of reasoning that is not far removed from the reasoning used by Greek mathematicians. This style can be characterized as ‘formalized informal reasoning’, meaning that while the proofs are expressed in natural language rather than in a formal system, there are conventions among mathematicians as to the forms of reasoning that are allowed. The deductive systems studied in this chapter were developed in an attempt to formalize mathematical reasoning.
Mordechai Ben-Ari
Chapter 4. Propositional Logic: Resolution
Abstract
The method of resolution, invented by J.A. Robinson in 1965, is an efficient method for searching for a proof. In this section, we introduce resolution for the propositional logic, though its advantages will not become apparent until it is extended to first-order logic. It is important to become familiar with resolution, because it is widely used in automatic theorem provers and it is also the basis of logic programming (Chap. 11).
Mordechai Ben-Ari
Chapter 5. Propositional Logic: Binary Decision Diagrams
Abstract
The problem of deciding the satisfiability of a formula in propositional logic has turned out to have many important applications in computer science. This chapter and the next one present two widely used approaches for computing with formulas in propositional logic.
Mordechai Ben-Ari
Chapter 6. Propositional Logic: SAT Solvers
Abstract
Although it is believed that there is no efficient algorithm for the decidability of satisfiability in propositional logic, many algorithms are efficient in practice. This is particularly true when a formula is satisfiable; for example, when you build a truth table for an unsatisfiable formula of size n you will have to generate all 2 n rows, but if the formula is satisfiable you might get lucky and find a model after generating only a few rows. Even an incomplete algorithm—one that can find a model if one exists but may not be able to detect if a formula is unsatisfiable—can be useful in practice.
Mordechai Ben-Ari
Chapter 7. First-Order Logic: Formulas, Models, Tableaux
Abstract
The axioms and theorems of mathematics are defined on sets such as the set of integers \( Z \). We need to be able to write and manipulate logical formulas that contain relations on values from arbitrary sets. First-order logic is an extension of propositional logic that includes predicates interpreted as relations on a domain.
Mordechai Ben-Ari
Chapter 8. First-Order Logic: Deductive Systems
Abstract
We extend the deductive systems \( G \) and \( H \) from propositional logic to first-order logic by adding axioms and rules of inference for the universal quantifier. (The existential quantifier is defined as the dual of the universal quantifier.) The construction of semantic tableaux for first-order logic included restrictions on the use of constants and similar restrictions will be needed here.
Mordechai Ben-Ari
Chapter 9. First-Order Logic: Terms and Normal Forms
Abstract
The formulas in first-order logic that we have defined are sufficient to express many interesting properties. Consider, for example, the formula:
$$ \forall x \forall y \forall z\, (p\,(x,y) \wedge p\,(y,z) \mathbin{\rightarrow} p\,(x,z)). $$
Under the interpretation:
$$ \{Z,\{ < \} ,\{ \} \} , $$
it expresses the true statement that the relation less-than is transitive in the domain of the integers. Suppose, now, that we want to express the following statement which is also true in the domain of integers:
$$ \mathit{for} \:\mathit{all}\; x, y, z: (x < y) \mathbin{\rightarrow} (x+z < y+z). $$
The difference between this statement and the previous one is that it uses the function +.
Mordechai Ben-Ari
Chapter 10. First-Order Logic: Resolution
Abstract
Resolution is a sound and complete algorithm for propositional logic: a formula in clausal form is unsatisfiable if and only if the algorithm reports that it is unsatisfiable. For propositional logic, the algorithm is also a decision procedure for unsatisfiability because it is guaranteed to terminate. When generalized to first-order logic, resolution is still sound and complete, but it is not a decision procedure because the algorithm may not terminate.
Mordechai Ben-Ari
Chapter 11. First-Order Logic: Logic Programming
Abstract
Resolution was originally developed as a method for automatic theorem proving. Later, it was discovered that a restricted form of resolution can be used for programming a computation. This approach is called logic programming. A program is expressed as a set of clauses and a query is expressed as an additional clause that can clash with one or more of the program clauses. The query is assumed to be the negation of result of the program. If a refutation succeeds, the query is not a logical consequence of the program, so its negation must be a logical consequence. Unifications done during the refutation provide answers to the query in addition to the simple fact that the negation of the query is true.
Mordechai Ben-Ari
Chapter 12. First-Order Logic: Undecidability and Model Theory *
Abstract
The chapter surveys several important theoretical results in first-order logic. In Sect. 12.1 we prove that validity in first-order logic is undecidable, a result first proved by Alonzo Church. Validity is decidable for several classes of formulas defined by syntactic restrictions on their form (Sect. 12.2). Next, we introduce model theory (Sect. 12.3): the fact that a semantic tableau has a countable number of nodes leads to some interesting results. Finally, Sect. 12.4 contains an overview of Gödel’s surprising incompleteness result.
Mordechai Ben-Ari
Chapter 13. Temporal Logic: Formulas, Models, Tableaux
Abstract
Temporal logic is a formal system for reasoning about time. Temporal logic has found extensive application in computer science, because the behavior of both hardware and software is a function of time. This section will follow the same approach that we used for other logics: we define the syntax of formulas and their interpretations and then describe the construction of semantic tableaux for deciding satisfiability.
Mordechai Ben-Ari
Chapter 14. Temporal Logic: A Deductive System
Abstract
This chapter defines the deductive system \( L \) for linear temporal logic. We will prove many of the formulas presented in the previous chapter, as well as the soundness and completeness of \( L \).
Mordechai Ben-Ari
Chapter 15. Verification of Sequential Programs
Abstract
A computer program is not very different from a logical formula. It consists of a sequence of symbols constructed according to formal syntactical rules and it has a meaning which is assigned by an interpretation of the elements of the language. In programming, the symbols are called statements or commands and the intended interpretation is the execution of the program on a computer. The syntax of programming languages is specified using formal systems such as BNF, but the semantics is usually informally specified.
Mordechai Ben-Ari
Chapter 16. Verification of Concurrent Programs
Abstract
Verification is routinely used when developing computer hardware and concurrent programs. A sequential program can always be tested and retested, but the nondeterministic nature of hardware and concurrent programs limits the effectiveness of testing as a method to demonstrate that the system is correct. Slight variations in timing, perhaps caused by congestion on a network, mean that two executions of the same program might give different results. Even if a bug is found by testing and then fixed, we have no way of knowing if the next test runs correctly because we fixed the bug or because the execution followed a different scenario, one in which the bug cannot occur.
Mordechai Ben-Ari
Backmatter
Metadata
Title
Mathematical Logic for Computer Science
Author
Mordechai Ben-Ari
Copyright Year
2012
Publisher
Springer London
Electronic ISBN
978-1-4471-4129-7
Print ISBN
978-1-4471-4128-0
DOI
https://doi.org/10.1007/978-1-4471-4129-7

Premium Partner

    Image Credits